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

Metamath Proof Explorer

Theorem frgpcyg

Description: A free group is cyclic iff it has zero or one generator. (Contributed by Mario Carneiro, 21-Apr-2016) (Proof shortened by AV, 18-Apr-2021)

Ref Expression
Hypothesis frgpcyg.g 
|- G = ( freeGrp ` I )
Assertion frgpcyg 
|- ( I ~<_ 1o <-> G e. CycGrp )

Proof

Step Hyp Ref Expression
1 frgpcyg.g 
 |-  G = ( freeGrp ` I )
2 brdom2 
 |-  ( I ~<_ 1o <-> ( I ~< 1o \/ I ~~ 1o ) )
3 sdom1 
 |-  ( I ~< 1o <-> I = (/) )
4 fveq2 
 |-  ( I = (/) -> ( freeGrp ` I ) = ( freeGrp ` (/) ) )
5 1 4 eqtrid 
 |-  ( I = (/) -> G = ( freeGrp ` (/) ) )
6 0ex 
 |-  (/) e. _V
7 eqid 
 |-  ( freeGrp ` (/) ) = ( freeGrp ` (/) )
8 7 frgpgrp 
 |-  ( (/) e. _V -> ( freeGrp ` (/) ) e. Grp )
9 6 8 ax-mp 
 |-  ( freeGrp ` (/) ) e. Grp
10 eqid 
 |-  ( Base ` ( freeGrp ` (/) ) ) = ( Base ` ( freeGrp ` (/) ) )
11 7 10 0frgp 
 |-  ( Base ` ( freeGrp ` (/) ) ) ~~ 1o
12 10 0cyg 
 |-  ( ( ( freeGrp ` (/) ) e. Grp /\ ( Base ` ( freeGrp ` (/) ) ) ~~ 1o ) -> ( freeGrp ` (/) ) e. CycGrp )
13 9 11 12 mp2an 
 |-  ( freeGrp ` (/) ) e. CycGrp
14 5 13 eqeltrdi 
 |-  ( I = (/) -> G e. CycGrp )
15 3 14 sylbi 
 |-  ( I ~< 1o -> G e. CycGrp )
16 eqid 
 |-  ( Base ` G ) = ( Base ` G )
17 eqid 
 |-  ( .g ` G ) = ( .g ` G )
18 relen 
 |-  Rel ~~
19 18 brrelex1i 
 |-  ( I ~~ 1o -> I e. _V )
20 1 frgpgrp 
 |-  ( I e. _V -> G e. Grp )
21 19 20 syl 
 |-  ( I ~~ 1o -> G e. Grp )
22 eqid 
 |-  ( ~FG ` I ) = ( ~FG ` I )
23 eqid 
 |-  ( varFGrp ` I ) = ( varFGrp ` I )
24 22 23 1 16 vrgpf 
 |-  ( I e. _V -> ( varFGrp ` I ) : I --> ( Base ` G ) )
25 19 24 syl 
 |-  ( I ~~ 1o -> ( varFGrp ` I ) : I --> ( Base ` G ) )
26 en1uniel 
 |-  ( I ~~ 1o -> U. I e. I )
27 25 26 ffvelcdmd 
 |-  ( I ~~ 1o -> ( ( varFGrp ` I ) ` U. I ) e. ( Base ` G ) )
28 zringgrp 
 |-  ZZring e. Grp
29 19 uniexd 
 |-  ( I ~~ 1o -> U. I e. _V )
30 1zzd 
 |-  ( I ~~ 1o -> 1 e. ZZ )
31 29 30 fsnd 
 |-  ( I ~~ 1o -> { <. U. I , 1 >. } : { U. I } --> ZZ )
32 en1b 
 |-  ( I ~~ 1o <-> I = { U. I } )
33 32 biimpi 
 |-  ( I ~~ 1o -> I = { U. I } )
34 33 feq2d 
 |-  ( I ~~ 1o -> ( { <. U. I , 1 >. } : I --> ZZ <-> { <. U. I , 1 >. } : { U. I } --> ZZ ) )
35 31 34 mpbird 
 |-  ( I ~~ 1o -> { <. U. I , 1 >. } : I --> ZZ )
36 zringbas 
 |-  ZZ = ( Base ` ZZring )
37 1 36 23 frgpup3 
 |-  ( ( ZZring e. Grp /\ I e. _V /\ { <. U. I , 1 >. } : I --> ZZ ) -> E! f e. ( G GrpHom ZZring ) ( f o. ( varFGrp ` I ) ) = { <. U. I , 1 >. } )
38 28 19 35 37 mp3an2i 
 |-  ( I ~~ 1o -> E! f e. ( G GrpHom ZZring ) ( f o. ( varFGrp ` I ) ) = { <. U. I , 1 >. } )
39 38 adantr 
 |-  ( ( I ~~ 1o /\ x e. ( Base ` G ) ) -> E! f e. ( G GrpHom ZZring ) ( f o. ( varFGrp ` I ) ) = { <. U. I , 1 >. } )
40 reurex 
 |-  ( E! f e. ( G GrpHom ZZring ) ( f o. ( varFGrp ` I ) ) = { <. U. I , 1 >. } -> E. f e. ( G GrpHom ZZring ) ( f o. ( varFGrp ` I ) ) = { <. U. I , 1 >. } )
41 39 40 syl 
 |-  ( ( I ~~ 1o /\ x e. ( Base ` G ) ) -> E. f e. ( G GrpHom ZZring ) ( f o. ( varFGrp ` I ) ) = { <. U. I , 1 >. } )
42 fveq1 
 |-  ( ( f o. ( varFGrp ` I ) ) = { <. U. I , 1 >. } -> ( ( f o. ( varFGrp ` I ) ) ` U. I ) = ( { <. U. I , 1 >. } ` U. I ) )
43 25 26 fvco3d 
 |-  ( I ~~ 1o -> ( ( f o. ( varFGrp ` I ) ) ` U. I ) = ( f ` ( ( varFGrp ` I ) ` U. I ) ) )
44 1z 
 |-  1 e. ZZ
45 fvsng 
 |-  ( ( U. I e. _V /\ 1 e. ZZ ) -> ( { <. U. I , 1 >. } ` U. I ) = 1 )
46 29 44 45 sylancl 
 |-  ( I ~~ 1o -> ( { <. U. I , 1 >. } ` U. I ) = 1 )
47 43 46 eqeq12d 
 |-  ( I ~~ 1o -> ( ( ( f o. ( varFGrp ` I ) ) ` U. I ) = ( { <. U. I , 1 >. } ` U. I ) <-> ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) )
