| Step | Hyp | Ref
| Expression |
| 1 | | brdom2 9022 |
. . 3
⊢ (𝐼 ≼ 1o ↔
(𝐼 ≺ 1o
∨ 𝐼 ≈
1o)) |
| 2 | | sdom1 9278 |
. . . . 5
⊢ (𝐼 ≺ 1o ↔
𝐼 =
∅) |
| 3 | | frgpcyg.g |
. . . . . . 7
⊢ 𝐺 = (freeGrp‘𝐼) |
| 4 | | fveq2 6906 |
. . . . . . 7
⊢ (𝐼 = ∅ →
(freeGrp‘𝐼) =
(freeGrp‘∅)) |
| 5 | 3, 4 | eqtrid 2789 |
. . . . . 6
⊢ (𝐼 = ∅ → 𝐺 =
(freeGrp‘∅)) |
| 6 | | 0ex 5307 |
. . . . . . . 8
⊢ ∅
∈ V |
| 7 | | eqid 2737 |
. . . . . . . . 9
⊢
(freeGrp‘∅) = (freeGrp‘∅) |
| 8 | 7 | frgpgrp 19780 |
. . . . . . . 8
⊢ (∅
∈ V → (freeGrp‘∅) ∈ Grp) |
| 9 | 6, 8 | ax-mp 5 |
. . . . . . 7
⊢
(freeGrp‘∅) ∈ Grp |
| 10 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘(freeGrp‘∅)) =
(Base‘(freeGrp‘∅)) |
| 11 | 7, 10 | 0frgp 19797 |
. . . . . . 7
⊢
(Base‘(freeGrp‘∅)) ≈
1o |
| 12 | 10 | 0cyg 19911 |
. . . . . . 7
⊢
(((freeGrp‘∅) ∈ Grp ∧
(Base‘(freeGrp‘∅)) ≈ 1o) →
(freeGrp‘∅) ∈ CycGrp) |
| 13 | 9, 11, 12 | mp2an 692 |
. . . . . 6
⊢
(freeGrp‘∅) ∈ CycGrp |
| 14 | 5, 13 | eqeltrdi 2849 |
. . . . 5
⊢ (𝐼 = ∅ → 𝐺 ∈ CycGrp) |
| 15 | 2, 14 | sylbi 217 |
. . . 4
⊢ (𝐼 ≺ 1o →
𝐺 ∈
CycGrp) |
| 16 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝐺) =
(Base‘𝐺) |
| 17 | | eqid 2737 |
. . . . 5
⊢
(.g‘𝐺) = (.g‘𝐺) |
| 18 | | relen 8990 |
. . . . . . 7
⊢ Rel
≈ |
| 19 | 18 | brrelex1i 5741 |
. . . . . 6
⊢ (𝐼 ≈ 1o →
𝐼 ∈
V) |
| 20 | 3 | frgpgrp 19780 |
. . . . . 6
⊢ (𝐼 ∈ V → 𝐺 ∈ Grp) |
| 21 | 19, 20 | syl 17 |
. . . . 5
⊢ (𝐼 ≈ 1o →
𝐺 ∈
Grp) |
| 22 | | eqid 2737 |
. . . . . . . 8
⊢ (
~FG ‘𝐼) = ( ~FG ‘𝐼) |
| 23 | | eqid 2737 |
. . . . . . . 8
⊢
(varFGrp‘𝐼) = (varFGrp‘𝐼) |
| 24 | 22, 23, 3, 16 | vrgpf 19786 |
. . . . . . 7
⊢ (𝐼 ∈ V →
(varFGrp‘𝐼):𝐼⟶(Base‘𝐺)) |
| 25 | 19, 24 | syl 17 |
. . . . . 6
⊢ (𝐼 ≈ 1o →
(varFGrp‘𝐼):𝐼⟶(Base‘𝐺)) |
| 26 | | en1uniel 9069 |
. . . . . 6
⊢ (𝐼 ≈ 1o →
∪ 𝐼 ∈ 𝐼) |
| 27 | 25, 26 | ffvelcdmd 7105 |
. . . . 5
⊢ (𝐼 ≈ 1o →
((varFGrp‘𝐼)‘∪ 𝐼) ∈ (Base‘𝐺)) |
| 28 | | zringgrp 21463 |
. . . . . . . . 9
⊢
ℤring ∈ Grp |
| 29 | 19 | uniexd 7762 |
. . . . . . . . . . 11
⊢ (𝐼 ≈ 1o →
∪ 𝐼 ∈ V) |
| 30 | | 1zzd 12648 |
. . . . . . . . . . 11
⊢ (𝐼 ≈ 1o → 1
∈ ℤ) |
| 31 | 29, 30 | fsnd 6891 |
. . . . . . . . . 10
⊢ (𝐼 ≈ 1o →
{〈∪ 𝐼, 1〉}:{∪
𝐼}⟶ℤ) |
| 32 | | en1b 9065 |
. . . . . . . . . . . 12
⊢ (𝐼 ≈ 1o ↔
𝐼 = {∪ 𝐼}) |
| 33 | 32 | biimpi 216 |
. . . . . . . . . . 11
⊢ (𝐼 ≈ 1o →
𝐼 = {∪ 𝐼}) |
| 34 | 33 | feq2d 6722 |
. . . . . . . . . 10
⊢ (𝐼 ≈ 1o →
({〈∪ 𝐼, 1〉}:𝐼⟶ℤ ↔ {〈∪ 𝐼,
1〉}:{∪ 𝐼}⟶ℤ)) |
| 35 | 31, 34 | mpbird 257 |
. . . . . . . . 9
⊢ (𝐼 ≈ 1o →
{〈∪ 𝐼, 1〉}:𝐼⟶ℤ) |
| 36 | | zringbas 21464 |
. . . . . . . . . 10
⊢ ℤ =
(Base‘ℤring) |
| 37 | 3, 36, 23 | frgpup3 19796 |
. . . . . . . . 9
⊢
((ℤring ∈ Grp ∧ 𝐼 ∈ V ∧ {〈∪ 𝐼,
1〉}:𝐼⟶ℤ)
→ ∃!𝑓 ∈
(𝐺 GrpHom
ℤring)(𝑓
∘ (varFGrp‘𝐼)) = {〈∪
𝐼,
1〉}) |
| 38 | 28, 19, 35, 37 | mp3an2i 1468 |
. . . . . . . 8
⊢ (𝐼 ≈ 1o →
∃!𝑓 ∈ (𝐺 GrpHom
ℤring)(𝑓
∘ (varFGrp‘𝐼)) = {〈∪
𝐼,
1〉}) |
| 39 | 38 | adantr 480 |
. . . . . . 7
⊢ ((𝐼 ≈ 1o ∧
𝑥 ∈ (Base‘𝐺)) → ∃!𝑓 ∈ (𝐺 GrpHom ℤring)(𝑓 ∘
(varFGrp‘𝐼)) = {〈∪
𝐼,
1〉}) |
| 40 | | reurex 3384 |
. . . . . . 7
⊢
(∃!𝑓 ∈
(𝐺 GrpHom
ℤring)(𝑓
∘ (varFGrp‘𝐼)) = {〈∪
𝐼, 1〉} →
∃𝑓 ∈ (𝐺 GrpHom
ℤring)(𝑓
∘ (varFGrp‘𝐼)) = {〈∪
𝐼,
1〉}) |
| 41 | 39, 40 | syl 17 |
. . . . . 6
⊢ ((𝐼 ≈ 1o ∧
𝑥 ∈ (Base‘𝐺)) → ∃𝑓 ∈ (𝐺 GrpHom ℤring)(𝑓 ∘
(varFGrp‘𝐼)) = {〈∪
𝐼,
1〉}) |
| 42 | | fveq1 6905 |
. . . . . . . . . 10
⊢ ((𝑓 ∘
(varFGrp‘𝐼)) = {〈∪
𝐼, 1〉} → ((𝑓 ∘
(varFGrp‘𝐼))‘∪ 𝐼) = ({〈∪ 𝐼,
1〉}‘∪ 𝐼)) |
| 43 | 25, 26 | fvco3d 7009 |
. . . . . . . . . . 11
⊢ (𝐼 ≈ 1o →
((𝑓 ∘
(varFGrp‘𝐼))‘∪ 𝐼) = (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼))) |
| 44 | | 1z 12647 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℤ |
| 45 | | fvsng 7200 |
. . . . . . . . . . . 12
⊢ ((∪ 𝐼
∈ V ∧ 1 ∈ ℤ) → ({〈∪
𝐼, 1〉}‘∪ 𝐼) =
1) |
| 46 | 29, 44, 45 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝐼 ≈ 1o →
({〈∪ 𝐼, 1〉}‘∪ 𝐼) =
1) |
| 47 | 43, 46 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (𝐼 ≈ 1o →
(((𝑓 ∘
(varFGrp‘𝐼))‘∪ 𝐼) = ({〈∪ 𝐼,
1〉}‘∪ 𝐼) ↔ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) |
| 48 | 42, 47 | imbitrid 244 |
. . . . . . . . 9
⊢ (𝐼 ≈ 1o →
((𝑓 ∘
(varFGrp‘𝐼)) = {〈∪
𝐼, 1〉} → (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) |
| 49 | 48 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝐼 ≈ 1o ∧
𝑥 ∈ (Base‘𝐺)) ∧ 𝑓 ∈ (𝐺 GrpHom ℤring)) →
((𝑓 ∘
(varFGrp‘𝐼)) = {〈∪
𝐼, 1〉} → (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) |
| 50 | 16, 36 | ghmf 19238 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ (𝐺 GrpHom ℤring) → 𝑓:(Base‘𝐺)⟶ℤ) |
| 51 | 50 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → 𝑓:(Base‘𝐺)⟶ℤ) |
| 52 | 51 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ (((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) ∧ 𝑥 ∈
(Base‘𝐺)) →
(𝑓‘𝑥) ∈ ℤ) |
| 53 | 52 | an32s 652 |
. . . . . . . . . 10
⊢ (((𝐼 ≈ 1o ∧
𝑥 ∈ (Base‘𝐺)) ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑓‘𝑥) ∈
ℤ) |
| 54 | | mptresid 6069 |
. . . . . . . . . . . . . 14
⊢ ( I
↾ (Base‘𝐺)) =
(𝑥 ∈ (Base‘𝐺) ↦ 𝑥) |
| 55 | 3, 16, 23 | frgpup3 19796 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ Grp ∧ 𝐼 ∈ V ∧
(varFGrp‘𝐼):𝐼⟶(Base‘𝐺)) → ∃!𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼)) |
| 56 | 21, 19, 25, 55 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐼 ≈ 1o →
∃!𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼)) |
| 57 | | reurmo 3383 |
. . . . . . . . . . . . . . . . 17
⊢
(∃!𝑔 ∈
(𝐺 GrpHom 𝐺)(𝑔 ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼) → ∃*𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼)) |
| 58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐼 ≈ 1o →
∃*𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼)) |
| 59 | 58 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ∃*𝑔 ∈
(𝐺 GrpHom 𝐺)(𝑔 ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼)) |
| 60 | 21 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → 𝐺 ∈
Grp) |
| 61 | 16 | idghm 19249 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ Grp → ( I ↾
(Base‘𝐺)) ∈
(𝐺 GrpHom 𝐺)) |
| 62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ( I ↾ (Base‘𝐺)) ∈ (𝐺 GrpHom 𝐺)) |
| 63 | 25 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (varFGrp‘𝐼):𝐼⟶(Base‘𝐺)) |
| 64 | | fcoi2 6783 |
. . . . . . . . . . . . . . . 16
⊢
((varFGrp‘𝐼):𝐼⟶(Base‘𝐺) → (( I ↾ (Base‘𝐺)) ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼)) |
| 65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (( I ↾ (Base‘𝐺)) ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼)) |
| 66 | 51 | feqmptd 6977 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → 𝑓 = (𝑥 ∈ (Base‘𝐺) ↦ (𝑓‘𝑥))) |
| 67 | | eqidd 2738 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑛 ∈ ℤ
↦ (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
= (𝑛 ∈ ℤ ↦
(𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))) |
| 68 | | oveq1 7438 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (𝑓‘𝑥) → (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))
= ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
| 69 | 52, 66, 67, 68 | fmptco 7149 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ((𝑛 ∈
ℤ ↦ (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
∘ 𝑓) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))) |
| 70 | 27 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ((varFGrp‘𝐼)‘∪ 𝐼) ∈ (Base‘𝐺)) |
| 71 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
= (𝑛 ∈ ℤ ↦
(𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
| 72 | 17, 71, 16 | mulgghm2 21487 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ Grp ∧
((varFGrp‘𝐼)‘∪ 𝐼) ∈ (Base‘𝐺)) → (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
∈ (ℤring GrpHom 𝐺)) |
| 73 | 60, 70, 72 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑛 ∈ ℤ
↦ (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
∈ (ℤring GrpHom 𝐺)) |
| 74 | | simprl 771 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → 𝑓 ∈ (𝐺 GrpHom
ℤring)) |
| 75 | | ghmco 19254 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
∈ (ℤring GrpHom 𝐺) ∧ 𝑓 ∈ (𝐺 GrpHom ℤring)) →
((𝑛 ∈ ℤ ↦
(𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
∘ 𝑓) ∈ (𝐺 GrpHom 𝐺)) |
| 76 | 73, 74, 75 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ((𝑛 ∈
ℤ ↦ (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
∘ 𝑓) ∈ (𝐺 GrpHom 𝐺)) |
| 77 | 69, 76 | eqeltrrd 2842 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑥 ∈
(Base‘𝐺) ↦
((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
∈ (𝐺 GrpHom 𝐺)) |
| 78 | 33 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → 𝐼 = {∪ 𝐼}) |
| 79 | 78 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑦 ∈ 𝐼 ↔ 𝑦 ∈ {∪ 𝐼})) |
| 80 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1) |
| 81 | 80 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ((𝑓‘((varFGrp‘𝐼)‘∪ 𝐼))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)) =
(1(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
| 82 | 16, 17 | mulg1 19099 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((varFGrp‘𝐼)‘∪ 𝐼) ∈ (Base‘𝐺) →
(1(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))
= ((varFGrp‘𝐼)‘∪ 𝐼)) |
| 83 | 70, 82 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (1(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)) =
((varFGrp‘𝐼)‘∪ 𝐼)) |
| 84 | 81, 83 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ((𝑓‘((varFGrp‘𝐼)‘∪ 𝐼))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)) =
((varFGrp‘𝐼)‘∪ 𝐼)) |
| 85 | | elsni 4643 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ {∪ 𝐼}
→ 𝑦 = ∪ 𝐼) |
| 86 | 85 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ {∪ 𝐼}
→ ((varFGrp‘𝐼)‘𝑦) = ((varFGrp‘𝐼)‘∪ 𝐼)) |
| 87 | 86 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ {∪ 𝐼}
→ (𝑓‘((varFGrp‘𝐼)‘𝑦)) = (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼))) |
| 88 | 87 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ {∪ 𝐼}
→ ((𝑓‘((varFGrp‘𝐼)‘𝑦))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)) =
((𝑓‘((varFGrp‘𝐼)‘∪ 𝐼))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
| 89 | 88, 86 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ {∪ 𝐼}
→ (((𝑓‘((varFGrp‘𝐼)‘𝑦))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)) =
((varFGrp‘𝐼)‘𝑦) ↔ ((𝑓‘((varFGrp‘𝐼)‘∪ 𝐼))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)) =
((varFGrp‘𝐼)‘∪ 𝐼))) |
| 90 | 84, 89 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑦 ∈ {∪ 𝐼}
→ ((𝑓‘((varFGrp‘𝐼)‘𝑦))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)) =
((varFGrp‘𝐼)‘𝑦))) |
| 91 | 79, 90 | sylbid 240 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑦 ∈ 𝐼 → ((𝑓‘((varFGrp‘𝐼)‘𝑦))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)) =
((varFGrp‘𝐼)‘𝑦))) |
| 92 | 91 | imp 406 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) ∧ 𝑦 ∈ 𝐼) → ((𝑓‘((varFGrp‘𝐼)‘𝑦))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)) =
((varFGrp‘𝐼)‘𝑦)) |
| 93 | 92 | mpteq2dva 5242 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑦 ∈ 𝐼 ↦ ((𝑓‘((varFGrp‘𝐼)‘𝑦))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
= (𝑦 ∈ 𝐼 ↦
((varFGrp‘𝐼)‘𝑦))) |
| 94 | 63 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) ∧ 𝑦 ∈ 𝐼) →
((varFGrp‘𝐼)‘𝑦) ∈ (Base‘𝐺)) |
| 95 | 63 | feqmptd 6977 |
. . . . . . . . . . . . . . . . 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 6906 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 =
((varFGrp‘𝐼)‘𝑦) → (𝑓‘𝑥) = (𝑓‘((varFGrp‘𝐼)‘𝑦))) |
| 98 | 97 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 =
((varFGrp‘𝐼)‘𝑦) → ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))
= ((𝑓‘((varFGrp‘𝐼)‘𝑦))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
| 99 | 94, 95, 96, 98 | fmptco 7149 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ((𝑥 ∈
(Base‘𝐺) ↦
((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
∘ (varFGrp‘𝐼)) = (𝑦 ∈ 𝐼 ↦ ((𝑓‘((varFGrp‘𝐼)‘𝑦))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))) |
| 100 | 93, 99, 95 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ((𝑥 ∈
(Base‘𝐺) ↦
((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
∘ (varFGrp‘𝐼)) = (varFGrp‘𝐼)) |
| 101 | | coeq1 5868 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = ( I ↾ (Base‘𝐺)) → (𝑔 ∘
(varFGrp‘𝐼)) = (( I ↾ (Base‘𝐺)) ∘
(varFGrp‘𝐼))) |
| 102 | 101 | eqeq1d 2739 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = ( I ↾ (Base‘𝐺)) → ((𝑔 ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼) ↔ (( I ↾
(Base‘𝐺)) ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼))) |
| 103 | | coeq1 5868 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
→ (𝑔 ∘
(varFGrp‘𝐼)) = ((𝑥 ∈ (Base‘𝐺) ↦ ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
∘ (varFGrp‘𝐼))) |
| 104 | 103 | eqeq1d 2739 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
→ ((𝑔 ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
∘ (varFGrp‘𝐼)) = (varFGrp‘𝐼))) |
| 105 | 102, 104 | rmoi 3891 |
. . . . . . . . . . . . . . 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‘𝐼)‘∪ 𝐼)))) |
| 106 | 59, 62, 65, 77, 100, 105 | syl122anc 1381 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ( I ↾ (Base‘𝐺)) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))) |
| 107 | 54, 106 | eqtr3id 2791 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑥 ∈
(Base‘𝐺) ↦ 𝑥) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))) |
| 108 | | mpteqb 7035 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
(Base‘𝐺)𝑥 ∈ (Base‘𝐺) → ((𝑥 ∈ (Base‘𝐺) ↦ 𝑥) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
↔ ∀𝑥 ∈
(Base‘𝐺)𝑥 = ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))) |
| 109 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (Base‘𝐺) → 𝑥 ∈ (Base‘𝐺)) |
| 110 | 108, 109 | mprg 3067 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (Base‘𝐺) ↦ 𝑥) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
↔ ∀𝑥 ∈
(Base‘𝐺)𝑥 = ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
| 111 | 107, 110 | sylib 218 |
. . . . . . . . . . . 12
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ∀𝑥 ∈
(Base‘𝐺)𝑥 = ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
| 112 | 111 | r19.21bi 3251 |
. . . . . . . . . . 11
⊢ (((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) ∧ 𝑥 ∈
(Base‘𝐺)) → 𝑥 = ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
| 113 | 112 | an32s 652 |
. . . . . . . . . 10
⊢ (((𝐼 ≈ 1o ∧
𝑥 ∈ (Base‘𝐺)) ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → 𝑥 = ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
| 114 | 68 | rspceeqv 3645 |
. . . . . . . . . 10
⊢ (((𝑓‘𝑥) ∈ ℤ ∧ 𝑥 = ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
→ ∃𝑛 ∈
ℤ 𝑥 = (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
| 115 | 53, 113, 114 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐼 ≈ 1o ∧
𝑥 ∈ (Base‘𝐺)) ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ∃𝑛 ∈
ℤ 𝑥 = (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
| 116 | 115 | expr 456 |
. . . . . . . 8
⊢ (((𝐼 ≈ 1o ∧
𝑥 ∈ (Base‘𝐺)) ∧ 𝑓 ∈ (𝐺 GrpHom ℤring)) →
((𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1 → ∃𝑛 ∈
ℤ 𝑥 = (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))) |
| 117 | 49, 116 | syld 47 |
. . . . . . 7
⊢ (((𝐼 ≈ 1o ∧
𝑥 ∈ (Base‘𝐺)) ∧ 𝑓 ∈ (𝐺 GrpHom ℤring)) →
((𝑓 ∘
(varFGrp‘𝐼)) = {〈∪
𝐼, 1〉} →
∃𝑛 ∈ ℤ
𝑥 = (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))) |
| 118 | 117 | rexlimdva 3155 |
. . . . . 6
⊢ ((𝐼 ≈ 1o ∧
𝑥 ∈ (Base‘𝐺)) → (∃𝑓 ∈ (𝐺 GrpHom ℤring)(𝑓 ∘
(varFGrp‘𝐼)) = {〈∪
𝐼, 1〉} →
∃𝑛 ∈ ℤ
𝑥 = (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))) |
| 119 | 41, 118 | mpd 15 |
. . . . 5
⊢ ((𝐼 ≈ 1o ∧
𝑥 ∈ (Base‘𝐺)) → ∃𝑛 ∈ ℤ 𝑥 = (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
| 120 | 16, 17, 21, 27, 119 | iscygd 19905 |
. . . 4
⊢ (𝐼 ≈ 1o →
𝐺 ∈
CycGrp) |
| 121 | 15, 120 | jaoi 858 |
. . 3
⊢ ((𝐼 ≺ 1o ∨
𝐼 ≈ 1o)
→ 𝐺 ∈
CycGrp) |
| 122 | 1, 121 | sylbi 217 |
. 2
⊢ (𝐼 ≼ 1o →
𝐺 ∈
CycGrp) |
| 123 | | cygabl 19909 |
. . 3
⊢ (𝐺 ∈ CycGrp → 𝐺 ∈ Abel) |
| 124 | 3 | frgpnabl 19893 |
. . . . 5
⊢
(1o ≺ 𝐼 → ¬ 𝐺 ∈ Abel) |
| 125 | 124 | con2i 139 |
. . . 4
⊢ (𝐺 ∈ Abel → ¬
1o ≺ 𝐼) |
| 126 | | ablgrp 19803 |
. . . . . 6
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
| 127 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 128 | 16, 127 | grpidcl 18983 |
. . . . . 6
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ (Base‘𝐺)) |
| 129 | 3, 16 | elbasfv 17253 |
. . . . . 6
⊢
((0g‘𝐺) ∈ (Base‘𝐺) → 𝐼 ∈ V) |
| 130 | 126, 128,
129 | 3syl 18 |
. . . . 5
⊢ (𝐺 ∈ Abel → 𝐼 ∈ V) |
| 131 | | 1onn 8678 |
. . . . . 6
⊢
1o ∈ ω |
| 132 | | nnfi 9207 |
. . . . . 6
⊢
(1o ∈ ω → 1o ∈
Fin) |
| 133 | 131, 132 | ax-mp 5 |
. . . . 5
⊢
1o ∈ Fin |
| 134 | | fidomtri2 10034 |
. . . . 5
⊢ ((𝐼 ∈ V ∧ 1o
∈ Fin) → (𝐼
≼ 1o ↔ ¬ 1o ≺ 𝐼)) |
| 135 | 130, 133,
134 | sylancl 586 |
. . . 4
⊢ (𝐺 ∈ Abel → (𝐼 ≼ 1o ↔
¬ 1o ≺ 𝐼)) |
| 136 | 125, 135 | mpbird 257 |
. . 3
⊢ (𝐺 ∈ Abel → 𝐼 ≼
1o) |
| 137 | 123, 136 | syl 17 |
. 2
⊢ (𝐺 ∈ CycGrp → 𝐼 ≼
1o) |
| 138 | 122, 137 | impbii 209 |
1
⊢ (𝐼 ≼ 1o ↔
𝐺 ∈
CycGrp) |