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 e. ( M MndHom N ) /\ W e. Word B ) -> ( H ` ( M gsum W ) ) = ( N gsum ( H o. W ) ) )

Proof

Step Hyp Ref Expression
1 gsumwmhm.b 
 |-  B = ( Base ` M )
2 oveq2 
 |-  ( W = (/) -> ( M gsum W ) = ( M gsum (/) ) )
3 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
4 3 gsum0 
 |-  ( M gsum (/) ) = ( 0g ` M )
5 2 4 eqtrdi 
 |-  ( W = (/) -> ( M gsum W ) = ( 0g ` M ) )
6 5 fveq2d 
 |-  ( W = (/) -> ( H ` ( M gsum W ) ) = ( H ` ( 0g ` M ) ) )
7 coeq2 
 |-  ( W = (/) -> ( H o. W ) = ( H o. (/) ) )
8 co02 
 |-  ( H o. (/) ) = (/)
9 7 8 eqtrdi 
 |-  ( W = (/) -> ( H o. W ) = (/) )
10 9 oveq2d 
 |-  ( W = (/) -> ( N gsum ( H o. W ) ) = ( N gsum (/) ) )
11 eqid 
 |-  ( 0g ` N ) = ( 0g ` N )
12 11 gsum0 
 |-  ( N gsum (/) ) = ( 0g ` N )
13 10 12 eqtrdi 
 |-  ( W = (/) -> ( N gsum ( H o. W ) ) = ( 0g ` N ) )
14 6 13 eqeq12d 
 |-  ( W = (/) -> ( ( H ` ( M gsum W ) ) = ( N gsum ( H o. W ) ) <-> ( H ` ( 0g ` M ) ) = ( 0g ` N ) ) )
15 mhmrcl1 
 |-  ( H e. ( M MndHom N ) -> M e. Mnd )
16 15 ad2antrr 
 |-  ( ( ( H e. ( M MndHom N ) /\ W e. Word B ) /\ W =/= (/) ) -> M e. Mnd )
17 eqid 
 |-  ( +g ` M ) = ( +g ` M )
18 1 17 mndcl 
 |-  ( ( M e. Mnd /\ x e. B /\ y e. B ) -> ( x ( +g ` M ) y ) e. B )
19 18 3expb 
 |-  ( ( M e. Mnd /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` M ) y ) e. B )
20 16 19 sylan 
 |-  ( ( ( ( H e. ( M MndHom N ) /\ W e. Word B ) /\ W =/= (/) ) /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` M ) y ) e. B )
