Metamath Proof Explorer

Theorem gsumwmhm

Description: Behavior of homomorphisms on finite monoidal sums. (Contributed by Stefan O'Rear, 27-Aug-2015)

Ref Expression
Hypothesis gsumwmhm.b ⊢ B = Base M
Assertion gsumwmhm ⊢ H ∈ M MndHom N ∧ W ∈ Word B → H ⁡ ∑ M W = ∑ N H ∘ W

Proof

Step Hyp Ref Expression
1 gsumwmhm.b ⊢ B = Base M
2 oveq2 ⊢ W = ∅ → ∑ M W = ∑ M ∅
3 eqid ⊢ 0 M = 0 M
4 3 gsum0 ⊢ ∑ M ∅ = 0 M
5 2 4 eqtrdi ⊢ W = ∅ → ∑ M W = 0 M
6 5 fveq2d ⊢ W = ∅ → H ⁡ ∑ M W = H ⁡ 0 M
7 coeq2 ⊢ W = ∅ → H ∘ W = H ∘ ∅
8 co02 ⊢ H ∘ ∅ = ∅
9 7 8 eqtrdi ⊢ W = ∅ → H ∘ W = ∅
10 9 oveq2d ⊢ W = ∅ → ∑ N H ∘ W = ∑ N ∅
11 eqid ⊢ 0 N = 0 N
12 11 gsum0 ⊢ ∑ N ∅ = 0 N
13 10 12 eqtrdi ⊢ W = ∅ → ∑ N H ∘ W = 0 N
14 6 13 eqeq12d ⊢ W = ∅ → H ⁡ ∑ M W = ∑ N H ∘ W ↔ H ⁡ 0 M = 0 N
15 mhmrcl1 ⊢ H ∈ M MndHom N → M ∈ Mnd
16 15 ad2antrr ⊢ H ∈ M MndHom N ∧ W ∈ Word B ∧ W ≠ ∅ → M ∈ Mnd
17 eqid ⊢ + M = + M
18 1 17 mndcl ⊢ M ∈ Mnd ∧ x ∈ B ∧ y ∈ B → x + M y ∈ B
19 18 3expb ⊢ M ∈ Mnd ∧ x ∈ B ∧ y ∈ B → x + M y ∈ B
20 16 19 sylan ⊢ H ∈ M MndHom N ∧ W ∈ Word B ∧ W ≠ ∅ ∧ x ∈ B ∧ y ∈ B → x + M y ∈ B
21 wrdf ⊢ W ∈ Word B → W : 0 ..^ W ⟶ B
22 21 ad2antlr ⊢ H ∈ M MndHom N ∧ W ∈ Word B ∧ W ≠ ∅ → W : 0 ..^ W ⟶ B
23 wrdfin ⊢ W ∈ Word B → W ∈ Fin
24 23 adantl ⊢ H ∈ M MndHom N ∧ W ∈ Word B → W ∈ Fin
25 hashnncl ⊢ W ∈ Fin → W ∈ ℕ ↔ W ≠ ∅
26 24 25 syl ⊢ H ∈ M MndHom N ∧ W ∈ Word B → W ∈ ℕ ↔ W ≠ ∅
27 26 biimpar ⊢ H ∈ M MndHom N ∧ W ∈ Word B ∧ W ≠ ∅ → W ∈ ℕ
28 27 nnzd ⊢ H ∈ M MndHom N ∧ W ∈ Word B ∧ W ≠ ∅ → W ∈ ℤ
29 fzoval ⊢ W ∈ ℤ → 0 ..^ W = 0 … W − 1
30 28 29 syl ⊢ H ∈ M MndHom N ∧ W ∈ Word B ∧ W ≠ ∅ → 0 ..^ W = 0 … W − 1
31 30 feq2d ⊢ H ∈ M MndHom N ∧ W ∈ Word B ∧ W ≠ ∅ → W : 0 ..^ W ⟶ B ↔ W : 0 … W − 1 ⟶ B
32 22 31 mpbid ⊢ H ∈ M MndHom N ∧ W ∈ Word B ∧ W ≠ ∅ → W : 0 … W − 1 ⟶ B
33 32 ffvelcdmda ⊢ H ∈ M MndHom N ∧ W ∈ Word B ∧ W ≠ ∅ ∧ x ∈ 0 … W − 1 → W ⁡ x ∈ B
34 nnm1nn0 ⊢ W ∈ ℕ → W − 1 ∈ ℕ 0
35 27 34 syl ⊢ H ∈ M MndHom N ∧ W ∈ Word B ∧ W ≠ ∅ → W − 1 ∈ ℕ 0
36 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
37 35 36 eleqtrdi ⊢ H ∈ M MndHom N ∧ W ∈ Word B ∧ W ≠ ∅ → W − 1 ∈ ℤ ≥ 0
38 eqid ⊢ + N = + N
39 1 17 38 mhmlin ⊢ H ∈ M MndHom N ∧ x ∈ B ∧ y ∈ B → H ⁡ x + M y = H ⁡ x + N H ⁡ y
40 39 3expb ⊢ H ∈ M MndHom N ∧ x ∈ B ∧ y ∈ B → H ⁡ x + M y = H ⁡ x + N H ⁡ y
41 40 ad4ant14 ⊢ H ∈ M MndHom N ∧ W ∈ Word B ∧ W ≠ ∅ ∧ x ∈ B ∧ y ∈ B → H ⁡ x + M y = H ⁡ x + N H ⁡ y
42 32 ffnd ⊢ H ∈ M MndHom N ∧ W ∈ Word B ∧ W ≠ ∅ → W Fn 0 … W − 1
43 fvco2 ⊢ W Fn 0 … W − 1 ∧ x ∈ 0 … W − 1 → H ∘ W ⁡ x = H ⁡ W ⁡ x
44 42 43 sylan ⊢ H ∈ M MndHom N ∧ W ∈ Word B ∧ W ≠ ∅ ∧ x ∈ 0 … W − 1 → H ∘ W ⁡ x = H ⁡ W ⁡ x
45 44 eqcomd ⊢ H ∈ M MndHom N ∧ W ∈ Word B ∧ W ≠ ∅ ∧ x ∈ 0 … W − 1 → H ⁡ W ⁡ x = H ∘ W ⁡ x
46 20 33 37 41 45 seqhomo ⊢ H ∈ M MndHom N ∧ W ∈ Word B ∧ W ≠ ∅ → H ⁡ seq 0 + M W ⁡ W − 1 = seq 0 + N H ∘ W ⁡ W − 1
47 1 17 16 37 32 gsumval2 ⊢ H ∈ M MndHom N ∧ W ∈ Word B ∧ W ≠ ∅ → ∑ M W = seq 0 + M W ⁡ W − 1
48 47 fveq2d ⊢ H ∈ M MndHom N ∧ W ∈ Word B ∧ W ≠ ∅ → H ⁡ ∑ M W = H ⁡ seq 0 + M W ⁡ W − 1
49 eqid ⊢ Base N = Base N
50 mhmrcl2 ⊢ H ∈ M MndHom N → N ∈ Mnd
51 50 ad2antrr ⊢ H ∈ M MndHom N ∧ W ∈ Word B ∧ W ≠ ∅ → N ∈ Mnd
52 1 49 mhmf ⊢ H ∈ M MndHom N → H : B ⟶ Base N
53 52 ad2antrr ⊢ H ∈ M MndHom N ∧ W ∈ Word B ∧ W ≠ ∅ → H : B ⟶ Base N
54 fco ⊢ H : B ⟶ Base N ∧ W : 0 … W − 1 ⟶ B → H ∘ W : 0 … W − 1 ⟶ Base N
55 53 32 54 syl2anc ⊢ H ∈ M MndHom N ∧ W ∈ Word B ∧ W ≠ ∅ → H ∘ W : 0 … W − 1 ⟶ Base N
56 49 38 51 37 55 gsumval2 ⊢ H ∈ M MndHom N ∧ W ∈ Word B ∧ W ≠ ∅ → ∑ N H ∘ W = seq 0 + N H ∘ W ⁡ W − 1
57 46 48 56 3eqtr4d ⊢ H ∈ M MndHom N ∧ W ∈ Word B ∧ W ≠ ∅ → H ⁡ ∑ M W = ∑ N H ∘ W
58 3 11 mhm0 ⊢ H ∈ M MndHom N → H ⁡ 0 M = 0 N
59 58 adantr ⊢ H ∈ M MndHom N ∧ W ∈ Word B → H ⁡ 0 M = 0 N
60 14 57 59 pm2.61ne ⊢ H ∈ M MndHom N ∧ W ∈ Word B → H ⁡ ∑ M W = ∑ N H ∘ W