Theorem ablmul 8068

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 5239	. . . 4 |- CC e. V
2		difexg 2712	. . . 4 |- (CC e. V -> (CC \ {0}) e. V)
3	1, 2	ax-mp 7	. . 3 |- (CC \ {0}) e. V
4		mulnzcnopr 5671	. . 3 |- ( x. |` ((CC \ {0}) X. (CC \ {0}))):((CC \ {0}) X. (CC \ {0}))-->(CC \ {0})
5		oprvalres 4018	. . . . . . . . 9 |- ((x e. (CC \ {0}) /\ y e. (CC \ {0})) -> (x( x. |` ((CC \ {0}) X. (CC \ {0})))y) = (x x. y))
6		axmulcl 5245	. . . . . . . . . . . . 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 5667	. . . . . . . . . . . 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 2453	. . . . . . . . . . 11 |- (x e. (CC \ {0}) <-> (x e. CC /\ x =/= 0))
11		eldifsn 2453	. . . . . . . . . . 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 2453	. . . . . . . . . 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 1540	. . . . . . . 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 826	. . . . . 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 4018	. . . . . 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 797	. . . . . 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 3960	. . . . 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 1499	. . . 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 5250	. . . . 5 |- ((x e. CC /\ y e. CC /\ z e. CC) -> ((x x. y) x. z) = (x x. (y x. z)))
24		eldifi 2152	. . . . 5 |- (x e. (CC \ {0}) -> x e. CC)
25		eldifi 2152	. . . . 5 |- (y e. (CC \ {0}) -> y e. CC)
26		eldifi 2152	. . . . 5 |- (z e. (CC \ {0}) -> z e. CC)
27	23, 24, 25, 26	syl3an 866	. . . 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 4018	. . . . . . . 8 |- ((y e. (CC \ {0}) /\ z e. (CC \ {0})) -> (y( x. |` ((CC \ {0}) X. (CC \ {0})))z) = (y x. z))
29	28	eqcomd 1472	. . . . . . 7 |- ((y e. (CC \ {0}) /\ z e. (CC \ {0})) -> (y x. z) = (y( x. |` ((CC \ {0}) X. (CC \ {0})))z))
30	29	3adant1 795	. . . . . 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 3961	. . . . 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 4018	. . . . . . . . 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 1472	. . . . . . . 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 4000	. . . . . . . . 9 |- ((y e. (CC \ {0}) /\ z e. (CC \ {0})) -> (y( x. |` ((CC \ {0}) X. (CC \ {0})))z) e. (CC \ {0}))
35	28, 34	eqeltrrd 1541	. . . . . . . 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 827	. . . . . 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 3961	. . . . . 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 1507	. . . . 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}