Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . . 5
⊢ (𝑊 = ∅ → (𝑀 Σg
𝑊) = (𝑀 Σg
∅)) |
2 | | eqid 2622 |
. . . . . 6
⊢
(0g‘𝑀) = (0g‘𝑀) |
3 | 2 | gsum0 17278 |
. . . . 5
⊢ (𝑀 Σg
∅) = (0g‘𝑀) |
4 | 1, 3 | syl6eq 2672 |
. . . 4
⊢ (𝑊 = ∅ → (𝑀 Σg
𝑊) =
(0g‘𝑀)) |
5 | 4 | fveq2d 6195 |
. . 3
⊢ (𝑊 = ∅ → (𝐻‘(𝑀 Σg 𝑊)) = (𝐻‘(0g‘𝑀))) |
6 | | coeq2 5280 |
. . . . . 6
⊢ (𝑊 = ∅ → (𝐻 ∘ 𝑊) = (𝐻 ∘ ∅)) |
7 | | co02 5649 |
. . . . . 6
⊢ (𝐻 ∘ ∅) =
∅ |
8 | 6, 7 | syl6eq 2672 |
. . . . 5
⊢ (𝑊 = ∅ → (𝐻 ∘ 𝑊) = ∅) |
9 | 8 | oveq2d 6666 |
. . . 4
⊢ (𝑊 = ∅ → (𝑁 Σg
(𝐻 ∘ 𝑊)) = (𝑁 Σg
∅)) |
10 | | eqid 2622 |
. . . . 5
⊢
(0g‘𝑁) = (0g‘𝑁) |
11 | 10 | gsum0 17278 |
. . . 4
⊢ (𝑁 Σg
∅) = (0g‘𝑁) |
12 | 9, 11 | syl6eq 2672 |
. . 3
⊢ (𝑊 = ∅ → (𝑁 Σg
(𝐻 ∘ 𝑊)) = (0g‘𝑁)) |
13 | 5, 12 | eqeq12d 2637 |
. 2
⊢ (𝑊 = ∅ → ((𝐻‘(𝑀 Σg 𝑊)) = (𝑁 Σg (𝐻 ∘ 𝑊)) ↔ (𝐻‘(0g‘𝑀)) = (0g‘𝑁))) |
14 | | mhmrcl1 17338 |
. . . . . 6
⊢ (𝐻 ∈ (𝑀 MndHom 𝑁) → 𝑀 ∈ Mnd) |
15 | 14 | ad2antrr 762 |
. . . . 5
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝑀 ∈ Mnd) |
16 | | gsumwmhm.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑀) |
17 | | eqid 2622 |
. . . . . . 7
⊢
(+g‘𝑀) = (+g‘𝑀) |
18 | 16, 17 | mndcl 17301 |
. . . . . 6
⊢ ((𝑀 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(+g‘𝑀)𝑦) ∈ 𝐵) |
19 | 18 | 3expb 1266 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑀)𝑦) ∈ 𝐵) |
20 | 15, 19 | sylan 488 |
. . . 4
⊢ ((((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑀)𝑦) ∈ 𝐵) |
21 | | wrdf 13310 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝐵 → 𝑊:(0..^(#‘𝑊))⟶𝐵) |
22 | 21 | ad2antlr 763 |
. . . . . 6
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝑊:(0..^(#‘𝑊))⟶𝐵) |
23 | | wrdfin 13323 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ Word 𝐵 → 𝑊 ∈ Fin) |
24 | 23 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) → 𝑊 ∈ Fin) |
25 | | hashnncl 13157 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Fin →
((#‘𝑊) ∈ ℕ
↔ 𝑊 ≠
∅)) |
26 | 24, 25 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) → ((#‘𝑊) ∈ ℕ ↔ 𝑊 ≠ ∅)) |
27 | 26 | biimpar 502 |
. . . . . . . . 9
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (#‘𝑊) ∈
ℕ) |
28 | 27 | nnzd 11481 |
. . . . . . . 8
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (#‘𝑊) ∈
ℤ) |
29 | | fzoval 12471 |
. . . . . . . 8
⊢
((#‘𝑊) ∈
ℤ → (0..^(#‘𝑊)) = (0...((#‘𝑊) − 1))) |
30 | 28, 29 | syl 17 |
. . . . . . 7
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (0..^(#‘𝑊)) = (0...((#‘𝑊) − 1))) |
31 | 30 | feq2d 6031 |
. . . . . 6
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝑊:(0..^(#‘𝑊))⟶𝐵 ↔ 𝑊:(0...((#‘𝑊) − 1))⟶𝐵)) |
32 | 22, 31 | mpbid 222 |
. . . . 5
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝑊:(0...((#‘𝑊) − 1))⟶𝐵) |
33 | 32 | ffvelrnda 6359 |
. . . 4
⊢ ((((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) ∧ 𝑥 ∈ (0...((#‘𝑊) − 1))) → (𝑊‘𝑥) ∈ 𝐵) |
34 | | nnm1nn0 11334 |
. . . . . 6
⊢
((#‘𝑊) ∈
ℕ → ((#‘𝑊)
− 1) ∈ ℕ0) |
35 | 27, 34 | syl 17 |
. . . . 5
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → ((#‘𝑊) − 1) ∈
ℕ0) |
36 | | nn0uz 11722 |
. . . . 5
⊢
ℕ0 = (ℤ≥‘0) |
37 | 35, 36 | syl6eleq 2711 |
. . . 4
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → ((#‘𝑊) − 1) ∈
(ℤ≥‘0)) |
38 | | simpll 790 |
. . . . 5
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝐻 ∈ (𝑀 MndHom 𝑁)) |
39 | | eqid 2622 |
. . . . . . 7
⊢
(+g‘𝑁) = (+g‘𝑁) |
40 | 16, 17, 39 | mhmlin 17342 |
. . . . . 6
⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝐻‘(𝑥(+g‘𝑀)𝑦)) = ((𝐻‘𝑥)(+g‘𝑁)(𝐻‘𝑦))) |
41 | 40 | 3expb 1266 |
. . . . 5
⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐻‘(𝑥(+g‘𝑀)𝑦)) = ((𝐻‘𝑥)(+g‘𝑁)(𝐻‘𝑦))) |
42 | 38, 41 | sylan 488 |
. . . 4
⊢ ((((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐻‘(𝑥(+g‘𝑀)𝑦)) = ((𝐻‘𝑥)(+g‘𝑁)(𝐻‘𝑦))) |
43 | | ffn 6045 |
. . . . . . 7
⊢ (𝑊:(0...((#‘𝑊) − 1))⟶𝐵 → 𝑊 Fn (0...((#‘𝑊) − 1))) |
44 | 32, 43 | syl 17 |
. . . . . 6
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝑊 Fn (0...((#‘𝑊) − 1))) |
45 | | fvco2 6273 |
. . . . . 6
⊢ ((𝑊 Fn (0...((#‘𝑊) − 1)) ∧ 𝑥 ∈ (0...((#‘𝑊) − 1))) → ((𝐻 ∘ 𝑊)‘𝑥) = (𝐻‘(𝑊‘𝑥))) |
46 | 44, 45 | sylan 488 |
. . . . 5
⊢ ((((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) ∧ 𝑥 ∈ (0...((#‘𝑊) − 1))) → ((𝐻 ∘ 𝑊)‘𝑥) = (𝐻‘(𝑊‘𝑥))) |
47 | 46 | eqcomd 2628 |
. . . 4
⊢ ((((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) ∧ 𝑥 ∈ (0...((#‘𝑊) − 1))) → (𝐻‘(𝑊‘𝑥)) = ((𝐻 ∘ 𝑊)‘𝑥)) |
48 | 20, 33, 37, 42, 47 | seqhomo 12848 |
. . 3
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐻‘(seq0((+g‘𝑀), 𝑊)‘((#‘𝑊) − 1))) =
(seq0((+g‘𝑁), (𝐻 ∘ 𝑊))‘((#‘𝑊) − 1))) |
49 | 16, 17, 15, 37, 32 | gsumval2 17280 |
. . . 4
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝑀 Σg 𝑊) =
(seq0((+g‘𝑀), 𝑊)‘((#‘𝑊) − 1))) |
50 | 49 | fveq2d 6195 |
. . 3
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐻‘(𝑀 Σg 𝑊)) = (𝐻‘(seq0((+g‘𝑀), 𝑊)‘((#‘𝑊) − 1)))) |
51 | | eqid 2622 |
. . . 4
⊢
(Base‘𝑁) =
(Base‘𝑁) |
52 | | mhmrcl2 17339 |
. . . . 5
⊢ (𝐻 ∈ (𝑀 MndHom 𝑁) → 𝑁 ∈ Mnd) |
53 | 52 | ad2antrr 762 |
. . . 4
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝑁 ∈ Mnd) |
54 | 16, 51 | mhmf 17340 |
. . . . . 6
⊢ (𝐻 ∈ (𝑀 MndHom 𝑁) → 𝐻:𝐵⟶(Base‘𝑁)) |
55 | 54 | ad2antrr 762 |
. . . . 5
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝐻:𝐵⟶(Base‘𝑁)) |
56 | | fco 6058 |
. . . . 5
⊢ ((𝐻:𝐵⟶(Base‘𝑁) ∧ 𝑊:(0...((#‘𝑊) − 1))⟶𝐵) → (𝐻 ∘ 𝑊):(0...((#‘𝑊) − 1))⟶(Base‘𝑁)) |
57 | 55, 32, 56 | syl2anc 693 |
. . . 4
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐻 ∘ 𝑊):(0...((#‘𝑊) − 1))⟶(Base‘𝑁)) |
58 | 51, 39, 53, 37, 57 | gsumval2 17280 |
. . 3
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝑁 Σg (𝐻 ∘ 𝑊)) = (seq0((+g‘𝑁), (𝐻 ∘ 𝑊))‘((#‘𝑊) − 1))) |
59 | 48, 50, 58 | 3eqtr4d 2666 |
. 2
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐻‘(𝑀 Σg 𝑊)) = (𝑁 Σg (𝐻 ∘ 𝑊))) |
60 | 2, 10 | mhm0 17343 |
. . 3
⊢ (𝐻 ∈ (𝑀 MndHom 𝑁) → (𝐻‘(0g‘𝑀)) = (0g‘𝑁)) |
61 | 60 | adantr 481 |
. 2
⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) → (𝐻‘(0g‘𝑀)) = (0g‘𝑁)) |
62 | 13, 59, 61 | pm2.61ne 2879 |
1
⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) → (𝐻‘(𝑀 Σg 𝑊)) = (𝑁 Σg (𝐻 ∘ 𝑊))) |