Step | Hyp | Ref
| Expression |
1 | | brdom2 7985 |
. . 3
⊢ (𝐼 ≼ 1𝑜
↔ (𝐼 ≺
1𝑜 ∨ 𝐼 ≈
1𝑜)) |
2 | | sdom1 8160 |
. . . . 5
⊢ (𝐼 ≺ 1𝑜
↔ 𝐼 =
∅) |
3 | | frgpcyg.g |
. . . . . . 7
⊢ 𝐺 = (freeGrp‘𝐼) |
4 | | fveq2 6191 |
. . . . . . 7
⊢ (𝐼 = ∅ →
(freeGrp‘𝐼) =
(freeGrp‘∅)) |
5 | 3, 4 | syl5eq 2668 |
. . . . . 6
⊢ (𝐼 = ∅ → 𝐺 =
(freeGrp‘∅)) |
6 | | 0ex 4790 |
. . . . . . . 8
⊢ ∅
∈ V |
7 | | eqid 2622 |
. . . . . . . . 9
⊢
(freeGrp‘∅) = (freeGrp‘∅) |
8 | 7 | frgpgrp 18175 |
. . . . . . . 8
⊢ (∅
∈ V → (freeGrp‘∅) ∈ Grp) |
9 | 6, 8 | ax-mp 5 |
. . . . . . 7
⊢
(freeGrp‘∅) ∈ Grp |
10 | | eqid 2622 |
. . . . . . . 8
⊢
(Base‘(freeGrp‘∅)) =
(Base‘(freeGrp‘∅)) |
11 | 7, 10 | 0frgp 18192 |
. . . . . . 7
⊢
(Base‘(freeGrp‘∅)) ≈
1𝑜 |
12 | 10 | 0cyg 18294 |
. . . . . . 7
⊢
(((freeGrp‘∅) ∈ Grp ∧
(Base‘(freeGrp‘∅)) ≈ 1𝑜) →
(freeGrp‘∅) ∈ CycGrp) |
13 | 9, 11, 12 | mp2an 708 |
. . . . . 6
⊢
(freeGrp‘∅) ∈ CycGrp |
14 | 5, 13 | syl6eqel 2709 |
. . . . 5
⊢ (𝐼 = ∅ → 𝐺 ∈ CycGrp) |
15 | 2, 14 | sylbi 207 |
. . . 4
⊢ (𝐼 ≺ 1𝑜
→ 𝐺 ∈
CycGrp) |
16 | | eqid 2622 |
. . . . 5
⊢
(Base‘𝐺) =
(Base‘𝐺) |
17 | | eqid 2622 |
. . . . 5
⊢
(.g‘𝐺) = (.g‘𝐺) |
18 | | relen 7960 |
. . . . . . 7
⊢ Rel
≈ |
19 | 18 | brrelexi 5158 |
. . . . . 6
⊢ (𝐼 ≈ 1𝑜
→ 𝐼 ∈
V) |
20 | 3 | frgpgrp 18175 |
. . . . . 6
⊢ (𝐼 ∈ V → 𝐺 ∈ Grp) |
21 | 19, 20 | syl 17 |
. . . . 5
⊢ (𝐼 ≈ 1𝑜
→ 𝐺 ∈
Grp) |
22 | | eqid 2622 |
. . . . . . . 8
⊢ (
~FG ‘𝐼) = ( ~FG ‘𝐼) |
23 | | eqid 2622 |
. . . . . . . 8
⊢
(varFGrp‘𝐼) = (varFGrp‘𝐼) |
24 | 22, 23, 3, 16 | vrgpf 18181 |
. . . . . . 7
⊢ (𝐼 ∈ V →
(varFGrp‘𝐼):𝐼⟶(Base‘𝐺)) |
25 | 19, 24 | syl 17 |
. . . . . 6
⊢ (𝐼 ≈ 1𝑜
→ (varFGrp‘𝐼):𝐼⟶(Base‘𝐺)) |
26 | | en1uniel 8028 |
. . . . . 6
⊢ (𝐼 ≈ 1𝑜
→ ∪ 𝐼 ∈ 𝐼) |
27 | 25, 26 | ffvelrnd 6360 |
. . . . 5
⊢ (𝐼 ≈ 1𝑜
→ ((varFGrp‘𝐼)‘∪ 𝐼) ∈ (Base‘𝐺)) |
28 | | zringgrp 19823 |
. . . . . . . . 9
⊢
ℤring ∈ Grp |
29 | | uniexg 6955 |
. . . . . . . . . . . 12
⊢ (𝐼 ∈ V → ∪ 𝐼
∈ V) |
30 | 19, 29 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐼 ≈ 1𝑜
→ ∪ 𝐼 ∈ V) |
31 | | 1zzd 11408 |
. . . . . . . . . . 11
⊢ (𝐼 ≈ 1𝑜
→ 1 ∈ ℤ) |
32 | 30, 31 | fsnd 6179 |
. . . . . . . . . 10
⊢ (𝐼 ≈ 1𝑜
→ {〈∪ 𝐼, 1〉}:{∪
𝐼}⟶ℤ) |
33 | | en1b 8024 |
. . . . . . . . . . . 12
⊢ (𝐼 ≈ 1𝑜
↔ 𝐼 = {∪ 𝐼}) |
34 | 33 | biimpi 206 |
. . . . . . . . . . 11
⊢ (𝐼 ≈ 1𝑜
→ 𝐼 = {∪ 𝐼}) |
35 | 34 | feq2d 6031 |
. . . . . . . . . 10
⊢ (𝐼 ≈ 1𝑜
→ ({〈∪ 𝐼, 1〉}:𝐼⟶ℤ ↔ {〈∪ 𝐼,
1〉}:{∪ 𝐼}⟶ℤ)) |
36 | 32, 35 | mpbird 247 |
. . . . . . . . 9
⊢ (𝐼 ≈ 1𝑜
→ {〈∪ 𝐼, 1〉}:𝐼⟶ℤ) |
37 | | zringbas 19824 |
. . . . . . . . . 10
⊢ ℤ =
(Base‘ℤring) |
38 | 3, 37, 23 | frgpup3 18191 |
. . . . . . . . 9
⊢
((ℤring ∈ Grp ∧ 𝐼 ∈ V ∧ {〈∪ 𝐼,
1〉}:𝐼⟶ℤ)
→ ∃!𝑓 ∈
(𝐺 GrpHom
ℤring)(𝑓
∘ (varFGrp‘𝐼)) = {〈∪
𝐼,
1〉}) |
39 | 28, 19, 36, 38 | mp3an2i 1429 |
. . . . . . . 8
⊢ (𝐼 ≈ 1𝑜
→ ∃!𝑓 ∈
(𝐺 GrpHom
ℤring)(𝑓
∘ (varFGrp‘𝐼)) = {〈∪
𝐼,
1〉}) |
40 | 39 | adantr 481 |
. . . . . . 7
⊢ ((𝐼 ≈ 1𝑜
∧ 𝑥 ∈
(Base‘𝐺)) →
∃!𝑓 ∈ (𝐺 GrpHom
ℤring)(𝑓
∘ (varFGrp‘𝐼)) = {〈∪
𝐼,
1〉}) |
41 | | reurex 3160 |
. . . . . . 7
⊢
(∃!𝑓 ∈
(𝐺 GrpHom
ℤring)(𝑓
∘ (varFGrp‘𝐼)) = {〈∪
𝐼, 1〉} →
∃𝑓 ∈ (𝐺 GrpHom
ℤring)(𝑓
∘ (varFGrp‘𝐼)) = {〈∪
𝐼,
1〉}) |
42 | 40, 41 | syl 17 |
. . . . . 6
⊢ ((𝐼 ≈ 1𝑜
∧ 𝑥 ∈
(Base‘𝐺)) →
∃𝑓 ∈ (𝐺 GrpHom
ℤring)(𝑓
∘ (varFGrp‘𝐼)) = {〈∪
𝐼,
1〉}) |
43 | | fveq1 6190 |
. . . . . . . . . 10
⊢ ((𝑓 ∘
(varFGrp‘𝐼)) = {〈∪
𝐼, 1〉} → ((𝑓 ∘
(varFGrp‘𝐼))‘∪ 𝐼) = ({〈∪ 𝐼,
1〉}‘∪ 𝐼)) |
44 | | fvco3 6275 |
. . . . . . . . . . . 12
⊢
(((varFGrp‘𝐼):𝐼⟶(Base‘𝐺) ∧ ∪ 𝐼 ∈ 𝐼) → ((𝑓 ∘
(varFGrp‘𝐼))‘∪ 𝐼) = (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼))) |
45 | 25, 26, 44 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝐼 ≈ 1𝑜
→ ((𝑓 ∘
(varFGrp‘𝐼))‘∪ 𝐼) = (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼))) |
46 | | 1z 11407 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℤ |
47 | | fvsng 6447 |
. . . . . . . . . . . 12
⊢ ((∪ 𝐼
∈ V ∧ 1 ∈ ℤ) → ({〈∪
𝐼, 1〉}‘∪ 𝐼) =
1) |
48 | 30, 46, 47 | sylancl 694 |
. . . . . . . . . . 11
⊢ (𝐼 ≈ 1𝑜
→ ({〈∪ 𝐼, 1〉}‘∪ 𝐼) =
1) |
49 | 45, 48 | eqeq12d 2637 |
. . . . . . . . . 10
⊢ (𝐼 ≈ 1𝑜
→ (((𝑓 ∘
(varFGrp‘𝐼))‘∪ 𝐼) = ({〈∪ 𝐼,
1〉}‘∪ 𝐼) ↔ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) |
50 | 43, 49 | syl5ib 234 |
. . . . . . . . 9
⊢ (𝐼 ≈ 1𝑜
→ ((𝑓 ∘
(varFGrp‘𝐼)) = {〈∪
𝐼, 1〉} → (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) |
51 | 50 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝐼 ≈ 1𝑜
∧ 𝑥 ∈
(Base‘𝐺)) ∧ 𝑓 ∈ (𝐺 GrpHom ℤring)) →
((𝑓 ∘
(varFGrp‘𝐼)) = {〈∪
𝐼, 1〉} → (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) |
52 | 16, 37 | ghmf 17664 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ (𝐺 GrpHom ℤring) → 𝑓:(Base‘𝐺)⟶ℤ) |
53 | 52 | ad2antrl 764 |
. . . . . . . . . . . 12
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → 𝑓:(Base‘𝐺)⟶ℤ) |
54 | 53 | ffvelrnda 6359 |
. . . . . . . . . . 11
⊢ (((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) ∧ 𝑥 ∈
(Base‘𝐺)) →
(𝑓‘𝑥) ∈ ℤ) |
55 | 54 | an32s 846 |
. . . . . . . . . 10
⊢ (((𝐼 ≈ 1𝑜
∧ 𝑥 ∈
(Base‘𝐺)) ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑓‘𝑥) ∈
ℤ) |
56 | | mptresid 5456 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (Base‘𝐺) ↦ 𝑥) = ( I ↾ (Base‘𝐺)) |
57 | 3, 16, 23 | frgpup3 18191 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ Grp ∧ 𝐼 ∈ V ∧
(varFGrp‘𝐼):𝐼⟶(Base‘𝐺)) → ∃!𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼)) |
58 | 21, 19, 25, 57 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐼 ≈ 1𝑜
→ ∃!𝑔 ∈
(𝐺 GrpHom 𝐺)(𝑔 ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼)) |
59 | | reurmo 3161 |
. . . . . . . . . . . . . . . . 17
⊢
(∃!𝑔 ∈
(𝐺 GrpHom 𝐺)(𝑔 ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼) → ∃*𝑔 ∈ (𝐺 GrpHom 𝐺)(𝑔 ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼)) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐼 ≈ 1𝑜
→ ∃*𝑔 ∈
(𝐺 GrpHom 𝐺)(𝑔 ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼)) |
61 | 60 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ∃*𝑔 ∈
(𝐺 GrpHom 𝐺)(𝑔 ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼)) |
62 | 21 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → 𝐺 ∈
Grp) |
63 | 16 | idghm 17675 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ Grp → ( I ↾
(Base‘𝐺)) ∈
(𝐺 GrpHom 𝐺)) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ( I ↾ (Base‘𝐺)) ∈ (𝐺 GrpHom 𝐺)) |
65 | 25 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (varFGrp‘𝐼):𝐼⟶(Base‘𝐺)) |
66 | | fcoi2 6079 |
. . . . . . . . . . . . . . . 16
⊢
((varFGrp‘𝐼):𝐼⟶(Base‘𝐺) → (( I ↾ (Base‘𝐺)) ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼)) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (( I ↾ (Base‘𝐺)) ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼)) |
68 | 53 | feqmptd 6249 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → 𝑓 = (𝑥 ∈ (Base‘𝐺) ↦ (𝑓‘𝑥))) |
69 | | eqidd 2623 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑛 ∈ ℤ
↦ (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
= (𝑛 ∈ ℤ ↦
(𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))) |
70 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (𝑓‘𝑥) → (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))
= ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
71 | 54, 68, 69, 70 | fmptco 6396 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ((𝑛 ∈
ℤ ↦ (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
∘ 𝑓) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))) |
72 | 27 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ((varFGrp‘𝐼)‘∪ 𝐼) ∈ (Base‘𝐺)) |
73 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
= (𝑛 ∈ ℤ ↦
(𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
74 | 17, 73, 16 | mulgghm2 19845 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ Grp ∧
((varFGrp‘𝐼)‘∪ 𝐼) ∈ (Base‘𝐺)) → (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
∈ (ℤring GrpHom 𝐺)) |
75 | 62, 72, 74 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑛 ∈ ℤ
↦ (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
∈ (ℤring GrpHom 𝐺)) |
76 | | simprl 794 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → 𝑓 ∈ (𝐺 GrpHom
ℤring)) |
77 | | ghmco 17680 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈ ℤ ↦ (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
∈ (ℤring GrpHom 𝐺) ∧ 𝑓 ∈ (𝐺 GrpHom ℤring)) →
((𝑛 ∈ ℤ ↦
(𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
∘ 𝑓) ∈ (𝐺 GrpHom 𝐺)) |
78 | 75, 76, 77 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ((𝑛 ∈
ℤ ↦ (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
∘ 𝑓) ∈ (𝐺 GrpHom 𝐺)) |
79 | 71, 78 | eqeltrrd 2702 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑥 ∈
(Base‘𝐺) ↦
((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
∈ (𝐺 GrpHom 𝐺)) |
80 | 34 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → 𝐼 = {∪ 𝐼}) |
81 | 80 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑦 ∈ 𝐼 ↔ 𝑦 ∈ {∪ 𝐼})) |
82 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1) |
83 | 82 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ((𝑓‘((varFGrp‘𝐼)‘∪ 𝐼))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)) =
(1(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
84 | 16, 17 | mulg1 17548 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((varFGrp‘𝐼)‘∪ 𝐼) ∈ (Base‘𝐺) →
(1(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))
= ((varFGrp‘𝐼)‘∪ 𝐼)) |
85 | 72, 84 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (1(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)) =
((varFGrp‘𝐼)‘∪ 𝐼)) |
86 | 83, 85 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ((𝑓‘((varFGrp‘𝐼)‘∪ 𝐼))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)) =
((varFGrp‘𝐼)‘∪ 𝐼)) |
87 | | elsni 4194 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ {∪ 𝐼}
→ 𝑦 = ∪ 𝐼) |
88 | 87 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ {∪ 𝐼}
→ ((varFGrp‘𝐼)‘𝑦) = ((varFGrp‘𝐼)‘∪ 𝐼)) |
89 | 88 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ {∪ 𝐼}
→ (𝑓‘((varFGrp‘𝐼)‘𝑦)) = (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼))) |
90 | 89 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ {∪ 𝐼}
→ ((𝑓‘((varFGrp‘𝐼)‘𝑦))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)) =
((𝑓‘((varFGrp‘𝐼)‘∪ 𝐼))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
91 | 90, 88 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ {∪ 𝐼}
→ (((𝑓‘((varFGrp‘𝐼)‘𝑦))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)) =
((varFGrp‘𝐼)‘𝑦) ↔ ((𝑓‘((varFGrp‘𝐼)‘∪ 𝐼))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)) =
((varFGrp‘𝐼)‘∪ 𝐼))) |
92 | 86, 91 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑦 ∈ {∪ 𝐼}
→ ((𝑓‘((varFGrp‘𝐼)‘𝑦))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)) =
((varFGrp‘𝐼)‘𝑦))) |
93 | 81, 92 | sylbid 230 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑦 ∈ 𝐼 → ((𝑓‘((varFGrp‘𝐼)‘𝑦))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)) =
((varFGrp‘𝐼)‘𝑦))) |
94 | 93 | imp 445 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) ∧ 𝑦 ∈ 𝐼) → ((𝑓‘((varFGrp‘𝐼)‘𝑦))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)) =
((varFGrp‘𝐼)‘𝑦)) |
95 | 94 | mpteq2dva 4744 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑦 ∈ 𝐼 ↦ ((𝑓‘((varFGrp‘𝐼)‘𝑦))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
= (𝑦 ∈ 𝐼 ↦
((varFGrp‘𝐼)‘𝑦))) |
96 | 65 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) ∧ 𝑦 ∈ 𝐼) →
((varFGrp‘𝐼)‘𝑦) ∈ (Base‘𝐺)) |
97 | 65 | feqmptd 6249 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (varFGrp‘𝐼) = (𝑦 ∈ 𝐼 ↦
((varFGrp‘𝐼)‘𝑦))) |
98 | | eqidd 2623 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑥 ∈
(Base‘𝐺) ↦
((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
= (𝑥 ∈
(Base‘𝐺) ↦
((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))) |
99 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 =
((varFGrp‘𝐼)‘𝑦) → (𝑓‘𝑥) = (𝑓‘((varFGrp‘𝐼)‘𝑦))) |
100 | 99 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 =
((varFGrp‘𝐼)‘𝑦) → ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))
= ((𝑓‘((varFGrp‘𝐼)‘𝑦))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
101 | 96, 97, 98, 100 | fmptco 6396 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ((𝑥 ∈
(Base‘𝐺) ↦
((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
∘ (varFGrp‘𝐼)) = (𝑦 ∈ 𝐼 ↦ ((𝑓‘((varFGrp‘𝐼)‘𝑦))(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))) |
102 | 95, 101, 97 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ((𝑥 ∈
(Base‘𝐺) ↦
((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
∘ (varFGrp‘𝐼)) = (varFGrp‘𝐼)) |
103 | | coeq1 5279 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = ( I ↾ (Base‘𝐺)) → (𝑔 ∘
(varFGrp‘𝐼)) = (( I ↾ (Base‘𝐺)) ∘
(varFGrp‘𝐼))) |
104 | 103 | eqeq1d 2624 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = ( I ↾ (Base‘𝐺)) → ((𝑔 ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼) ↔ (( I ↾
(Base‘𝐺)) ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼))) |
105 | | coeq1 5279 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
→ (𝑔 ∘
(varFGrp‘𝐼)) = ((𝑥 ∈ (Base‘𝐺) ↦ ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
∘ (varFGrp‘𝐼))) |
106 | 105 | eqeq1d 2624 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
→ ((𝑔 ∘
(varFGrp‘𝐼)) = (varFGrp‘𝐼) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
∘ (varFGrp‘𝐼)) = (varFGrp‘𝐼))) |
107 | 104, 106 | rmoi 3530 |
. . . . . . . . . . . . . . 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‘𝐼)‘∪ 𝐼)))) |
108 | 61, 64, 67, 79, 102, 107 | syl122anc 1335 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ( I ↾ (Base‘𝐺)) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))) |
109 | 56, 108 | syl5eq 2668 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → (𝑥 ∈
(Base‘𝐺) ↦ 𝑥) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))) |
110 | | mpteqb 6299 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
(Base‘𝐺)𝑥 ∈ (Base‘𝐺) → ((𝑥 ∈ (Base‘𝐺) ↦ 𝑥) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
↔ ∀𝑥 ∈
(Base‘𝐺)𝑥 = ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))) |
111 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (Base‘𝐺) → 𝑥 ∈ (Base‘𝐺)) |
112 | 110, 111 | mprg 2926 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (Base‘𝐺) ↦ 𝑥) = (𝑥 ∈ (Base‘𝐺) ↦ ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
↔ ∀𝑥 ∈
(Base‘𝐺)𝑥 = ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
113 | 109, 112 | sylib 208 |
. . . . . . . . . . . 12
⊢ ((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ∀𝑥 ∈
(Base‘𝐺)𝑥 = ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
114 | 113 | r19.21bi 2932 |
. . . . . . . . . . 11
⊢ (((𝐼 ≈ 1𝑜
∧ (𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) ∧ 𝑥 ∈
(Base‘𝐺)) → 𝑥 = ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
115 | 114 | an32s 846 |
. . . . . . . . . 10
⊢ (((𝐼 ≈ 1𝑜
∧ 𝑥 ∈
(Base‘𝐺)) ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → 𝑥 = ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
116 | 70 | eqeq2d 2632 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑓‘𝑥) → (𝑥 = (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))
↔ 𝑥 = ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))) |
117 | 116 | rspcev 3309 |
. . . . . . . . . 10
⊢ (((𝑓‘𝑥) ∈ ℤ ∧ 𝑥 = ((𝑓‘𝑥)(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))
→ ∃𝑛 ∈
ℤ 𝑥 = (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
118 | 55, 115, 117 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝐼 ≈ 1𝑜
∧ 𝑥 ∈
(Base‘𝐺)) ∧
(𝑓 ∈ (𝐺 GrpHom ℤring)
∧ (𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1)) → ∃𝑛 ∈
ℤ 𝑥 = (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
119 | 118 | expr 643 |
. . . . . . . 8
⊢ (((𝐼 ≈ 1𝑜
∧ 𝑥 ∈
(Base‘𝐺)) ∧ 𝑓 ∈ (𝐺 GrpHom ℤring)) →
((𝑓‘((varFGrp‘𝐼)‘∪ 𝐼)) =
1 → ∃𝑛 ∈
ℤ 𝑥 = (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))) |
120 | 51, 119 | syld 47 |
. . . . . . 7
⊢ (((𝐼 ≈ 1𝑜
∧ 𝑥 ∈
(Base‘𝐺)) ∧ 𝑓 ∈ (𝐺 GrpHom ℤring)) →
((𝑓 ∘
(varFGrp‘𝐼)) = {〈∪
𝐼, 1〉} →
∃𝑛 ∈ ℤ
𝑥 = (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))) |
121 | 120 | rexlimdva 3031 |
. . . . . 6
⊢ ((𝐼 ≈ 1𝑜
∧ 𝑥 ∈
(Base‘𝐺)) →
(∃𝑓 ∈ (𝐺 GrpHom
ℤring)(𝑓
∘ (varFGrp‘𝐼)) = {〈∪
𝐼, 1〉} →
∃𝑛 ∈ ℤ
𝑥 = (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼)))) |
122 | 42, 121 | mpd 15 |
. . . . 5
⊢ ((𝐼 ≈ 1𝑜
∧ 𝑥 ∈
(Base‘𝐺)) →
∃𝑛 ∈ ℤ
𝑥 = (𝑛(.g‘𝐺)((varFGrp‘𝐼)‘∪ 𝐼))) |
123 | 16, 17, 21, 27, 122 | iscygd 18289 |
. . . 4
⊢ (𝐼 ≈ 1𝑜
→ 𝐺 ∈
CycGrp) |
124 | 15, 123 | jaoi 394 |
. . 3
⊢ ((𝐼 ≺ 1𝑜
∨ 𝐼 ≈
1𝑜) → 𝐺 ∈ CycGrp) |
125 | 1, 124 | sylbi 207 |
. 2
⊢ (𝐼 ≼ 1𝑜
→ 𝐺 ∈
CycGrp) |
126 | | cygabl 18292 |
. . 3
⊢ (𝐺 ∈ CycGrp → 𝐺 ∈ Abel) |
127 | 3 | frgpnabl 18278 |
. . . . 5
⊢
(1𝑜 ≺ 𝐼 → ¬ 𝐺 ∈ Abel) |
128 | 127 | con2i 134 |
. . . 4
⊢ (𝐺 ∈ Abel → ¬
1𝑜 ≺ 𝐼) |
129 | | ablgrp 18198 |
. . . . . 6
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
130 | | eqid 2622 |
. . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) |
131 | 16, 130 | grpidcl 17450 |
. . . . . 6
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ (Base‘𝐺)) |
132 | 3, 16 | elbasfv 15920 |
. . . . . 6
⊢
((0g‘𝐺) ∈ (Base‘𝐺) → 𝐼 ∈ V) |
133 | 129, 131,
132 | 3syl 18 |
. . . . 5
⊢ (𝐺 ∈ Abel → 𝐼 ∈ V) |
134 | | 1onn 7719 |
. . . . . 6
⊢
1𝑜 ∈ ω |
135 | | nnfi 8153 |
. . . . . 6
⊢
(1𝑜 ∈ ω → 1𝑜
∈ Fin) |
136 | 134, 135 | ax-mp 5 |
. . . . 5
⊢
1𝑜 ∈ Fin |
137 | | fidomtri2 8820 |
. . . . 5
⊢ ((𝐼 ∈ V ∧
1𝑜 ∈ Fin) → (𝐼 ≼ 1𝑜 ↔ ¬
1𝑜 ≺ 𝐼)) |
138 | 133, 136,
137 | sylancl 694 |
. . . 4
⊢ (𝐺 ∈ Abel → (𝐼 ≼ 1𝑜
↔ ¬ 1𝑜 ≺ 𝐼)) |
139 | 128, 138 | mpbird 247 |
. . 3
⊢ (𝐺 ∈ Abel → 𝐼 ≼
1𝑜) |
140 | 126, 139 | syl 17 |
. 2
⊢ (𝐺 ∈ CycGrp → 𝐼 ≼
1𝑜) |
141 | 125, 140 | impbii 199 |
1
⊢ (𝐼 ≼ 1𝑜
↔ 𝐺 ∈
CycGrp) |