Metamath Proof Explorer

Theorem cygablOLD

Description: Obsolete proof of cygabl as of 20-Jan-2024. A cyclic group is abelian. (Contributed by Mario Carneiro, 21-Apr-2016) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion cygablOLD 
|- ( G e. CycGrp -> G e. Abel )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` G ) = ( Base ` G )
2 eqid 
 |-  ( .g ` G ) = ( .g ` G )
3 1 2 iscyg3 
 |-  ( G e. CycGrp <-> ( G e. Grp /\ E. x e. ( Base ` G ) A. y e. ( Base ` G ) E. n e. ZZ y = ( n ( .g ` G ) x ) ) )
4 eqidd 
 |-  ( ( ( G e. Grp /\ x e. ( Base ` G ) ) /\ A. y e. ( Base ` G ) E. n e. ZZ y = ( n ( .g ` G ) x ) ) -> ( Base ` G ) = ( Base ` G ) )
5 eqidd 
 |-  ( ( ( G e. Grp /\ x e. ( Base ` G ) ) /\ A. y e. ( Base ` G ) E. n e. ZZ y = ( n ( .g ` G ) x ) ) -> ( +g ` G ) = ( +g ` G ) )
6 simpll 
 |-  ( ( ( G e. Grp /\ x e. ( Base ` G ) ) /\ A. y e. ( Base ` G ) E. n e. ZZ y = ( n ( .g ` G ) x ) ) -> G e. Grp )
7 eqeq1 
 |-  ( y = a -> ( y = ( n ( .g ` G ) x ) <-> a = ( n ( .g ` G ) x ) ) )
8 7 rexbidv 
 |-  ( y = a -> ( E. n e. ZZ y = ( n ( .g ` G ) x ) <-> E. n e. ZZ a = ( n ( .g ` G ) x ) ) )
9 oveq1 
 |-  ( n = m -> ( n ( .g ` G ) x ) = ( m ( .g ` G ) x ) )
10 9 eqeq2d 
 |-  ( n = m -> ( a = ( n ( .g ` G ) x ) <-> a = ( m ( .g ` G ) x ) ) )
11 10 cbvrexv 
 |-  ( E. n e. ZZ a = ( n ( .g ` G ) x ) <-> E. m e. ZZ a = ( m ( .g ` G ) x ) )
12 8 11 bitrdi 
 |-  ( y = a -> ( E. n e. ZZ y = ( n ( .g ` G ) x ) <-> E. m e. ZZ a = ( m ( .g ` G ) x ) ) )
13 12 rspccv 
 |-  ( A. y e. ( Base ` G ) E. n e. ZZ y = ( n ( .g ` G ) x ) -> ( a e. ( Base ` G ) -> E. m e. ZZ a = ( m ( .g ` G ) x ) ) )