48 42 47 imbitrid 
 |-  ( I ~~ 1o -> ( ( f o. ( varFGrp ` I ) ) = { <. U. I , 1 >. } -> ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) )
49 48 ad2antrr 
 |-  ( ( ( I ~~ 1o /\ x e. ( Base ` G ) ) /\ f e. ( G GrpHom ZZring ) ) -> ( ( f o. ( varFGrp ` I ) ) = { <. U. I , 1 >. } -> ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) )
50 16 36 ghmf 
 |-  ( f e. ( G GrpHom ZZring ) -> f : ( Base ` G ) --> ZZ )
51 50 ad2antrl 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> f : ( Base ` G ) --> ZZ )
52 51 ffvelcdmda 
 |-  ( ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) /\ x e. ( Base ` G ) ) -> ( f ` x ) e. ZZ )
53 52 an32s 
 |-  ( ( ( I ~~ 1o /\ x e. ( Base ` G ) ) /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> ( f ` x ) e. ZZ )
54 mptresid 
 |-  ( _I |` ( Base ` G ) ) = ( x e. ( Base ` G ) |-> x )
55 1 16 23 frgpup3 
 |-  ( ( G e. Grp /\ I e. _V /\ ( varFGrp ` I ) : I --> ( Base ` G ) ) -> E! g e. ( G GrpHom G ) ( g o. ( varFGrp ` I ) ) = ( varFGrp ` I ) )
56 21 19 25 55 syl3anc 
 |-  ( I ~~ 1o -> E! g e. ( G GrpHom G ) ( g o. ( varFGrp ` I ) ) = ( varFGrp ` I ) )
57 reurmo 
 |-  ( E! g e. ( G GrpHom G ) ( g o. ( varFGrp ` I ) ) = ( varFGrp ` I ) -> E* g e. ( G GrpHom G ) ( g o. ( varFGrp ` I ) ) = ( varFGrp ` I ) )
58 56 57 syl 
 |-  ( I ~~ 1o -> E* g e. ( G GrpHom G ) ( g o. ( varFGrp ` I ) ) = ( varFGrp ` I ) )
59 58 adantr 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> E* g e. ( G GrpHom G ) ( g o. ( varFGrp ` I ) ) = ( varFGrp ` I ) )
60 21 adantr 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> G e. Grp )
61 16 idghm 
 |-  ( G e. Grp -> ( _I |` ( Base ` G ) ) e. ( G GrpHom G ) )
62 60 61 syl 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> ( _I |` ( Base ` G ) ) e. ( G GrpHom G ) )
63 25 adantr 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> ( varFGrp ` I ) : I --> ( Base ` G ) )
64 fcoi2 
 |-  ( ( varFGrp ` I ) : I --> ( Base ` G ) -> ( ( _I |` ( Base ` G ) ) o. ( varFGrp ` I ) ) = ( varFGrp ` I ) )
