Theorem circgrpOLD 8677

Description: The circle group T is an Abelian group. (Contributed by Paul Chapman, 25-Mar-2008.)

Hypotheses

Ref	Expression
circgrpOLD.1	|- C = {w e. CC | (abs` w) = 1}
circgrpOLD.2	|- T = ( x. |` (C X. C))

Assertion

Ref	Expression
circgrpOLD	|- T e. Abel

Proof of Theorem circgrpOLD

Step	Hyp	Ref	Expression
1		circgrpOLD.1	. . . 4 |- C = {w e. CC | (abs` w) = 1}
2		axcnex 5247	. . . . 5 |- CC e. V
3	2	rabex 2720	. . . 4 |- {w e. CC | (abs` w) = 1} e. V
4	1, 3	eqeltr 1541	. . 3 |- C e. V
5		ffnoprval 4005	. . . 4 |- (T:(C X. C)-->C <-> (T Fn (C X. C) /\ A.x e. C A.y e. C (xTy) e. C))
6		axmulopr 5246	. . . . . . 7 |- x. :(CC X. CC)-->CC
7		ffn 3619	. . . . . . 7 |- ( x. :(CC X. CC)-->CC -> x. Fn (CC X. CC))
8	6, 7	ax-mp 7	. . . . . 6 |- x. Fn (CC X. CC)
9		ssrab2 2127	. . . . . . . 8 |- {w e. CC | (abs` w) = 1} (_ CC
10	1, 9	eqsstr 2087	. . . . . . 7 |- C (_ CC
11		ssxp 3251	. . . . . . 7 |- ((C (_ CC /\ C (_ CC) -> (C X. C) (_ (CC X. CC))
12	10, 10, 11	mp2an 696	. . . . . 6 |- (C X. C) (_ (CC X. CC)
13		fnssres 3592	. . . . . 6 |- (( x. Fn (CC X. CC) /\ (C X. C) (_ (CC X. CC)) -> ( x. |` (C X. C)) Fn (C X. C))
14	8, 12, 13	mp2an 696	. . . . 5 |- ( x. |` (C X. C)) Fn (C X. C)
15		circgrpOLD.2	. . . . . 6 |- T = ( x. |` (C X. C))
16		fneq1 3574	. . . . . 6 |- (T = ( x. |` (C X. C)) -> (T Fn (C X. C) <-> ( x. |` (C X. C)) Fn (C X. C)))
17	15, 16	ax-mp 7	. . . . 5 |- (T Fn (C X. C) <-> ( x. |` (C X. C)) Fn (C X. C))
18	14, 17	mpbir 190	. . . 4 |- T Fn (C X. C)
19	1, 15	circoprvalOLD 8676	. . . . . 6 |- ((x e. C /\ y e. C) -> (xTy) = (x x. y))
20	1	circcltOLD 8675	. . . . . 6 |- ((x e. C /\ y e. C) -> (x x. y) e. C)
21	19, 20	eqeltrd 1545	. . . . 5 |- ((x e. C /\ y e. C) -> (xTy) e. C)
22	21	rgen2a 1696	. . . 4 |- A.x e. C A.y e. C (xTy) e. C
23	5, 18, 22	mpbir2an 729	. . 3 |- T:(C X. C)-->C
24		axmulass 5258	. . . . 5 |- ((a e. CC /\ b e. CC /\ c e. CC) -> ((a x. b) x. c) = (a x. (b x. c)))
25	1	elcircOLD 8673	. . . . . 6 |- (a e. C <-> (a e. CC /\ (abs` a) = 1))
26	25	pm3.26bi 322	. . . . 5 |- (a e. C -> a e. CC)
27	1	elcircOLD 8673	. . . . . 6 |- (b e. C <-> (b e. CC /\ (abs` b) = 1))
28	27	pm3.26bi 322	. . . . 5 |- (b e. C -> b e. CC)
29	1	elcircOLD 8673	. . . . . 6 |- (c e. C <-> (c e. CC /\ (abs` c) = 1))
30	29	pm3.26bi 322	. . . . 5 |- (c e. C -> c e. CC)
31	24, 26, 28, 30	syl3an 867	. . . 4 |- ((a e. C /\ b e. C /\ c e. C) -> ((a x. b) x. c) = (a x. (b x. c)))
32	1, 15	circoprvalOLD 8676	. . . . . . 7 |- ((a e. C /\ b e. C) -> (aTb) = (a x. b))
33	32	3adant3 798	. . . . . 6 |- ((a e. C /\ b e. C /\ c e. C) -> (aTb) = (a x. b))
34	33	opreq1d 3966	. . . . 5 |- ((a e. C /\ b e. C /\ c e. C) -> ((aTb)Tc) = ((a x. b)Tc))
35	1, 15	circoprvalOLD 8676	. . . . . . 7 |- (((a x. b) e. C /\ c e. C) -> ((a x. b)Tc) = ((a x. b) x. c))
36	1	circcltOLD 8675	. . . . . . 7 |- ((a e. C /\ b e. C) -> (a x. b) e. C)
37	35, 36	sylan 448	. . . . . 6 |- (((a e. C /\ b e. C) /\ c e. C) -> ((a x. b)Tc) = ((a x. b) x. c))
38	37	3impa 827	. . . . 5 |- ((a e. C /\ b e. C /\ c e. C) -> ((a x. b)Tc) = ((a x. b) x. c))
39	34, 38	eqtrd 1504	. . . 4 |- ((a e. C /\ b e. C /\ c e. C) -> ((aTb)Tc) = ((a x. b) x. c))
40	1, 15	circoprvalOLD 8676	. . . . . . 7 |- ((b e. C /\ c e. C) -> (bTc) = (b x. c))
41	40	3adant1 796	. . . . . 6 |- ((a e. C /\ b e. C /\ c e. C) -> (bTc) = (b x. c))
42	41	opreq2d 3967	. . . . 5 |- ((a e. C /\ b e. C /\ c e. C) -> (aT(bTc)) = (aT(b x. c)))
43	1, 15	circoprvalOLD 8676	. . . . . . 7 |- ((a e. C /\ (b x. c) e. C) -> (aT(b x. c)) = (a x. (b x. c)))
44	1	circcltOLD 8675	. . . . . . 7 |- ((b e. C /\ c e. C) -> (b x. c) e. C)
45	43, 44	sylan2 451	. . . . . 6 |- ((a e. C /\ (b e. C /\ c e. C)) -> (aT(b x. c)) = (a x. (b x. c)))
46	45	3impb 828	. . . . 5 |- ((a e. C /\ b e. C /\ c e. C) -> (aT(b x. c)) = (a x. (b x. c)))
47	42, 46	eqtrd 1504	. . . 4 |- ((a e. C /\ b e. C /\ c e. C) -> (aT(bTc)) = (a x. (b x. c)))
48	31, 39, 47	3eqtr4d 1514	. . 3 |- ((a e. C /\ b e. C /\ c e. C) -> ((aTb)Tc) = (aT(bTc)))
49	1	elcircOLD 8673	. . . 4 |- (1 e. C <-> (1 e. CC /\ (abs` 1) = 1))
50		ax1cn 5249	. . . 4 |- 1 e. CC
51		0re 5420	. . . . . 6 |- 0 e. RR
52		1re 5415	. . . . . 6 |- 1 e. RR
53		lt01 5661	. . . . . 6 |- 0 < 1
54	51, 52, 53	ltlei 5562	. . . . 5 |- 0 <_ 1
55	52	absid 6804	. . . . 5 |- (0 <_ 1 -> (abs` 1) = 1)
56	54, 55	ax-mp 7	. . . 4 |- (abs` 1) = 1
57	49, 50, 56	mpbir2an 729	. . 3 |- 1 e. C
58	1, 15	circoprvalOLD 8676	. . . . 5 |- ((1 e. C /\ a e. C) -> (1Ta) = (1 x. a))
59	57, 58	mpan 694	. . . 4 |- (a e. C -> (1Ta) = (1 x. a))
60		mulid2t 5397	. . . . 5 |- (a e. CC -> (1 x. a) = a)
61	26, 60	syl 10	. . . 4 |- (a e. C -> (1 x. a) = a)
62	59, 61	eqtrd 1504	. . 3 |- (a e. C -> (1Ta) = a)
63	1	elcircOLD 8673	. . . . 5 |- ((*` a) e. C <-> ((*` a) e. CC /\ (abs` (*` a)) = 1))
64	63	biimpr 152	. . . 4 |- (((*` a) e. CC /\ (abs` (*` a)) = 1) -> (*` a) e. C)
65		cjclt 6704	. . . . 5 |- (a e. CC -> (*` a) e. CC)
66	26, 65	syl 10	. . . 4 |- (a e. C -> (*` a) e. CC)
67		abscjt 6777	. . . . . 6 |- (a e. CC -> (abs` (*` a)) = (abs` a))
68	26, 67	syl 10	. . . . 5 |- (a e. C -> (abs` (*` a)) = (abs` a))
69	25	pm3.27bi 326	. . . . 5 |- (a e. C -> (abs` a) = 1)
70	68, 69	eqtrd 1504	. . . 4 |- (a e. C -> (abs` (*` a)) = 1)
71	64, 66, 70	sylanc 471	. . 3 |- (a e. C -> (*` a) e. C)
72		axmulcom 5256	. . . . . . 7 |- (((*` a) e. CC /\ a e. CC) -> ((*` a) x. a) = (a x. (*` a)))
73	65, 72	mpancom 704	. . . . . 6 |- (a e. CC -> ((*` a) x. a) = (a x. (*` a)))
74	26, 73	syl 10	. . . . 5 |- (a e. C -> ((*` a) x. a) = (a x. (*` a)))
75	1, 15	circoprvalOLD 8676	. . . . . 6 |- (((*` a) e. C /\ a e. C) -> ((*` a)Ta) = ((*` a) x. a))
76	71, 75	mpancom 704	. . . . 5 |- (a e. C -> ((*` a)Ta) = ((*` a) x. a))
77		absvalsqt 6778	. . . . . 6 |- (a e. CC -> ((abs` a)^2) = (a x. (*` a)))
78	26, 77	syl 10	. . . . 5 |- (a e. C -> ((abs` a)^2) = (a x. (*` a)))
79	74, 76, 78	3eqtr4d 1514	. . . 4 |- (a e. C -> ((*` a)Ta) = ((abs` a)^2))
80	69	opreq1d 3966	. . . . 5 |- (a e. C -> ((abs` a)^2) = (1^2))
81		sq1 6576	. . . . 5 |- (1^2) = 1
82	80, 81	syl6eq 1520	. . . 4 |- (a e. C -> ((abs` a)^2) = 1)
83	79, 82	eqtrd 1504	. . 3 |- (a e. C -> ((*` a)Ta) = 1)
84	4, 23, 48, 57, 62, 71, 83	isgrpi 7992	. 2 |- T e. Grp
85		axmulcom 5256	. . . 4 |- ((a e. CC /\ b e. CC) -> (a x. b) = (b x. a))
86	85, 26, 28	syl2an 454	. . 3 |- ((a e. C /\ b e. C) -> (a x. b) = (b x. a))
87	1, 15	circoprvalOLD 8676	. . . 4 |- ((b e. C /\ a e. C) -> (bTa) = (b x. a))
88	87	ancoms 436	. . 3 |- ((a e. C /\ b e. C) -> (bTa) = (b x. a))
89	86, 32, 88	3eqtr4d 1514	. 2 |- ((a e. C /\ b e. C) -> (aTb) = (bT