Step | Hyp | Ref
| Expression |
1 | | eqid 2193 |
. . . . 5
⊢
(0g‘𝑀) = (0g‘𝑀) |
2 | | eqid 2193 |
. . . . 5
⊢
(0g‘𝑁) = (0g‘𝑁) |
3 | 1, 2 | mhm0 13030 |
. . . 4
⊢ (𝐻 ∈ (𝑀 MndHom 𝑁) → (𝐻‘(0g‘𝑀)) = (0g‘𝑁)) |
4 | 3 | ad2antrr 488 |
. . 3
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 = ∅) → (𝐻‘(0g‘𝑀)) = (0g‘𝑁)) |
5 | | oveq2 5918 |
. . . . . 6
⊢ (𝑊 = ∅ → (𝑀 Σg
𝑊) = (𝑀 Σg
∅)) |
6 | 5 | adantl 277 |
. . . . 5
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 = ∅) → (𝑀 Σg 𝑊) = (𝑀 Σg
∅)) |
7 | | mhmrcl1 13025 |
. . . . . . 7
⊢ (𝐻 ∈ (𝑀 MndHom 𝑁) → 𝑀 ∈ Mnd) |
8 | 7 | ad2antrr 488 |
. . . . . 6
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 = ∅) → 𝑀 ∈ Mnd) |
9 | 1 | gsum0g 12969 |
. . . . . 6
⊢ (𝑀 ∈ Mnd → (𝑀 Σg
∅) = (0g‘𝑀)) |
10 | 8, 9 | syl 14 |
. . . . 5
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 = ∅) → (𝑀 Σg ∅) =
(0g‘𝑀)) |
11 | 6, 10 | eqtrd 2226 |
. . . 4
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 = ∅) → (𝑀 Σg 𝑊) = (0g‘𝑀)) |
12 | 11 | fveq2d 5550 |
. . 3
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 = ∅) → (𝐻‘(𝑀 Σg 𝑊)) = (𝐻‘(0g‘𝑀))) |
13 | | coeq2 4814 |
. . . . . . 7
⊢ (𝑊 = ∅ → (𝐻 ∘ 𝑊) = (𝐻 ∘ ∅)) |
14 | | co02 5171 |
. . . . . . 7
⊢ (𝐻 ∘ ∅) =
∅ |
15 | 13, 14 | eqtrdi 2242 |
. . . . . 6
⊢ (𝑊 = ∅ → (𝐻 ∘ 𝑊) = ∅) |
16 | 15 | oveq2d 5926 |
. . . . 5
⊢ (𝑊 = ∅ → (𝑁 Σg
(𝐻 ∘ 𝑊)) = (𝑁 Σg
∅)) |
17 | 16 | adantl 277 |
. . . 4
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 = ∅) → (𝑁 Σg (𝐻 ∘ 𝑊)) = (𝑁 Σg
∅)) |
18 | | mhmrcl2 13026 |
. . . . . 6
⊢ (𝐻 ∈ (𝑀 MndHom 𝑁) → 𝑁 ∈ Mnd) |
19 | 18 | ad2antrr 488 |
. . . . 5
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 = ∅) → 𝑁 ∈ Mnd) |
20 | 2 | gsum0g 12969 |
. . . . 5
⊢ (𝑁 ∈ Mnd → (𝑁 Σg
∅) = (0g‘𝑁)) |
21 | 19, 20 | syl 14 |
. . . 4
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 = ∅) → (𝑁 Σg ∅) =
(0g‘𝑁)) |
22 | 17, 21 | eqtrd 2226 |
. . 3
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 = ∅) → (𝑁 Σg (𝐻 ∘ 𝑊)) = (0g‘𝑁)) |
23 | 4, 12, 22 | 3eqtr4d 2236 |
. 2
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 = ∅) → (𝐻‘(𝑀 Σg 𝑊)) = (𝑁 Σg (𝐻 ∘ 𝑊))) |
24 | 7 | ad2antrr 488 |
. . . . 5
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝑀 ∈ Mnd) |
25 | | gsumwmhm.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑀) |
26 | | eqid 2193 |
. . . . . . 7
⊢
(+g‘𝑀) = (+g‘𝑀) |
27 | 25, 26 | mndcl 12994 |
. . . . . 6
⊢ ((𝑀 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(+g‘𝑀)𝑦) ∈ 𝐵) |
28 | 27 | 3expb 1206 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑀)𝑦) ∈ 𝐵) |
29 | 24, 28 | sylan 283 |
. . . 4
⊢ ((((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑀)𝑦) ∈ 𝐵) |
30 | | wrdf 10910 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝐵 → 𝑊:(0..^(♯‘𝑊))⟶𝐵) |
31 | 30 | ad2antlr 489 |
. . . . . 6
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝑊:(0..^(♯‘𝑊))⟶𝐵) |
32 | | wrdfin 10923 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ Word 𝐵 → 𝑊 ∈ Fin) |
33 | 32 | adantl 277 |
. . . . . . . . . . 11
⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) → 𝑊 ∈ Fin) |
34 | | hashnncl 10856 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Fin →
((♯‘𝑊) ∈
ℕ ↔ 𝑊 ≠
∅)) |
35 | 33, 34 | syl 14 |
. . . . . . . . . 10
⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) → ((♯‘𝑊) ∈ ℕ ↔ 𝑊 ≠ ∅)) |
36 | 35 | biimpar 297 |
. . . . . . . . 9
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈
ℕ) |
37 | 36 | nnzd 9428 |
. . . . . . . 8
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈
ℤ) |
38 | | fzoval 10204 |
. . . . . . . 8
⊢
((♯‘𝑊)
∈ ℤ → (0..^(♯‘𝑊)) = (0...((♯‘𝑊) − 1))) |
39 | 37, 38 | syl 14 |
. . . . . . 7
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) →
(0..^(♯‘𝑊)) =
(0...((♯‘𝑊)
− 1))) |
40 | 39 | feq2d 5383 |
. . . . . 6
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝑊:(0..^(♯‘𝑊))⟶𝐵 ↔ 𝑊:(0...((♯‘𝑊) − 1))⟶𝐵)) |
41 | 31, 40 | mpbid 147 |
. . . . 5
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝑊:(0...((♯‘𝑊) − 1))⟶𝐵) |
42 | 41 | ffvelcdmda 5685 |
. . . 4
⊢ ((((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) ∧ 𝑥 ∈ (0...((♯‘𝑊) − 1))) → (𝑊‘𝑥) ∈ 𝐵) |
43 | | nnm1nn0 9271 |
. . . . . 6
⊢
((♯‘𝑊)
∈ ℕ → ((♯‘𝑊) − 1) ∈
ℕ0) |
44 | 36, 43 | syl 14 |
. . . . 5
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → ((♯‘𝑊) − 1) ∈
ℕ0) |
45 | | nn0uz 9617 |
. . . . 5
⊢
ℕ0 = (ℤ≥‘0) |
46 | 44, 45 | eleqtrdi 2286 |
. . . 4
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → ((♯‘𝑊) − 1) ∈
(ℤ≥‘0)) |
47 | | eqid 2193 |
. . . . . . 7
⊢
(+g‘𝑁) = (+g‘𝑁) |
48 | 25, 26, 47 | mhmlin 13029 |
. . . . . 6
⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝐻‘(𝑥(+g‘𝑀)𝑦)) = ((𝐻‘𝑥)(+g‘𝑁)(𝐻‘𝑦))) |
49 | 48 | 3expb 1206 |
. . . . 5
⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐻‘(𝑥(+g‘𝑀)𝑦)) = ((𝐻‘𝑥)(+g‘𝑁)(𝐻‘𝑦))) |
50 | 49 | ad4ant14 514 |
. . . 4
⊢ ((((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐻‘(𝑥(+g‘𝑀)𝑦)) = ((𝐻‘𝑥)(+g‘𝑁)(𝐻‘𝑦))) |
51 | 41 | ffnd 5396 |
. . . . . 6
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝑊 Fn (0...((♯‘𝑊) − 1))) |
52 | | fvco2 5618 |
. . . . . 6
⊢ ((𝑊 Fn (0...((♯‘𝑊) − 1)) ∧ 𝑥 ∈
(0...((♯‘𝑊)
− 1))) → ((𝐻
∘ 𝑊)‘𝑥) = (𝐻‘(𝑊‘𝑥))) |
53 | 51, 52 | sylan 283 |
. . . . 5
⊢ ((((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) ∧ 𝑥 ∈ (0...((♯‘𝑊) − 1))) → ((𝐻 ∘ 𝑊)‘𝑥) = (𝐻‘(𝑊‘𝑥))) |
54 | 53 | eqcomd 2199 |
. . . 4
⊢ ((((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) ∧ 𝑥 ∈ (0...((♯‘𝑊) − 1))) → (𝐻‘(𝑊‘𝑥)) = ((𝐻 ∘ 𝑊)‘𝑥)) |
55 | | simplr 528 |
. . . 4
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝑊 ∈ Word 𝐵) |
56 | | coexg 5202 |
. . . . 5
⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) → (𝐻 ∘ 𝑊) ∈ V) |
57 | 56 | adantr 276 |
. . . 4
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐻 ∘ 𝑊) ∈ V) |
58 | | plusgslid 12720 |
. . . . . . 7
⊢
(+g = Slot (+g‘ndx) ∧
(+g‘ndx) ∈ ℕ) |
59 | 58 | slotex 12635 |
. . . . . 6
⊢ (𝑀 ∈ Mnd →
(+g‘𝑀)
∈ V) |
60 | 7, 59 | syl 14 |
. . . . 5
⊢ (𝐻 ∈ (𝑀 MndHom 𝑁) → (+g‘𝑀) ∈ V) |
61 | 60 | ad2antrr 488 |
. . . 4
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) →
(+g‘𝑀)
∈ V) |
62 | 58 | slotex 12635 |
. . . . . 6
⊢ (𝑁 ∈ Mnd →
(+g‘𝑁)
∈ V) |
63 | 18, 62 | syl 14 |
. . . . 5
⊢ (𝐻 ∈ (𝑀 MndHom 𝑁) → (+g‘𝑁) ∈ V) |
64 | 63 | ad2antrr 488 |
. . . 4
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) →
(+g‘𝑁)
∈ V) |
65 | 29, 42, 46, 50, 54, 55, 57, 61, 64 | seqhomog 10591 |
. . 3
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐻‘(seq0((+g‘𝑀), 𝑊)‘((♯‘𝑊) − 1))) =
(seq0((+g‘𝑁), (𝐻 ∘ 𝑊))‘((♯‘𝑊) − 1))) |
66 | 25, 26, 24, 46, 41 | gsumval2 12970 |
. . . 4
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝑀 Σg 𝑊) =
(seq0((+g‘𝑀), 𝑊)‘((♯‘𝑊) − 1))) |
67 | 66 | fveq2d 5550 |
. . 3
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐻‘(𝑀 Σg 𝑊)) = (𝐻‘(seq0((+g‘𝑀), 𝑊)‘((♯‘𝑊) − 1)))) |
68 | | eqid 2193 |
. . . 4
⊢
(Base‘𝑁) =
(Base‘𝑁) |
69 | 18 | ad2antrr 488 |
. . . 4
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝑁 ∈ Mnd) |
70 | 25, 68 | mhmf 13027 |
. . . . . 6
⊢ (𝐻 ∈ (𝑀 MndHom 𝑁) → 𝐻:𝐵⟶(Base‘𝑁)) |
71 | 70 | ad2antrr 488 |
. . . . 5
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝐻:𝐵⟶(Base‘𝑁)) |
72 | | fco 5411 |
. . . . 5
⊢ ((𝐻:𝐵⟶(Base‘𝑁) ∧ 𝑊:(0...((♯‘𝑊) − 1))⟶𝐵) → (𝐻 ∘ 𝑊):(0...((♯‘𝑊) − 1))⟶(Base‘𝑁)) |
73 | 71, 41, 72 | syl2anc 411 |
. . . 4
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐻 ∘ 𝑊):(0...((♯‘𝑊) − 1))⟶(Base‘𝑁)) |
74 | 68, 47, 69, 46, 73 | gsumval2 12970 |
. . 3
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝑁 Σg (𝐻 ∘ 𝑊)) = (seq0((+g‘𝑁), (𝐻 ∘ 𝑊))‘((♯‘𝑊) − 1))) |
75 | 65, 67, 74 | 3eqtr4d 2236 |
. 2
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐻‘(𝑀 Σg 𝑊)) = (𝑁 Σg (𝐻 ∘ 𝑊))) |
76 | | fin0or 6933 |
. . . 4
⊢ (𝑊 ∈ Fin → (𝑊 = ∅ ∨ ∃𝑗 𝑗 ∈ 𝑊)) |
77 | | n0r 3460 |
. . . . 5
⊢
(∃𝑗 𝑗 ∈ 𝑊 → 𝑊 ≠ ∅) |
78 | 77 | orim2i 762 |
. . . 4
⊢ ((𝑊 = ∅ ∨ ∃𝑗 𝑗 ∈ 𝑊) → (𝑊 = ∅ ∨ 𝑊 ≠ ∅)) |
79 | 76, 78 | syl 14 |
. . 3
⊢ (𝑊 ∈ Fin → (𝑊 = ∅ ∨ 𝑊 ≠ ∅)) |
80 | 33, 79 | syl 14 |
. 2
⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) → (𝑊 = ∅ ∨ 𝑊 ≠ ∅)) |
81 | 23, 75, 80 | mpjaodan 799 |
1
⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) → (𝐻‘(𝑀 Σg 𝑊)) = (𝑁 Σg (𝐻 ∘ 𝑊))) |