Step | Hyp | Ref
| Expression |
1 | | frmdup.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑋) |
2 | | frmdup.m |
. . . . 5
⊢ 𝑀 = (freeMnd‘𝐼) |
3 | 2 | frmdmnd 17396 |
. . . 4
⊢ (𝐼 ∈ 𝑋 → 𝑀 ∈ Mnd) |
4 | 1, 3 | syl 17 |
. . 3
⊢ (𝜑 → 𝑀 ∈ Mnd) |
5 | | frmdup.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ Mnd) |
6 | 4, 5 | jca 554 |
. 2
⊢ (𝜑 → (𝑀 ∈ Mnd ∧ 𝐺 ∈ Mnd)) |
7 | 5 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ Word 𝐼) → 𝐺 ∈ Mnd) |
8 | | simpr 477 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ Word 𝐼) → 𝑥 ∈ Word 𝐼) |
9 | | frmdup.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴:𝐼⟶𝐵) |
10 | 9 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ Word 𝐼) → 𝐴:𝐼⟶𝐵) |
11 | | wrdco 13577 |
. . . . . . 7
⊢ ((𝑥 ∈ Word 𝐼 ∧ 𝐴:𝐼⟶𝐵) → (𝐴 ∘ 𝑥) ∈ Word 𝐵) |
12 | 8, 10, 11 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ Word 𝐼) → (𝐴 ∘ 𝑥) ∈ Word 𝐵) |
13 | | frmdup.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐺) |
14 | 13 | gsumwcl 17377 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ (𝐴 ∘ 𝑥) ∈ Word 𝐵) → (𝐺 Σg (𝐴 ∘ 𝑥)) ∈ 𝐵) |
15 | 7, 12, 14 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ Word 𝐼) → (𝐺 Σg (𝐴 ∘ 𝑥)) ∈ 𝐵) |
16 | | frmdup.e |
. . . . 5
⊢ 𝐸 = (𝑥 ∈ Word 𝐼 ↦ (𝐺 Σg (𝐴 ∘ 𝑥))) |
17 | 15, 16 | fmptd 6385 |
. . . 4
⊢ (𝜑 → 𝐸:Word 𝐼⟶𝐵) |
18 | | eqid 2622 |
. . . . . . 7
⊢
(Base‘𝑀) =
(Base‘𝑀) |
19 | 2, 18 | frmdbas 17389 |
. . . . . 6
⊢ (𝐼 ∈ 𝑋 → (Base‘𝑀) = Word 𝐼) |
20 | 1, 19 | syl 17 |
. . . . 5
⊢ (𝜑 → (Base‘𝑀) = Word 𝐼) |
21 | 20 | feq2d 6031 |
. . . 4
⊢ (𝜑 → (𝐸:(Base‘𝑀)⟶𝐵 ↔ 𝐸:Word 𝐼⟶𝐵)) |
22 | 17, 21 | mpbird 247 |
. . 3
⊢ (𝜑 → 𝐸:(Base‘𝑀)⟶𝐵) |
23 | 2, 18 | frmdelbas 17390 |
. . . . . . . . 9
⊢ (𝑦 ∈ (Base‘𝑀) → 𝑦 ∈ Word 𝐼) |
24 | 23 | ad2antrl 764 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → 𝑦 ∈ Word 𝐼) |
25 | 2, 18 | frmdelbas 17390 |
. . . . . . . . 9
⊢ (𝑧 ∈ (Base‘𝑀) → 𝑧 ∈ Word 𝐼) |
26 | 25 | ad2antll 765 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → 𝑧 ∈ Word 𝐼) |
27 | 9 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → 𝐴:𝐼⟶𝐵) |
28 | | ccatco 13581 |
. . . . . . . 8
⊢ ((𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ Word 𝐼 ∧ 𝐴:𝐼⟶𝐵) → (𝐴 ∘ (𝑦 ++ 𝑧)) = ((𝐴 ∘ 𝑦) ++ (𝐴 ∘ 𝑧))) |
29 | 24, 26, 27, 28 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝐴 ∘ (𝑦 ++ 𝑧)) = ((𝐴 ∘ 𝑦) ++ (𝐴 ∘ 𝑧))) |
30 | 29 | oveq2d 6666 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝐺 Σg (𝐴 ∘ (𝑦 ++ 𝑧))) = (𝐺 Σg ((𝐴 ∘ 𝑦) ++ (𝐴 ∘ 𝑧)))) |
31 | 5 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → 𝐺 ∈ Mnd) |
32 | | wrdco 13577 |
. . . . . . . 8
⊢ ((𝑦 ∈ Word 𝐼 ∧ 𝐴:𝐼⟶𝐵) → (𝐴 ∘ 𝑦) ∈ Word 𝐵) |
33 | 24, 27, 32 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝐴 ∘ 𝑦) ∈ Word 𝐵) |
34 | | wrdco 13577 |
. . . . . . . 8
⊢ ((𝑧 ∈ Word 𝐼 ∧ 𝐴:𝐼⟶𝐵) → (𝐴 ∘ 𝑧) ∈ Word 𝐵) |
35 | 26, 27, 34 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝐴 ∘ 𝑧) ∈ Word 𝐵) |
36 | | eqid 2622 |
. . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) |
37 | 13, 36 | gsumccat 17378 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ (𝐴 ∘ 𝑦) ∈ Word 𝐵 ∧ (𝐴 ∘ 𝑧) ∈ Word 𝐵) → (𝐺 Σg ((𝐴 ∘ 𝑦) ++ (𝐴 ∘ 𝑧))) = ((𝐺 Σg (𝐴 ∘ 𝑦))(+g‘𝐺)(𝐺 Σg (𝐴 ∘ 𝑧)))) |
38 | 31, 33, 35, 37 | syl3anc 1326 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝐺 Σg ((𝐴 ∘ 𝑦) ++ (𝐴 ∘ 𝑧))) = ((𝐺 Σg (𝐴 ∘ 𝑦))(+g‘𝐺)(𝐺 Σg (𝐴 ∘ 𝑧)))) |
39 | 30, 38 | eqtrd 2656 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝐺 Σg (𝐴 ∘ (𝑦 ++ 𝑧))) = ((𝐺 Σg (𝐴 ∘ 𝑦))(+g‘𝐺)(𝐺 Σg (𝐴 ∘ 𝑧)))) |
40 | | eqid 2622 |
. . . . . . . . 9
⊢
(+g‘𝑀) = (+g‘𝑀) |
41 | 2, 18, 40 | frmdadd 17392 |
. . . . . . . 8
⊢ ((𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀)) → (𝑦(+g‘𝑀)𝑧) = (𝑦 ++ 𝑧)) |
42 | 41 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝑦(+g‘𝑀)𝑧) = (𝑦 ++ 𝑧)) |
43 | 42 | fveq2d 6195 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝐸‘(𝑦(+g‘𝑀)𝑧)) = (𝐸‘(𝑦 ++ 𝑧))) |
44 | | ccatcl 13359 |
. . . . . . . 8
⊢ ((𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ Word 𝐼) → (𝑦 ++ 𝑧) ∈ Word 𝐼) |
45 | 24, 26, 44 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝑦 ++ 𝑧) ∈ Word 𝐼) |
46 | | coeq2 5280 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 ++ 𝑧) → (𝐴 ∘ 𝑥) = (𝐴 ∘ (𝑦 ++ 𝑧))) |
47 | 46 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 ++ 𝑧) → (𝐺 Σg (𝐴 ∘ 𝑥)) = (𝐺 Σg (𝐴 ∘ (𝑦 ++ 𝑧)))) |
48 | | ovex 6678 |
. . . . . . . 8
⊢ (𝐺 Σg
(𝐴 ∘ 𝑥)) ∈ V |
49 | 47, 16, 48 | fvmpt3i 6287 |
. . . . . . 7
⊢ ((𝑦 ++ 𝑧) ∈ Word 𝐼 → (𝐸‘(𝑦 ++ 𝑧)) = (𝐺 Σg (𝐴 ∘ (𝑦 ++ 𝑧)))) |
50 | 45, 49 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝐸‘(𝑦 ++ 𝑧)) = (𝐺 Σg (𝐴 ∘ (𝑦 ++ 𝑧)))) |
51 | 43, 50 | eqtrd 2656 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝐸‘(𝑦(+g‘𝑀)𝑧)) = (𝐺 Σg (𝐴 ∘ (𝑦 ++ 𝑧)))) |
52 | | coeq2 5280 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝐴 ∘ 𝑥) = (𝐴 ∘ 𝑦)) |
53 | 52 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝐺 Σg (𝐴 ∘ 𝑥)) = (𝐺 Σg (𝐴 ∘ 𝑦))) |
54 | 53, 16, 48 | fvmpt3i 6287 |
. . . . . . 7
⊢ (𝑦 ∈ Word 𝐼 → (𝐸‘𝑦) = (𝐺 Σg (𝐴 ∘ 𝑦))) |
55 | | coeq2 5280 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝐴 ∘ 𝑥) = (𝐴 ∘ 𝑧)) |
56 | 55 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝐺 Σg (𝐴 ∘ 𝑥)) = (𝐺 Σg (𝐴 ∘ 𝑧))) |
57 | 56, 16, 48 | fvmpt3i 6287 |
. . . . . . 7
⊢ (𝑧 ∈ Word 𝐼 → (𝐸‘𝑧) = (𝐺 Σg (𝐴 ∘ 𝑧))) |
58 | 54, 57 | oveqan12d 6669 |
. . . . . 6
⊢ ((𝑦 ∈ Word 𝐼 ∧ 𝑧 ∈ Word 𝐼) → ((𝐸‘𝑦)(+g‘𝐺)(𝐸‘𝑧)) = ((𝐺 Σg (𝐴 ∘ 𝑦))(+g‘𝐺)(𝐺 Σg (𝐴 ∘ 𝑧)))) |
59 | 24, 26, 58 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → ((𝐸‘𝑦)(+g‘𝐺)(𝐸‘𝑧)) = ((𝐺 Σg (𝐴 ∘ 𝑦))(+g‘𝐺)(𝐺 Σg (𝐴 ∘ 𝑧)))) |
60 | 39, 51, 59 | 3eqtr4d 2666 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘𝑀) ∧ 𝑧 ∈ (Base‘𝑀))) → (𝐸‘(𝑦(+g‘𝑀)𝑧)) = ((𝐸‘𝑦)(+g‘𝐺)(𝐸‘𝑧))) |
61 | 60 | ralrimivva 2971 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ (Base‘𝑀)∀𝑧 ∈ (Base‘𝑀)(𝐸‘(𝑦(+g‘𝑀)𝑧)) = ((𝐸‘𝑦)(+g‘𝐺)(𝐸‘𝑧))) |
62 | | wrd0 13330 |
. . . 4
⊢ ∅
∈ Word 𝐼 |
63 | | coeq2 5280 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (𝐴 ∘ 𝑥) = (𝐴 ∘ ∅)) |
64 | | co02 5649 |
. . . . . . . 8
⊢ (𝐴 ∘ ∅) =
∅ |
65 | 63, 64 | syl6eq 2672 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝐴 ∘ 𝑥) = ∅) |
66 | 65 | oveq2d 6666 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝐺 Σg
(𝐴 ∘ 𝑥)) = (𝐺 Σg
∅)) |
67 | | eqid 2622 |
. . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) |
68 | 67 | gsum0 17278 |
. . . . . 6
⊢ (𝐺 Σg
∅) = (0g‘𝐺) |
69 | 66, 68 | syl6eq 2672 |
. . . . 5
⊢ (𝑥 = ∅ → (𝐺 Σg
(𝐴 ∘ 𝑥)) = (0g‘𝐺)) |
70 | 69, 16, 48 | fvmpt3i 6287 |
. . . 4
⊢ (∅
∈ Word 𝐼 → (𝐸‘∅) =
(0g‘𝐺)) |
71 | 62, 70 | mp1i 13 |
. . 3
⊢ (𝜑 → (𝐸‘∅) = (0g‘𝐺)) |
72 | 22, 61, 71 | 3jca 1242 |
. 2
⊢ (𝜑 → (𝐸:(Base‘𝑀)⟶𝐵 ∧ ∀𝑦 ∈ (Base‘𝑀)∀𝑧 ∈ (Base‘𝑀)(𝐸‘(𝑦(+g‘𝑀)𝑧)) = ((𝐸‘𝑦)(+g‘𝐺)(𝐸‘𝑧)) ∧ (𝐸‘∅) = (0g‘𝐺))) |
73 | 2 | frmd0 17397 |
. . 3
⊢ ∅ =
(0g‘𝑀) |
74 | 18, 13, 40, 36, 73, 67 | ismhm 17337 |
. 2
⊢ (𝐸 ∈ (𝑀 MndHom 𝐺) ↔ ((𝑀 ∈ Mnd ∧ 𝐺 ∈ Mnd) ∧ (𝐸:(Base‘𝑀)⟶𝐵 ∧ ∀𝑦 ∈ (Base‘𝑀)∀𝑧 ∈ (Base‘𝑀)(𝐸‘(𝑦(+g‘𝑀)𝑧)) = ((𝐸‘𝑦)(+g‘𝐺)(𝐸‘𝑧)) ∧ (𝐸‘∅) = (0g‘𝐺)))) |
75 | 6, 72, 74 | sylanbrc 698 |
1
⊢ (𝜑 → 𝐸 ∈ (𝑀 MndHom 𝐺)) |