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

Theorem frgpcyg 20543
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 (𝐼 ≼ 1o𝐺 ∈ CycGrp)

Proof of Theorem frgpcyg
Dummy variables 𝑓 𝑔 𝑛 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 brdom2 8663 . . 3 (𝐼 ≼ 1o ↔ (𝐼 ≺ 1o𝐼 ≈ 1o))
2 sdom1 8883 . . . . 5 (𝐼 ≺ 1o𝐼 = ∅)
3 frgpcyg.g . . . . . . 7 𝐺 = (freeGrp‘𝐼)
4 fveq2 6722 . . . . . . 7 (𝐼 = ∅ → (freeGrp‘𝐼) = (freeGrp‘∅))
53, 4syl5eq 2790 . . . . . 6 (𝐼 = ∅ → 𝐺 = (freeGrp‘∅))
6 0ex 5205 . . . . . . . 8 ∅ ∈ V
7 eqid 2737 . . . . . . . . 9 (freeGrp‘∅) = (freeGrp‘∅)
87frgpgrp 19157 . . . . . . . 8 (∅ ∈ V → (freeGrp‘∅) ∈ Grp)
96, 8ax-mp 5 . . . . . . 7 (freeGrp‘∅) ∈ Grp
10 eqid 2737 . . . . . . . 8 (Base‘(freeGrp‘∅)) = (Base‘(freeGrp‘∅))
117, 100frgp 19174 . . . . . . 7 (Base‘(freeGrp‘∅)) ≈ 1o
12100cyg 19283 . . . . . . 7 (((freeGrp‘∅) ∈ Grp ∧ (Base‘(freeGrp‘∅)) ≈ 1o) → (freeGrp‘∅) ∈ CycGrp)
139, 11, 12mp2an 692 . . . . . 6 (freeGrp‘∅) ∈ CycGrp
145, 13eqeltrdi 2846 . . . . 5 (𝐼 = ∅ → 𝐺 ∈ CycGrp)
152, 14sylbi 220 . . . 4 (𝐼 ≺ 1o𝐺 ∈ CycGrp)
16 eqid 2737 . . . . 5 (Base‘𝐺) = (Base‘𝐺)
17 eqid 2737 . . . . 5 (.g𝐺) = (.g𝐺)
18 relen 8636 . . . . . . 7 Rel ≈
1918brrelex1i 5610 . . . . . 6 (𝐼 ≈ 1o𝐼 ∈ V)
203frgpgrp 19157 . . . . . 6 (𝐼 ∈ V → 𝐺 ∈ Grp)
2119, 20syl 17 . . . . 5 (𝐼 ≈ 1o𝐺 ∈ Grp)
22 eqid 2737 . . . . . . . 8 ( ~FG𝐼) = ( ~FG𝐼)
23 eqid 2737 . . . . . . . 8 (varFGrp𝐼) = (varFGrp𝐼)
2422, 23, 3, 16vrgpf 19163 . . . . . . 7 (𝐼 ∈ V → (varFGrp𝐼):𝐼⟶(Base‘𝐺))
2519, 24syl 17 . . . . . 6 (𝐼 ≈ 1o → (varFGrp𝐼):𝐼⟶(Base‘𝐺))
26 en1uniel 8710 . . . . . 6 (𝐼 ≈ 1o 𝐼𝐼)
2725, 26ffvelrnd 6910 . . . . 5 (𝐼 ≈ 1o → ((varFGrp𝐼)‘ 𝐼) ∈ (Base‘𝐺))
28 zringgrp 20445 . . . . . . . . 9 ring ∈ Grp
2919uniexd 7535 . . . . . . . . . . 11 (𝐼 ≈ 1o 𝐼 ∈ V)
30 1zzd 12213 . . . . . . . . . . 11 (𝐼 ≈ 1o → 1 ∈ ℤ)
3129, 30fsnd 6708 . . . . . . . . . 10 (𝐼 ≈ 1o → {⟨ 𝐼, 1⟩}:{ 𝐼}⟶ℤ)
32 en1b 8705 . . . . . . . . . . . 12 (𝐼 ≈ 1o𝐼 = { 𝐼})
3332biimpi 219 . . . . . . . . . . 11 (𝐼 ≈ 1o𝐼 = { 𝐼})
3433feq2d 6536 . . . . . . . . . 10 (𝐼 ≈ 1o → ({⟨ 𝐼, 1⟩}:𝐼⟶ℤ ↔ {⟨ 𝐼, 1⟩}:{ 𝐼}⟶ℤ))
3531, 34mpbird 260 . . . . . . . . 9 (𝐼 ≈ 1o → {⟨ 𝐼, 1⟩}:𝐼⟶ℤ)
36 zringbas 20446 . . . . . . . . . 10 ℤ = (Base‘ℤring)
373, 36, 23frgpup3 19173 . . . . . . . . 9 ((ℤring ∈ Grp ∧ 𝐼 ∈ V ∧ {⟨ 𝐼, 1⟩}:𝐼⟶ℤ) → ∃!𝑓 ∈ (𝐺 GrpHom ℤring)(𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩})
3828, 19, 35, 37mp3an2i 1468 . . . . . . . 8 (𝐼 ≈ 1o → ∃!𝑓 ∈ (𝐺 GrpHom ℤring)(𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩})
3938adantr 484 . . . . . . 7 ((𝐼 ≈ 1o𝑥 ∈ (Base‘𝐺)) → ∃!𝑓 ∈ (𝐺 GrpHom ℤring)(𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩})
40 reurex 3343 . . . . . . 7 (∃!𝑓 ∈ (𝐺 GrpHom ℤring)(𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩} → ∃𝑓 ∈ (𝐺 GrpHom ℤring)(𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩})
4139, 40syl 17 . . . . . 6 ((𝐼 ≈ 1o𝑥 ∈ (Base‘𝐺)) → ∃𝑓 ∈ (𝐺 GrpHom ℤring)(𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩})
42 fveq1 6721 . . . . . . . . . 10 ((𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩} → ((𝑓 ∘ (varFGrp𝐼))‘ 𝐼) = ({⟨ 𝐼, 1⟩}‘ 𝐼))
4325, 26fvco3d 6816 . . . . . . . . . . 11 (𝐼 ≈ 1o → ((𝑓 ∘ (varFGrp𝐼))‘ 𝐼) = (𝑓‘((varFGrp𝐼)‘ 𝐼)))
44 1z 12212 . . . . . . . . . . . 12 1 ∈ ℤ
45 fvsng 7000 . . . . . . . . . . . 12 (( 𝐼 ∈ V ∧ 1 ∈ ℤ) → ({⟨ 𝐼, 1⟩}‘ 𝐼) = 1)
4629, 44, 45sylancl 589 . . . . . . . . . . 11 (𝐼 ≈ 1o → ({⟨ 𝐼, 1⟩}‘ 𝐼) = 1)
4743, 46eqeq12d 2753 . . . . . . . . . 10 (𝐼 ≈ 1o → (((𝑓 ∘ (varFGrp𝐼))‘ 𝐼) = ({⟨ 𝐼, 1⟩}‘ 𝐼) ↔ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1))
4842, 47syl5ib 247 . . . . . . . . 9 (𝐼 ≈ 1o → ((𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩} → (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1))
4948ad2antrr 726 . . . . . . . 8 (((𝐼 ≈ 1o𝑥 ∈ (Base‘𝐺)) ∧ 𝑓 ∈ (𝐺 GrpHom ℤring)) → ((𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩} → (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1))
5016, 36ghmf 18631 . . . . . . . . . . . . 13 (𝑓 ∈ (𝐺 GrpHom ℤring) → 𝑓:(Base‘𝐺)⟶ℤ)
5150ad2antrl 728 . . . . . . . . . . . 12 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → 𝑓:(Base‘𝐺)⟶ℤ)
5251ffvelrnda 6909 . . . . . . . . . . 11 (((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) ∧ 𝑥 ∈ (Base‘𝐺)) → (𝑓𝑥) ∈ ℤ)
5352an32s 652 . . . . . . . . . 10 (((𝐼 ≈ 1o𝑥 ∈ (Base‘𝐺)) ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑓𝑥) ∈ ℤ)
54 mptresid 5923 . . . . . . . . . . . . . 14 ( I ↾ (Base‘𝐺)) = (𝑥 ∈ (Base‘𝐺) ↦ 𝑥)
553, 16, 23frgpup3 19173 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ Grp ∧ 𝐼 ∈ V ∧ (varFGrp𝐼):𝐼⟶(Base‘𝐺)) → ∃!𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘ (varFGrp𝐼)) = (varFGrp𝐼))
5621, 19, 25, 55syl3anc 1373 . . . . . . . . . . . . . . . . 17 (𝐼 ≈ 1o → ∃!𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘ (varFGrp𝐼)) = (varFGrp𝐼))
57 reurmo 3345 . . . . . . . . . . . . . . . . 17 (∃!𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘ (varFGrp𝐼)) = (varFGrp𝐼) → ∃*𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘ (varFGrp𝐼)) = (varFGrp𝐼))
5856, 57syl 17 . . . . . . . . . . . . . . . 16 (𝐼 ≈ 1o → ∃*𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘ (varFGrp𝐼)) = (varFGrp𝐼))
5958adantr 484 . . . . . . . . . . . . . . 15 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ∃*𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘ (varFGrp𝐼)) = (varFGrp𝐼))
6021adantr 484 . . . . . . . . . . . . . . . 16 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → 𝐺 ∈ Grp)
6116idghm 18642 . . . . . . . . . . . . . . . 16 (𝐺 ∈ Grp → ( I ↾ (Base‘𝐺)) ∈ (𝐺 GrpHom 𝐺))
6260, 61syl 17 . . . . . . . . . . . . . . 15 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ( I ↾ (Base‘𝐺)) ∈ (𝐺 GrpHom 𝐺))
6325adantr 484 . . . . . . . . . . . . . . . 16 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (varFGrp𝐼):𝐼⟶(Base‘𝐺))
64 fcoi2 6599 . . . . . . . . . . . . . . . 16 ((varFGrp𝐼):𝐼⟶(Base‘𝐺) → (( I ↾ (Base‘𝐺)) ∘ (varFGrp𝐼)) = (varFGrp𝐼))
6563, 64syl 17 . . . . . . . . . . . . . . 15 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (( I ↾ (Base‘𝐺)) ∘ (varFGrp𝐼)) = (varFGrp𝐼))
6651feqmptd 6785 . . . . . . . . . . . . . . . . 17 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → 𝑓 = (𝑥 ∈ (Base‘𝐺) ↦ (𝑓𝑥)))
67 eqidd 2738 . . . . . . . . . . . . . . . . 17 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))) = (𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
68 oveq1 7225 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑓𝑥) → (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
6952, 66, 67, 68fmptco 6949 . . . . . . . . . . . . . . . 16 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ((𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∘ 𝑓) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
7027adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ((varFGrp𝐼)‘ 𝐼) ∈ (Base‘𝐺))
71 eqid 2737 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))) = (𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
7217, 71, 16mulgghm2 20468 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ Grp ∧ ((varFGrp𝐼)‘ 𝐼) ∈ (Base‘𝐺)) → (𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∈ (ℤring GrpHom 𝐺))
7360, 70, 72syl2anc 587 . . . . . . . . . . . . . . . . 17 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∈ (ℤring GrpHom 𝐺))
74 simprl 771 . . . . . . . . . . . . . . . . 17 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → 𝑓 ∈ (𝐺 GrpHom ℤring))
75 ghmco 18647 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∈ (ℤring GrpHom 𝐺) ∧ 𝑓 ∈ (𝐺 GrpHom ℤring)) → ((𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∘ 𝑓) ∈ (𝐺 GrpHom 𝐺))
7673, 74, 75syl2anc 587 . . . . . . . . . . . . . . . 16 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ((𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∘ 𝑓) ∈ (𝐺 GrpHom 𝐺))
7769, 76eqeltrrd 2839 . . . . . . . . . . . . . . 15 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∈ (𝐺 GrpHom 𝐺))
7833adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → 𝐼 = { 𝐼})
7978eleq2d 2823 . . . . . . . . . . . . . . . . . . 19 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑦𝐼𝑦 ∈ { 𝐼}))
80 simprr 773 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)
8180oveq1d 7233 . . . . . . . . . . . . . . . . . . . . 21 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ((𝑓‘((varFGrp𝐼)‘ 𝐼))(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = (1(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
8216, 17mulg1 18504 . . . . . . . . . . . . . . . . . . . . . 22 (((varFGrp𝐼)‘ 𝐼) ∈ (Base‘𝐺) → (1(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((varFGrp𝐼)‘ 𝐼))
8370, 82syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (1(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((varFGrp𝐼)‘ 𝐼))
8481, 83eqtrd 2777 . . . . . . . . . . . . . . . . . . . 20 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ((𝑓‘((varFGrp𝐼)‘ 𝐼))(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((varFGrp𝐼)‘ 𝐼))
85 elsni 4563 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ { 𝐼} → 𝑦 = 𝐼)
8685fveq2d 6726 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ { 𝐼} → ((varFGrp𝐼)‘𝑦) = ((varFGrp𝐼)‘ 𝐼))
8786fveq2d 6726 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ { 𝐼} → (𝑓‘((varFGrp𝐼)‘𝑦)) = (𝑓‘((varFGrp𝐼)‘ 𝐼)))
8887oveq1d 7233 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ { 𝐼} → ((𝑓‘((varFGrp𝐼)‘𝑦))(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((𝑓‘((varFGrp𝐼)‘ 𝐼))(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
8988, 86eqeq12d 2753 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ { 𝐼} → (((𝑓‘((varFGrp𝐼)‘𝑦))(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((varFGrp𝐼)‘𝑦) ↔ ((𝑓‘((varFGrp𝐼)‘ 𝐼))(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((varFGrp𝐼)‘ 𝐼)))
9084, 89syl5ibrcom 250 . . . . . . . . . . . . . . . . . . 19 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑦 ∈ { 𝐼} → ((𝑓‘((varFGrp𝐼)‘𝑦))(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((varFGrp𝐼)‘𝑦)))
9179, 90sylbid 243 . . . . . . . . . . . . . . . . . 18 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑦𝐼 → ((𝑓‘((varFGrp𝐼)‘𝑦))(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((varFGrp𝐼)‘𝑦)))
9291imp 410 . . . . . . . . . . . . . . . . 17 (((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) ∧ 𝑦𝐼) → ((𝑓‘((varFGrp𝐼)‘𝑦))(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((varFGrp𝐼)‘𝑦))
9392mpteq2dva 5155 . . . . . . . . . . . . . . . 16 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑦𝐼 ↦ ((𝑓‘((varFGrp𝐼)‘𝑦))(.g𝐺)((varFGrp𝐼)‘ 𝐼))) = (𝑦𝐼 ↦ ((varFGrp𝐼)‘𝑦)))
9463ffvelrnda 6909 . . . . . . . . . . . . . . . . 17 (((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) ∧ 𝑦𝐼) → ((varFGrp𝐼)‘𝑦) ∈ (Base‘𝐺))
9563feqmptd 6785 . . . . . . . . . . . . . . . . 17 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (varFGrp𝐼) = (𝑦𝐼 ↦ ((varFGrp𝐼)‘𝑦)))
96 eqidd 2738 . . . . . . . . . . . . . . . . 17 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
97 fveq2 6722 . . . . . . . . . . . . . . . . . 18 (𝑥 = ((varFGrp𝐼)‘𝑦) → (𝑓𝑥) = (𝑓‘((varFGrp𝐼)‘𝑦)))
9897oveq1d 7233 . . . . . . . . . . . . . . . . 17 (𝑥 = ((varFGrp𝐼)‘𝑦) → ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((𝑓‘((varFGrp𝐼)‘𝑦))(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
9994, 95, 96, 98fmptco 6949 . . . . . . . . . . . . . . . 16 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ((𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∘ (varFGrp𝐼)) = (𝑦𝐼 ↦ ((𝑓‘((varFGrp𝐼)‘𝑦))(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
10093, 99, 953eqtr4d 2787 . . . . . . . . . . . . . . 15 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ((𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∘ (varFGrp𝐼)) = (varFGrp𝐼))
101 coeq1 5731 . . . . . . . . . . . . . . . . 17 (𝑔 = ( I ↾ (Base‘𝐺)) → (𝑔 ∘ (varFGrp𝐼)) = (( I ↾ (Base‘𝐺)) ∘ (varFGrp𝐼)))
102101eqeq1d 2739 . . . . . . . . . . . . . . . 16 (𝑔 = ( I ↾ (Base‘𝐺)) → ((𝑔 ∘ (varFGrp𝐼)) = (varFGrp𝐼) ↔ (( I ↾ (Base‘𝐺)) ∘ (varFGrp𝐼)) = (varFGrp𝐼)))
103 coeq1 5731 . . . . . . . . . . . . . . . . 17 (𝑔 = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) → (𝑔 ∘ (varFGrp𝐼)) = ((𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∘ (varFGrp𝐼)))
104103eqeq1d 2739 . . . . . . . . . . . . . . . 16 (𝑔 = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) → ((𝑔 ∘ (varFGrp𝐼)) = (varFGrp𝐼) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∘ (varFGrp𝐼)) = (varFGrp𝐼)))
105102, 104rmoi 3808 . . . . . . . . . . . . . . 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𝐼)‘ 𝐼))))
10659, 62, 65, 77, 100, 105syl122anc 1381 . . . . . . . . . . . . . 14 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ( I ↾ (Base‘𝐺)) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
10754, 106eqtr3id 2792 . . . . . . . . . . . . 13 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑥 ∈ (Base‘𝐺) ↦ 𝑥) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
108 mpteqb 6842 . . . . . . . . . . . . . 14 (∀𝑥 ∈ (Base‘𝐺)𝑥 ∈ (Base‘𝐺) → ((𝑥 ∈ (Base‘𝐺) ↦ 𝑥) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ↔ ∀𝑥 ∈ (Base‘𝐺)𝑥 = ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
109 id 22 . . . . . . . . . . . . . 14 (𝑥 ∈ (Base‘𝐺) → 𝑥 ∈ (Base‘𝐺))
110108, 109mprg 3075 . . . . . . . . . . . . 13 ((𝑥 ∈ (Base‘𝐺) ↦ 𝑥) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ↔ ∀𝑥 ∈ (Base‘𝐺)𝑥 = ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
111107, 110sylib 221 . . . . . . . . . . . 12 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ∀𝑥 ∈ (Base‘𝐺)𝑥 = ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
112111r19.21bi 3130 . . . . . . . . . . 11 (((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) ∧ 𝑥 ∈ (Base‘𝐺)) → 𝑥 = ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
113112an32s 652 . . . . . . . . . 10 (((𝐼 ≈ 1o𝑥 ∈ (Base‘𝐺)) ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → 𝑥 = ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
11468rspceeqv 3557 . . . . . . . . . 10 (((𝑓𝑥) ∈ ℤ ∧ 𝑥 = ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) → ∃𝑛 ∈ ℤ 𝑥 = (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
11553, 113, 114syl2anc 587 . . . . . . . . 9 (((𝐼 ≈ 1o𝑥 ∈ (Base‘𝐺)) ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ∃𝑛 ∈ ℤ 𝑥 = (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
116115expr 460 . . . . . . . 8 (((𝐼 ≈ 1o𝑥 ∈ (Base‘𝐺)) ∧ 𝑓 ∈ (𝐺 GrpHom ℤring)) → ((𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1 → ∃𝑛 ∈ ℤ 𝑥 = (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
11749, 116syld 47 . . . . . . 7 (((𝐼 ≈ 1o𝑥 ∈ (Base‘𝐺)) ∧ 𝑓 ∈ (𝐺 GrpHom ℤring)) → ((𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩} → ∃𝑛 ∈ ℤ 𝑥 = (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
118117rexlimdva 3208 . . . . . 6 ((𝐼 ≈ 1o𝑥 ∈ (Base‘𝐺)) → (∃𝑓 ∈ (𝐺 GrpHom ℤring)(𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩} → ∃𝑛 ∈ ℤ 𝑥 = (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
11941, 118mpd 15 . . . . 5 ((𝐼 ≈ 1o𝑥 ∈ (Base‘𝐺)) → ∃𝑛 ∈ ℤ 𝑥 = (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
12016, 17, 21, 27, 119iscygd 19276 . . . 4 (𝐼 ≈ 1o𝐺 ∈ CycGrp)
12115, 120jaoi 857 . . 3 ((𝐼 ≺ 1o𝐼 ≈ 1o) → 𝐺 ∈ CycGrp)
1221, 121sylbi 220 . 2 (𝐼 ≼ 1o𝐺 ∈ CycGrp)
123 cygabl 19280 . . 3 (𝐺 ∈ CycGrp → 𝐺 ∈ Abel)
1243frgpnabl 19265 . . . . 5 (1o𝐼 → ¬ 𝐺 ∈ Abel)
125124con2i 141 . . . 4 (𝐺 ∈ Abel → ¬ 1o𝐼)
126 ablgrp 19180 . . . . . 6 (𝐺 ∈ Abel → 𝐺 ∈ Grp)
127 eqid 2737 . . . . . . 7 (0g𝐺) = (0g𝐺)
12816, 127grpidcl 18400 . . . . . 6 (𝐺 ∈ Grp → (0g𝐺) ∈ (Base‘𝐺))
1293, 16elbasfv 16771 . . . . . 6 ((0g𝐺) ∈ (Base‘𝐺) → 𝐼 ∈ V)
130126, 128, 1293syl 18 . . . . 5 (𝐺 ∈ Abel → 𝐼 ∈ V)
131 1onn 8372 . . . . . 6 1o ∈ ω
132 nnfi 8850 . . . . . 6 (1o ∈ ω → 1o ∈ Fin)
133131, 132ax-mp 5 . . . . 5 1o ∈ Fin
134 fidomtri2 9615 . . . . 5 ((𝐼 ∈ V ∧ 1o ∈ Fin) → (𝐼 ≼ 1o ↔ ¬ 1o𝐼))
135130, 133, 134sylancl 589 . . . 4 (𝐺 ∈ Abel → (𝐼 ≼ 1o ↔ ¬ 1o𝐼))
136125, 135mpbird 260 . . 3 (𝐺 ∈ Abel → 𝐼 ≼ 1o)
137123, 136syl 17 . 2 (𝐺 ∈ CycGrp → 𝐼 ≼ 1o)
138122, 137impbii 212 1 (𝐼 ≼ 1o𝐺 ∈ CycGrp)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 847   = wceq 1543  wcel 2110  wral 3061  wrex 3062  ∃!wreu 3063  ∃*wrmo 3064  Vcvv 3413  c0 4242  {csn 4546  cop 4552   cuni 4824   class class class wbr 5058  cmpt 5140   I cid 5459  cres 5558  ccom 5560  wf 6381  cfv 6385  (class class class)co 7218  ωcom 7649  1oc1o 8200  cen 8628  cdom 8629  csdm 8630  Fincfn 8631  1c1 10735  cz 12181  Basecbs 16765  0gc0g 16949  Grpcgrp 18370  .gcmg 18493   GrpHom cghm 18624   ~FG cefg 19101  freeGrpcfrgp 19102  varFGrpcvrgp 19103  Abelcabl 19176  CycGrpccyg 19266  ringzring 20440
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5184  ax-sep 5197  ax-nul 5204  ax-pow 5263  ax-pr 5327  ax-un 7528  ax-cnex 10790  ax-resscn 10791  ax-1cn 10792  ax-icn 10793  ax-addcl 10794  ax-addrcl 10795  ax-mulcl 10796  ax-mulrcl 10797  ax-mulcom 10798  ax-addass 10799  ax-mulass 10800  ax-distr 10801  ax-i2m1 10802  ax-1ne0 10803  ax-1rid 10804  ax-rnegex 10805  ax-rrecex 10806  ax-cnre 10807  ax-pre-lttri 10808  ax-pre-lttrn 10809  ax-pre-ltadd 10810  ax-pre-mulgt0 10811  ax-addf 10813  ax-mulf 10814
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3415  df-sbc 3700  df-csb 3817  df-dif 3874  df-un 3876  df-in 3878  df-ss 3888  df-pss 3890  df-nul 4243  df-if 4445  df-pw 4520  df-sn 4547  df-pr 4549  df-tp 4551  df-op 4553  df-ot 4555  df-uni 4825  df-int 4865  df-iun 4911  df-iin 4912  df-br 5059  df-opab 5121  df-mpt 5141  df-tr 5167  df-id 5460  df-eprel 5465  df-po 5473  df-so 5474  df-fr 5514  df-we 5516  df-xp 5562  df-rel 5563  df-cnv 5564  df-co 5565  df-dm 5566  df-rn 5567  df-res 5568  df-ima 5569  df-pred 6165  df-ord 6221  df-on 6222  df-lim 6223  df-suc 6224  df-iota 6343  df-fun 6387  df-fn 6388  df-f 6389  df-f1 6390  df-fo 6391  df-f1o 6392  df-fv 6393  df-riota 7175  df-ov 7221  df-oprab 7222  df-mpo 7223  df-om 7650  df-1st 7766  df-2nd 7767  df-wrecs 8052  df-recs 8113  df-rdg 8151  df-1o 8207  df-2o 8208  df-er 8396  df-ec 8398  df-qs 8402  df-map 8515  df-en 8632  df-dom 8633  df-sdom 8634  df-fin 8635  df-sup 9063  df-inf 9064  df-card 9560  df-pnf 10874  df-mnf 10875  df-xr 10876  df-ltxr 10877  df-le 10878  df-sub 11069  df-neg 11070  df-nn 11836  df-2 11898  df-3 11899  df-4 11900  df-5 11901  df-6 11902  df-7 11903  df-8 11904  df-9 11905  df-n0 12096  df-xnn0 12168  df-z 12182  df-dec 12299  df-uz 12444  df-rp 12592  df-fz 13101  df-fzo 13244  df-seq 13580  df-hash 13902  df-word 14075  df-lsw 14123  df-concat 14131  df-s1 14158  df-substr 14211  df-pfx 14241  df-splice 14320  df-reverse 14329  df-s2 14418  df-struct 16705  df-sets 16722  df-slot 16740  df-ndx 16750  df-base 16766  df-ress 16790  df-plusg 16820  df-mulr 16821  df-starv 16822  df-sca 16823  df-vsca 16824  df-ip 16825  df-tset 16826  df-ple 16827  df-ds 16829  df-unif 16830  df-0g 16951  df-gsum 16952  df-imas 17018  df-qus 17019  df-mgm 18119  df-sgrp 18168  df-mnd 18179  df-mhm 18223  df-submnd 18224  df-frmd 18281  df-vrmd 18282  df-grp 18373  df-minusg 18374  df-mulg 18494  df-subg 18545  df-ghm 18625  df-efg 19104  df-frgp 19105  df-vrgp 19106  df-cmn 19177  df-abl 19178  df-cyg 19267  df-mgp 19510  df-ur 19522  df-ring 19569  df-cring 19570  df-subrg 19803  df-cnfld 20369  df-zring 20441
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator