Associativity of join and meet in MV-algebra lattice

Question

I'm trying to prove that MV-algebra is a lattice, where join and meet operations are defined as follows: $$x \vee y = (x \odot \neg y) \oplus y,$$ $$x \wedge y = x \odot (\neg x \oplus y).$$ I've already shown that they are idempotent and commutative, and that the absorption laws hold. I don't know however how to prove that they are associative. Take for example $\vee$ (I suspect $\wedge$ will be analogous). I tried writing $x \vee y$ as $\neg (\neg x \oplus y) \oplus y$, and then $$(x \vee y) \vee z = \neg (\neg z \oplus \neg (\neg x \oplus y) \oplus y) \oplus \neg (\neg x \oplus y) \oplus y,$$ $$x \vee (y \vee z) = \neg (\neg x \oplus \neg (\neg z \oplus y) \oplus y) \oplus \neg(\neg z \oplus y) \oplus y.$$ I also tried rewriting the above in other ways but to no avail...

Answer 1

Ok, I think I finally got it right (axioms numbering from here). Commutativity allows us to write it as $$(x \vee y) \vee z = \neg (\neg z \oplus y \oplus \neg(\neg x \oplus y)) \oplus \neg (\neg x \oplus y) \oplus y. $$ From 2., this equals $$= \neg (\neg \neg (\neg z \oplus y)\oplus \neg (\neg x \oplus y))\oplus \neg (\neg x \oplus y) \oplus y. $$ Apply 4. to get $$=\neg (\neg x \oplus y \oplus \neg (\neg z \oplus y))\oplus \neg (\neg z\oplus y) \oplus y. =x \vee (y \vee z)$$