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 ⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
Assertion frgpcyg ( 𝐼 ≼ 1o ↔ 𝐺 ∈ CycGrp )

Proof

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