| Step | Hyp | Ref
| Expression |
| 1 | | oveq2 7439 |
. . . . 5
⊢ (𝑊 = ∅ → (𝑀 Σg
𝑊) = (𝑀 Σg
∅)) |
| 2 | | eqid 2737 |
. . . . . 6
⊢
(0g‘𝑀) = (0g‘𝑀) |
| 3 | 2 | gsum0 18697 |
. . . . 5
⊢ (𝑀 Σg
∅) = (0g‘𝑀) |
| 4 | 1, 3 | eqtrdi 2793 |
. . . 4
⊢ (𝑊 = ∅ → (𝑀 Σg
𝑊) =
(0g‘𝑀)) |
| 5 | 4 | fveq2d 6910 |
. . 3
⊢ (𝑊 = ∅ → (𝐻‘(𝑀 Σg 𝑊)) = (𝐻‘(0g‘𝑀))) |
| 6 | | coeq2 5869 |
. . . . . 6
⊢ (𝑊 = ∅ → (𝐻 ∘ 𝑊) = (𝐻 ∘ ∅)) |
| 7 | | co02 6280 |
. . . . . 6
⊢ (𝐻 ∘ ∅) =
∅ |
| 8 | 6, 7 | eqtrdi 2793 |
. . . . 5
⊢ (𝑊 = ∅ → (𝐻 ∘ 𝑊) = ∅) |
| 9 | 8 | oveq2d 7447 |
. . . 4
⊢ (𝑊 = ∅ → (𝑁 Σg
(𝐻 ∘ 𝑊)) = (𝑁 Σg
∅)) |
| 10 | | eqid 2737 |
. . . . 5
⊢
(0g‘𝑁) = (0g‘𝑁) |
| 11 | 10 | gsum0 18697 |
. . . 4
⊢ (𝑁 Σg
∅) = (0g‘𝑁) |
| 12 | 9, 11 | eqtrdi 2793 |
. . 3
⊢ (𝑊 = ∅ → (𝑁 Σg
(𝐻 ∘ 𝑊)) = (0g‘𝑁)) |
| 13 | 5, 12 | eqeq12d 2753 |
. 2
⊢ (𝑊 = ∅ → ((𝐻‘(𝑀 Σg 𝑊)) = (𝑁 Σg (𝐻 ∘ 𝑊)) ↔ (𝐻‘(0g‘𝑀)) = (0g‘𝑁))) |
| 14 | | mhmrcl1 18800 |
. . . . . 6
⊢ (𝐻 ∈ (𝑀 MndHom 𝑁) → 𝑀 ∈ Mnd) |
| 15 | 14 | ad2antrr 726 |
. . . . 5
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝑀 ∈ Mnd) |
| 16 | | gsumwmhm.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑀) |
| 17 | | eqid 2737 |
. . . . . . 7
⊢
(+g‘𝑀) = (+g‘𝑀) |
| 18 | 16, 17 | mndcl 18755 |
. . . . . 6
⊢ ((𝑀 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(+g‘𝑀)𝑦) ∈ 𝐵) |
| 19 | 18 | 3expb 1121 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑀)𝑦) ∈ 𝐵) |
| 20 | 15, 19 | sylan 580 |
. . . 4
⊢ ((((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑀)𝑦) ∈ 𝐵) |
| 21 | | wrdf 14557 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝐵 → 𝑊:(0..^(♯‘𝑊))⟶𝐵) |
| 22 | 21 | ad2antlr 727 |
. . . . . 6
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝑊:(0..^(♯‘𝑊))⟶𝐵) |
| 23 | | wrdfin 14570 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ Word 𝐵 → 𝑊 ∈ Fin) |
| 24 | 23 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) → 𝑊 ∈ Fin) |
| 25 | | hashnncl 14405 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Fin →
((♯‘𝑊) ∈
ℕ ↔ 𝑊 ≠
∅)) |
| 26 | 24, 25 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) → ((♯‘𝑊) ∈ ℕ ↔ 𝑊 ≠ ∅)) |
| 27 | 26 | biimpar 477 |
. . . . . . . . 9
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈
ℕ) |
| 28 | 27 | nnzd 12640 |
. . . . . . . 8
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈
ℤ) |
| 29 | | fzoval 13700 |
. . . . . . . 8
⊢
((♯‘𝑊)
∈ ℤ → (0..^(♯‘𝑊)) = (0...((♯‘𝑊) − 1))) |
| 30 | 28, 29 | syl 17 |
. . . . . . 7
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) →
(0..^(♯‘𝑊)) =
(0...((♯‘𝑊)
− 1))) |
| 31 | 30 | feq2d 6722 |
. . . . . 6
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝑊:(0..^(♯‘𝑊))⟶𝐵 ↔ 𝑊:(0...((♯‘𝑊) − 1))⟶𝐵)) |
| 32 | 22, 31 | mpbid 232 |
. . . . 5
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝑊:(0...((♯‘𝑊) − 1))⟶𝐵) |
| 33 | 32 | ffvelcdmda 7104 |
. . . 4
⊢ ((((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) ∧ 𝑥 ∈ (0...((♯‘𝑊) − 1))) → (𝑊‘𝑥) ∈ 𝐵) |
| 34 | | nnm1nn0 12567 |
. . . . . 6
⊢
((♯‘𝑊)
∈ ℕ → ((♯‘𝑊) − 1) ∈
ℕ0) |
| 35 | 27, 34 | syl 17 |
. . . . 5
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → ((♯‘𝑊) − 1) ∈
ℕ0) |
| 36 | | nn0uz 12920 |
. . . . 5
⊢
ℕ0 = (ℤ≥‘0) |
| 37 | 35, 36 | eleqtrdi 2851 |
. . . 4
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → ((♯‘𝑊) − 1) ∈
(ℤ≥‘0)) |
| 38 | | eqid 2737 |
. . . . . . 7
⊢
(+g‘𝑁) = (+g‘𝑁) |
| 39 | 16, 17, 38 | mhmlin 18806 |
. . . . . 6
⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝐻‘(𝑥(+g‘𝑀)𝑦)) = ((𝐻‘𝑥)(+g‘𝑁)(𝐻‘𝑦))) |
| 40 | 39 | 3expb 1121 |
. . . . 5
⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐻‘(𝑥(+g‘𝑀)𝑦)) = ((𝐻‘𝑥)(+g‘𝑁)(𝐻‘𝑦))) |
| 41 | 40 | ad4ant14 752 |
. . . 4
⊢ ((((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐻‘(𝑥(+g‘𝑀)𝑦)) = ((𝐻‘𝑥)(+g‘𝑁)(𝐻‘𝑦))) |
| 42 | 32 | ffnd 6737 |
. . . . . 6
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝑊 Fn (0...((♯‘𝑊) − 1))) |
| 43 | | fvco2 7006 |
. . . . . 6
⊢ ((𝑊 Fn (0...((♯‘𝑊) − 1)) ∧ 𝑥 ∈
(0...((♯‘𝑊)
− 1))) → ((𝐻
∘ 𝑊)‘𝑥) = (𝐻‘(𝑊‘𝑥))) |
| 44 | 42, 43 | sylan 580 |
. . . . 5
⊢ ((((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) ∧ 𝑥 ∈ (0...((♯‘𝑊) − 1))) → ((𝐻 ∘ 𝑊)‘𝑥) = (𝐻‘(𝑊‘𝑥))) |
| 45 | 44 | eqcomd 2743 |
. . . 4
⊢ ((((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) ∧ 𝑥 ∈ (0...((♯‘𝑊) − 1))) → (𝐻‘(𝑊‘𝑥)) = ((𝐻 ∘ 𝑊)‘𝑥)) |
| 46 | 20, 33, 37, 41, 45 | seqhomo 14090 |
. . 3
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐻‘(seq0((+g‘𝑀), 𝑊)‘((♯‘𝑊) − 1))) =
(seq0((+g‘𝑁), (𝐻 ∘ 𝑊))‘((♯‘𝑊) − 1))) |
| 47 | 16, 17, 15, 37, 32 | gsumval2 18699 |
. . . 4
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝑀 Σg 𝑊) =
(seq0((+g‘𝑀), 𝑊)‘((♯‘𝑊) − 1))) |
| 48 | 47 | fveq2d 6910 |
. . 3
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐻‘(𝑀 Σg 𝑊)) = (𝐻‘(seq0((+g‘𝑀), 𝑊)‘((♯‘𝑊) − 1)))) |
| 49 | | eqid 2737 |
. . . 4
⊢
(Base‘𝑁) =
(Base‘𝑁) |
| 50 | | mhmrcl2 18801 |
. . . . 5
⊢ (𝐻 ∈ (𝑀 MndHom 𝑁) → 𝑁 ∈ Mnd) |
| 51 | 50 | ad2antrr 726 |
. . . 4
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝑁 ∈ Mnd) |
| 52 | 16, 49 | mhmf 18802 |
. . . . . 6
⊢ (𝐻 ∈ (𝑀 MndHom 𝑁) → 𝐻:𝐵⟶(Base‘𝑁)) |
| 53 | 52 | ad2antrr 726 |
. . . . 5
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝐻:𝐵⟶(Base‘𝑁)) |
| 54 | | fco 6760 |
. . . . 5
⊢ ((𝐻:𝐵⟶(Base‘𝑁) ∧ 𝑊:(0...((♯‘𝑊) − 1))⟶𝐵) → (𝐻 ∘ 𝑊):(0...((♯‘𝑊) − 1))⟶(Base‘𝑁)) |
| 55 | 53, 32, 54 | syl2anc 584 |
. . . 4
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐻 ∘ 𝑊):(0...((♯‘𝑊) − 1))⟶(Base‘𝑁)) |
| 56 | 49, 38, 51, 37, 55 | gsumval2 18699 |
. . 3
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝑁 Σg (𝐻 ∘ 𝑊)) = (seq0((+g‘𝑁), (𝐻 ∘ 𝑊))‘((♯‘𝑊) − 1))) |
| 57 | 46, 48, 56 | 3eqtr4d 2787 |
. 2
⊢ (((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐻‘(𝑀 Σg 𝑊)) = (𝑁 Σg (𝐻 ∘ 𝑊))) |
| 58 | 2, 10 | mhm0 18807 |
. . 3
⊢ (𝐻 ∈ (𝑀 MndHom 𝑁) → (𝐻‘(0g‘𝑀)) = (0g‘𝑁)) |
| 59 | 58 | adantr 480 |
. 2
⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) → (𝐻‘(0g‘𝑀)) = (0g‘𝑁)) |
| 60 | 13, 57, 59 | pm2.61ne 3027 |
1
⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) → (𝐻‘(𝑀 Σg 𝑊)) = (𝑁 Σg (𝐻 ∘ 𝑊))) |