21 wrdf 
 |-  ( W e. Word B -> W : ( 0 ..^ ( # ` W ) ) --> B )
22 21 ad2antlr 
 |-  ( ( ( H e. ( M MndHom N ) /\ W e. Word B ) /\ W =/= (/) ) -> W : ( 0 ..^ ( # ` W ) ) --> B )
23 wrdfin 
 |-  ( W e. Word B -> W e. Fin )
24 23 adantl 
 |-  ( ( H e. ( M MndHom N ) /\ W e. Word B ) -> W e. Fin )
25 hashnncl 
 |-  ( W e. Fin -> ( ( # ` W ) e. NN <-> W =/= (/) ) )
26 24 25 syl 
 |-  ( ( H e. ( M MndHom N ) /\ W e. Word B ) -> ( ( # ` W ) e. NN <-> W =/= (/) ) )
27 26 biimpar 
 |-  ( ( ( H e. ( M MndHom N ) /\ W e. Word B ) /\ W =/= (/) ) -> ( # ` W ) e. NN )
28 27 nnzd 
 |-  ( ( ( H e. ( M MndHom N ) /\ W e. Word B ) /\ W =/= (/) ) -> ( # ` W ) e. ZZ )
29 fzoval 
 |-  ( ( # ` W ) e. ZZ -> ( 0 ..^ ( # ` W ) ) = ( 0 ... ( ( # ` W ) - 1 ) ) )
30 28 29 syl 
 |-  ( ( ( H e. ( M MndHom N ) /\ W e. Word B ) /\ W =/= (/) ) -> ( 0 ..^ ( # ` W ) ) = ( 0 ... ( ( # ` W ) - 1 ) ) )
31 30 feq2d 
 |-  ( ( ( H e. ( M MndHom N ) /\ W e. Word B ) /\ W =/= (/) ) -> ( W : ( 0 ..^ ( # ` W ) ) --> B <-> W : ( 0 ... ( ( # ` W ) - 1 ) ) --> B ) )
32 22 31 mpbid 
 |-  ( ( ( H e. ( M MndHom N ) /\ W e. Word B ) /\ W =/= (/) ) -> W : ( 0 ... ( ( # ` W ) - 1 ) ) --> B )
33 32 ffvelrnda 
 |-  ( ( ( ( H e. ( M MndHom N ) /\ W e. Word B ) /\ W =/= (/) ) /\ x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) -> ( W ` x ) e. B )
34 nnm1nn0 
 |-  ( ( # ` W ) e. NN -> ( ( # ` W ) - 1 ) e. NN0 )
35 27 34 syl 
 |-  ( ( ( H e. ( M MndHom N ) /\ W e. Word B ) /\ W =/= (/) ) -> ( ( # ` W ) - 1 ) e. NN0 )
36 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
37 35 36 eleqtrdi 
 |-  ( ( ( H e. ( M MndHom N ) /\ W e. Word B ) /\ W =/= (/) ) -> ( ( # ` W ) - 1 ) e. ( ZZ>= ` 0 ) )
38 eqid 
 |-  ( +g ` N ) = ( +g ` N )
39 1 17 38 mhmlin 
 |-  ( ( H e. ( M MndHom N ) /\ x e. B /\ y e. B ) -> ( H ` ( x ( +g ` M ) y ) ) = ( ( H ` x ) ( +g ` N ) ( H ` y ) ) )
40 39 3expb 
 |-  ( ( H e. ( M MndHom N ) /\ ( x e. B /\ y e. B ) ) -> ( H ` ( x ( +g ` M ) y ) ) = ( ( H ` x ) ( +g ` N ) ( H ` y ) ) )
41 40 ad4ant14 
 |-  ( ( ( ( H e. ( M MndHom N ) /\ W e. Word B ) /\ W =/= (/) ) /\ ( x e. B /\ y e. B ) ) -> ( H ` ( x ( +g ` M ) y ) ) = ( ( H ` x ) ( +g ` N ) ( H ` y ) ) )
42 32 ffnd 
 |-  ( ( ( H e. ( M MndHom N ) /\ W e. Word B ) /\ W =/= (/) ) -> W Fn ( 0 ... ( ( # ` W ) - 1 ) ) )
43 fvco2 
 |-  ( ( W Fn ( 0 ... ( ( # ` W ) - 1 ) ) /\ x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) -> ( ( H o. W ) ` x ) = ( H ` ( W ` x ) ) )
44 42 43 sylan 
 |-  ( ( ( ( H e. ( M MndHom N ) /\ W e. Word B ) /\ W =/= (/) ) /\ x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) -> ( ( H o. W ) ` x ) = ( H ` ( W ` x ) ) )
45 44 eqcomd 
 |-  ( ( ( ( H e. ( M MndHom N ) /\ W e. Word B ) /\ W =/= (/) ) /\ x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) -> ( H ` ( W ` x ) ) = ( ( H o. W ) ` x ) )
46 20 33 37 41 45 seqhomo 
 |-  ( ( ( H e. ( M MndHom N ) /\ W e. Word B ) /\ W =/= (/) ) -> ( H ` ( seq 0 ( ( +g ` M ) , W ) ` ( ( # ` W ) - 1 ) ) ) = ( seq 0 ( ( +g ` N ) , ( H o. W ) ) ` ( ( # ` W ) - 1 ) ) )
47 1 17 16 37 32 gsumval2 
 |-  ( ( ( H e. ( M MndHom N ) /\ W e. Word B ) /\ W =/= (/) ) -> ( M gsum W ) = ( seq 0 ( ( +g ` M ) , W ) ` ( ( # ` W ) - 1 ) ) )
48 47 fveq2d 
 |-  ( ( ( H e. ( M MndHom N ) /\ W e. Word B ) /\ W =/= (/) ) -> ( H ` ( M gsum W ) ) = ( H ` ( seq 0 ( ( +g ` M ) , W ) ` ( ( # ` W ) - 1 ) ) ) )
49 eqid 
 |-  ( Base ` N ) = ( Base ` N )
50 mhmrcl2 
 |-  ( H e. ( M MndHom N ) -> N e. Mnd )
51 50 ad2antrr 
 |-  ( ( ( H e. ( M MndHom N ) /\ W e. Word B ) /\ W =/= (/) ) -> N e. Mnd )
52 1 49 mhmf 
 |-  ( H e. ( M MndHom N ) -> H : B --> ( Base ` N ) )
53 52 ad2antrr 
 |-  ( ( ( H e. ( M MndHom N ) /\ W e. Word B ) /\ W =/= (/) ) -> H : B --> ( Base ` N ) )
54 fco 
 |-  ( ( H : B --> ( Base ` N ) /\ W : ( 0 ... ( ( # ` W ) - 1 ) ) --> B ) -> ( H o. W ) : ( 0 ... ( ( # ` W ) - 1 ) ) --> ( Base ` N ) )
55 53 32 54 syl2anc 
 |-  ( ( ( H e. ( M MndHom N ) /\ W e. Word B ) /\ W =/= (/) ) -> ( H o. W ) : ( 0 ... ( ( # ` W ) - 1 ) ) --> ( Base ` N ) )
56 49 38 51 37 55 gsumval2 
 |-  ( ( ( H e. ( M MndHom N ) /\ W e. Word B ) /\ W =/= (/) ) -> ( N gsum ( H o. W ) ) = ( seq 0 ( ( +g ` N ) , ( H o. W ) ) ` ( ( # ` W ) - 1 ) ) )
57 46 48 56 3eqtr4d 
 |-  ( ( ( H e. ( M MndHom N ) /\ W e. Word B ) /\ W =/= (/) ) -> ( H ` ( M gsum W ) ) = ( N gsum ( H o. W ) ) )
58 3 11 mhm0 
 |-  ( H e. ( M MndHom N ) -> ( H ` ( 0g ` M ) ) = ( 0g ` N ) )
59 58 adantr 
 |-  ( ( H e. ( M MndHom N ) /\ W e. Word B ) -> ( H ` ( 0g ` M ) ) = ( 0g ` N ) )
60 14 57 59 pm2.61ne 
 |-  ( ( H e. ( M MndHom N ) /\ W e. Word B ) -> ( H ` ( M gsum W ) ) = ( N gsum ( H o. W ) ) )