14 13 adantl 
 |-  ( ( ( G e. Grp /\ x e. ( Base ` G ) ) /\ A. y e. ( Base ` G ) E. n e. ZZ y = ( n ( .g ` G ) x ) ) -> ( a e. ( Base ` G ) -> E. m e. ZZ a = ( m ( .g ` G ) x ) ) )
15 eqeq1 
 |-  ( y = b -> ( y = ( n ( .g ` G ) x ) <-> b = ( n ( .g ` G ) x ) ) )
16 15 rexbidv 
 |-  ( y = b -> ( E. n e. ZZ y = ( n ( .g ` G ) x ) <-> E. n e. ZZ b = ( n ( .g ` G ) x ) ) )
17 16 rspccv 
 |-  ( A. y e. ( Base ` G ) E. n e. ZZ y = ( n ( .g ` G ) x ) -> ( b e. ( Base ` G ) -> E. n e. ZZ b = ( n ( .g ` G ) x ) ) )
18 17 adantl 
 |-  ( ( ( G e. Grp /\ x e. ( Base ` G ) ) /\ A. y e. ( Base ` G ) E. n e. ZZ y = ( n ( .g ` G ) x ) ) -> ( b e. ( Base ` G ) -> E. n e. ZZ b = ( n ( .g ` G ) x ) ) )
19 reeanv 
 |-  ( E. m e. ZZ E. n e. ZZ ( a = ( m ( .g ` G ) x ) /\ b = ( n ( .g ` G ) x ) ) <-> ( E. m e. ZZ a = ( m ( .g ` G ) x ) /\ E. n e. ZZ b = ( n ( .g ` G ) x ) ) )
20 zcn 
 |-  ( m e. ZZ -> m e. CC )
21 20 ad2antrl 
 |-  ( ( ( G e. Grp /\ x e. ( Base ` G ) ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> m e. CC )
22 zcn 
 |-  ( n e. ZZ -> n e. CC )
23 22 ad2antll 
 |-  ( ( ( G e. Grp /\ x e. ( Base ` G ) ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> n e. CC )
24 21 23 addcomd 
 |-  ( ( ( G e. Grp /\ x e. ( Base ` G ) ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> ( m + n ) = ( n + m ) )
25 24 oveq1d 
 |-  ( ( ( G e. Grp /\ x e. ( Base ` G ) ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> ( ( m + n ) ( .g ` G ) x ) = ( ( n + m ) ( .g ` G ) x ) )
26 simpll 
 |-  ( ( ( G e. Grp /\ x e. ( Base ` G ) ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> G e. Grp )
27 simprl 
 |-  ( ( ( G e. Grp /\ x e. ( Base ` G ) ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> m e. ZZ )
28 simprr 
 |-  ( ( ( G e. Grp /\ x e. ( Base ` G ) ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> n e. ZZ )
29 simplr 
 |-  ( ( ( G e. Grp /\ x e. ( Base ` G ) ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> x e. ( Base ` G ) )
30 eqid 
 |-  ( +g ` G ) = ( +g ` G )
31 1 2 30 mulgdir 
 |-  ( ( G e. Grp /\ ( m e. ZZ /\ n e. ZZ /\ x e. ( Base ` G ) ) ) -> ( ( m + n ) ( .g ` G ) x ) = ( ( m ( .g ` G ) x ) ( +g ` G ) ( n ( .g ` G ) x ) ) )
32 26 27 28 29 31 syl13anc 
 |-  ( ( ( G e. Grp /\ x e. ( Base ` G ) ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> ( ( m + n ) ( .g ` G ) x ) = ( ( m ( .g ` G ) x ) ( +g ` G ) ( n ( .g ` G ) x ) ) )
33 1 2 30 mulgdir 
 |-  ( ( G e. Grp /\ ( n e. ZZ /\ m e. ZZ /\ x e. ( Base ` G ) ) ) -> ( ( n + m ) ( .g ` G ) x ) = ( ( n ( .g ` G ) x ) ( +g ` G ) ( m ( .g ` G ) x ) ) )
34 26 28 27 29 33 syl13anc 
 |-  ( ( ( G e. Grp /\ x e. ( Base ` G ) ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> ( ( n + m ) ( .g ` G ) x ) = ( ( n ( .g ` G ) x ) ( +g ` G ) ( m ( .g ` G ) x ) ) )
35 25 32 34 3eqtr3d 
 |-  ( ( ( G e. Grp /\ x e. ( Base ` G ) ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> ( ( m ( .g ` G ) x ) ( +g ` G ) ( n ( .g ` G ) x ) ) = ( ( n ( .g ` G ) x ) ( +g ` G ) ( m ( .g ` G ) x ) ) )
36 oveq12 
 |-  ( ( a = ( m ( .g ` G ) x ) /\ b = ( n ( .g ` G ) x ) ) -> ( a ( +g ` G ) b ) = ( ( m ( .g ` G ) x ) ( +g ` G ) ( n ( .g ` G ) x ) ) )
37 oveq12 
 |-  ( ( b = ( n ( .g ` G ) x ) /\ a = ( m ( .g ` G ) x ) ) -> ( b ( +g ` G ) a ) = ( ( n ( .g ` G ) x ) ( +g ` G ) ( m ( .g ` G ) x ) ) )
38 37 ancoms 
 |-  ( ( a = ( m ( .g ` G ) x ) /\ b = ( n ( .g ` G ) x ) ) -> ( b ( +g ` G ) a ) = ( ( n ( .g ` G ) x ) ( +g ` G ) ( m ( .g ` G ) x ) ) )
39 36 38 eqeq12d 
 |-  ( ( a = ( m ( .g ` G ) x ) /\ b = ( n ( .g ` G ) x ) ) -> ( ( a ( +g ` G ) b ) = ( b ( +g ` G ) a ) <-> ( ( m ( .g ` G ) x ) ( +g ` G ) ( n ( .g ` G ) x ) ) = ( ( n ( .g ` G ) x ) ( +g ` G ) ( m ( .g ` G ) x ) ) ) )
40 35 39 syl5ibrcom 
 |-  ( ( ( G e. Grp /\ x e. ( Base ` G ) ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> ( ( a = ( m ( .g ` G ) x ) /\ b = ( n ( .g ` G ) x ) ) -> ( a ( +g ` G ) b ) = ( b ( +g ` G ) a ) ) )
41 40 rexlimdvva 
 |-  ( ( G e. Grp /\ x e. ( Base ` G ) ) -> ( E. m e. ZZ E. n e. ZZ ( a = ( m ( .g ` G ) x ) /\ b = ( n ( .g ` G ) x ) ) -> ( a ( +g ` G ) b ) = ( b ( +g ` G ) a ) ) )
42 19 41 syl5bir 
 |-  ( ( G e. Grp /\ x e. ( Base ` G ) ) -> ( ( E. m e. ZZ a = ( m ( .g ` G ) x ) /\ E. n e. ZZ b = ( n ( .g ` G ) x ) ) -> ( a ( +g ` G ) b ) = ( b ( +g ` G ) a ) ) )
43 42 adantr 
 |-  ( ( ( G e. Grp /\ x e. ( Base ` G ) ) /\ A. y e. ( Base ` G ) E. n e. ZZ y = ( n ( .g ` G ) x ) ) -> ( ( E. m e. ZZ a = ( m ( .g ` G ) x ) /\ E. n e. ZZ b = ( n ( .g ` G ) x ) ) -> ( a ( +g ` G ) b ) = ( b ( +g ` G ) a ) ) )
44 14 18 43 syl2and 
 |-  ( ( ( G e. Grp /\ x e. ( Base ` G ) ) /\ A. y e. ( Base ` G ) E. n e. ZZ y = ( n ( .g ` G ) x ) ) -> ( ( a e. ( Base ` G ) /\ b e. ( Base ` G ) ) -> ( a ( +g ` G ) b ) = ( b ( +g ` G ) a ) ) )
45 44 3impib 
 |-  ( ( ( ( G e. Grp /\ x e. ( Base ` G ) ) /\ A. y e. ( Base ` G ) E. n e. ZZ y = ( n ( .g ` G ) x ) ) /\ a e. ( Base ` G ) /\ b e. ( Base ` G ) ) -> ( a ( +g ` G ) b ) = ( b ( +g ` G ) a ) )
46 4 5 6 45 isabld 
 |-  ( ( ( G e. Grp /\ x e. ( Base ` G ) ) /\ A. y e. ( Base ` G ) E. n e. ZZ y = ( n ( .g ` G ) x ) ) -> G e. Abel )
47 46 r19.29an 
 |-  ( ( G e. Grp /\ E. x e. ( Base ` G ) A. y e. ( Base ` G ) E. n e. ZZ y = ( n ( .g ` G ) x ) ) -> G e. Abel )
48 3 47 sylbi 
 |-  ( G e. CycGrp -> G e. Abel )