65 63 64 syl 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> ( ( _I |` ( Base ` G ) ) o. ( varFGrp ` I ) ) = ( varFGrp ` I ) )
66 51 feqmptd 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> f = ( x e. ( Base ` G ) |-> ( f ` x ) ) )
67 eqidd 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> ( n e. ZZ |-> ( n ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) = ( n e. ZZ |-> ( n ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) )
68 oveq1 
 |-  ( n = ( f ` x ) -> ( n ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) = ( ( f ` x ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) )
69 52 66 67 68 fmptco 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> ( ( n e. ZZ |-> ( n ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) o. f ) = ( x e. ( Base ` G ) |-> ( ( f ` x ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) )
70 27 adantr 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> ( ( varFGrp ` I ) ` U. I ) e. ( Base ` G ) )
71 eqid 
 |-  ( n e. ZZ |-> ( n ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) = ( n e. ZZ |-> ( n ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) )
72 17 71 16 mulgghm2 
 |-  ( ( G e. Grp /\ ( ( varFGrp ` I ) ` U. I ) e. ( Base ` G ) ) -> ( n e. ZZ |-> ( n ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) e. ( ZZring GrpHom G ) )
73 60 70 72 syl2anc 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> ( n e. ZZ |-> ( n ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) e. ( ZZring GrpHom G ) )
74 simprl 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> f e. ( G GrpHom ZZring ) )
75 ghmco 
 |-  ( ( ( n e. ZZ |-> ( n ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) e. ( ZZring GrpHom G ) /\ f e. ( G GrpHom ZZring ) ) -> ( ( n e. ZZ |-> ( n ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) o. f ) e. ( G GrpHom G ) )
76 73 74 75 syl2anc 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> ( ( n e. ZZ |-> ( n ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) o. f ) e. ( G GrpHom G ) )
77 69 76 eqeltrrd 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> ( x e. ( Base ` G ) |-> ( ( f ` x ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) e. ( G GrpHom G ) )
78 33 adantr 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> I = { U. I } )
79 78 eleq2d 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> ( y e. I <-> y e. { U. I } ) )
80 simprr 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 )
81 80 oveq1d 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> ( ( f ` ( ( varFGrp ` I ) ` U. I ) ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) = ( 1 ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) )
82 16 17 mulg1 
 |-  ( ( ( varFGrp ` I ) ` U. I ) e. ( Base ` G ) -> ( 1 ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) = ( ( varFGrp ` I ) ` U. I ) )
83 70 82 syl 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> ( 1 ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) = ( ( varFGrp ` I ) ` U. I ) )
84 81 83 eqtrd 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> ( ( f ` ( ( varFGrp ` I ) ` U. I ) ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) = ( ( varFGrp ` I ) ` U. I ) )
85 elsni 
 |-  ( y e. { U. I } -> y = U. I )
86 85 fveq2d 
 |-  ( y e. { U. I } -> ( ( varFGrp ` I ) ` y ) = ( ( varFGrp ` I ) ` U. I ) )
87 86 fveq2d 
 |-  ( y e. { U. I } -> ( f ` ( ( varFGrp ` I ) ` y ) ) = ( f ` ( ( varFGrp ` I ) ` U. I ) ) )
88 87 oveq1d 
 |-  ( y e. { U. I } -> ( ( f ` ( ( varFGrp ` I ) ` y ) ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) = ( ( f ` ( ( varFGrp ` I ) ` U. I ) ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) )
89 88 86 eqeq12d 
 |-  ( y e. { U. I } -> ( ( ( f ` ( ( varFGrp ` I ) ` y ) ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) = ( ( varFGrp ` I ) ` y ) <-> ( ( f ` ( ( varFGrp ` I ) ` U. I ) ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) = ( ( varFGrp ` I ) ` U. I ) ) )
90 84 89 syl5ibrcom 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> ( y e. { U. I } -> ( ( f ` ( ( varFGrp ` I ) ` y ) ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) = ( ( varFGrp ` I ) ` y ) ) )
91 79 90 sylbid 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> ( y e. I -> ( ( f ` ( ( varFGrp ` I ) ` y ) ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) = ( ( varFGrp ` I ) ` y ) ) )
92 91 imp 
 |-  ( ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) /\ y e. I ) -> ( ( f ` ( ( varFGrp ` I ) ` y ) ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) = ( ( varFGrp ` I ) ` y ) )
93 92 mpteq2dva 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> ( y e. I |-> ( ( f ` ( ( varFGrp ` I ) ` y ) ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) = ( y e. I |-> ( ( varFGrp ` I ) ` y ) ) )
94 63 ffvelcdmda 
 |-  ( ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) /\ y e. I ) -> ( ( varFGrp ` I ) ` y ) e. ( Base ` G ) )
