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 ffvelrnda ( ( ( ( 𝐻 ∈ ( 𝑀 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 ( 𝐻𝑊 ) ) )