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 \in (M MndHom N) \land W \in Word B) \to H (\sum_{M} W) = \sum_{N} (H \circ W)$

Proof

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

Metamath Proof Explorer

Theorem gsumwmhm

Proof