Step | Hyp | Ref
| Expression |
1 | | brdom2 8663 |
. . 3
⊢ (𝐼 ≼ 1o ↔
(𝐼 ≺ 1o
∨ 𝐼 ≈
1o)) |
2 | | sdom1 8883 |
. . . . 5
⊢ (𝐼 ≺ 1o ↔
𝐼 =
∅) |
3 | | frgpcyg.g |
. . . . . . 7
⊢ 𝐺 = (freeGrp‘𝐼) |
4 | | fveq2 6722 |
. . . . . . 7
⊢ (𝐼 = ∅ →
(freeGrp‘𝐼) =
(freeGrp‘∅)) |
5 | 3, 4 | syl5eq 2790 |
. . . . . 6
⊢ (𝐼 = ∅ → 𝐺 =
(freeGrp‘∅)) |
6 | | 0ex 5205 |
. . . . . . . 8
⊢ ∅
∈ V |
7 | | eqid 2737 |
. . . . . . . . 9
⊢
(freeGrp‘∅) = (freeGrp‘∅) |
8 | 7 | frgpgrp 19157 |
. . . . . . . 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 19174 |
. . . . . . 7
⊢
(Base‘(freeGrp‘∅)) ≈
1o |
12 | 10 | 0cyg 19283 |
. . . . . . 7
⊢
(((freeGrp‘∅) ∈ Grp ∧
(Base‘(freeGrp‘∅)) ≈ 1o) →
(freeGrp‘∅) ∈ CycGrp) |
13 | 9, 11, 12 | mp2an 692 |
. . . . . 6
⊢
(freeGrp‘∅) ∈ CycGrp |
14 | 5, 13 | eqeltrdi 2846 |
. . . . 5
⊢ (𝐼 = ∅ → 𝐺 ∈ CycGrp) |
15 | 2, 14 | sylbi 220 |
. . . 4
⊢ (𝐼 ≺ 1o →
𝐺 ∈
CycGrp) |
16 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝐺) =
(Base‘𝐺) |
17 | | eqid 2737 |
. . . . 5
⊢
(.g‘𝐺) = (.g‘𝐺) |
18 | | relen 8636 |
. . . . . . 7
⊢ Rel
≈ |
19 | 18 | brrelex1i 5610 |
. . . . . 6
⊢ (𝐼 ≈ 1o →
𝐼 ∈
V) |
20 | 3 | frgpgrp 19157 |
. . . . . 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 19163 |
. . . . . . 7
⊢ (𝐼 ∈ V →
(varFGrp‘𝐼):𝐼⟶(Base‘𝐺)) |
25 | 19, 24 | syl 17 |
. . . . . 6
⊢ (𝐼 ≈ 1o →
(varFGrp‘𝐼):𝐼⟶(Base‘𝐺)) |
26 | | en1uniel 8710 |
. . . . . 6
⊢ (𝐼 ≈ 1o →
∪ 𝐼 ∈ 𝐼) |
27 | 25, 26 | ffvelrnd 6910 |
. . . . 5
⊢ (𝐼 ≈ 1o →
((varFGrp‘𝐼)‘∪ 𝐼) ∈ (Base‘𝐺)) |
28 | | zringgrp 20445 |
. . . . . . . . 9
⊢
ℤring ∈ Grp |
29 | 19 | uniexd 7535 |
. . . . . . . . . . 11
⊢ (𝐼 ≈ 1o →
∪ 𝐼 ∈ V) |
30 | | 1zzd 12213 |
. . . . . . . . . . 11
⊢ (𝐼 ≈ 1o → 1
∈ ℤ) |
31 | 29, 30 | fsnd 6708 |
. . . . . . . . . 10
⊢ (𝐼 ≈ 1o →
{〈∪ 𝐼, 1〉}:{∪
𝐼}⟶ℤ) |
32 | | en1b 8705 |
. . . . . . . . . . . 12
⊢ (𝐼 ≈ 1o ↔
𝐼 = {∪ 𝐼}) |
33 | 32 | biimpi 219 |
. . . . . . . . . . 11
⊢ (𝐼 ≈ 1o →
𝐼 = {∪ 𝐼}) |
34 | 33 | feq2d 6536 |
. . . . . . . . . 10
⊢ (𝐼 ≈ 1o →
({〈∪ 𝐼, 1〉}:𝐼⟶ℤ ↔ {〈∪ 𝐼,
1〉}:{∪ 𝐼}⟶ℤ)) |
35 | 31, 34 | mpbird 260 |
. . . . . . . . 9
⊢ (𝐼 ≈ 1o →
{〈∪ 𝐼, 1〉}:𝐼⟶ℤ) |
36 | | zringbas 20446 |
. . . . . . . . . 10
⊢ ℤ =
(Base‘ℤring) |
37 | 3, 36, 23 | frgpup3 19173 |
. . . . . . . . 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 484 |
. . . . . . 7
⊢ ((𝐼 ≈ 1o ∧
𝑥 ∈ (Base‘𝐺)) → ∃!𝑓 ∈ (𝐺 GrpHom ℤring)(𝑓 ∘
(varFGrp‘𝐼)) = {〈∪
𝐼,
1〉}) |
40 | | reurex 3343 |
. . . . . . 7
⊢
(∃!𝑓 ∈
(𝐺 GrpHom
ℤring)(𝑓
∘ (varFGrp‘𝐼)) = {〈∪
𝐼, 1〉} →
∃𝑓 ∈ (𝐺 GrpHom
ℤring)(𝑓
∘ (varFGrp‘𝐼)) = {〈∪
𝐼,
1〉}) |
41 | 39, 40 | syl 17 |
. . . . . 6
⊢ ((𝐼 ≈ 1o ∧
𝑥 ∈ (Base‘𝐺)) → ∃𝑓 ∈ (𝐺 GrpHom ℤring)(𝑓 ∘
(varFGrp‘𝐼)) = {〈∪
𝐼,
1〉}) |
42 | | fveq1 6721 |
. . . . . . . . . 10
⊢ ((𝑓 ∘
(varFGrp‘𝐼)) = {〈∪
𝐼, 1〉} → ((𝑓 ∘
(varFGrp‘𝐼))‘∪ 𝐼) = ({〈∪ 𝐼,
1〉}‘∪ 𝐼)) |
43 | 25, 26 | fvco3d 6816 |
. . . . . . . . . . 11
⊢ (𝐼 ≈ 1o →
((𝑓 ∘
(varFGrp‘𝐼))‘∪ 𝐼) = (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼))) |
44 | | 1z 12212 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℤ |
45 | | fvsng 7000 |
. . . . . . . . . . . 12
⊢ ((∪ 𝐼
∈ V ∧ 1 ∈ ℤ) → ({〈∪
𝐼, 1〉}‘∪ 𝐼) =
1) |
46 | 29, 44, 45 | sylancl 589 |
. . . . . . . . . . 11
⊢ (𝐼 ≈ 1o →
({〈∪ 𝐼, 1〉}‘∪ 𝐼) =
1) |
47 | 43, 46 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (𝐼 ≈ 1o →
(((𝑓 ∘
(varFGrp‘𝐼))‘∪ 𝐼) = ({〈∪ 𝐼,
1〉}‘∪ 𝐼) ↔ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) |
48 | 42, 47 | syl5ib 247 |
. . . . . . . . 9
⊢ (𝐼 ≈ 1o →
((𝑓 ∘
(varFGrp‘𝐼)) = {〈∪
𝐼, 1〉} → (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) |
49 | 48 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝐼 ≈ 1o ∧
𝑥 ∈ (Base‘𝐺)) ∧ 𝑓 ∈ (𝐺 GrpHom ℤring)) →
((𝑓 ∘
(varFGrp‘𝐼)) = {〈∪
𝐼, 1〉} → (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) |
50 | 16, 36 | ghmf 18631 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ (𝐺 GrpHom ℤring) → 𝑓:(Base‘𝐺)⟶ℤ) |
51 | 50 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → 𝑓:(Base‘𝐺)⟶ℤ) |
52 | 51 | ffvelrnda 6909 |
. . . . . . . . . . 11
⊢ (((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) ∧ 𝑥 ∈
(Base‘𝐺)) →
(𝑓‘𝑥) ∈ ℤ) |
53 | 52 | an32s 652 |
. . . . . . . . . 10
⊢ (((𝐼 ≈ 1o ∧
𝑥 ∈ (Base‘𝐺)) ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑓‘𝑥) ∈
ℤ) |
54 | | mptresid 5923 |
. . . . . . . . . . . . . 14
⊢ ( I
↾ (Base‘𝐺)) =
(𝑥 ∈ (Base‘𝐺) ↦ 𝑥) |
55 | 3, 16, 23 | frgpup3 19173 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ Grp ∧ 𝐼 ∈ V ∧
(varFGrp‘𝐼):𝐼⟶(Base‘𝐺)) → ∃!𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼)) |
56 | 21, 19, 25, 55 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐼 ≈ 1o →
∃!𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼)) |
57 | | reurmo 3345 |
. . . . . . . . . . . . . . . . 17
⊢
(∃!𝑔 ∈
(𝐺 GrpHom 𝐺)(𝑔 ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼) → ∃*𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼)) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐼 ≈ 1o →
∃*𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼)) |
59 | 58 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ∃*𝑔 ∈
(𝐺 GrpHom 𝐺)(𝑔 ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼)) |
60 | 21 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → 𝐺 ∈
Grp) |
61 | 16 | idghm 18642 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ Grp → ( I ↾
(Base‘𝐺)) ∈
(𝐺 GrpHom 𝐺)) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ( I ↾ (Base‘𝐺)) ∈ (𝐺 GrpHom 𝐺)) |
63 | 25 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (varFGrp‘𝐼):𝐼⟶(Base‘𝐺)) |
64 | | fcoi2 6599 |
. . . . . . . . . . . . . . . 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 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‘𝐼)‘∪ 𝐼))) |
69 | 52, 66, 67, 68 | fmptco 6949 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ((𝑛 ∈
ℤ ↦ (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
∘ 𝑓) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))) |
70 | 27 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ((varFGrp‘𝐼)‘∪ 𝐼) ∈ (Base‘𝐺)) |
71 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
= (𝑛 ∈ ℤ ↦
(𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
72 | 17, 71, 16 | mulgghm2 20468 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ Grp ∧
((varFGrp‘𝐼)‘∪ 𝐼) ∈ (Base‘𝐺)) → (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
∈ (ℤring GrpHom 𝐺)) |
73 | 60, 70, 72 | syl2anc 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 𝐺)) |
76 | 73, 74, 75 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ((𝑛 ∈
ℤ ↦ (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
∘ 𝑓) ∈ (𝐺 GrpHom 𝐺)) |
77 | 69, 76 | eqeltrrd 2839 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑥 ∈
(Base‘𝐺) ↦
((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
∈ (𝐺 GrpHom 𝐺)) |
78 | 33 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → 𝐼 = {∪ 𝐼}) |
79 | 78 | eleq2d 2823 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑦 ∈ 𝐼 ↔ 𝑦 ∈ {∪ 𝐼})) |
80 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1) |
81 | 80 | oveq1d 7233 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ((𝑓‘((varFGrp‘𝐼)‘∪ 𝐼))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)) =
(1(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
82 | 16, 17 | mulg1 18504 |
. . . . . . . . . . . . . . . . . . . . . 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 4563 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ {∪ 𝐼}
→ 𝑦 = ∪ 𝐼) |
86 | 85 | fveq2d 6726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ {∪ 𝐼}
→ ((varFGrp‘𝐼)‘𝑦) = ((varFGrp‘𝐼)‘∪ 𝐼)) |
87 | 86 | fveq2d 6726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ {∪ 𝐼}
→ (𝑓‘((varFGrp‘𝐼)‘𝑦)) = (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼))) |
88 | 87 | oveq1d 7233 |
. . . . . . . . . . . . . . . . . . . . 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 250 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑦 ∈ {∪ 𝐼}
→ ((𝑓‘((varFGrp‘𝐼)‘𝑦))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)) =
((varFGrp‘𝐼)‘𝑦))) |
91 | 79, 90 | sylbid 243 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑦 ∈ 𝐼 → ((𝑓‘((varFGrp‘𝐼)‘𝑦))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)) =
((varFGrp‘𝐼)‘𝑦))) |
92 | 91 | imp 410 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) ∧ 𝑦 ∈ 𝐼) → ((𝑓‘((varFGrp‘𝐼)‘𝑦))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)) =
((varFGrp‘𝐼)‘𝑦)) |
93 | 92 | mpteq2dva 5155 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑦 ∈ 𝐼 ↦ ((𝑓‘((varFGrp‘𝐼)‘𝑦))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
= (𝑦 ∈ 𝐼 ↦
((varFGrp‘𝐼)‘𝑦))) |
94 | 63 | ffvelrnda 6909 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) ∧ 𝑦 ∈ 𝐼) →
((varFGrp‘𝐼)‘𝑦) ∈ (Base‘𝐺)) |
95 | 63 | feqmptd 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‘𝐼)‘𝑦))) |
98 | 97 | oveq1d 7233 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 =
((varFGrp‘𝐼)‘𝑦) → ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))
= ((𝑓‘((varFGrp‘𝐼)‘𝑦))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
99 | 94, 95, 96, 98 | fmptco 6949 |
. . . . . . . . . . . . . . . 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 5731 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = ( I ↾ (Base‘𝐺)) → (𝑔 ∘
(varFGrp‘𝐼)) = (( I ↾ (Base‘𝐺)) ∘
(varFGrp‘𝐼))) |
102 | 101 | eqeq1d 2739 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = ( I ↾ (Base‘𝐺)) → ((𝑔 ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼) ↔ (( I ↾
(Base‘𝐺)) ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼))) |
103 | | coeq1 5731 |
. . . . . . . . . . . . . . . . 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 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‘𝐼)‘∪ 𝐼)))) |
106 | 59, 62, 65, 77, 100, 105 | syl122anc 1381 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ( I ↾ (Base‘𝐺)) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))) |
107 | 54, 106 | eqtr3id 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‘𝐺)) |
110 | 108, 109 | mprg 3075 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (Base‘𝐺) ↦ 𝑥) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
↔ ∀𝑥 ∈
(Base‘𝐺)𝑥 = ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
111 | 107, 110 | sylib 221 |
. . . . . . . . . . . 12
⊢ ((𝐼 ≈ 1o ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ∀𝑥 ∈
(Base‘𝐺)𝑥 = ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
112 | 111 | r19.21bi 3130 |
. . . . . . . . . . 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 3557 |
. . . . . . . . . 10
⊢ (((𝑓‘𝑥) ∈ ℤ ∧ 𝑥 = ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
→ ∃𝑛 ∈
ℤ 𝑥 = (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
115 | 53, 113, 114 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝐼 ≈ 1o ∧
𝑥 ∈ (Base‘𝐺)) ∧ (𝑓 ∈ (𝐺 GrpHom ℤring) ∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ∃𝑛 ∈
ℤ 𝑥 = (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
116 | 115 | expr 460 |
. . . . . . . 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 3208 |
. . . . . 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 19276 |
. . . 4
⊢ (𝐼 ≈ 1o →
𝐺 ∈
CycGrp) |
121 | 15, 120 | jaoi 857 |
. . 3
⊢ ((𝐼 ≺ 1o ∨
𝐼 ≈ 1o)
→ 𝐺 ∈
CycGrp) |
122 | 1, 121 | sylbi 220 |
. 2
⊢ (𝐼 ≼ 1o →
𝐺 ∈
CycGrp) |
123 | | cygabl 19280 |
. . 3
⊢ (𝐺 ∈ CycGrp → 𝐺 ∈ Abel) |
124 | 3 | frgpnabl 19265 |
. . . . 5
⊢
(1o ≺ 𝐼 → ¬ 𝐺 ∈ Abel) |
125 | 124 | con2i 141 |
. . . 4
⊢ (𝐺 ∈ Abel → ¬
1o ≺ 𝐼) |
126 | | ablgrp 19180 |
. . . . . 6
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
127 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) |
128 | 16, 127 | grpidcl 18400 |
. . . . . 6
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ (Base‘𝐺)) |
129 | 3, 16 | elbasfv 16771 |
. . . . . 6
⊢
((0g‘𝐺) ∈ (Base‘𝐺) → 𝐼 ∈ V) |
130 | 126, 128,
129 | 3syl 18 |
. . . . 5
⊢ (𝐺 ∈ Abel → 𝐼 ∈ V) |
131 | | 1onn 8372 |
. . . . . 6
⊢
1o ∈ ω |
132 | | nnfi 8850 |
. . . . . 6
⊢
(1o ∈ ω → 1o ∈
Fin) |
133 | 131, 132 | ax-mp 5 |
. . . . 5
⊢
1o ∈ Fin |
134 | | fidomtri2 9615 |
. . . . 5
⊢ ((𝐼 ∈ V ∧ 1o
∈ Fin) → (𝐼
≼ 1o ↔ ¬ 1o ≺ 𝐼)) |
135 | 130, 133,
134 | sylancl 589 |
. . . 4
⊢ (𝐺 ∈ Abel → (𝐼 ≼ 1o ↔
¬ 1o ≺ 𝐼)) |
136 | 125, 135 | mpbird 260 |
. . 3
⊢ (𝐺 ∈ Abel → 𝐼 ≼
1o) |
137 | 123, 136 | syl 17 |
. 2
⊢ (𝐺 ∈ CycGrp → 𝐼 ≼
1o) |
138 | 122, 137 | impbii 212 |
1
⊢ (𝐼 ≼ 1o ↔
𝐺 ∈
CycGrp) |