Theorem ablmul 8131

Description: Nonzero complex number multiplication is an Abelian group operation. (Contributed by Steve Rodriguez, 12-Feb-2007.)

Assertion

Ref	Expression
ablmul	|- ( x. |` ((CC \ {0}) X. (CC \ {0}))) e. Abel

Proof of Theorem ablmul

Step	Hyp	Ref	Expression
1		axcnex 5267	. . . 4 |- CC e. V
2		difexg 2722	. . . 4 |- (CC e. V -> (CC \ {0}) e. V)
3	1, 2	ax-mp 7	. . 3 |- (CC \ {0}) e. V
4		mulnzcnopr 5702	. . 3 |- ( x. |` ((CC \ {0}) X. (CC \ {0}))):((CC \ {0}) X. (CC \ {0}))-->(CC \ {0})
5		oprvalres 4033	. . . . . . . . 9 |- ((x e. (CC \ {0}) /\ y e. (CC \ {0})) -> (x( x. |` ((CC \ {0}) X. (CC \ {0})))y) = (x x. y))
6		axmulcl 5273	. . . . . . . . . . . . 13 |- ((x e. CC /\ y e. CC) -> (x x. y) e. CC)
7	6	ad2ant2r 409	. . . . . . . . . . . 12 |- (((x e. CC /\ x =/= 0) /\ (y e. CC /\ y =/= 0)) -> (x x. y) e. CC)
8		muln0t 5698	. . . . . . . . . . . 12 |- (((x e. CC /\ x =/= 0) /\ (y e. CC /\ y =/= 0)) -> (x x. y) =/= 0)
9	7, 8	jca 288	. . . . . . . . . . 11 |- (((x e. CC /\ x =/= 0) /\ (y e. CC /\ y =/= 0)) -> ((x x. y) e. CC /\ (x x. y) =/= 0))
10		eldifsn 2462	. . . . . . . . . . 11 |- (x e. (CC \ {0}) <-> (x e. CC /\ x =/= 0))
11		eldifsn 2462	. . . . . . . . . . 11 |- (y e. (CC \ {0}) <-> (y e. CC /\ y =/= 0))
12	9, 10, 11	syl2anb 455	. . . . . . . . . 10 |- ((x e. (CC \ {0}) /\ y e. (CC \ {0})) -> ((x x. y) e. CC /\ (x x. y) =/= 0))
13		eldifsn 2462	. . . . . . . . . 10 |- ((x x. y) e. (CC \ {0}) <-> ((x x. y) e. CC /\ (x x. y) =/= 0))
14	12, 13	sylibr 200	. . . . . . . . 9 |- ((x e. (CC \ {0}) /\ y e. (CC \ {0})) -> (x x. y) e. (CC \ {0}))
15	5, 14	eqeltrd 1548	. . . . . . . 8 |- ((x e. (CC \ {0}) /\ y e. (CC \ {0})) -> (x( x. |` ((CC \ {0}) X. (CC \ {0})))y) e. (CC \ {0}))
16	15	anim1i 334	. . . . . . 7 |- (((x e. (CC \ {0}) /\ y e. (CC \ {0})) /\ z e. (CC \ {0})) -> ((x( x. |` ((CC \ {0}) X. (CC \ {0})))y) e. (CC \ {0}) /\ z e. (CC \ {0})))
17	16	3impa 828	. . . . . 6 |- ((x e. (CC \ {0}) /\ y e. (CC \ {0}) /\ z e. (CC \ {0})) -> ((x( x. |` ((CC \ {0}) X. (CC \ {0})))y) e. (CC \ {0}) /\ z e. (CC \ {0})))
18		oprvalres 4033	. . . . . 6 |- (((x( x. |` ((CC \ {0}) X. (CC \ {0})))y) e. (CC \ {0}) /\ z e. (CC \ {0})) -> ((x( x. |` ((CC \ {0}) X. (CC \ {0})))y)( x. |` ((CC \ {0}) X. (CC \ {0})))z) = ((x( x. |` ((CC \ {0}) X. (CC \ {0})))y) x. z))
19	17, 18	syl 10	. . . . 5 |- ((x e. (CC \ {0}) /\ y e. (CC \ {0}) /\ z e. (CC \ {0})) -> ((x( x. |` ((CC \ {0}) X. (CC \ {0})))y)( x. |` ((CC \ {0}) X. (CC \ {0})))z) = ((x( x. |` ((CC \ {0}) X. (CC \ {0})))y) x. z))
20	5	3adant3 799	. . . . . 6 |- ((x e. (CC \ {0}) /\ y e. (CC \ {0}) /\ z e. (CC \ {0})) -> (x( x. |` ((CC \ {0}) X. (CC \ {0})))y) = (x x. y))
21	20	opreq1d 3975	. . . . 5 |- ((x e. (CC \ {0}) /\ y e. (CC \ {0}) /\ z e. (CC \ {0})) -> ((x( x. |` ((CC \ {0}) X. (CC \ {0})))y) x. z) = ((x x. y) x. z))
22	19, 21	eqtrd 1507	. . . 4 |- ((x e. (CC \ {0}) /\ y e. (CC \ {0}) /\ z e. (CC \ {0})) -> ((x( x. |` ((CC \ {0}) X. (CC \ {0})))y)( x. |` ((CC \ {0}) X. (CC \ {0})))z) = ((x x. y) x. z))
23		axmulass 5278	. . . . 5 |- ((x e. CC /\ y e. CC /\ z e. CC) -> ((x x. y) x. z) = (x x. (y x. z)))
24		eldifi 2162	. . . . 5 |- (x e. (CC \ {0}) -> x e. CC)
25		eldifi 2162	. . . . 5 |- (y e. (CC \ {0}) -> y e. CC)
26		eldifi 2162	. . . . 5 |- (z e. (CC \ {0}) -> z e. CC)
27	23, 24, 25, 26	syl3an 868	. . . 4 |- ((x e. (CC \ {0}) /\ y e. (CC \ {0}) /\ z e. (CC \ {0})) -> ((x x. y) x. z) = (x x. (y x. z)))
28		oprvalres 4033	. . . . . . . 8 |- ((y e. (CC \ {0}) /\ z e. (CC \ {0})) -> (y( x. |` ((CC \ {0}) X. (CC \ {0})))z) = (y x. z))
29	28	eqcomd 1480	. . . . . . 7 |- ((y e. (CC \ {0}) /\ z e. (CC \ {0})) -> (y x. z) = (y( x. |` ((CC \ {0}) X. (CC \ {0})))z))
30	29	3adant1 797	. . . . . 6 |- ((x e. (CC \ {0}) /\ y e. (CC \ {0}) /\ z e. (CC \ {0})) -> (y x. z) = (y( x. |` ((CC \ {0}) X. (CC \ {0})))z))
31	30	opreq2d 3976	. . . . 5 |- ((x e. (CC \ {0}) /\ y e. (CC \ {0}) /\ z e. (CC \ {0})) -> (x x. (y x. z)) = (x x. (y( x. |` ((CC \ {0}) X. (CC \ {0})))z)))
32		oprvalres 4033	. . . . . . . . 9 |- ((x e. (CC \ {0}) /\ (y x. z) e. (CC \ {0})) -> (x( x. |` ((CC \ {0}) X. (CC \ {0})))(y x. z)) = (x x. (y x. z)))
33	32	eqcomd 1480	. . . . . . . 8 |- ((x e. (CC \ {0}) /\ (y x. z) e. (CC \ {0})) -> (x x. (y x. z)) = (x( x. |` ((CC \ {0}) X. (CC \ {0})))(y x. z)))
34	4	foprcl 4015	. . . . . . . . 9 |- ((y e. (CC \ {0}) /\ z e. (CC \ {0})) -> (y( x. |` ((CC \ {0}) X. (CC \ {0})))z) e. (CC \ {0}))
35	28, 34	eqeltrrd 1549	. . . . . . . 8 |- ((y e. (CC \ {0}) /\ z e. (CC \ {0})) -> (y x. z) e. (CC \ {0}))
36	33, 35	sylan2 451	. . . . . . 7 |- ((x e. (CC \ {0}) /\ (y e. (CC \ {0}) /\ z e. (CC \ {0}))) -> (x x. (y x. z)) = (x( x. |` ((CC \ {0}) X. (CC \ {0})))(y x. z)))
37	36	3impb 829	. . . . . 6 |- ((x e. (CC \ {0}) /\ y e. (CC \ {0}) /\ z e. (CC \ {0})) -> (x x. (y x. z)) = (x( x. |` ((CC \ {0}) X. (CC \ {0})))(y x. z)))
38	30	opreq2d 3976	. . . . . 6 |- ((x e. (CC \ {0}) /\ y e. (CC \ {0}) /\ z e. (CC \ {0})) -> (x( x. |` ((CC \ {0}) X. (CC \ {0})))(y x. z)) = (x( x. |` ((CC \ {0}) X. (CC \ {0})))(y( x. |` ((CC \ {0}) X. (CC \ {0})))z)))
39	37, 31, 38	3eqtr3d 1515	. . . . 5 |- ((x e. (CC \ {0}) /\ y e. (CC \ {0}) /\ z e. (CC \ {0})) -> (x x. (y( x. |` ((CC \ {0}) X. (CC \ {0})))z)) = (x( x. |` ((CC \ {0}) X. (CC \ {0