Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  frgpcyg Structured version   Visualization version   GIF version

Theorem frgpcyg 19741
 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.)
Hypothesis
Ref Expression
frgpcyg.g 𝐺 = (freeGrp‘𝐼)
Assertion
Ref Expression
frgpcyg (𝐼 ≼ 1𝑜𝐺 ∈ CycGrp)

Proof of Theorem frgpcyg
Dummy variables 𝑓 𝑔 𝑛 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 brdom2 7871 . . 3 (𝐼 ≼ 1𝑜 ↔ (𝐼 ≺ 1𝑜𝐼 ≈ 1𝑜))
2 sdom1 8045 . . . . 5 (𝐼 ≺ 1𝑜𝐼 = ∅)
3 frgpcyg.g . . . . . . 7 𝐺 = (freeGrp‘𝐼)
4 fveq2 6103 . . . . . . 7 (𝐼 = ∅ → (freeGrp‘𝐼) = (freeGrp‘∅))
53, 4syl5eq 2656 . . . . . 6 (𝐼 = ∅ → 𝐺 = (freeGrp‘∅))
6 0ex 4718 . . . . . . . 8 ∅ ∈ V
7 eqid 2610 . . . . . . . . 9 (freeGrp‘∅) = (freeGrp‘∅)
87frgpgrp 17998 . . . . . . . 8 (∅ ∈ V → (freeGrp‘∅) ∈ Grp)
96, 8ax-mp 5 . . . . . . 7 (freeGrp‘∅) ∈ Grp
10 eqid 2610 . . . . . . . 8 (Base‘(freeGrp‘∅)) = (Base‘(freeGrp‘∅))
117, 100frgp 18015 . . . . . . 7 (Base‘(freeGrp‘∅)) ≈ 1𝑜
12100cyg 18117 . . . . . . 7 (((freeGrp‘∅) ∈ Grp ∧ (Base‘(freeGrp‘∅)) ≈ 1𝑜) → (freeGrp‘∅) ∈ CycGrp)
139, 11, 12mp2an 704 . . . . . 6 (freeGrp‘∅) ∈ CycGrp
145, 13syl6eqel 2696 . . . . 5 (𝐼 = ∅ → 𝐺 ∈ CycGrp)
152, 14sylbi 206 . . . 4 (𝐼 ≺ 1𝑜𝐺 ∈ CycGrp)
16 eqid 2610 . . . . 5 (Base‘𝐺) = (Base‘𝐺)
17 eqid 2610 . . . . 5 (.g𝐺) = (.g𝐺)
18 relen 7846 . . . . . . 7 Rel ≈
1918brrelexi 5082 . . . . . 6 (𝐼 ≈ 1𝑜𝐼 ∈ V)
203frgpgrp 17998 . . . . . 6 (𝐼 ∈ V → 𝐺 ∈ Grp)
2119, 20syl 17 . . . . 5 (𝐼 ≈ 1𝑜𝐺 ∈ Grp)
22 eqid 2610 . . . . . . . 8 ( ~FG𝐼) = ( ~FG𝐼)
23 eqid 2610 . . . . . . . 8 (varFGrp𝐼) = (varFGrp𝐼)
2422, 23, 3, 16vrgpf 18004 . . . . . . 7 (𝐼 ∈ V → (varFGrp𝐼):𝐼⟶(Base‘𝐺))
2519, 24syl 17 . . . . . 6 (𝐼 ≈ 1𝑜 → (varFGrp𝐼):𝐼⟶(Base‘𝐺))
26 en1uniel 7914 . . . . . 6 (𝐼 ≈ 1𝑜 𝐼𝐼)
2725, 26ffvelrnd 6268 . . . . 5 (𝐼 ≈ 1𝑜 → ((varFGrp𝐼)‘ 𝐼) ∈ (Base‘𝐺))
28 zringgrp 19642 . . . . . . . . 9 ring ∈ Grp
29 uniexg 6853 . . . . . . . . . . . 12 (𝐼 ∈ V → 𝐼 ∈ V)
3019, 29syl 17 . . . . . . . . . . 11 (𝐼 ≈ 1𝑜 𝐼 ∈ V)
31 1zzd 11285 . . . . . . . . . . 11 (𝐼 ≈ 1𝑜 → 1 ∈ ℤ)
3230, 31fsnd 6091 . . . . . . . . . 10 (𝐼 ≈ 1𝑜 → {⟨ 𝐼, 1⟩}:{ 𝐼}⟶ℤ)
33 en1b 7910 . . . . . . . . . . . 12 (𝐼 ≈ 1𝑜𝐼 = { 𝐼})
3433biimpi 205 . . . . . . . . . . 11 (𝐼 ≈ 1𝑜𝐼 = { 𝐼})
3534feq2d 5944 . . . . . . . . . 10 (𝐼 ≈ 1𝑜 → ({⟨ 𝐼, 1⟩}:𝐼⟶ℤ ↔ {⟨ 𝐼, 1⟩}:{ 𝐼}⟶ℤ))
3632, 35mpbird 246 . . . . . . . . 9 (𝐼 ≈ 1𝑜 → {⟨ 𝐼, 1⟩}:𝐼⟶ℤ)
37 zringbas 19643 . . . . . . . . . 10 ℤ = (Base‘ℤring)
383, 37, 23frgpup3 18014 . . . . . . . . 9 ((ℤring ∈ Grp ∧ 𝐼 ∈ V ∧ {⟨ 𝐼, 1⟩}:𝐼⟶ℤ) → ∃!𝑓 ∈ (𝐺 GrpHom ℤring)(𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩})
3928, 19, 36, 38mp3an2i 1421 . . . . . . . 8 (𝐼 ≈ 1𝑜 → ∃!𝑓 ∈ (𝐺 GrpHom ℤring)(𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩})
4039adantr 480 . . . . . . 7 ((𝐼 ≈ 1𝑜𝑥 ∈ (Base‘𝐺)) → ∃!𝑓 ∈ (𝐺 GrpHom ℤring)(𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩})
41 reurex 3137 . . . . . . 7 (∃!𝑓 ∈ (𝐺 GrpHom ℤring)(𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩} → ∃𝑓 ∈ (𝐺 GrpHom ℤring)(𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩})
4240, 41syl 17 . . . . . 6 ((𝐼 ≈ 1𝑜𝑥 ∈ (Base‘𝐺)) → ∃𝑓 ∈ (𝐺 GrpHom ℤring)(𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩})
43 fveq1 6102 . . . . . . . . . 10 ((𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩} → ((𝑓 ∘ (varFGrp𝐼))‘ 𝐼) = ({⟨ 𝐼, 1⟩}‘ 𝐼))
44 fvco3 6185 . . . . . . . . . . . 12 (((varFGrp𝐼):𝐼⟶(Base‘𝐺) ∧ 𝐼𝐼) → ((𝑓 ∘ (varFGrp𝐼))‘ 𝐼) = (𝑓‘((varFGrp𝐼)‘ 𝐼)))
4525, 26, 44syl2anc 691 . . . . . . . . . . 11 (𝐼 ≈ 1𝑜 → ((𝑓 ∘ (varFGrp𝐼))‘ 𝐼) = (𝑓‘((varFGrp𝐼)‘ 𝐼)))
46 1z 11284 . . . . . . . . . . . 12 1 ∈ ℤ
47 fvsng 6352 . . . . . . . . . . . 12 (( 𝐼 ∈ V ∧ 1 ∈ ℤ) → ({⟨ 𝐼, 1⟩}‘ 𝐼) = 1)
4830, 46, 47sylancl 693 . . . . . . . . . . 11 (𝐼 ≈ 1𝑜 → ({⟨ 𝐼, 1⟩}‘ 𝐼) = 1)
4945, 48eqeq12d 2625 . . . . . . . . . 10 (𝐼 ≈ 1𝑜 → (((𝑓 ∘ (varFGrp𝐼))‘ 𝐼) = ({⟨ 𝐼, 1⟩}‘ 𝐼) ↔ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1))
5043, 49syl5ib 233 . . . . . . . . 9 (𝐼 ≈ 1𝑜 → ((𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩} → (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1))
5150ad2antrr 758 . . . . . . . 8 (((𝐼 ≈ 1𝑜𝑥 ∈ (Base‘𝐺)) ∧ 𝑓 ∈ (𝐺 GrpHom ℤring)) → ((𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩} → (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1))
5216, 37ghmf 17487 . . . . . . . . . . . . 13 (𝑓 ∈ (𝐺 GrpHom ℤring) → 𝑓:(Base‘𝐺)⟶ℤ)
5352ad2antrl 760 . . . . . . . . . . . 12 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → 𝑓:(Base‘𝐺)⟶ℤ)
5453ffvelrnda 6267 . . . . . . . . . . 11 (((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) ∧ 𝑥 ∈ (Base‘𝐺)) → (𝑓𝑥) ∈ ℤ)
5554an32s 842 . . . . . . . . . 10 (((𝐼 ≈ 1𝑜𝑥 ∈ (Base‘𝐺)) ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑓𝑥) ∈ ℤ)
56 mptresid 5375 . . . . . . . . . . . . . 14 (𝑥 ∈ (Base‘𝐺) ↦ 𝑥) = ( I ↾ (Base‘𝐺))
573, 16, 23frgpup3 18014 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ Grp ∧ 𝐼 ∈ V ∧ (varFGrp𝐼):𝐼⟶(Base‘𝐺)) → ∃!𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘ (varFGrp𝐼)) = (varFGrp𝐼))
5821, 19, 25, 57syl3anc 1318 . . . . . . . . . . . . . . . . 17 (𝐼 ≈ 1𝑜 → ∃!𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘ (varFGrp𝐼)) = (varFGrp𝐼))
59 reurmo 3138 . . . . . . . . . . . . . . . . 17 (∃!𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘ (varFGrp𝐼)) = (varFGrp𝐼) → ∃*𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘ (varFGrp𝐼)) = (varFGrp𝐼))
6058, 59syl 17 . . . . . . . . . . . . . . . 16 (𝐼 ≈ 1𝑜 → ∃*𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘ (varFGrp𝐼)) = (varFGrp𝐼))
6160adantr 480 . . . . . . . . . . . . . . 15 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ∃*𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘ (varFGrp𝐼)) = (varFGrp𝐼))
6221adantr 480 . . . . . . . . . . . . . . . 16 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → 𝐺 ∈ Grp)
6316idghm 17498 . . . . . . . . . . . . . . . 16 (𝐺 ∈ Grp → ( I ↾ (Base‘𝐺)) ∈ (𝐺 GrpHom 𝐺))
6462, 63syl 17 . . . . . . . . . . . . . . 15 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ( I ↾ (Base‘𝐺)) ∈ (𝐺 GrpHom 𝐺))
6525adantr 480 . . . . . . . . . . . . . . . 16 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (varFGrp𝐼):𝐼⟶(Base‘𝐺))
66 fcoi2 5992 . . . . . . . . . . . . . . . 16 ((varFGrp𝐼):𝐼⟶(Base‘𝐺) → (( I ↾ (Base‘𝐺)) ∘ (varFGrp𝐼)) = (varFGrp𝐼))
6765, 66syl 17 . . . . . . . . . . . . . . 15 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (( I ↾ (Base‘𝐺)) ∘ (varFGrp𝐼)) = (varFGrp𝐼))
6853feqmptd 6159 . . . . . . . . . . . . . . . . 17 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → 𝑓 = (𝑥 ∈ (Base‘𝐺) ↦ (𝑓𝑥)))
69 eqidd 2611 . . . . . . . . . . . . . . . . 17 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))) = (𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
70 oveq1 6556 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑓𝑥) → (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
7154, 68, 69, 70fmptco 6303 . . . . . . . . . . . . . . . 16 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ((𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∘ 𝑓) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
7227adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ((varFGrp𝐼)‘ 𝐼) ∈ (Base‘𝐺))
73 eqid 2610 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))) = (𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
7417, 73, 16mulgghm2 19664 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ Grp ∧ ((varFGrp𝐼)‘ 𝐼) ∈ (Base‘𝐺)) → (𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∈ (ℤring GrpHom 𝐺))
7562, 72, 74syl2anc 691 . . . . . . . . . . . . . . . . 17 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∈ (ℤring GrpHom 𝐺))
76 simprl 790 . . . . . . . . . . . . . . . . 17 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → 𝑓 ∈ (𝐺 GrpHom ℤring))
77 ghmco 17503 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∈ (ℤring GrpHom 𝐺) ∧ 𝑓 ∈ (𝐺 GrpHom ℤring)) → ((𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∘ 𝑓) ∈ (𝐺 GrpHom 𝐺))
7875, 76, 77syl2anc 691 . . . . . . . . . . . . . . . 16 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ((𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∘ 𝑓) ∈ (𝐺 GrpHom 𝐺))
7971, 78eqeltrrd 2689 . . . . . . . . . . . . . . 15 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∈ (𝐺 GrpHom 𝐺))
8034adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → 𝐼 = { 𝐼})
8180eleq2d 2673 . . . . . . . . . . . . . . . . . . 19 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑦𝐼𝑦 ∈ { 𝐼}))
82 simprr 792 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)
8382oveq1d 6564 . . . . . . . . . . . . . . . . . . . . 21 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ((𝑓‘((varFGrp𝐼)‘ 𝐼))(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = (1(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
8416, 17mulg1 17371 . . . . . . . . . . . . . . . . . . . . . 22 (((varFGrp𝐼)‘ 𝐼) ∈ (Base‘𝐺) → (1(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((varFGrp𝐼)‘ 𝐼))
8572, 84syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (1(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((varFGrp𝐼)‘ 𝐼))
8683, 85eqtrd 2644 . . . . . . . . . . . . . . . . . . . 20 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ((𝑓‘((varFGrp𝐼)‘ 𝐼))(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((varFGrp𝐼)‘ 𝐼))
87 elsni 4142 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ { 𝐼} → 𝑦 = 𝐼)
8887fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ { 𝐼} → ((varFGrp𝐼)‘𝑦) = ((varFGrp𝐼)‘ 𝐼))
8988fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ { 𝐼} → (𝑓‘((varFGrp𝐼)‘𝑦)) = (𝑓‘((varFGrp𝐼)‘ 𝐼)))
9089oveq1d 6564 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ { 𝐼} → ((𝑓‘((varFGrp𝐼)‘𝑦))(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((𝑓‘((varFGrp𝐼)‘ 𝐼))(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
9190, 88eqeq12d 2625 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ { 𝐼} → (((𝑓‘((varFGrp𝐼)‘𝑦))(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((varFGrp𝐼)‘𝑦) ↔ ((𝑓‘((varFGrp𝐼)‘ 𝐼))(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((varFGrp𝐼)‘ 𝐼)))
9286, 91syl5ibrcom 236 . . . . . . . . . . . . . . . . . . 19 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑦 ∈ { 𝐼} → ((𝑓‘((varFGrp𝐼)‘𝑦))(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((varFGrp𝐼)‘𝑦)))
9381, 92sylbid 229 . . . . . . . . . . . . . . . . . 18 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑦𝐼 → ((𝑓‘((varFGrp𝐼)‘𝑦))(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((varFGrp𝐼)‘𝑦)))
9493imp 444 . . . . . . . . . . . . . . . . 17 (((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) ∧ 𝑦𝐼) → ((𝑓‘((varFGrp𝐼)‘𝑦))(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((varFGrp𝐼)‘𝑦))
9594mpteq2dva 4672 . . . . . . . . . . . . . . . 16 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑦𝐼 ↦ ((𝑓‘((varFGrp𝐼)‘𝑦))(.g𝐺)((varFGrp𝐼)‘ 𝐼))) = (𝑦𝐼 ↦ ((varFGrp𝐼)‘𝑦)))
9665ffvelrnda 6267 . . . . . . . . . . . . . . . . 17 (((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) ∧ 𝑦𝐼) → ((varFGrp𝐼)‘𝑦) ∈ (Base‘𝐺))
9765feqmptd 6159 . . . . . . . . . . . . . . . . 17 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (varFGrp𝐼) = (𝑦𝐼 ↦ ((varFGrp𝐼)‘𝑦)))
98 eqidd 2611 . . . . . . . . . . . . . . . . 17 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
99 fveq2 6103 . . . . . . . . . . . . . . . . . 18 (𝑥 = ((varFGrp𝐼)‘𝑦) → (𝑓𝑥) = (𝑓‘((varFGrp𝐼)‘𝑦)))
10099oveq1d 6564 . . . . . . . . . . . . . . . . 17 (𝑥 = ((varFGrp𝐼)‘𝑦) → ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((𝑓‘((varFGrp𝐼)‘𝑦))(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
10196, 97, 98, 100fmptco 6303 . . . . . . . . . . . . . . . 16 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ((𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∘ (varFGrp𝐼)) = (𝑦𝐼 ↦ ((𝑓‘((varFGrp𝐼)‘𝑦))(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
10295, 101, 973eqtr4d 2654 . . . . . . . . . . . . . . 15 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ((𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∘ (varFGrp𝐼)) = (varFGrp𝐼))
103 coeq1 5201 . . . . . . . . . . . . . . . . 17 (𝑔 = ( I ↾ (Base‘𝐺)) → (𝑔 ∘ (varFGrp𝐼)) = (( I ↾ (Base‘𝐺)) ∘ (varFGrp𝐼)))
104103eqeq1d 2612 . . . . . . . . . . . . . . . 16 (𝑔 = ( I ↾ (Base‘𝐺)) → ((𝑔 ∘ (varFGrp𝐼)) = (varFGrp𝐼) ↔ (( I ↾ (Base‘𝐺)) ∘ (varFGrp𝐼)) = (varFGrp𝐼)))
105 coeq1 5201 . . . . . . . . . . . . . . . . 17 (𝑔 = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) → (𝑔 ∘ (varFGrp𝐼)) = ((𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∘ (varFGrp𝐼)))
106105eqeq1d 2612 . . . . . . . . . . . . . . . 16 (𝑔 = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) → ((𝑔 ∘ (varFGrp𝐼)) = (varFGrp𝐼) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∘ (varFGrp𝐼)) = (varFGrp𝐼)))
107104, 106rmoi 3496 . . . . . . . . . . . . . . 15 ((∃*𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘ (varFGrp𝐼)) = (varFGrp𝐼) ∧ (( I ↾ (Base‘𝐺)) ∈ (𝐺 GrpHom 𝐺) ∧ (( I ↾ (Base‘𝐺)) ∘ (varFGrp𝐼)) = (varFGrp𝐼)) ∧ ((𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∈ (𝐺 GrpHom 𝐺) ∧ ((𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∘ (varFGrp𝐼)) = (varFGrp𝐼))) → ( I ↾ (Base‘𝐺)) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
10861, 64, 67, 79, 102, 107syl122anc 1327 . . . . . . . . . . . . . 14 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ( I ↾ (Base‘𝐺)) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
10956, 108syl5eq 2656 . . . . . . . . . . . . 13 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑥 ∈ (Base‘𝐺) ↦ 𝑥) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
110 mpteqb 6207 . . . . . . . . . . . . . 14 (∀𝑥 ∈ (Base‘𝐺)𝑥 ∈ (Base‘𝐺) → ((𝑥 ∈ (Base‘𝐺) ↦ 𝑥) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ↔ ∀𝑥 ∈ (Base‘𝐺)𝑥 = ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
111 id 22 . . . . . . . . . . . . . 14 (𝑥 ∈ (Base‘𝐺) → 𝑥 ∈ (Base‘𝐺))
112110, 111mprg 2910 . . . . . . . . . . . . 13 ((𝑥 ∈ (Base‘𝐺) ↦ 𝑥) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ↔ ∀𝑥 ∈ (Base‘𝐺)𝑥 = ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
113109, 112sylib 207 . . . . . . . . . . . 12 ((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ∀𝑥 ∈ (Base‘𝐺)𝑥 = ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
114113r19.21bi 2916 . . . . . . . . . . 11 (((𝐼 ≈ 1𝑜 ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) ∧ 𝑥 ∈ (Base‘𝐺)) → 𝑥 = ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
115114an32s 842 . . . . . . . . . 10 (((𝐼 ≈ 1𝑜𝑥 ∈ (Base‘𝐺)) ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → 𝑥 = ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
11670eqeq2d 2620 . . . . . . . . . . 11 (𝑛 = (𝑓𝑥) → (𝑥 = (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼)) ↔ 𝑥 = ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
117116rspcev 3282 . . . . . . . . . 10 (((𝑓𝑥) ∈ ℤ ∧ 𝑥 = ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) → ∃𝑛 ∈ ℤ 𝑥 = (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
11855, 115, 117syl2anc 691 . . . . . . . . 9 (((𝐼 ≈ 1𝑜𝑥 ∈ (Base‘𝐺)) ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ∃𝑛 ∈ ℤ 𝑥 = (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
119118expr 641 . . . . . . . 8 (((𝐼 ≈ 1𝑜𝑥 ∈ (Base‘𝐺)) ∧ 𝑓 ∈ (𝐺 GrpHom ℤring)) → ((𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1 → ∃𝑛 ∈ ℤ 𝑥 = (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
12051, 119syld 46 . . . . . . 7 (((𝐼 ≈ 1𝑜𝑥 ∈ (Base‘𝐺)) ∧ 𝑓 ∈ (𝐺 GrpHom ℤring)) → ((𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩} → ∃𝑛 ∈ ℤ 𝑥 = (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
121120rexlimdva 3013 . . . . . 6 ((𝐼 ≈ 1𝑜𝑥 ∈ (Base‘𝐺)) → (∃𝑓 ∈ (𝐺 GrpHom ℤring)(𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩} → ∃𝑛 ∈ ℤ 𝑥 = (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
12242, 121mpd 15 . . . . 5 ((𝐼 ≈ 1𝑜𝑥 ∈ (Base‘𝐺)) → ∃𝑛 ∈ ℤ 𝑥 = (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
12316, 17, 21, 27, 122iscygd 18112 . . . 4 (𝐼 ≈ 1𝑜𝐺 ∈ CycGrp)
12415, 123jaoi 393 . . 3 ((𝐼 ≺ 1𝑜𝐼 ≈ 1𝑜) → 𝐺 ∈ CycGrp)
1251, 124sylbi 206 . 2 (𝐼 ≼ 1𝑜𝐺 ∈ CycGrp)
126 cygabl 18115 . . 3 (𝐺 ∈ CycGrp → 𝐺 ∈ Abel)
1273frgpnabl 18101 . . . . 5 (1𝑜𝐼 → ¬ 𝐺 ∈ Abel)
128127con2i 133 . . . 4 (𝐺 ∈ Abel → ¬ 1𝑜𝐼)
129 ablgrp 18021 . . . . . 6 (𝐺 ∈ Abel → 𝐺 ∈ Grp)
130 eqid 2610 . . . . . . 7 (0g𝐺) = (0g𝐺)
13116, 130grpidcl 17273 . . . . . 6 (𝐺 ∈ Grp → (0g𝐺) ∈ (Base‘𝐺))
1323, 16elbasfv 15748 . . . . . 6 ((0g𝐺) ∈ (Base‘𝐺) → 𝐼 ∈ V)
133129, 131, 1323syl 18 . . . . 5 (𝐺 ∈ Abel → 𝐼 ∈ V)
134 1onn 7606 . . . . . 6 1𝑜 ∈ ω
135 nnfi 8038 . . . . . 6 (1𝑜 ∈ ω → 1𝑜 ∈ Fin)
136134, 135ax-mp 5 . . . . 5 1𝑜 ∈ Fin
137 fidomtri2 8703 . . . . 5 ((𝐼 ∈ V ∧ 1𝑜 ∈ Fin) → (𝐼 ≼ 1𝑜 ↔ ¬ 1𝑜𝐼))
138133, 136, 137sylancl 693 . . . 4 (𝐺 ∈ Abel → (𝐼 ≼ 1𝑜 ↔ ¬ 1𝑜𝐼))
139128, 138mpbird 246 . . 3 (𝐺 ∈ Abel → 𝐼 ≼ 1𝑜)
140126, 139syl 17 . 2 (𝐺 ∈ CycGrp → 𝐼 ≼ 1𝑜)
141125, 140impbii 198 1 (𝐼 ≼ 1𝑜𝐺 ∈ CycGrp)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897  ∃!wreu 2898  ∃*wrmo 2899  Vcvv 3173  ∅c0 3874  {csn 4125  ⟨cop 4131  ∪ cuni 4372   class class class wbr 4583   ↦ cmpt 4643   I cid 4948   ↾ cres 5040   ∘ ccom 5042  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  ωcom 6957  1𝑜c1o 7440   ≈ cen 7838   ≼ cdom 7839   ≺ csdm 7840  Fincfn 7841  1c1 9816  ℤcz 11254  Basecbs 15695  0gc0g 15923  Grpcgrp 17245  .gcmg 17363   GrpHom cghm 17480   ~FG cefg 17942  freeGrpcfrgp 17943  varFGrpcvrgp 17944  Abelcabl 18017  CycGrpccyg 18102  ℤringzring 19637 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-addf 9894  ax-mulf 9895 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-ot 4134  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-ec 7631  df-qs 7635  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-inf 8232  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-xnn0 11241  df-z 11255  df-dec 11370  df-uz 11564  df-rp 11709  df-fz 12198  df-fzo 12335  df-seq 12664  df-hash 12980  df-word 13154  df-lsw 13155  df-concat 13156  df-s1 13157  df-substr 13158  df-splice 13159  df-reverse 13160  df-s2 13444  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-starv 15783  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-unif 15792  df-0g 15925  df-gsum 15926  df-imas 15991  df-qus 15992  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-mhm 17158  df-submnd 17159  df-frmd 17209  df-vrmd 17210  df-grp 17248  df-minusg 17249  df-mulg 17364  df-subg 17414  df-ghm 17481  df-efg 17945  df-frgp 17946  df-vrgp 17947  df-cmn 18018  df-abl 18019  df-cyg 18103  df-mgp 18313  df-ur 18325  df-ring 18372  df-cring 18373  df-subrg 18601  df-cnfld 19568  df-zring 19638 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator