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 ⊢ 𝐵 = ( Base ‘ 𝑀 )
Assertion gsumwmhm ( ( 𝐻 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑊 ∈ Word 𝐵 ) → ( 𝐻 ‘ ( 𝑀 Σg 𝑊 ) ) = ( 𝑁 Σg ( 𝐻 ∘ 𝑊 ) ) )

Proof

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