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

Theorem frgpcyg 20636
 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 8531 . . 3 (𝐼 ≼ 1o ↔ (𝐼 ≺ 1o𝐼 ≈ 1o))
2 sdom1 8710 . . . . 5 (𝐼 ≺ 1o𝐼 = ∅)
3 frgpcyg.g . . . . . . 7 𝐺 = (freeGrp‘𝐼)
4 fveq2 6666 . . . . . . 7 (𝐼 = ∅ → (freeGrp‘𝐼) = (freeGrp‘∅))
53, 4syl5eq 2872 . . . . . 6 (𝐼 = ∅ → 𝐺 = (freeGrp‘∅))
6 0ex 5207 . . . . . . . 8 ∅ ∈ V
7 eqid 2825 . . . . . . . . 9 (freeGrp‘∅) = (freeGrp‘∅)
87frgpgrp 18810 . . . . . . . 8 (∅ ∈ V → (freeGrp‘∅) ∈ Grp)
96, 8ax-mp 5 . . . . . . 7 (freeGrp‘∅) ∈ Grp
10 eqid 2825 . . . . . . . 8 (Base‘(freeGrp‘∅)) = (Base‘(freeGrp‘∅))
117, 100frgp 18827 . . . . . . 7 (Base‘(freeGrp‘∅)) ≈ 1o
12100cyg 18935 . . . . . . 7 (((freeGrp‘∅) ∈ Grp ∧ (Base‘(freeGrp‘∅)) ≈ 1o) → (freeGrp‘∅) ∈ CycGrp)
139, 11, 12mp2an 688 . . . . . 6 (freeGrp‘∅) ∈ CycGrp
145, 13syl6eqel 2925 . . . . 5 (𝐼 = ∅ → 𝐺 ∈ CycGrp)
152, 14sylbi 218 . . . 4 (𝐼 ≺ 1o𝐺 ∈ CycGrp)
16 eqid 2825 . . . . 5 (Base‘𝐺) = (Base‘𝐺)
17 eqid 2825 . . . . 5 (.g𝐺) = (.g𝐺)
18 relen 8506 . . . . . . 7 Rel ≈
1918brrelex1i 5606 . . . . . 6 (𝐼 ≈ 1o𝐼 ∈ V)
203frgpgrp 18810 . . . . . 6 (𝐼 ∈ V → 𝐺 ∈ Grp)
2119, 20syl 17 . . . . 5 (𝐼 ≈ 1o𝐺 ∈ Grp)
22 eqid 2825 . . . . . . . 8 ( ~FG𝐼) = ( ~FG𝐼)
23 eqid 2825 . . . . . . . 8 (varFGrp𝐼) = (varFGrp𝐼)
2422, 23, 3, 16vrgpf 18816 . . . . . . 7 (𝐼 ∈ V → (varFGrp𝐼):𝐼⟶(Base‘𝐺))
2519, 24syl 17 . . . . . 6 (𝐼 ≈ 1o → (varFGrp𝐼):𝐼⟶(Base‘𝐺))
26 en1uniel 8573 . . . . . 6 (𝐼 ≈ 1o 𝐼𝐼)
2725, 26ffvelrnd 6847 . . . . 5 (𝐼 ≈ 1o → ((varFGrp𝐼)‘ 𝐼) ∈ (Base‘𝐺))
28 zringgrp 20538 . . . . . . . . 9 ring ∈ Grp
29 uniexg 7460 . . . . . . . . . . . 12 (𝐼 ∈ V → 𝐼 ∈ V)
3019, 29syl 17 . . . . . . . . . . 11 (𝐼 ≈ 1o 𝐼 ∈ V)
31 1zzd 12005 . . . . . . . . . . 11 (𝐼 ≈ 1o → 1 ∈ ℤ)
3230, 31fsnd 6653 . . . . . . . . . 10 (𝐼 ≈ 1o → {⟨ 𝐼, 1⟩}:{ 𝐼}⟶ℤ)
33 en1b 8569 . . . . . . . . . . . 12 (𝐼 ≈ 1o𝐼 = { 𝐼})
3433biimpi 217 . . . . . . . . . . 11 (𝐼 ≈ 1o𝐼 = { 𝐼})
3534feq2d 6496 . . . . . . . . . 10 (𝐼 ≈ 1o → ({⟨ 𝐼, 1⟩}:𝐼⟶ℤ ↔ {⟨ 𝐼, 1⟩}:{ 𝐼}⟶ℤ))
3632, 35mpbird 258 . . . . . . . . 9 (𝐼 ≈ 1o → {⟨ 𝐼, 1⟩}:𝐼⟶ℤ)
37 zringbas 20539 . . . . . . . . . 10 ℤ = (Base‘ℤring)
383, 37, 23frgpup3 18826 . . . . . . . . 9 ((ℤring ∈ Grp ∧ 𝐼 ∈ V ∧ {⟨ 𝐼, 1⟩}:𝐼⟶ℤ) → ∃!𝑓 ∈ (𝐺 GrpHom ℤring)(𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩})
3928, 19, 36, 38mp3an2i 1459 . . . . . . . 8 (𝐼 ≈ 1o → ∃!𝑓 ∈ (𝐺 GrpHom ℤring)(𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩})
4039adantr 481 . . . . . . 7 ((𝐼 ≈ 1o𝑥 ∈ (Base‘𝐺)) → ∃!𝑓 ∈ (𝐺 GrpHom ℤring)(𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩})
41 reurex 3436 . . . . . . 7 (∃!𝑓 ∈ (𝐺 GrpHom ℤring)(𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩} → ∃𝑓 ∈ (𝐺 GrpHom ℤring)(𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩})
4240, 41syl 17 . . . . . 6 ((𝐼 ≈ 1o𝑥 ∈ (Base‘𝐺)) → ∃𝑓 ∈ (𝐺 GrpHom ℤring)(𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩})
43 fveq1 6665 . . . . . . . . . 10 ((𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩} → ((𝑓 ∘ (varFGrp𝐼))‘ 𝐼) = ({⟨ 𝐼, 1⟩}‘ 𝐼))
4425, 26fvco3d 6757 . . . . . . . . . . 11 (𝐼 ≈ 1o → ((𝑓 ∘ (varFGrp𝐼))‘ 𝐼) = (𝑓‘((varFGrp𝐼)‘ 𝐼)))
45 1z 12004 . . . . . . . . . . . 12 1 ∈ ℤ
46 fvsng 6937 . . . . . . . . . . . 12 (( 𝐼 ∈ V ∧ 1 ∈ ℤ) → ({⟨ 𝐼, 1⟩}‘ 𝐼) = 1)
4730, 45, 46sylancl 586 . . . . . . . . . . 11 (𝐼 ≈ 1o → ({⟨ 𝐼, 1⟩}‘ 𝐼) = 1)
4844, 47eqeq12d 2841 . . . . . . . . . 10 (𝐼 ≈ 1o → (((𝑓 ∘ (varFGrp𝐼))‘ 𝐼) = ({⟨ 𝐼, 1⟩}‘ 𝐼) ↔ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1))
4943, 48syl5ib 245 . . . . . . . . 9 (𝐼 ≈ 1o → ((𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩} → (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1))
5049ad2antrr 722 . . . . . . . 8 (((𝐼 ≈ 1o𝑥 ∈ (Base‘𝐺)) ∧ 𝑓 ∈ (𝐺 GrpHom ℤring)) → ((𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩} → (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1))
5116, 37ghmf 18294 . . . . . . . . . . . . 13 (𝑓 ∈ (𝐺 GrpHom ℤring) → 𝑓:(Base‘𝐺)⟶ℤ)
5251ad2antrl 724 . . . . . . . . . . . 12 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → 𝑓:(Base‘𝐺)⟶ℤ)
5352ffvelrnda 6846 . . . . . . . . . . 11 (((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) ∧ 𝑥 ∈ (Base‘𝐺)) → (𝑓𝑥) ∈ ℤ)
5453an32s 648 . . . . . . . . . 10 (((𝐼 ≈ 1o𝑥 ∈ (Base‘𝐺)) ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑓𝑥) ∈ ℤ)
55 mptresid 5916 . . . . . . . . . . . . . 14 ( I ↾ (Base‘𝐺)) = (𝑥 ∈ (Base‘𝐺) ↦ 𝑥)
563, 16, 23frgpup3 18826 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ Grp ∧ 𝐼 ∈ V ∧ (varFGrp𝐼):𝐼⟶(Base‘𝐺)) → ∃!𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘ (varFGrp𝐼)) = (varFGrp𝐼))
5721, 19, 25, 56syl3anc 1365 . . . . . . . . . . . . . . . . 17 (𝐼 ≈ 1o → ∃!𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘ (varFGrp𝐼)) = (varFGrp𝐼))
58 reurmo 3438 . . . . . . . . . . . . . . . . 17 (∃!𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘ (varFGrp𝐼)) = (varFGrp𝐼) → ∃*𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘ (varFGrp𝐼)) = (varFGrp𝐼))
5957, 58syl 17 . . . . . . . . . . . . . . . 16 (𝐼 ≈ 1o → ∃*𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘ (varFGrp𝐼)) = (varFGrp𝐼))
6059adantr 481 . . . . . . . . . . . . . . 15 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ∃*𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘ (varFGrp𝐼)) = (varFGrp𝐼))
6121adantr 481 . . . . . . . . . . . . . . . 16 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → 𝐺 ∈ Grp)
6216idghm 18305 . . . . . . . . . . . . . . . 16 (𝐺 ∈ Grp → ( I ↾ (Base‘𝐺)) ∈ (𝐺 GrpHom 𝐺))
6361, 62syl 17 . . . . . . . . . . . . . . 15 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ( I ↾ (Base‘𝐺)) ∈ (𝐺 GrpHom 𝐺))
6425adantr 481 . . . . . . . . . . . . . . . 16 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (varFGrp𝐼):𝐼⟶(Base‘𝐺))
65 fcoi2 6549 . . . . . . . . . . . . . . . 16 ((varFGrp𝐼):𝐼⟶(Base‘𝐺) → (( I ↾ (Base‘𝐺)) ∘ (varFGrp𝐼)) = (varFGrp𝐼))
6664, 65syl 17 . . . . . . . . . . . . . . 15 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (( I ↾ (Base‘𝐺)) ∘ (varFGrp𝐼)) = (varFGrp𝐼))
6752feqmptd 6729 . . . . . . . . . . . . . . . . 17 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → 𝑓 = (𝑥 ∈ (Base‘𝐺) ↦ (𝑓𝑥)))
68 eqidd 2826 . . . . . . . . . . . . . . . . 17 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))) = (𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
69 oveq1 7158 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑓𝑥) → (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
7053, 67, 68, 69fmptco 6886 . . . . . . . . . . . . . . . 16 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ((𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∘ 𝑓) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
7127adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ((varFGrp𝐼)‘ 𝐼) ∈ (Base‘𝐺))
72 eqid 2825 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))) = (𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
7317, 72, 16mulgghm2 20560 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ Grp ∧ ((varFGrp𝐼)‘ 𝐼) ∈ (Base‘𝐺)) → (𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∈ (ℤring GrpHom 𝐺))
7461, 71, 73syl2anc 584 . . . . . . . . . . . . . . . . 17 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∈ (ℤring GrpHom 𝐺))
75 simprl 767 . . . . . . . . . . . . . . . . 17 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → 𝑓 ∈ (𝐺 GrpHom ℤring))
76 ghmco 18310 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∈ (ℤring GrpHom 𝐺) ∧ 𝑓 ∈ (𝐺 GrpHom ℤring)) → ((𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∘ 𝑓) ∈ (𝐺 GrpHom 𝐺))
7774, 75, 76syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ((𝑛 ∈ ℤ ↦ (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∘ 𝑓) ∈ (𝐺 GrpHom 𝐺))
7870, 77eqeltrrd 2918 . . . . . . . . . . . . . . 15 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∈ (𝐺 GrpHom 𝐺))
7934adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → 𝐼 = { 𝐼})
8079eleq2d 2902 . . . . . . . . . . . . . . . . . . 19 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑦𝐼𝑦 ∈ { 𝐼}))
81 simprr 769 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)
8281oveq1d 7166 . . . . . . . . . . . . . . . . . . . . 21 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ((𝑓‘((varFGrp𝐼)‘ 𝐼))(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = (1(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
8316, 17mulg1 18167 . . . . . . . . . . . . . . . . . . . . . 22 (((varFGrp𝐼)‘ 𝐼) ∈ (Base‘𝐺) → (1(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((varFGrp𝐼)‘ 𝐼))
8471, 83syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (1(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((varFGrp𝐼)‘ 𝐼))
8582, 84eqtrd 2860 . . . . . . . . . . . . . . . . . . . 20 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ((𝑓‘((varFGrp𝐼)‘ 𝐼))(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((varFGrp𝐼)‘ 𝐼))
86 elsni 4580 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ { 𝐼} → 𝑦 = 𝐼)
8786fveq2d 6670 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ { 𝐼} → ((varFGrp𝐼)‘𝑦) = ((varFGrp𝐼)‘ 𝐼))
8887fveq2d 6670 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ { 𝐼} → (𝑓‘((varFGrp𝐼)‘𝑦)) = (𝑓‘((varFGrp𝐼)‘ 𝐼)))
8988oveq1d 7166 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ { 𝐼} → ((𝑓‘((varFGrp𝐼)‘𝑦))(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((𝑓‘((varFGrp𝐼)‘ 𝐼))(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
9089, 87eqeq12d 2841 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ { 𝐼} → (((𝑓‘((varFGrp𝐼)‘𝑦))(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((varFGrp𝐼)‘𝑦) ↔ ((𝑓‘((varFGrp𝐼)‘ 𝐼))(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((varFGrp𝐼)‘ 𝐼)))
9185, 90syl5ibrcom 248 . . . . . . . . . . . . . . . . . . 19 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑦 ∈ { 𝐼} → ((𝑓‘((varFGrp𝐼)‘𝑦))(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((varFGrp𝐼)‘𝑦)))
9280, 91sylbid 241 . . . . . . . . . . . . . . . . . 18 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑦𝐼 → ((𝑓‘((varFGrp𝐼)‘𝑦))(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((varFGrp𝐼)‘𝑦)))
9392imp 407 . . . . . . . . . . . . . . . . 17 (((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) ∧ 𝑦𝐼) → ((𝑓‘((varFGrp𝐼)‘𝑦))(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((varFGrp𝐼)‘𝑦))
9493mpteq2dva 5157 . . . . . . . . . . . . . . . 16 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑦𝐼 ↦ ((𝑓‘((varFGrp𝐼)‘𝑦))(.g𝐺)((varFGrp𝐼)‘ 𝐼))) = (𝑦𝐼 ↦ ((varFGrp𝐼)‘𝑦)))
9564ffvelrnda 6846 . . . . . . . . . . . . . . . . 17 (((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) ∧ 𝑦𝐼) → ((varFGrp𝐼)‘𝑦) ∈ (Base‘𝐺))
9664feqmptd 6729 . . . . . . . . . . . . . . . . 17 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (varFGrp𝐼) = (𝑦𝐼 ↦ ((varFGrp𝐼)‘𝑦)))
97 eqidd 2826 . . . . . . . . . . . . . . . . 17 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
98 fveq2 6666 . . . . . . . . . . . . . . . . . 18 (𝑥 = ((varFGrp𝐼)‘𝑦) → (𝑓𝑥) = (𝑓‘((varFGrp𝐼)‘𝑦)))
9998oveq1d 7166 . . . . . . . . . . . . . . . . 17 (𝑥 = ((varFGrp𝐼)‘𝑦) → ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼)) = ((𝑓‘((varFGrp𝐼)‘𝑦))(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
10095, 96, 97, 99fmptco 6886 . . . . . . . . . . . . . . . 16 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ((𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∘ (varFGrp𝐼)) = (𝑦𝐼 ↦ ((𝑓‘((varFGrp𝐼)‘𝑦))(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
10194, 100, 963eqtr4d 2870 . . . . . . . . . . . . . . 15 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ((𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∘ (varFGrp𝐼)) = (varFGrp𝐼))
102 coeq1 5726 . . . . . . . . . . . . . . . . 17 (𝑔 = ( I ↾ (Base‘𝐺)) → (𝑔 ∘ (varFGrp𝐼)) = (( I ↾ (Base‘𝐺)) ∘ (varFGrp𝐼)))
103102eqeq1d 2827 . . . . . . . . . . . . . . . 16 (𝑔 = ( I ↾ (Base‘𝐺)) → ((𝑔 ∘ (varFGrp𝐼)) = (varFGrp𝐼) ↔ (( I ↾ (Base‘𝐺)) ∘ (varFGrp𝐼)) = (varFGrp𝐼)))
104 coeq1 5726 . . . . . . . . . . . . . . . . 17 (𝑔 = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) → (𝑔 ∘ (varFGrp𝐼)) = ((𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∘ (varFGrp𝐼)))
105104eqeq1d 2827 . . . . . . . . . . . . . . . 16 (𝑔 = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) → ((𝑔 ∘ (varFGrp𝐼)) = (varFGrp𝐼) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ∘ (varFGrp𝐼)) = (varFGrp𝐼)))
106103, 105rmoi 3878 . . . . . . . . . . . . . . 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𝐼)‘ 𝐼))))
10760, 63, 66, 78, 101, 106syl122anc 1373 . . . . . . . . . . . . . 14 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ( I ↾ (Base‘𝐺)) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
10855, 107syl5eqr 2874 . . . . . . . . . . . . 13 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → (𝑥 ∈ (Base‘𝐺) ↦ 𝑥) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
109 mpteqb 6782 . . . . . . . . . . . . . 14 (∀𝑥 ∈ (Base‘𝐺)𝑥 ∈ (Base‘𝐺) → ((𝑥 ∈ (Base‘𝐺) ↦ 𝑥) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ↔ ∀𝑥 ∈ (Base‘𝐺)𝑥 = ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
110 id 22 . . . . . . . . . . . . . 14 (𝑥 ∈ (Base‘𝐺) → 𝑥 ∈ (Base‘𝐺))
111109, 110mprg 3156 . . . . . . . . . . . . 13 ((𝑥 ∈ (Base‘𝐺) ↦ 𝑥) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) ↔ ∀𝑥 ∈ (Base‘𝐺)𝑥 = ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
112108, 111sylib 219 . . . . . . . . . . . 12 ((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ∀𝑥 ∈ (Base‘𝐺)𝑥 = ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
113112r19.21bi 3212 . . . . . . . . . . 11 (((𝐼 ≈ 1o ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) ∧ 𝑥 ∈ (Base‘𝐺)) → 𝑥 = ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
114113an32s 648 . . . . . . . . . 10 (((𝐼 ≈ 1o𝑥 ∈ (Base‘𝐺)) ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → 𝑥 = ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
11569rspceeqv 3641 . . . . . . . . . 10 (((𝑓𝑥) ∈ ℤ ∧ 𝑥 = ((𝑓𝑥)(.g𝐺)((varFGrp𝐼)‘ 𝐼))) → ∃𝑛 ∈ ℤ 𝑥 = (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
11654, 114, 115syl2anc 584 . . . . . . . . 9 (((𝐼 ≈ 1o𝑥 ∈ (Base‘𝐺)) ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1)) → ∃𝑛 ∈ ℤ 𝑥 = (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
117116expr 457 . . . . . . . 8 (((𝐼 ≈ 1o𝑥 ∈ (Base‘𝐺)) ∧ 𝑓 ∈ (𝐺 GrpHom ℤring)) → ((𝑓‘((varFGrp𝐼)‘ 𝐼)) = 1 → ∃𝑛 ∈ ℤ 𝑥 = (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
11850, 117syld 47 . . . . . . 7 (((𝐼 ≈ 1o𝑥 ∈ (Base‘𝐺)) ∧ 𝑓 ∈ (𝐺 GrpHom ℤring)) → ((𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩} → ∃𝑛 ∈ ℤ 𝑥 = (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
119118rexlimdva 3288 . . . . . 6 ((𝐼 ≈ 1o𝑥 ∈ (Base‘𝐺)) → (∃𝑓 ∈ (𝐺 GrpHom ℤring)(𝑓 ∘ (varFGrp𝐼)) = {⟨ 𝐼, 1⟩} → ∃𝑛 ∈ ℤ 𝑥 = (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼))))
12042, 119mpd 15 . . . . 5 ((𝐼 ≈ 1o𝑥 ∈ (Base‘𝐺)) → ∃𝑛 ∈ ℤ 𝑥 = (𝑛(.g𝐺)((varFGrp𝐼)‘ 𝐼)))
12116, 17, 21, 27, 120iscygd 18928 . . . 4 (𝐼 ≈ 1o𝐺 ∈ CycGrp)
12215, 121jaoi 853 . . 3 ((𝐼 ≺ 1o𝐼 ≈ 1o) → 𝐺 ∈ CycGrp)
1231, 122sylbi 218 . 2 (𝐼 ≼ 1o𝐺 ∈ CycGrp)
124 cygabl 18932 . . 3 (𝐺 ∈ CycGrp → 𝐺 ∈ Abel)
1253frgpnabl 18917 . . . . 5 (1o𝐼 → ¬ 𝐺 ∈ Abel)
126125con2i 141 . . . 4 (𝐺 ∈ Abel → ¬ 1o𝐼)
127 ablgrp 18833 . . . . . 6 (𝐺 ∈ Abel → 𝐺 ∈ Grp)
128 eqid 2825 . . . . . . 7 (0g𝐺) = (0g𝐺)
12916, 128grpidcl 18063 . . . . . 6 (𝐺 ∈ Grp → (0g𝐺) ∈ (Base‘𝐺))
1303, 16elbasfv 16536 . . . . . 6 ((0g𝐺) ∈ (Base‘𝐺) → 𝐼 ∈ V)
131127, 129, 1303syl 18 . . . . 5 (𝐺 ∈ Abel → 𝐼 ∈ V)
132 1onn 8258 . . . . . 6 1o ∈ ω
133 nnfi 8703 . . . . . 6 (1o ∈ ω → 1o ∈ Fin)
134132, 133ax-mp 5 . . . . 5 1o ∈ Fin
135 fidomtri2 9415 . . . . 5 ((𝐼 ∈ V ∧ 1o ∈ Fin) → (𝐼 ≼ 1o ↔ ¬ 1o𝐼))
136131, 134, 135sylancl 586 . . . 4 (𝐺 ∈ Abel → (𝐼 ≼ 1o ↔ ¬ 1o𝐼))
137126, 136mpbird 258 . . 3 (𝐺 ∈ Abel → 𝐼 ≼ 1o)
138124, 137syl 17 . 2 (𝐺 ∈ CycGrp → 𝐼 ≼ 1o)
139123, 138impbii 210 1 (𝐼 ≼ 1o𝐺 ∈ CycGrp)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 843   = wceq 1530   ∈ wcel 2107  ∀wral 3142  ∃wrex 3143  ∃!wreu 3144  ∃*wrmo 3145  Vcvv 3499  ∅c0 4294  {csn 4563  ⟨cop 4569  ∪ cuni 4836   class class class wbr 5062   ↦ cmpt 5142   I cid 5457   ↾ cres 5555   ∘ ccom 5557  ⟶wf 6347  ‘cfv 6351  (class class class)co 7151  ωcom 7571  1oc1o 8089   ≈ cen 8498   ≼ cdom 8499   ≺ csdm 8500  Fincfn 8501  1c1 10530  ℤcz 11973  Basecbs 16475  0gc0g 16705  Grpcgrp 18035  .gcmg 18156   GrpHom cghm 18287   ~FG cefg 18754  freeGrpcfrgp 18755  varFGrpcvrgp 18756  Abelcabl 18829  CycGrpccyg 18918  ℤringzring 20533 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-addf 10608  ax-mulf 10609 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-nel 3128  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-ot 4572  df-uni 4837  df-int 4874  df-iun 4918  df-iin 4919  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7572  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-2o 8097  df-oadd 8100  df-er 8282  df-ec 8284  df-qs 8288  df-map 8401  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-sup 8898  df-inf 8899  df-card 9360  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-nn 11631  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-xnn0 11960  df-z 11974  df-dec 12091  df-uz 12236  df-rp 12383  df-fz 12886  df-fzo 13027  df-seq 13363  df-hash 13684  df-word 13855  df-lsw 13908  df-concat 13916  df-s1 13943  df-substr 13996  df-pfx 14026  df-splice 14105  df-reverse 14114  df-s2 14203  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-mulr 16571  df-starv 16572  df-sca 16573  df-vsca 16574  df-ip 16575  df-tset 16576  df-ple 16577  df-ds 16579  df-unif 16580  df-0g 16707  df-gsum 16708  df-imas 16773  df-qus 16774  df-mgm 17844  df-sgrp 17892  df-mnd 17903  df-mhm 17946  df-submnd 17947  df-frmd 17999  df-vrmd 18000  df-grp 18038  df-minusg 18039  df-mulg 18157  df-subg 18208  df-ghm 18288  df-efg 18757  df-frgp 18758  df-vrgp 18759  df-cmn 18830  df-abl 18831  df-cyg 18919  df-mgp 19162  df-ur 19174  df-ring 19221  df-cring 19222  df-subrg 19455  df-cnfld 20462  df-zring 20534 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator