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		fex	$$⊢\left(F:A⟶B\wedge A\in V\right)\to F\in \mathrm{V}$$
25	7 5 24	syl2anc	$$⊢\phi \to F\in \mathrm{V}$$
26		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]$$
27	25 23 26	syl2anc	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}=F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
28		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]$$
29	27 28	eqsstrdi	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\subseteq F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
30	7 5 23 29	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)$$
31		eqid	$$⊢{\mathrm{Base}}_H={\mathrm{Base}}_H$$
32	1 31	mhmf	$$⊢K\in \left(G\mathrm{MndHom}H\right)\to K:B⟶{\mathrm{Base}}_H$$
33	6 32	syl	$$⊢\phi \to K:B⟶{\mathrm{Base}}_H$$
34	33	feqmptd	$$⊢\phi \to K=\left(x\in B⟼K\left(x\right)\right)$$
35	34	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)$$
36		fveq2	$$⊢x=\underset{\dot{}}{0}\to K\left(x\right)=K\left(\underset{\dot{}}{0}\right)$$
37	21 30 35 36	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)$$
38	16	mpteq2dv	$$⊢\phi \to \left(k\in A⟼K\left(\underset{\dot{}}{0}\right)\right)=\left(k\in A⟼0_H\right)$$
39	38	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)$$
40	37 39	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)$$
41	40	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$$
42	30	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}$$
43	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}$$
44	3 5 43	syl2anc	$$⊢\phi \to \underset{k\in A}{{\sum }_G}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
45	44	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}$$
46	42 45	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}$$
47	46	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)$$
48	18 41 47	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)$$
49	48	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)$$
50	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}$$
51		eqid	$$⊢{+}_G={+}_G$$
52	1 51	mndcl	$$⊢\left(G\in \mathrm{Mnd}\wedge x\in B\wedge y\in B\right)\to x{+}_{G}y\in B$$
53	52	3expb	$$⊢\left(G\in \mathrm{Mnd}\wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{G}y\in B$$
54	50 53	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$$
55		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]$$
56	55	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]$$
57		cnvimass	$$⊢F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\subseteq \mathrm{dom}F$$
58	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$$
59	57 58	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$$
60		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$$
61	56 59 60	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$$
62		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$$
63	61 62	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$$
64		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$$
65	7 63 64	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$$
66	65	ffvelrnda	$$⊢\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$$
67		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}$$
68		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
69	67 68	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}$$
70	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)$$
71		eqid	$$⊢{+}_H={+}_H$$
72	1 51 71	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)$$
73	72	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)$$
74	70 73	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)$$
75		coass	$$⊢\left(K\circ F\right)\circ f=K\circ \left(F\circ f\right)$$
76	75	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)$$
77		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)$$
78	65 77	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)$$
79	76 78	syl5req	$$⊢\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)$$
80	54 66 69 74 79	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)$$
81	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$$
82	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)$$
83	29	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]$$
84		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]$$
85		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]$$
86	84 85	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]$$
87	86	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]$$
88	83 87	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$$
89		eqid	$$⊢\left(F\circ f\right)\mathrm{supp}\underset{\dot{}}{0}=\left(F\circ f\right)\mathrm{supp}\underset{\dot{}}{0}$$
90	1 9 51 2 50 81 58 82 67 61 88 89	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)$$
91	90	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)$$
92		eqid	$$⊢\mathrm{Cntz}\left(H\right)=\mathrm{Cntz}\left(H\right)$$
93	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}$$
94		fco	$$⊢\left(K:B⟶{\mathrm{Base}}_H\wedge F:A⟶B\right)\to \left(K\circ F\right):A⟶{\mathrm{Base}}_H$$
95	33 58 94	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$$
96	2 92	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)$$
97	6 82 96	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)$$
98		rnco2	$$⊢\mathrm{ran}\left(K\circ F\right)=K\left[\mathrm{ran}F\right]$$
99	98	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)$$
100	97 98 99	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)$$
101		eldifi	$$⊢x\in \left(A\setminus F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)\to x\in A$$
102		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)$$
103	58 101 102	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)$$
104	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}$$
105	58 83 81 104	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}$$
106	105	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)$$
107	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$$
108	103 106 107	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$$
109	95 108	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]$$
110	109 87	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$$
111		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$$
112	31 11 71 92 93 81 95 100 67 61 110 111	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)$$
113	80 91 112	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)$$
114	113	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)$$
115	114	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)$$
116	115	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)$$
117	10	fsuppimpd	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
118	27 117	eqeltrrd	$$⊢\phi \to F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\in \mathrm{Fin}$$
119		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)$$
120	118 119	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)$$
121	49 116 120	mpjaod	$$⊢\phi \to {\sum }_H\left(K\circ F\right)=K\left({\sum }_{G}F\right)$$