95 63 feqmptd 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> ( varFGrp ` I ) = ( y e. I |-> ( ( varFGrp ` I ) ` y ) ) )
96 eqidd 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> ( x e. ( Base ` G ) |-> ( ( f ` x ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) = ( x e. ( Base ` G ) |-> ( ( f ` x ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) )
97 fveq2 
 |-  ( x = ( ( varFGrp ` I ) ` y ) -> ( f ` x ) = ( f ` ( ( varFGrp ` I ) ` y ) ) )
98 97 oveq1d 
 |-  ( x = ( ( varFGrp ` I ) ` y ) -> ( ( f ` x ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) = ( ( f ` ( ( varFGrp ` I ) ` y ) ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) )
99 94 95 96 98 fmptco 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> ( ( x e. ( Base ` G ) |-> ( ( f ` x ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) o. ( varFGrp ` I ) ) = ( y e. I |-> ( ( f ` ( ( varFGrp ` I ) ` y ) ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) )
100 93 99 95 3eqtr4d 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> ( ( x e. ( Base ` G ) |-> ( ( f ` x ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) o. ( varFGrp ` I ) ) = ( varFGrp ` I ) )
101 coeq1 
 |-  ( g = ( _I |` ( Base ` G ) ) -> ( g o. ( varFGrp ` I ) ) = ( ( _I |` ( Base ` G ) ) o. ( varFGrp ` I ) ) )
102 101 eqeq1d 
 |-  ( g = ( _I |` ( Base ` G ) ) -> ( ( g o. ( varFGrp ` I ) ) = ( varFGrp ` I ) <-> ( ( _I |` ( Base ` G ) ) o. ( varFGrp ` I ) ) = ( varFGrp ` I ) ) )
103 coeq1 
 |-  ( g = ( x e. ( Base ` G ) |-> ( ( f ` x ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) -> ( g o. ( varFGrp ` I ) ) = ( ( x e. ( Base ` G ) |-> ( ( f ` x ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) o. ( varFGrp ` I ) ) )
104 103 eqeq1d 
 |-  ( g = ( x e. ( Base ` G ) |-> ( ( f ` x ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) -> ( ( g o. ( varFGrp ` I ) ) = ( varFGrp ` I ) <-> ( ( x e. ( Base ` G ) |-> ( ( f ` x ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) o. ( varFGrp ` I ) ) = ( varFGrp ` I ) ) )
105 102 104 rmoi 
 |-  ( ( E* g e. ( G GrpHom G ) ( g o. ( varFGrp ` I ) ) = ( varFGrp ` I ) /\ ( ( _I |` ( Base ` G ) ) e. ( G GrpHom G ) /\ ( ( _I |` ( Base ` G ) ) o. ( varFGrp ` I ) ) = ( varFGrp ` I ) ) /\ ( ( x e. ( Base ` G ) |-> ( ( f ` x ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) e. ( G GrpHom G ) /\ ( ( x e. ( Base ` G ) |-> ( ( f ` x ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) o. ( varFGrp ` I ) ) = ( varFGrp ` I ) ) ) -> ( _I |` ( Base ` G ) ) = ( x e. ( Base ` G ) |-> ( ( f ` x ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) )
106 59 62 65 77 100 105 syl122anc 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> ( _I |` ( Base ` G ) ) = ( x e. ( Base ` G ) |-> ( ( f ` x ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) )
107 54 106 eqtr3id 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> ( x e. ( Base ` G ) |-> x ) = ( x e. ( Base ` G ) |-> ( ( f ` x ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) )
108 mpteqb 
 |-  ( A. x e. ( Base ` G ) x e. ( Base ` G ) -> ( ( x e. ( Base ` G ) |-> x ) = ( x e. ( Base ` G ) |-> ( ( f ` x ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) <-> A. x e. ( Base ` G ) x = ( ( f ` x ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) )
109 id 
 |-  ( x e. ( Base ` G ) -> x e. ( Base ` G ) )
110 108 109 mprg 
 |-  ( ( x e. ( Base ` G ) |-> x ) = ( x e. ( Base ` G ) |-> ( ( f ` x ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) <-> A. x e. ( Base ` G ) x = ( ( f ` x ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) )
111 107 110 sylib 
 |-  ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> A. x e. ( Base ` G ) x = ( ( f ` x ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) )
112 111 r19.21bi 
 |-  ( ( ( I ~~ 1o /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) /\ x e. ( Base ` G ) ) -> x = ( ( f ` x ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) )
113 112 an32s 
 |-  ( ( ( I ~~ 1o /\ x e. ( Base ` G ) ) /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> x = ( ( f ` x ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) )
114 68 rspceeqv 
 |-  ( ( ( f ` x ) e. ZZ /\ x = ( ( f ` x ) ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) -> E. n e. ZZ x = ( n ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) )
115 53 113 114 syl2anc 
 |-  ( ( ( I ~~ 1o /\ x e. ( Base ` G ) ) /\ ( f e. ( G GrpHom ZZring ) /\ ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 ) ) -> E. n e. ZZ x = ( n ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) )
116 115 expr 
 |-  ( ( ( I ~~ 1o /\ x e. ( Base ` G ) ) /\ f e. ( G GrpHom ZZring ) ) -> ( ( f ` ( ( varFGrp ` I ) ` U. I ) ) = 1 -> E. n e. ZZ x = ( n ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) )
117 49 116 syld 
 |-  ( ( ( I ~~ 1o /\ x e. ( Base ` G ) ) /\ f e. ( G GrpHom ZZring ) ) -> ( ( f o. ( varFGrp ` I ) ) = { <. U. I , 1 >. } -> E. n e. ZZ x = ( n ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) )
118 117 rexlimdva 
 |-  ( ( I ~~ 1o /\ x e. ( Base ` G ) ) -> ( E. f e. ( G GrpHom ZZring ) ( f o. ( varFGrp ` I ) ) = { <. U. I , 1 >. } -> E. n e. ZZ x = ( n ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) ) )
119 41 118 mpd 
 |-  ( ( I ~~ 1o /\ x e. ( Base ` G ) ) -> E. n e. ZZ x = ( n ( .g ` G ) ( ( varFGrp ` I ) ` U. I ) ) )
120 16 17 21 27 119 iscygd 
 |-  ( I ~~ 1o -> G e. CycGrp )
121 15 120 jaoi 
 |-  ( ( I ~< 1o \/ I ~~ 1o ) -> G e. CycGrp )
122 2 121 sylbi 
 |-  ( I ~<_ 1o -> G e. CycGrp )
123 cygabl 
 |-  ( G e. CycGrp -> G e. Abel )
124 1 frgpnabl 
 |-  ( 1o ~< I -> -. G e. Abel )
125 124 con2i 
 |-  ( G e. Abel -> -. 1o ~< I )
126 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
127 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
128 16 127 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. ( Base ` G ) )
129 1 16 elbasfv 
 |-  ( ( 0g ` G ) e. ( Base ` G ) -> I e. _V )
130 126 128 129 3syl 
 |-  ( G e. Abel -> I e. _V )
131 1onn 
 |-  1o e. _om
132 nnfi 
 |-  ( 1o e. _om -> 1o e. Fin )
133 131 132 ax-mp 
 |-  1o e. Fin
134 fidomtri2 
 |-  ( ( I e. _V /\ 1o e. Fin ) -> ( I ~<_ 1o <-> -. 1o ~< I ) )
135 130 133 134 sylancl 
 |-  ( G e. Abel -> ( I ~<_ 1o <-> -. 1o ~< I ) )
136 125 135 mpbird 
 |-  ( G e. Abel -> I ~<_ 1o )
137 123 136 syl 
 |-  ( G e. CycGrp -> I ~<_ 1o )
138 122 137 impbii 
 |-  ( I ~<_ 1o <-> G e. CycGrp )