Theorem ablmul 8215

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 5332	. . . 4 |- CC e. V
2		difexg 2777	. . . 4 |- (CC e. V -> (CC \ {0}) e. V)
3	1, 2	ax-mp 7	. . 3 |- (CC \ {0}) e. V
4		mulnzcnopr 5767	. . 3 |- ( x. |` ((CC \ {0}) X. (CC \ {0}))):((CC \ {0}) X. (CC \ {0}))-->(CC \ {0})
5		oprvalres 4091	. . . . . . . . 9 |- ((x e. (CC \ {0}) /\ y e. (CC \ {0})) -> (x( x. |` ((CC \ {0}) X. (CC \ {0})))y) = (x x. y))
6		mulcl 5368	. . . . . . . . . . . . 13 |- ((x e. CC /\ y e. CC) -> (x x. y) e. CC)
7	6	ad2ant2r 418	. . . . . . . . . . . 12 |- (((x e. CC /\ x =/= 0) /\ (y e. CC /\ y =/= 0)) -> (x x. y) e. CC)
8		muln0 5763	. . . . . . . . . . . 12 |- (((x e. CC /\ x =/= 0) /\ (y e. CC /\ y =/= 0)) -> (x x. y) =/= 0)
9	7, 8	jca 295	. . . . . . . . . . 11 |- (((x e. CC /\ x =/= 0) /\ (y e. CC /\ y =/= 0)) -> ((x x. y) e. CC /\ (x x. y) =/= 0))
10		eldifsn 2516	. . . . . . . . . . 11 |- (x e. (CC \ {0}) <-> (x e. CC /\ x =/= 0))
11		eldifsn 2516	. . . . . . . . . . 11 |- (y e. (CC \ {0}) <-> (y e. CC /\ y =/= 0))
12	9, 10, 11	syl2anb 466	. . . . . . . . . 10 |- ((x e. (CC \ {0}) /\ y e. (CC \ {0})) -> ((x x. y) e. CC /\ (x x. y) =/= 0))
13		eldifsn 2516	. . . . . . . . . 10 |- ((x x. y) e. (CC \ {0}) <-> ((x x. y) e. CC /\ (x x. y) =/= 0))
14	12, 13	sylibr 207	. . . . . . . . 9 |- ((x e. (CC \ {0}) /\ y e. (CC \ {0})) -> (x x. y) e. (CC \ {0}))
15	5, 14	eqeltrd 1595	. . . . . . . 8 |- ((x e. (CC \ {0}) /\ y e. (CC \ {0})) -> (x( x. |` ((CC \ {0}) X. (CC \ {0})))y) e. (CC \ {0}))
16	15	anim1i 341	. . . . . . 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 840	. . . . . 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 4091	. . . . . 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 811	. . . . . 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 4033	. . . . 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 1554	. . . 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		mulass 5373	. . . . 5 |- ((x e. CC /\ y e. CC /\ z e. CC) -> ((x x. y) x. z) = (x x. (y x. z)))
24		eldifi 2213	. . . . 5 |- (x e. (CC \ {0}) -> x e. CC)
25		eldifi 2213	. . . . 5 |- (y e. (CC \ {0}) -> y e. CC)
26		eldifi 2213	. . . . 5 |- (z e. (CC \ {0}) -> z e. CC)
27	23, 24, 25, 26	syl3an 880	. . . 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 4091	. . . . . . . 8 |- ((y e. (CC \ {0}) /\ z e. (CC \ {0})) -> (y( x. |` ((CC \ {0}) X. (CC \ {0})))z) = (y x. z))
29	28	eqcomd 1527	. . . . . . 7 |- ((y e. (CC \ {0}) /\ z e. (CC \ {0})) -> (y x. z) = (y( x. |` ((CC \ {0}) X. (CC \ {0})))z))
30	29	3adant1 809	. . . . . 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 4034	. . . . 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 4091	. . . . . . . . 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 1527	. . . . . . . 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 4073	. . . . . . . . 9 |- ((y e. (CC \ {0}) /\ z e. (CC \ {0})) -> (y( x. |` ((CC \ {0}) X. (CC \ {0})))z) e. (CC \ {0}))
35	28, 34	eqeltrrd 1596	. . . . . . . 8 |- ((y e. (CC \ {0}) /\ z e. (CC \ {0})) -> (y x. z) e. (CC \ {0}))
36	33, 35	sylan2 462	. . . . . . 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 841	. . . . . 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 4034	. . . . . 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 1562	. . . . 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}