Theorem gsumzoppg

Description: The opposite of a group sum is the same as the original. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 6-Jun-2019)

	Ref	Expression
Hypotheses	gsumzoppg.b	$$⊢B={\mathrm{Base}}_G$$
	gsumzoppg.0	$$⊢\underset{\dot{}}{0}=0_G$$
	gsumzoppg.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
	gsumzoppg.o	$$⊢O={opp}_{𝑔}\left(G\right)$$
	gsumzoppg.g	$$⊢\phi \to G\in \mathrm{Mnd}$$
	gsumzoppg.a	$$⊢\phi \to A\in V$$
	gsumzoppg.f	$$⊢\phi \to F:A⟶B$$
	gsumzoppg.c	$$⊢\phi \to \mathrm{ran}F\subseteq Z\left(\mathrm{ran}F\right)$$
	gsumzoppg.n	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
Assertion	gsumzoppg	$$⊢\phi \to {\sum }_{O}F={\sum }_{G}F$$

Proof

Step	Hyp	Ref	Expression
1		gsumzoppg.b	$$⊢B={\mathrm{Base}}_G$$
2		gsumzoppg.0	$$⊢\underset{\dot{}}{0}=0_G$$
3		gsumzoppg.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
4		gsumzoppg.o	$$⊢O={opp}_{𝑔}\left(G\right)$$
5		gsumzoppg.g	$$⊢\phi \to G\in \mathrm{Mnd}$$
6		gsumzoppg.a	$$⊢\phi \to A\in V$$
7		gsumzoppg.f	$$⊢\phi \to F:A⟶B$$
8		gsumzoppg.c	$$⊢\phi \to \mathrm{ran}F\subseteq Z\left(\mathrm{ran}F\right)$$
9		gsumzoppg.n	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
10	4	oppgmnd	$$⊢G\in \mathrm{Mnd}\to O\in \mathrm{Mnd}$$
11	5 10	syl	$$⊢\phi \to O\in \mathrm{Mnd}$$
12	4 2	oppgid	$$⊢\underset{\dot{}}{0}=0_O$$
13	12	gsumz	$$⊢\left(O\in \mathrm{Mnd}\wedge A\in V\right)\to \underset{k\in A}{{\sum }_O}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
14	11 6 13	syl2anc	$$⊢\phi \to \underset{k\in A}{{\sum }_O}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
15	2	gsumz	$$⊢\left(G\in \mathrm{Mnd}\wedge A\in V\right)\to \underset{k\in A}{{\sum }_G}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
16	5 6 15	syl2anc	$$⊢\phi \to \underset{k\in A}{{\sum }_G}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
17	14 16	eqtr4d	$$⊢\phi \to \underset{k\in A}{{\sum }_O}\underset{\dot{}}{0}=\underset{k\in A}{{\sum }_G}\underset{\dot{}}{0}$$
18	17	adantr	$$⊢\left(\phi \wedge F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=\varnothing \right)\to \underset{k\in A}{{\sum }_O}\underset{\dot{}}{0}=\underset{k\in A}{{\sum }_G}\underset{\dot{}}{0}$$
19	2	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
20	19	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
21		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]$$
22	7 6	fexd	$$⊢\phi \to F\in \mathrm{V}$$
23		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]$$
24	22 19 23	sylancl	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}=F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
25	24	sseq1d	$$⊢\phi \to \left(F\mathrm{supp}\underset{\dot{}}{0}\subseteq F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\leftrightarrow 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]\right)$$
26	21 25	mpbiri	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\subseteq F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
27	7 6 20 26	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)$$
28	27	oveq2d	$$⊢\left(\phi \wedge F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=\varnothing \right)\to {\sum }_{O}F=\underset{k\in A}{{\sum }_O}\underset{\dot{}}{0}$$
29	27	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}$$
30	18 28 29	3eqtr4d	$$⊢\left(\phi \wedge F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=\varnothing \right)\to {\sum }_{O}F={\sum }_{G}F$$
31	30	ex	$$⊢\phi \to \left(F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=\varnothing \to {\sum }_{O}F={\sum }_{G}F\right)$$
32		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}$$
33		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
34	32 33	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}$$
35	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$$
36		ffn	$$⊢F:A⟶B\to FFnA$$
37		dffn4	$$⊢FFnA\leftrightarrow F:A\underset{onto}{⟶}\mathrm{ran}F$$
38	36 37	sylib	$$⊢F:A⟶B\to F:A\underset{onto}{⟶}\mathrm{ran}F$$
39		fof	$$⊢F:A\underset{onto}{⟶}\mathrm{ran}F\to F:A⟶\mathrm{ran}F$$
40	35 38 39	3syl	$$⊢\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⟶\mathrm{ran}F$$
41	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 G\in \mathrm{Mnd}$$
42	1	submacs	$$⊢G\in \mathrm{Mnd}\to \mathrm{SubMnd}\left(G\right)\in \mathrm{ACS}\left(B\right)$$
43		acsmre	$$⊢\mathrm{SubMnd}\left(G\right)\in \mathrm{ACS}\left(B\right)\to \mathrm{SubMnd}\left(G\right)\in \mathrm{Moore}\left(B\right)$$
44	41 42 43	3syl	$$⊢\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{SubMnd}\left(G\right)\in \mathrm{Moore}\left(B\right)$$
45		eqid	$$⊢\mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)=\mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)$$
46	35	frnd	$$⊢\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 B$$
47	44 45 46	mrcssidd	$$⊢\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 \mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)$$
48	40 47	fssd	$$⊢\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⟶\mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)$$
49		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]$$
50	49	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]$$
51		cnvimass	$$⊢F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\subseteq \mathrm{dom}F$$
52	51 35	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$$
53		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$$
54	50 52 53	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$$
55		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$$
56	54 55	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$$
57		fco	$$⊢\left(F:A⟶\mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\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)⟶\mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)$$
58	48 56 57	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 \left(F\circ f\right):\left(1\dots \left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)⟶\mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)$$
59	58	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 \mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)$$
60	45	mrccl	$$⊢\left(\mathrm{SubMnd}\left(G\right)\in \mathrm{Moore}\left(B\right)\wedge \mathrm{ran}F\subseteq B\right)\to \mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\in \mathrm{SubMnd}\left(G\right)$$
61	44 46 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 \mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\in \mathrm{SubMnd}\left(G\right)$$
62	4	oppgsubm	$$⊢\mathrm{SubMnd}\left(G\right)=\mathrm{SubMnd}\left(O\right)$$
63	61 62	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 \mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\in \mathrm{SubMnd}\left(O\right)$$
64		eqid	$$⊢{+}_O={+}_O$$
65	64	submcl	$$⊢\left(\mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\in \mathrm{SubMnd}\left(O\right)\wedge x\in \mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\wedge y\in \mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\right)\to x{+}_{O}y\in \mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)$$
66	65	3expb	$$⊢\left(\mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\in \mathrm{SubMnd}\left(O\right)\wedge \left(x\in \mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\wedge y\in \mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\right)\right)\to x{+}_{O}y\in \mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)$$
67	63 66	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 \mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\wedge y\in \mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\right)\right)\to x{+}_{O}y\in \mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)$$
68		eqid	$$⊢{+}_G={+}_G$$
69	68 4 64	oppgplus	$$⊢x{+}_{O}y=y{+}_{G}x$$
70	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)$$
71		eqid	$$⊢G{\upharpoonright }_{𝑠}\mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)=G{\upharpoonright }_{𝑠}\mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)$$
72	3 45 71	cntzspan	$$⊢\left(G\in \mathrm{Mnd}\wedge \mathrm{ran}F\subseteq Z\left(\mathrm{ran}F\right)\right)\to G{\upharpoonright }_{𝑠}\mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\in \mathrm{CMnd}$$
73	41 70 72	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 G{\upharpoonright }_{𝑠}\mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\in \mathrm{CMnd}$$
74	71 3	submcmn2	$$⊢\mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\in \mathrm{SubMnd}\left(G\right)\to \left(G{\upharpoonright }_{𝑠}\mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\in \mathrm{CMnd}\leftrightarrow \mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\subseteq Z\left(\mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\right)\right)$$
75	61 74	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 \left(G{\upharpoonright }_{𝑠}\mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\in \mathrm{CMnd}\leftrightarrow \mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\subseteq Z\left(\mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\right)\right)$$
76	73 75	mpbid	$$⊢\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{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\subseteq Z\left(\mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\right)$$
77	76	sselda	$$⊢\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 \mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\right)\to x\in Z\left(\mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\right)$$
78	68 3	cntzi	$$⊢\left(x\in Z\left(\mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\right)\wedge y\in \mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\right)\to x{+}_{G}y=y{+}_{G}x$$
79	77 78	sylan	$$⊢\left(\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 \mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\right)\wedge y\in \mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\right)\to x{+}_{G}y=y{+}_{G}x$$
80	69 79	eqtr4id	$$⊢\left(\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 \mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\right)\wedge y\in \mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\right)\to x{+}_{O}y=x{+}_{G}y$$
81	80	anasss	$$⊢\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 \mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\wedge y\in \mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)\left(\mathrm{ran}F\right)\right)\right)\to x{+}_{O}y=x{+}_{G}y$$
82	34 59 67 81	seqfeq4	$$⊢\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 seq1\left({+}_O,\left(F\circ f\right)\right)\left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)=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)$$
83	4 1	oppgbas	$$⊢B={\mathrm{Base}}_O$$
84		eqid	$$⊢\mathrm{Cntz}\left(O\right)=\mathrm{Cntz}\left(O\right)$$
85	41 10	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 O\in \mathrm{Mnd}$$
86	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 A\in V$$
87	4 3	oppgcntz	$$⊢Z\left(\mathrm{ran}F\right)=\mathrm{Cntz}\left(O\right)\left(\mathrm{ran}F\right)$$
88	70 87	sseqtrdi	$$⊢\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 \mathrm{Cntz}\left(O\right)\left(\mathrm{ran}F\right)$$
89		suppssdm	$$⊢F\mathrm{supp}\underset{\dot{}}{0}\subseteq \mathrm{dom}F$$
90	24 89	eqsstrrdi	$$⊢\phi \to F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\subseteq \mathrm{dom}F$$
91	7 90	fssdmd	$$⊢\phi \to F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\subseteq A$$
92	91	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^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\subseteq A$$
93	50 92 53	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$$
94	25	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 \left(F\mathrm{supp}\underset{\dot{}}{0}\subseteq F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\leftrightarrow 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]\right)$$
95	21 94	mpbiri	$$⊢\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]$$
96		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]$$
97		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]$$
98	96 97	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]$$
99	98	sseq2d	$$⊢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 \left(F\mathrm{supp}\underset{\dot{}}{0}\subseteq \mathrm{ran}f\leftrightarrow F\mathrm{supp}\underset{\dot{}}{0}\subseteq F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)$$
100	99	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 \left(F\mathrm{supp}\underset{\dot{}}{0}\subseteq \mathrm{ran}f\leftrightarrow F\mathrm{supp}\underset{\dot{}}{0}\subseteq F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right)$$
101	95 100	mpbird	$$⊢\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$$
102		eqid	$$⊢\left(F\circ f\right)\mathrm{supp}\underset{\dot{}}{0}=\left(F\circ f\right)\mathrm{supp}\underset{\dot{}}{0}$$
103	83 12 64 84 85 86 35 88 32 93 101 102	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 }_{O}F=seq1\left({+}_O,\left(F\circ f\right)\right)\left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)$$
104	26	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]$$
105	104 100	mpbird	$$⊢\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$$
106	1 2 68 3 41 86 35 70 32 93 105 102	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)$$
107	82 103 106	3eqtr4d	$$⊢\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 }_{O}F={\sum }_{G}F$$
108	107	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 }_{O}F={\sum }_{G}F\right)$$
109	108	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 }_{O}F={\sum }_{G}F\right)$$
110	109	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 }_{O}F={\sum }_{G}F\right)$$
111	9	fsuppimpd	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
112	24 111	eqeltrrd	$$⊢\phi \to F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\in \mathrm{Fin}$$
113		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)$$
114	112 113	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)$$
115	31 110 114	mpjaod	$$⊢\phi \to {\sum }_{O}F={\sum }_{G}F$$