This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cygabl

Description: A cyclic group is abelian. (Contributed by Mario Carneiro, 21-Apr-2016) (Proof shortened by AV, 20-Jan-2024)

Ref Expression
Assertion cygabl 
|- ( 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 oveq1 
 |-  ( n = i -> ( n ( .g ` G ) x ) = ( i ( .g ` G ) x ) )
8 7 eqeq2d 
 |-  ( n = i -> ( y = ( n ( .g ` G ) x ) <-> y = ( i ( .g ` G ) x ) ) )
9 8 cbvrexvw 
 |-  ( E. n e. ZZ y = ( n ( .g ` G ) x ) <-> E. i e. ZZ y = ( i ( .g ` G ) x ) )
10 9 biimpi 
 |-  ( E. n e. ZZ y = ( n ( .g ` G ) x ) -> E. i e. ZZ y = ( i ( .g ` G ) x ) )
11 10 ralimi 
 |-  ( A. y e. ( Base ` G ) E. n e. ZZ y = ( n ( .g ` G ) x ) -> A. y e. ( Base ` G ) E. i e. ZZ y = ( i ( .g ` G ) x ) )
12 11 adantl 
 |-  ( ( ( G e. Grp /\ x e. ( Base ` G ) ) /\ A. y e. ( Base ` G ) E. n e. ZZ y = ( n ( .g ` G ) x ) ) -> A. y e. ( Base ` G ) E. i e. ZZ y = ( i ( .g ` G ) x ) )
13 12 3ad2ant1 
 |-  ( ( ( ( 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. y e. ( Base ` G ) E. i e. ZZ y = ( i ( .g ` G ) x ) )
14 simpll 
 |-  ( ( ( G e. Grp /\ x e. ( Base ` G ) ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> G e. Grp )
15 simpr 
 |-  ( ( G e. Grp /\ x e. ( Base ` G ) ) -> x e. ( Base ` G ) )
16 15 anim1ci 
 |-  ( ( ( G e. Grp /\ x e. ( Base ` G ) ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> ( ( m e. ZZ /\ n e. ZZ ) /\ x e. ( Base ` G ) ) )
17 df-3an 
 |-  ( ( m e. ZZ /\ n e. ZZ /\ x e. ( Base ` G ) ) <-> ( ( m e. ZZ /\ n e. ZZ ) /\ x e. ( Base ` G ) ) )
18 16 17 sylibr 
 |-  ( ( ( G e. Grp /\ x e. ( Base ` G ) ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> ( m e. ZZ /\ n e. ZZ /\ x e. ( Base ` G ) ) )
19 eqid 
 |-  ( +g ` G ) = ( +g ` G )
20 1 2 19 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 ) ) )
21 14 18 20 syl2anc 
 |-  ( ( ( 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 ) ) )
22 21 ralrimivva 
 |-  ( ( G e. Grp /\ x e. ( Base ` G ) ) -> A. m e. ZZ A. n e. ZZ ( ( m + n ) ( .g ` G ) x ) = ( ( m ( .g ` G ) x ) ( +g ` G ) ( n ( .g ` G ) x ) ) )
23 22 adantr 
 |-  ( ( ( G e. Grp /\ x e. ( Base ` G ) ) /\ A. y e. ( Base ` G ) E. n e. ZZ y = ( n ( .g ` G ) x ) ) -> A. m e. ZZ A. n e. ZZ ( ( m + n ) ( .g ` G ) x ) = ( ( m ( .g ` G ) x ) ( +g ` G ) ( n ( .g ` G ) x ) ) )
24 23 3ad2ant1 
 |-  ( ( ( ( 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. m e. ZZ A. n e. ZZ ( ( m + n ) ( .g ` G ) x ) = ( ( m ( .g ` G ) x ) ( +g ` G ) ( n ( .g ` G ) x ) ) )
25 simp2 
 |-  ( ( ( ( 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 e. ( Base ` G ) )
26 simp3 
 |-  ( ( ( ( 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 ) ) -> b e. ( Base ` G ) )
27 zsscn 
 |-  ZZ C_ CC
28 27 a1i 
 |-  ( ( ( ( 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 ) ) -> ZZ C_ CC )
29 13 24 25 26 28 cyccom 
 |-  ( ( ( ( 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 ) )
30 4 5 6 29 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 )
31 30 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 )
32 3 31 sylbi 
 |-  ( G e. CycGrp -> G e. Abel )