Theorem gsumzmhm

Description: Apply a group homomorphism to a group sum. (Contributed by Mario Carneiro, 24-Apr-2016) (Revised by AV, 6-Jun-2019)

	Ref	Expression
Hypotheses	gsumzmhm.b	$$⊢B={\mathrm{Base}}_G$$
	gsumzmhm.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
	gsumzmhm.g	$$⊢\phi \to G\in \mathrm{Mnd}$$
	gsumzmhm.h	$$⊢\phi \to H\in \mathrm{Mnd}$$
	gsumzmhm.a	$$⊢\phi \to A\in V$$
	gsumzmhm.k	$$⊢\phi \to K\in \left(G\mathrm{MndHom}H\right)$$
	gsumzmhm.f	$$⊢\phi \to F:A⟶B$$
	gsumzmhm.c	$$⊢\phi \to \mathrm{ran}F\subseteq Z\left(\mathrm{ran}F\right)$$
	gsumzmhm.0	$$⊢\underset{\dot{}}{0}=0_G$$
	gsumzmhm.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
Assertion	gsumzmhm	$$⊢\phi \to {\sum }_H\left(K\circ F\right)=K\left({\sum }_{G}F\right)$$

Proof

Step	Hyp	Ref	Expression
1		gsumzmhm.b	$$⊢B={\mathrm{Base}}_G$$
2		gsumzmhm.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
3		gsumzmhm.g	$$⊢\phi \to G\in \mathrm{Mnd}$$
4		gsumzmhm.h	$$⊢\phi \to H\in \mathrm{Mnd}$$
5		gsumzmhm.a	$$⊢\phi \to A\in V$$
6		gsumzmhm.k	$$⊢\phi \to K\in \left(G\mathrm{MndHom}H\right)$$
7		gsumzmhm.f	$$⊢\phi \to F:A⟶B$$
8		gsumzmhm.c	$$⊢\phi \to \mathrm{ran}F\subseteq Z\left(\mathrm{ran}F\right)$$
9		gsumzmhm.0	$$⊢\underset{\dot{}}{0}=0_G$$
10		gsumzmhm.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
11		eqid	$$⊢0_H=0_H$$
12	11	gsumz	$$⊢\left(H\in \mathrm{Mnd}\wedge A\in V\right)\to \underset{k\in A}{{\sum }_H}{0}_H=0_H$$
13	4 5 12	syl2anc	$$⊢\phi \to \underset{k\in A}{{\sum }_H}{0}_H=0_H$$
14	13	adantr	$$⊢\left(\phi \wedge F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=\varnothing \right)\to \underset{k\in A}{{\sum }_H}{0}_H=0_H$$
15	9 11	mhm0	$$⊢K\in \left(G\mathrm{MndHom}H\right)\to K\left(\underset{\dot{}}{0}\right)=0_H$$
16	6 15	syl	$$⊢\phi \to K\left(\underset{\dot{}}{0}\right)=0_H$$
17	16	adantr	$$⊢\left(\phi \wedge F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=\varnothing \right)\to K\left(\underset{\dot{}}{0}\right)=0_H$$
18	14 17	eqtr4d	$$⊢\left(\phi \wedge F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=\varnothing \right)\to \underset{k\in A}{{\sum }_H}{0}_H=K\left(\underset{\dot{}}{0}\right)$$
19	1 9	mndidcl	$$⊢G\in \mathrm{Mnd}\to \underset{\dot{}}{0}\in B$$
20	3 19	syl	$$⊢\phi \to \underset{\dot{}}{0}\in B$$
21	20	ad2antrr	$$⊢\left(\left(\phi \wedge F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=\varnothing \right)\wedge k\in A\right)\to \underset{\dot{}}{0}\in B$$
22	9	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
23	22	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
24	7 5	fexd	$$⊢\phi \to F\in \mathrm{V}$$
25		suppimacnv	$$⊢\left(F\in \mathrm{V}\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)\to F\mathrm{supp}\underset{\dot{}}{0}=F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
26	24 23 25	syl2anc	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}=F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
27		ssid	$$⊢F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\subseteq F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
28	26 27	eqsstrdi	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\subseteq F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
29	7 5 23 28	gsumcllem	$$⊢\left(\phi \wedge F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=\varnothing \right)\to F=\left(k\in A⟼\underset{\dot{}}{0}\right)$$
30		eqid	$$⊢{\mathrm{Base}}_H={\mathrm{Base}}_H$$
31	1 30	mhmf	$$⊢K\in \left(G\mathrm{MndHom}H\right)\to K:B⟶{\mathrm{Base}}_H$$
32	6 31	syl	$$⊢\phi \to K:B⟶{\mathrm{Base}}_H$$
33	32	feqmptd	$$⊢\phi \to K=\left(x\in B⟼K\left(x\right)\right)$$
34	33	adantr	$$⊢\left(\phi \wedge F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=\varnothing \right)\to K=\left(x\in B⟼K\left(x\right)\right)$$
35		fveq2	$$⊢x=\underset{\dot{}}{0}\to K\left(x\right)=K\left(\underset{\dot{}}{0}\right)$$
36	21 29 34 35	fmptco	$$⊢\left(\phi \wedge F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=\varnothing \right)\to K\circ F=\left(k\in A⟼K\left(\underset{\dot{}}{0}\right)\right)$$
37	16	mpteq2dv	$$⊢\phi \to \left(k\in A⟼K\left(\underset{\dot{}}{0}\right)\right)=\left(k\in A⟼0_H\right)$$
38	37	adantr	$$⊢\left(\phi \wedge F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=\varnothing \right)\to \left(k\in A⟼K\left(\underset{\dot{}}{0}\right)\right)=\left(k\in A⟼0_H\right)$$
39	36 38	eqtrd	$$⊢\left(\phi \wedge F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=\varnothing \right)\to K\circ F=\left(k\in A⟼0_H\right)$$
40	39	oveq2d	$$⊢\left(\phi \wedge F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=\varnothing \right)\to {\sum }_H\left(K\circ F\right)=\underset{k\in A}{{\sum }_H}{0}_H$$
41	29	oveq2d	$$⊢\left(\phi \wedge F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=\varnothing \right)\to {\sum }_{G}F=\underset{k\in A}{{\sum }_G}\underset{\dot{}}{0}$$
42	9	gsumz	$$⊢\left(G\in \mathrm{Mnd}\wedge A\in V\right)\to \underset{k\in A}{{\sum }_G}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
43	3 5 42	syl2anc	$$⊢\phi \to \underset{k\in A}{{\sum }_G}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
44	43	adantr	$$⊢\left(\phi \wedge F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=\varnothing \right)\to \underset{k\in A}{{\sum }_G}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
45	41 44	eqtrd	$$⊢\left(\phi \wedge F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=\varnothing \right)\to {\sum }_{G}F=\underset{\dot{}}{0}$$
46	45	fveq2d	$$⊢\left(\phi \wedge F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=\varnothing \right)\to K\left({\sum }_{G}F\right)=K\left(\underset{\dot{}}{0}\right)$$
47	18 40 46	3eqtr4d	$$⊢\left(\phi \wedge F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=\varnothing \right)\to {\sum }_H\left(K\circ F\right)=K\left({\sum }_{G}F\right)$$
48	47	ex	$$⊢\phi \to \left(F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=\varnothing \to {\sum }_H\left(K\circ F\right)=K\left({\sum }_{G}F\right)\right)$$
49	3	adantr	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to G\in \mathrm{Mnd}$$
50		eqid	$$⊢{+}_G={+}_G$$
51	1 50	mndcl	$$⊢\left(G\in \mathrm{Mnd}\wedge x\in B\wedge y\in B\right)\to x{+}_{G}y\in B$$
52	51	3expb	$$⊢\left(G\in \mathrm{Mnd}\wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{G}y\in B$$
53	49 52	sylan	$$⊢\left(\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{G}y\in B$$
54		f1of1	$$⊢f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\to f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
55	54	ad2antll	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
56		cnvimass	$$⊢F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\subseteq \mathrm{dom}F$$
57	7	adantr	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to F:A⟶B$$
58	56 57	fssdm	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\subseteq A$$
59		f1ss	$$⊢\left(f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\wedge F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\subseteq A\right)\to f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1}{⟶}A$$
60	55 58 59	syl2anc	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1}{⟶}A$$
61		f1f	$$⊢f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1}{⟶}A\to f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)⟶A$$
62	60 61	syl	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)⟶A$$
63		fco	$$⊢\left(F:A⟶B\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)⟶A\right)\to \left(F\circ f\right):\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)⟶B$$
64	7 62 63	syl2an2r	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to \left(F\circ f\right):\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)⟶B$$
65	64	ffvelcdmda	$$⊢\left(\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\wedge x\in \left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\right)\to \left(F\circ f\right)\left(x\right)\in B$$
66		simprl	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}$$
67		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
68	66 67	eleqtrdi	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in {\mathbb{Z}}_{\ge 1}$$
69	6	adantr	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to K\in \left(G\mathrm{MndHom}H\right)$$
70		eqid	$$⊢{+}_H={+}_H$$
71	1 50 70	mhmlin	$$⊢\left(K\in \left(G\mathrm{MndHom}H\right)\wedge x\in B\wedge y\in B\right)\to K\left(x{+}_{G}y\right)=K\left(x\right){+}_{H}K\left(y\right)$$
72	71	3expb	$$⊢\left(K\in \left(G\mathrm{MndHom}H\right)\wedge \left(x\in B\wedge y\in B\right)\right)\to K\left(x{+}_{G}y\right)=K\left(x\right){+}_{H}K\left(y\right)$$
73	69 72	sylan	$$⊢\left(\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\wedge \left(x\in B\wedge y\in B\right)\right)\to K\left(x{+}_{G}y\right)=K\left(x\right){+}_{H}K\left(y\right)$$
74		coass	$$⊢\left(K\circ F\right)\circ f=K\circ \left(F\circ f\right)$$
75	74	fveq1i	$$⊢\left(\left(K\circ F\right)\circ f\right)\left(x\right)=\left(K\circ \left(F\circ f\right)\right)\left(x\right)$$
76		fvco3	$$⊢\left(\left(F\circ f\right):\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)⟶B\wedge x\in \left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\right)\to \left(K\circ \left(F\circ f\right)\right)\left(x\right)=K\left(\left(F\circ f\right)\left(x\right)\right)$$
77	64 76	sylan	$$⊢\left(\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\wedge x\in \left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\right)\to \left(K\circ \left(F\circ f\right)\right)\left(x\right)=K\left(\left(F\circ f\right)\left(x\right)\right)$$
78	75 77	eqtr2id	$$⊢\left(\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\wedge x\in \left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\right)\to K\left(\left(F\circ f\right)\left(x\right)\right)=\left(\left(K\circ F\right)\circ f\right)\left(x\right)$$
79	53 65 68 73 78	seqhomo	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to K\left(seq1\left({+}_G,\left(F\circ f\right)\right)\left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\right)=seq1\left({+}_H,\left(\left(K\circ F\right)\circ f\right)\right)\left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)$$
80	5	adantr	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to A\in V$$
81	8	adantr	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to \mathrm{ran}F\subseteq Z\left(\mathrm{ran}F\right)$$
82	28	adantr	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to F\mathrm{supp}\underset{\dot{}}{0}\subseteq F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
83		f1ofo	$$⊢f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\to f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
84		forn	$$⊢f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\to \mathrm{ran}f=F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
85	83 84	syl	$$⊢f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\to \mathrm{ran}f=F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
86	85	ad2antll	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to \mathrm{ran}f=F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
87	82 86	sseqtrrd	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to F\mathrm{supp}\underset{\dot{}}{0}\subseteq \mathrm{ran}f$$
88		eqid	$$⊢\left(F\circ f\right)\mathrm{supp}\underset{\dot{}}{0}=\left(F\circ f\right)\mathrm{supp}\underset{\dot{}}{0}$$
89	1 9 50 2 49 80 57 81 66 60 87 88	gsumval3	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to {\sum }_{G}F=seq1\left({+}_G,\left(F\circ f\right)\right)\left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)$$
90	89	fveq2d	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to K\left({\sum }_{G}F\right)=K\left(seq1\left({+}_G,\left(F\circ f\right)\right)\left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\right)$$
91		eqid	$$⊢\mathrm{Cntz}\left(H\right)=\mathrm{Cntz}\left(H\right)$$
92	4	adantr	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to H\in \mathrm{Mnd}$$
93		fco	$$⊢\left(K:B⟶{\mathrm{Base}}_H\wedge F:A⟶B\right)\to \left(K\circ F\right):A⟶{\mathrm{Base}}_H$$
94	32 57 93	syl2an2r	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to \left(K\circ F\right):A⟶{\mathrm{Base}}_H$$
95	2 91	cntzmhm2	$$⊢\left(K\in \left(G\mathrm{MndHom}H\right)\wedge \mathrm{ran}F\subseteq Z\left(\mathrm{ran}F\right)\right)\to K\left[\mathrm{ran}F\right]\subseteq \mathrm{Cntz}\left(H\right)\left(K\left[\mathrm{ran}F\right]\right)$$
96	6 81 95	syl2an2r	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to K\left[\mathrm{ran}F\right]\subseteq \mathrm{Cntz}\left(H\right)\left(K\left[\mathrm{ran}F\right]\right)$$
97		rnco2	$$⊢\mathrm{ran}\left(K\circ F\right)=K\left[\mathrm{ran}F\right]$$
98	97	fveq2i	$$⊢\mathrm{Cntz}\left(H\right)\left(\mathrm{ran}\left(K\circ F\right)\right)=\mathrm{Cntz}\left(H\right)\left(K\left[\mathrm{ran}F\right]\right)$$
99	96 97 98	3sstr4g	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to \mathrm{ran}\left(K\circ F\right)\subseteq \mathrm{Cntz}\left(H\right)\left(\mathrm{ran}\left(K\circ F\right)\right)$$
100		eldifi	$$⊢x\in \left(A\setminus F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\to x\in A$$
101		fvco3	$$⊢\left(F:A⟶B\wedge x\in A\right)\to \left(K\circ F\right)\left(x\right)=K\left(F\left(x\right)\right)$$
102	57 100 101	syl2an	$$⊢\left(\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\wedge x\in \left(A\setminus F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to \left(K\circ F\right)\left(x\right)=K\left(F\left(x\right)\right)$$
103	22	a1i	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to \underset{\dot{}}{0}\in \mathrm{V}$$
104	57 82 80 103	suppssr	$$⊢\left(\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\wedge x\in \left(A\setminus F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to F\left(x\right)=\underset{\dot{}}{0}$$
105	104	fveq2d	$$⊢\left(\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\wedge x\in \left(A\setminus F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to K\left(F\left(x\right)\right)=K\left(\underset{\dot{}}{0}\right)$$
106	16	ad2antrr	$$⊢\left(\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\wedge x\in \left(A\setminus F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to K\left(\underset{\dot{}}{0}\right)=0_H$$
107	102 105 106	3eqtrd	$$⊢\left(\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\wedge x\in \left(A\setminus F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to \left(K\circ F\right)\left(x\right)=0_H$$
108	94 107	suppss	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to \left(K\circ F\right)\mathrm{supp}{0}_H\subseteq F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
109	108 86	sseqtrrd	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to \left(K\circ F\right)\mathrm{supp}{0}_H\subseteq \mathrm{ran}f$$
110		eqid	$$⊢\left(\left(K\circ F\right)\circ f\right)\mathrm{supp}{0}_H=\left(\left(K\circ F\right)\circ f\right)\mathrm{supp}{0}_H$$
111	30 11 70 91 92 80 94 99 66 60 109 110	gsumval3	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to {\sum }_H\left(K\circ F\right)=seq1\left({+}_H,\left(\left(K\circ F\right)\circ f\right)\right)\left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)$$
112	79 90 111	3eqtr4rd	$$⊢\left(\phi \wedge \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)\to {\sum }_H\left(K\circ F\right)=K\left({\sum }_{G}F\right)$$
113	112	expr	$$⊢\left(\phi \wedge \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\right)\to \left(f:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\to {\sum }_H\left(K\circ F\right)=K\left({\sum }_{G}F\right)\right)$$
114	113	exlimdv	$$⊢\left(\phi \wedge \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\right)\to \left(\exists ff:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\to {\sum }_H\left(K\circ F\right)=K\left({\sum }_{G}F\right)\right)$$
115	114	expimpd	$$⊢\phi \to \left(\left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge \exists ff:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\to {\sum }_H\left(K\circ F\right)=K\left({\sum }_{G}F\right)\right)$$
116	10	fsuppimpd	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
117	26 116	eqeltrrd	$$⊢\phi \to F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\in \mathrm{Fin}$$
118		fz1f1o	$$⊢F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\in \mathrm{Fin}\to \left(F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=\varnothing \vee \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge \exists ff:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)$$
119	117 118	syl	$$⊢\phi \to \left(F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=\varnothing \vee \left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\in \mathbb{N}\wedge \exists ff:\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\underset{1-1\; onto}{⟶}{F}^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\right)$$
120	48 115 119	mpjaod	$$⊢\phi \to {\sum }_H\left(K\circ F\right)=K\left({\sum }_{G}F\right)$$