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		fex	$$⊢\left(F:A⟶B\wedge A\in V\right)\to F\in \mathrm{V}$$
23	7 6 22	syl2anc	$$⊢\phi \to F\in \mathrm{V}$$
24		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]$$
25	23 19 24	sylancl	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}=F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
26	25	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)$$
27	21 26	mpbiri	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\subseteq F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
28	7 6 20 27	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)$$
29	28	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}$$
30	28	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}$$
31	18 29 30	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$$
32	31	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)$$
33		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}$$
34		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
35	33 34	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}$$
36	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$$
37		ffn	$$⊢F:A⟶B\to FFnA$$
38		dffn4	$$⊢FFnA\leftrightarrow F:A\underset{onto}{⟶}\mathrm{ran}F$$
39	37 38	sylib	$$⊢F:A⟶B\to F:A\underset{onto}{⟶}\mathrm{ran}F$$
40		fof	$$⊢F:A\underset{onto}{⟶}\mathrm{ran}F\to F:A⟶\mathrm{ran}F$$
41	36 39 40	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$$
42	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}$$
43	1	submacs	$$⊢G\in \mathrm{Mnd}\to \mathrm{SubMnd}\left(G\right)\in \mathrm{ACS}\left(B\right)$$
44		acsmre	$$⊢\mathrm{SubMnd}\left(G\right)\in \mathrm{ACS}\left(B\right)\to \mathrm{SubMnd}\left(G\right)\in \mathrm{Moore}\left(B\right)$$
45	42 43 44	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)$$
46		eqid	$$⊢\mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)=\mathrm{mrCls}\left(\mathrm{SubMnd}\left(G\right)\right)$$
47	36	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$$
48	45 46 47	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)$$
49	41 48	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)$$
50		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]$$
51	50	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]$$
52		cnvimass	$$⊢F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\subseteq \mathrm{dom}F$$
53	52 36	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$$
54		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$$
55	51 53 54	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$$
56		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$$
57	55 56	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$$
58		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)$$
59	49 57 58	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)$$
60	59	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)$$
61	46	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)$$
62	45 47 61	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)$$
63	4	oppgsubm	$$⊢\mathrm{SubMnd}\left(G\right)=\mathrm{SubMnd}\left(O\right)$$
64	62 63	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)$$
65		eqid	$$⊢{+}_O={+}_O$$
66	65	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)$$
67	66	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)$$
68	64 67	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)$$
69		eqid	$$⊢{+}_G={+}_G$$
70	69 4 65	oppgplus	$$⊢x{+}_{O}y=y{+}_{G}x$$
71	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)$$
72		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)$$
73	3 46 72	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}$$
74	42 71 73	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}$$
75	72 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)$$
76	62 75	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)$$
77	74 76	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)$$
78	77	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)$$
79	69 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$$
80	78 79	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$$
81	70 80	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$$
82	81	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$$
83	35 60 68 82	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)$$
84	4 1	oppgbas	$$⊢B={\mathrm{Base}}_O$$
85		eqid	$$⊢\mathrm{Cntz}\left(O\right)=\mathrm{Cntz}\left(O\right)$$
86	42 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}$$
87	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$$
88	4 3	oppgcntz	$$⊢Z\left(\mathrm{ran}F\right)=\mathrm{Cntz}\left(O\right)\left(\mathrm{ran}F\right)$$
89	71 88	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)$$
90		suppssdm	$$⊢F\mathrm{supp}\underset{\dot{}}{0}\subseteq \mathrm{dom}F$$
91	25 90	eqsstrrdi	$$⊢\phi \to F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\subseteq \mathrm{dom}F$$
92	7 91	fssdmd	$$⊢\phi \to F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\subseteq A$$
93	92	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$$
94	51 93 54	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$$
95	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 \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)$$
96	21 95	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]$$
97		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]$$
98		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]$$
99	97 98	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]$$
100	99	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)$$
101	100	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)$$
102	96 101	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$$
103		eqid	$$⊢\left(F\circ f\right)\mathrm{supp}\underset{\dot{}}{0}=\left(F\circ f\right)\mathrm{supp}\underset{\dot{}}{0}$$
104	84 12 65 85 86 87 36 89 33 94 102 103	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)$$
105	27	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]$$
106	105 101	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$$
107	1 2 69 3 42 87 36 71 33 94 106 103	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)$$
108	83 104 107	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$$
109	108	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)$$
110	109	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)$$
111	110	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)$$
112	9	fsuppimpd	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
113	25 112	eqeltrrd	$$⊢\phi \to F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\in \mathrm{Fin}$$
114		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)$$
115	113 114	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)$$
116	32 111 115	mpjaod	$$⊢\phi \to {\sum }_{O}F={\sum }_{G}F$$