Step | Hyp | Ref
| Expression |
1 | | frgpup3.k |
. . 3
⊢ (𝜑 → 𝐾 ∈ (𝐺 GrpHom 𝐻)) |
2 | | frgpup.x |
. . . 4
⊢ 𝑋 = (Base‘𝐺) |
3 | | frgpup.b |
. . . 4
⊢ 𝐵 = (Base‘𝐻) |
4 | 2, 3 | ghmf 17487 |
. . 3
⊢ (𝐾 ∈ (𝐺 GrpHom 𝐻) → 𝐾:𝑋⟶𝐵) |
5 | | ffn 5958 |
. . 3
⊢ (𝐾:𝑋⟶𝐵 → 𝐾 Fn 𝑋) |
6 | 1, 4, 5 | 3syl 18 |
. 2
⊢ (𝜑 → 𝐾 Fn 𝑋) |
7 | | frgpup.n |
. . . 4
⊢ 𝑁 = (invg‘𝐻) |
8 | | frgpup.t |
. . . 4
⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) |
9 | | frgpup.h |
. . . 4
⊢ (𝜑 → 𝐻 ∈ Grp) |
10 | | frgpup.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
11 | | frgpup.a |
. . . 4
⊢ (𝜑 → 𝐹:𝐼⟶𝐵) |
12 | | frgpup.w |
. . . 4
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2𝑜)) |
13 | | frgpup.r |
. . . 4
⊢ ∼ = (
~FG ‘𝐼) |
14 | | frgpup.g |
. . . 4
⊢ 𝐺 = (freeGrp‘𝐼) |
15 | | frgpup.e |
. . . 4
⊢ 𝐸 = ran (𝑔 ∈ 𝑊 ↦ 〈[𝑔] ∼ , (𝐻 Σg
(𝑇 ∘ 𝑔))〉) |
16 | 3, 7, 8, 9, 10, 11, 12, 13, 14, 2, 15 | frgpup1 18011 |
. . 3
⊢ (𝜑 → 𝐸 ∈ (𝐺 GrpHom 𝐻)) |
17 | 2, 3 | ghmf 17487 |
. . 3
⊢ (𝐸 ∈ (𝐺 GrpHom 𝐻) → 𝐸:𝑋⟶𝐵) |
18 | | ffn 5958 |
. . 3
⊢ (𝐸:𝑋⟶𝐵 → 𝐸 Fn 𝑋) |
19 | 16, 17, 18 | 3syl 18 |
. 2
⊢ (𝜑 → 𝐸 Fn 𝑋) |
20 | | eqid 2610 |
. . . . . . . . 9
⊢
(freeMnd‘(𝐼
× 2𝑜)) = (freeMnd‘(𝐼 ×
2𝑜)) |
21 | 14, 20, 13 | frgpval 17994 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑉 → 𝐺 = ((freeMnd‘(𝐼 × 2𝑜))
/s ∼ )) |
22 | 10, 21 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺 = ((freeMnd‘(𝐼 × 2𝑜))
/s ∼ )) |
23 | | 2on 7455 |
. . . . . . . . . . 11
⊢
2𝑜 ∈ On |
24 | | xpexg 6858 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 2𝑜 ∈ On)
→ (𝐼 ×
2𝑜) ∈ V) |
25 | 10, 23, 24 | sylancl 693 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐼 × 2𝑜) ∈
V) |
26 | | wrdexg 13170 |
. . . . . . . . . 10
⊢ ((𝐼 × 2𝑜)
∈ V → Word (𝐼
× 2𝑜) ∈ V) |
27 | | fvi 6165 |
. . . . . . . . . 10
⊢ (Word
(𝐼 ×
2𝑜) ∈ V → ( I ‘Word (𝐼 × 2𝑜)) = Word
(𝐼 ×
2𝑜)) |
28 | 25, 26, 27 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → ( I ‘Word (𝐼 × 2𝑜))
= Word (𝐼 ×
2𝑜)) |
29 | 12, 28 | syl5eq 2656 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 = Word (𝐼 ×
2𝑜)) |
30 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘(freeMnd‘(𝐼 × 2𝑜))) =
(Base‘(freeMnd‘(𝐼 ×
2𝑜))) |
31 | 20, 30 | frmdbas 17212 |
. . . . . . . . 9
⊢ ((𝐼 × 2𝑜)
∈ V → (Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word
(𝐼 ×
2𝑜)) |
32 | 25, 31 | syl 17 |
. . . . . . . 8
⊢ (𝜑 →
(Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word
(𝐼 ×
2𝑜)) |
33 | 29, 32 | eqtr4d 2647 |
. . . . . . 7
⊢ (𝜑 → 𝑊 = (Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
34 | | fvex 6113 |
. . . . . . . . 9
⊢ (
~FG ‘𝐼) ∈ V |
35 | 13, 34 | eqeltri 2684 |
. . . . . . . 8
⊢ ∼ ∈
V |
36 | 35 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ∼ ∈
V) |
37 | | fvex 6113 |
. . . . . . . 8
⊢
(freeMnd‘(𝐼
× 2𝑜)) ∈ V |
38 | 37 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (freeMnd‘(𝐼 × 2𝑜))
∈ V) |
39 | 22, 33, 36, 38 | qusbas 16028 |
. . . . . 6
⊢ (𝜑 → (𝑊 / ∼ ) =
(Base‘𝐺)) |
40 | 39, 2 | syl6reqr 2663 |
. . . . 5
⊢ (𝜑 → 𝑋 = (𝑊 / ∼ )) |
41 | | eqimss 3620 |
. . . . 5
⊢ (𝑋 = (𝑊 / ∼ ) → 𝑋 ⊆ (𝑊 / ∼ )) |
42 | 40, 41 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑋 ⊆ (𝑊 / ∼ )) |
43 | 42 | sselda 3568 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑋) → 𝑎 ∈ (𝑊 / ∼ )) |
44 | | eqid 2610 |
. . . 4
⊢ (𝑊 / ∼ ) = (𝑊 / ∼ ) |
45 | | fveq2 6103 |
. . . . 5
⊢ ([𝑡] ∼ = 𝑎 → (𝐾‘[𝑡] ∼ ) = (𝐾‘𝑎)) |
46 | | fveq2 6103 |
. . . . 5
⊢ ([𝑡] ∼ = 𝑎 → (𝐸‘[𝑡] ∼ ) = (𝐸‘𝑎)) |
47 | 45, 46 | eqeq12d 2625 |
. . . 4
⊢ ([𝑡] ∼ = 𝑎 → ((𝐾‘[𝑡] ∼ ) = (𝐸‘[𝑡] ∼ ) ↔ (𝐾‘𝑎) = (𝐸‘𝑎))) |
48 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → 𝑡 ∈ 𝑊) |
49 | 29 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → 𝑊 = Word (𝐼 ×
2𝑜)) |
50 | 48, 49 | eleqtrd 2690 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → 𝑡 ∈ Word (𝐼 ×
2𝑜)) |
51 | | wrdf 13165 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ Word (𝐼 × 2𝑜) → 𝑡:(0..^(#‘𝑡))⟶(𝐼 ×
2𝑜)) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → 𝑡:(0..^(#‘𝑡))⟶(𝐼 ×
2𝑜)) |
53 | 52 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑊) ∧ 𝑛 ∈ (0..^(#‘𝑡))) → (𝑡‘𝑛) ∈ (𝐼 ×
2𝑜)) |
54 | | elxp2 5056 |
. . . . . . . . . . 11
⊢ ((𝑡‘𝑛) ∈ (𝐼 × 2𝑜) ↔
∃𝑖 ∈ 𝐼 ∃𝑗 ∈ 2𝑜 (𝑡‘𝑛) = 〈𝑖, 𝑗〉) |
55 | 53, 54 | sylib 207 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑊) ∧ 𝑛 ∈ (0..^(#‘𝑡))) → ∃𝑖 ∈ 𝐼 ∃𝑗 ∈ 2𝑜 (𝑡‘𝑛) = 〈𝑖, 𝑗〉) |
56 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑖 → (𝐹‘𝑦) = (𝐹‘𝑖)) |
57 | 56 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑖 → (𝑁‘(𝐹‘𝑦)) = (𝑁‘(𝐹‘𝑖))) |
58 | 56, 57 | ifeq12d 4056 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑖 → if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))) = if(𝑧 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖)))) |
59 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑗 → (𝑧 = ∅ ↔ 𝑗 = ∅)) |
60 | 59 | ifbid 4058 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑗 → if(𝑧 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖))) = if(𝑗 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖)))) |
61 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹‘𝑖) ∈ V |
62 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁‘(𝐹‘𝑖)) ∈ V |
63 | 61, 62 | ifex 4106 |
. . . . . . . . . . . . . . . 16
⊢ if(𝑗 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖))) ∈ V |
64 | 58, 60, 8, 63 | ovmpt2 6694 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 2𝑜) → (𝑖𝑇𝑗) = if(𝑗 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖)))) |
65 | 64 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 2𝑜)) → (𝑖𝑇𝑗) = if(𝑗 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖)))) |
66 | | elpri 4145 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ {∅,
1𝑜} → (𝑗 = ∅ ∨ 𝑗 = 1𝑜)) |
67 | | df2o3 7460 |
. . . . . . . . . . . . . . . . 17
⊢
2𝑜 = {∅,
1𝑜} |
68 | 66, 67 | eleq2s 2706 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ 2𝑜
→ (𝑗 = ∅ ∨
𝑗 =
1𝑜)) |
69 | | frgpup3.e |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐾 ∘ 𝑈) = 𝐹) |
70 | 69 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝐾 ∘ 𝑈) = 𝐹) |
71 | 70 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → ((𝐾 ∘ 𝑈)‘𝑖) = (𝐹‘𝑖)) |
72 | | frgpup.u |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑈 =
(varFGrp‘𝐼) |
73 | 13, 72, 14, 2 | vrgpf 18004 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐼 ∈ 𝑉 → 𝑈:𝐼⟶𝑋) |
74 | 10, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑈:𝐼⟶𝑋) |
75 | | fvco3 6185 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑈:𝐼⟶𝑋 ∧ 𝑖 ∈ 𝐼) → ((𝐾 ∘ 𝑈)‘𝑖) = (𝐾‘(𝑈‘𝑖))) |
76 | 74, 75 | sylan 487 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → ((𝐾 ∘ 𝑈)‘𝑖) = (𝐾‘(𝑈‘𝑖))) |
77 | 71, 76 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝐹‘𝑖) = (𝐾‘(𝑈‘𝑖))) |
78 | 77 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = ∅) → (𝐹‘𝑖) = (𝐾‘(𝑈‘𝑖))) |
79 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = ∅ → if(𝑗 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖))) = (𝐹‘𝑖)) |
80 | 79 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = ∅) → if(𝑗 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖))) = (𝐹‘𝑖)) |
81 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = ∅) → 𝑗 = ∅) |
82 | 81 | opeq2d 4347 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = ∅) → 〈𝑖, 𝑗〉 = 〈𝑖, ∅〉) |
83 | 82 | s1eqd 13234 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = ∅) → 〈“〈𝑖, 𝑗〉”〉 =
〈“〈𝑖,
∅〉”〉) |
84 | 83 | eceq1d 7670 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = ∅) → [〈“〈𝑖, 𝑗〉”〉] ∼ =
[〈“〈𝑖,
∅〉”〉] ∼ ) |
85 | 13, 72 | vrgpval 18003 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑖 ∈ 𝐼) → (𝑈‘𝑖) = [〈“〈𝑖, ∅〉”〉] ∼
) |
86 | 10, 85 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝑈‘𝑖) = [〈“〈𝑖, ∅〉”〉] ∼
) |
87 | 86 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = ∅) → (𝑈‘𝑖) = [〈“〈𝑖, ∅〉”〉] ∼
) |
88 | 84, 87 | eqtr4d 2647 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = ∅) → [〈“〈𝑖, 𝑗〉”〉] ∼ = (𝑈‘𝑖)) |
89 | 88 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = ∅) → (𝐾‘[〈“〈𝑖, 𝑗〉”〉] ∼ ) = (𝐾‘(𝑈‘𝑖))) |
90 | 78, 80, 89 | 3eqtr4d 2654 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = ∅) → if(𝑗 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖))) = (𝐾‘[〈“〈𝑖, 𝑗〉”〉] ∼ )) |
91 | 77 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝑁‘(𝐹‘𝑖)) = (𝑁‘(𝐾‘(𝑈‘𝑖)))) |
92 | 1 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝐾 ∈ (𝐺 GrpHom 𝐻)) |
93 | 74 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝑈‘𝑖) ∈ 𝑋) |
94 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(invg‘𝐺) = (invg‘𝐺) |
95 | 2, 94, 7 | ghminv 17490 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐾 ∈ (𝐺 GrpHom 𝐻) ∧ (𝑈‘𝑖) ∈ 𝑋) → (𝐾‘((invg‘𝐺)‘(𝑈‘𝑖))) = (𝑁‘(𝐾‘(𝑈‘𝑖)))) |
96 | 92, 93, 95 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝐾‘((invg‘𝐺)‘(𝑈‘𝑖))) = (𝑁‘(𝐾‘(𝑈‘𝑖)))) |
97 | 91, 96 | eqtr4d 2647 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝑁‘(𝐹‘𝑖)) = (𝐾‘((invg‘𝐺)‘(𝑈‘𝑖)))) |
98 | 97 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = 1𝑜) → (𝑁‘(𝐹‘𝑖)) = (𝐾‘((invg‘𝐺)‘(𝑈‘𝑖)))) |
99 | | 1n0 7462 |
. . . . . . . . . . . . . . . . . . . 20
⊢
1𝑜 ≠ ∅ |
100 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = 1𝑜) → 𝑗 =
1𝑜) |
101 | 100 | neeq1d 2841 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = 1𝑜) → (𝑗 ≠ ∅ ↔
1𝑜 ≠ ∅)) |
102 | 99, 101 | mpbiri 247 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = 1𝑜) → 𝑗 ≠ ∅) |
103 | | ifnefalse 4048 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ≠ ∅ → if(𝑗 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖))) = (𝑁‘(𝐹‘𝑖))) |
104 | 102, 103 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = 1𝑜) → if(𝑗 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖))) = (𝑁‘(𝐹‘𝑖))) |
105 | 100 | opeq2d 4347 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = 1𝑜) → 〈𝑖, 𝑗〉 = 〈𝑖,
1𝑜〉) |
106 | 105 | s1eqd 13234 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = 1𝑜) →
〈“〈𝑖, 𝑗〉”〉 =
〈“〈𝑖,
1𝑜〉”〉) |
107 | 106 | eceq1d 7670 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = 1𝑜) →
[〈“〈𝑖,
𝑗〉”〉] ∼ =
[〈“〈𝑖,
1𝑜〉”〉] ∼ ) |
108 | 13, 72, 14, 94 | vrgpinv 18005 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑖 ∈ 𝐼) → ((invg‘𝐺)‘(𝑈‘𝑖)) = [〈“〈𝑖, 1𝑜〉”〉]
∼
) |
109 | 10, 108 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → ((invg‘𝐺)‘(𝑈‘𝑖)) = [〈“〈𝑖, 1𝑜〉”〉]
∼
) |
110 | 109 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = 1𝑜) →
((invg‘𝐺)‘(𝑈‘𝑖)) = [〈“〈𝑖, 1𝑜〉”〉]
∼
) |
111 | 107, 110 | eqtr4d 2647 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = 1𝑜) →
[〈“〈𝑖,
𝑗〉”〉] ∼ =
((invg‘𝐺)‘(𝑈‘𝑖))) |
112 | 111 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = 1𝑜) → (𝐾‘[〈“〈𝑖, 𝑗〉”〉] ∼ ) = (𝐾‘((invg‘𝐺)‘(𝑈‘𝑖)))) |
113 | 98, 104, 112 | 3eqtr4d 2654 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = 1𝑜) → if(𝑗 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖))) = (𝐾‘[〈“〈𝑖, 𝑗〉”〉] ∼ )) |
114 | 90, 113 | jaodan 822 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ (𝑗 = ∅ ∨ 𝑗 = 1𝑜)) → if(𝑗 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖))) = (𝐾‘[〈“〈𝑖, 𝑗〉”〉] ∼ )) |
115 | 68, 114 | sylan2 490 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 2𝑜) →
if(𝑗 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖))) = (𝐾‘[〈“〈𝑖, 𝑗〉”〉] ∼ )) |
116 | 115 | anasss 677 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 2𝑜)) →
if(𝑗 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖))) = (𝐾‘[〈“〈𝑖, 𝑗〉”〉] ∼ )) |
117 | 65, 116 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 2𝑜)) → (𝑖𝑇𝑗) = (𝐾‘[〈“〈𝑖, 𝑗〉”〉] ∼ )) |
118 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡‘𝑛) = 〈𝑖, 𝑗〉 → (𝑇‘(𝑡‘𝑛)) = (𝑇‘〈𝑖, 𝑗〉)) |
119 | | df-ov 6552 |
. . . . . . . . . . . . . . 15
⊢ (𝑖𝑇𝑗) = (𝑇‘〈𝑖, 𝑗〉) |
120 | 118, 119 | syl6eqr 2662 |
. . . . . . . . . . . . . 14
⊢ ((𝑡‘𝑛) = 〈𝑖, 𝑗〉 → (𝑇‘(𝑡‘𝑛)) = (𝑖𝑇𝑗)) |
121 | | s1eq 13233 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡‘𝑛) = 〈𝑖, 𝑗〉 → 〈“(𝑡‘𝑛)”〉 = 〈“〈𝑖, 𝑗〉”〉) |
122 | 121 | eceq1d 7670 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡‘𝑛) = 〈𝑖, 𝑗〉 → [〈“(𝑡‘𝑛)”〉] ∼ =
[〈“〈𝑖,
𝑗〉”〉] ∼
) |
123 | 122 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ ((𝑡‘𝑛) = 〈𝑖, 𝑗〉 → (𝐾‘[〈“(𝑡‘𝑛)”〉] ∼ ) = (𝐾‘[〈“〈𝑖, 𝑗〉”〉] ∼ )) |
124 | 120, 123 | eqeq12d 2625 |
. . . . . . . . . . . . 13
⊢ ((𝑡‘𝑛) = 〈𝑖, 𝑗〉 → ((𝑇‘(𝑡‘𝑛)) = (𝐾‘[〈“(𝑡‘𝑛)”〉] ∼ ) ↔ (𝑖𝑇𝑗) = (𝐾‘[〈“〈𝑖, 𝑗〉”〉] ∼
))) |
125 | 117, 124 | syl5ibrcom 236 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 2𝑜)) →
((𝑡‘𝑛) = 〈𝑖, 𝑗〉 → (𝑇‘(𝑡‘𝑛)) = (𝐾‘[〈“(𝑡‘𝑛)”〉] ∼
))) |
126 | 125 | rexlimdvva 3020 |
. . . . . . . . . . 11
⊢ (𝜑 → (∃𝑖 ∈ 𝐼 ∃𝑗 ∈ 2𝑜 (𝑡‘𝑛) = 〈𝑖, 𝑗〉 → (𝑇‘(𝑡‘𝑛)) = (𝐾‘[〈“(𝑡‘𝑛)”〉] ∼
))) |
127 | 126 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑊) ∧ 𝑛 ∈ (0..^(#‘𝑡))) → (∃𝑖 ∈ 𝐼 ∃𝑗 ∈ 2𝑜 (𝑡‘𝑛) = 〈𝑖, 𝑗〉 → (𝑇‘(𝑡‘𝑛)) = (𝐾‘[〈“(𝑡‘𝑛)”〉] ∼
))) |
128 | 55, 127 | mpd 15 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑊) ∧ 𝑛 ∈ (0..^(#‘𝑡))) → (𝑇‘(𝑡‘𝑛)) = (𝐾‘[〈“(𝑡‘𝑛)”〉] ∼ )) |
129 | 128 | mpteq2dva 4672 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝑛 ∈ (0..^(#‘𝑡)) ↦ (𝑇‘(𝑡‘𝑛))) = (𝑛 ∈ (0..^(#‘𝑡)) ↦ (𝐾‘[〈“(𝑡‘𝑛)”〉] ∼
))) |
130 | 3, 7, 8, 9, 10, 11 | frgpuptf 18006 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇:(𝐼 × 2𝑜)⟶𝐵) |
131 | 130 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → 𝑇:(𝐼 × 2𝑜)⟶𝐵) |
132 | | fcompt 6306 |
. . . . . . . . 9
⊢ ((𝑇:(𝐼 × 2𝑜)⟶𝐵 ∧ 𝑡:(0..^(#‘𝑡))⟶(𝐼 × 2𝑜)) →
(𝑇 ∘ 𝑡) = (𝑛 ∈ (0..^(#‘𝑡)) ↦ (𝑇‘(𝑡‘𝑛)))) |
133 | 131, 52, 132 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝑇 ∘ 𝑡) = (𝑛 ∈ (0..^(#‘𝑡)) ↦ (𝑇‘(𝑡‘𝑛)))) |
134 | 53 | s1cld 13236 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑊) ∧ 𝑛 ∈ (0..^(#‘𝑡))) → 〈“(𝑡‘𝑛)”〉 ∈ Word (𝐼 ×
2𝑜)) |
135 | 29 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑊) ∧ 𝑛 ∈ (0..^(#‘𝑡))) → 𝑊 = Word (𝐼 ×
2𝑜)) |
136 | 134, 135 | eleqtrrd 2691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑊) ∧ 𝑛 ∈ (0..^(#‘𝑡))) → 〈“(𝑡‘𝑛)”〉 ∈ 𝑊) |
137 | 14, 13, 12, 2 | frgpeccl 17997 |
. . . . . . . . . 10
⊢
(〈“(𝑡‘𝑛)”〉 ∈ 𝑊 → [〈“(𝑡‘𝑛)”〉] ∼ ∈ 𝑋) |
138 | 136, 137 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑊) ∧ 𝑛 ∈ (0..^(#‘𝑡))) → [〈“(𝑡‘𝑛)”〉] ∼ ∈ 𝑋) |
139 | 52 | feqmptd 6159 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → 𝑡 = (𝑛 ∈ (0..^(#‘𝑡)) ↦ (𝑡‘𝑛))) |
140 | 10 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → 𝐼 ∈ 𝑉) |
141 | 140, 23, 24 | sylancl 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝐼 × 2𝑜) ∈
V) |
142 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(varFMnd‘(𝐼 × 2𝑜)) =
(varFMnd‘(𝐼 ×
2𝑜)) |
143 | 142 | vrmdfval 17216 |
. . . . . . . . . . . 12
⊢ ((𝐼 × 2𝑜)
∈ V → (varFMnd‘(𝐼 × 2𝑜)) = (𝑤 ∈ (𝐼 × 2𝑜) ↦
〈“𝑤”〉)) |
144 | 141, 143 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) →
(varFMnd‘(𝐼 × 2𝑜)) = (𝑤 ∈ (𝐼 × 2𝑜) ↦
〈“𝑤”〉)) |
145 | | s1eq 13233 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝑡‘𝑛) → 〈“𝑤”〉 = 〈“(𝑡‘𝑛)”〉) |
146 | 53, 139, 144, 145 | fmptco 6303 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) →
((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡) = (𝑛 ∈ (0..^(#‘𝑡)) ↦ 〈“(𝑡‘𝑛)”〉)) |
147 | | eqidd 2611 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) = (𝑤 ∈ 𝑊 ↦ [𝑤] ∼ )) |
148 | | eceq1 7669 |
. . . . . . . . . 10
⊢ (𝑤 = 〈“(𝑡‘𝑛)”〉 → [𝑤] ∼ =
[〈“(𝑡‘𝑛)”〉] ∼ ) |
149 | 136, 146,
147, 148 | fmptco 6303 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡)) = (𝑛 ∈ (0..^(#‘𝑡)) ↦ [〈“(𝑡‘𝑛)”〉] ∼ )) |
150 | 1 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → 𝐾 ∈ (𝐺 GrpHom 𝐻)) |
151 | 150, 4 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → 𝐾:𝑋⟶𝐵) |
152 | 151 | feqmptd 6159 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → 𝐾 = (𝑤 ∈ 𝑋 ↦ (𝐾‘𝑤))) |
153 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑤 = [〈“(𝑡‘𝑛)”〉] ∼ → (𝐾‘𝑤) = (𝐾‘[〈“(𝑡‘𝑛)”〉] ∼ )) |
154 | 138, 149,
152, 153 | fmptco 6303 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝐾 ∘ ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡))) = (𝑛 ∈ (0..^(#‘𝑡)) ↦ (𝐾‘[〈“(𝑡‘𝑛)”〉] ∼
))) |
155 | 129, 133,
154 | 3eqtr4d 2654 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝑇 ∘ 𝑡) = (𝐾 ∘ ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡)))) |
156 | 155 | oveq2d 6565 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝐻 Σg (𝑇 ∘ 𝑡)) = (𝐻 Σg (𝐾 ∘ ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡))))) |
157 | 3, 7, 8, 9, 10, 11, 12, 13, 14, 2, 15 | frgpupval 18010 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝐸‘[𝑡] ∼ ) = (𝐻 Σg
(𝑇 ∘ 𝑡))) |
158 | | ghmmhm 17493 |
. . . . . . . 8
⊢ (𝐾 ∈ (𝐺 GrpHom 𝐻) → 𝐾 ∈ (𝐺 MndHom 𝐻)) |
159 | 150, 158 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → 𝐾 ∈ (𝐺 MndHom 𝐻)) |
160 | 142 | vrmdf 17218 |
. . . . . . . . . . 11
⊢ ((𝐼 × 2𝑜)
∈ V → (varFMnd‘(𝐼 × 2𝑜)):(𝐼 ×
2𝑜)⟶Word (𝐼 ×
2𝑜)) |
161 | 141, 160 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) →
(varFMnd‘(𝐼 × 2𝑜)):(𝐼 ×
2𝑜)⟶Word (𝐼 ×
2𝑜)) |
162 | 49 | feq3d 5945 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) →
((varFMnd‘(𝐼 × 2𝑜)):(𝐼 ×
2𝑜)⟶𝑊 ↔
(varFMnd‘(𝐼 × 2𝑜)):(𝐼 ×
2𝑜)⟶Word (𝐼 ×
2𝑜))) |
163 | 161, 162 | mpbird 246 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) →
(varFMnd‘(𝐼 × 2𝑜)):(𝐼 ×
2𝑜)⟶𝑊) |
164 | | wrdco 13428 |
. . . . . . . . 9
⊢ ((𝑡 ∈ Word (𝐼 × 2𝑜) ∧
(varFMnd‘(𝐼 × 2𝑜)):(𝐼 ×
2𝑜)⟶𝑊) →
((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡) ∈ Word 𝑊) |
165 | 50, 163, 164 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) →
((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡) ∈ Word 𝑊) |
166 | 33 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → 𝑊 = (Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
167 | 166 | mpteq1d 4666 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) = (𝑤 ∈
(Base‘(freeMnd‘(𝐼 × 2𝑜))) ↦
[𝑤] ∼ )) |
168 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈
(Base‘(freeMnd‘(𝐼 × 2𝑜))) ↦
[𝑤] ∼ ) = (𝑤 ∈
(Base‘(freeMnd‘(𝐼 × 2𝑜))) ↦
[𝑤] ∼ ) |
169 | 20, 30, 14, 13, 168 | frgpmhm 18001 |
. . . . . . . . . . . 12
⊢ (𝐼 ∈ 𝑉 → (𝑤 ∈ (Base‘(freeMnd‘(𝐼 ×
2𝑜))) ↦ [𝑤] ∼ ) ∈
((freeMnd‘(𝐼 ×
2𝑜)) MndHom 𝐺)) |
170 | 140, 169 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝑤 ∈ (Base‘(freeMnd‘(𝐼 ×
2𝑜))) ↦ [𝑤] ∼ ) ∈
((freeMnd‘(𝐼 ×
2𝑜)) MndHom 𝐺)) |
171 | 167, 170 | eqeltrd 2688 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∈
((freeMnd‘(𝐼 ×
2𝑜)) MndHom 𝐺)) |
172 | 30, 2 | mhmf 17163 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∈
((freeMnd‘(𝐼 ×
2𝑜)) MndHom 𝐺) → (𝑤 ∈ 𝑊 ↦ [𝑤] ∼
):(Base‘(freeMnd‘(𝐼 ×
2𝑜)))⟶𝑋) |
173 | 171, 172 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝑤 ∈ 𝑊 ↦ [𝑤] ∼
):(Base‘(freeMnd‘(𝐼 ×
2𝑜)))⟶𝑋) |
174 | 166 | feq2d 5944 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ):𝑊⟶𝑋 ↔ (𝑤 ∈ 𝑊 ↦ [𝑤] ∼
):(Base‘(freeMnd‘(𝐼 ×
2𝑜)))⟶𝑋)) |
175 | 173, 174 | mpbird 246 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ):𝑊⟶𝑋) |
176 | | wrdco 13428 |
. . . . . . . 8
⊢
((((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡) ∈ Word 𝑊 ∧ (𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ):𝑊⟶𝑋) → ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡)) ∈ Word 𝑋) |
177 | 165, 175,
176 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡)) ∈ Word 𝑋) |
178 | 2 | gsumwmhm 17205 |
. . . . . . 7
⊢ ((𝐾 ∈ (𝐺 MndHom 𝐻) ∧ ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡)) ∈ Word 𝑋) → (𝐾‘(𝐺 Σg ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡)))) = (𝐻 Σg (𝐾 ∘ ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡))))) |
179 | 159, 177,
178 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝐾‘(𝐺 Σg ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡)))) = (𝐻 Σg (𝐾 ∘ ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡))))) |
180 | 156, 157,
179 | 3eqtr4d 2654 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝐸‘[𝑡] ∼ ) = (𝐾‘(𝐺 Σg ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡))))) |
181 | 20, 142 | frmdgsum 17222 |
. . . . . . . . 9
⊢ (((𝐼 × 2𝑜)
∈ V ∧ 𝑡 ∈
Word (𝐼 ×
2𝑜)) → ((freeMnd‘(𝐼 × 2𝑜))
Σg ((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡)) = 𝑡) |
182 | 141, 50, 181 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → ((freeMnd‘(𝐼 × 2𝑜))
Σg ((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡)) = 𝑡) |
183 | 182 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼
)‘((freeMnd‘(𝐼
× 2𝑜)) Σg
((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡))) = ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ )‘𝑡)) |
184 | | wrdco 13428 |
. . . . . . . . . 10
⊢ ((𝑡 ∈ Word (𝐼 × 2𝑜) ∧
(varFMnd‘(𝐼 × 2𝑜)):(𝐼 ×
2𝑜)⟶Word (𝐼 × 2𝑜)) →
((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡) ∈ Word Word (𝐼 ×
2𝑜)) |
185 | 50, 161, 184 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) →
((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡) ∈ Word Word (𝐼 ×
2𝑜)) |
186 | 32 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (Base‘(freeMnd‘(𝐼 ×
2𝑜))) = Word (𝐼 ×
2𝑜)) |
187 | | wrdeq 13182 |
. . . . . . . . . 10
⊢
((Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word
(𝐼 ×
2𝑜) → Word (Base‘(freeMnd‘(𝐼 ×
2𝑜))) = Word Word (𝐼 ×
2𝑜)) |
188 | 186, 187 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → Word
(Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word
Word (𝐼 ×
2𝑜)) |
189 | 185, 188 | eleqtrrd 2691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) →
((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡) ∈ Word
(Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
190 | 30 | gsumwmhm 17205 |
. . . . . . . 8
⊢ (((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∈
((freeMnd‘(𝐼 ×
2𝑜)) MndHom 𝐺) ∧
((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡) ∈ Word
(Base‘(freeMnd‘(𝐼 × 2𝑜)))) →
((𝑤 ∈ 𝑊 ↦ [𝑤] ∼
)‘((freeMnd‘(𝐼
× 2𝑜)) Σg
((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡))) = (𝐺 Σg ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡)))) |
191 | 171, 189,
190 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼
)‘((freeMnd‘(𝐼
× 2𝑜)) Σg
((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡))) = (𝐺 Σg ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡)))) |
192 | 12, 13 | efger 17954 |
. . . . . . . . 9
⊢ ∼ Er
𝑊 |
193 | 192 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → ∼ Er 𝑊) |
194 | | fvex 6113 |
. . . . . . . . . 10
⊢ ( I
‘Word (𝐼 ×
2𝑜)) ∈ V |
195 | 12, 194 | eqeltri 2684 |
. . . . . . . . 9
⊢ 𝑊 ∈ V |
196 | 195 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → 𝑊 ∈ V) |
197 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) = (𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) |
198 | 193, 196,
197 | divsfval 16030 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ )‘𝑡) = [𝑡] ∼ ) |
199 | 183, 191,
198 | 3eqtr3d 2652 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝐺 Σg ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡))) = [𝑡] ∼ ) |
200 | 199 | fveq2d 6107 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝐾‘(𝐺 Σg ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2𝑜)) ∘
𝑡)))) = (𝐾‘[𝑡] ∼ )) |
201 | 180, 200 | eqtr2d 2645 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝐾‘[𝑡] ∼ ) = (𝐸‘[𝑡] ∼ )) |
202 | 44, 47, 201 | ectocld 7701 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑊 / ∼ )) → (𝐾‘𝑎) = (𝐸‘𝑎)) |
203 | 43, 202 | syldan 486 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑋) → (𝐾‘𝑎) = (𝐸‘𝑎)) |
204 | 6, 19, 203 | eqfnfvd 6222 |
1
⊢ (𝜑 → 𝐾 = 𝐸) |