Theorem gsumress

Description: The group sum in a substructure is the same as the group sum in the original structure. The only requirement on the substructure is that it contain the identity element; neither G nor H need be groups. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Hypotheses	gsumress.b	$$⊢B={\mathrm{Base}}_G$$
	gsumress.o	$$⊢\underset{\dot{}}{+}={+}_G$$
	gsumress.h	$$⊢H=G{\upharpoonright }_{𝑠}S$$
	gsumress.g	$$⊢\phi \to G\in V$$
	gsumress.a	$$⊢\phi \to A\in X$$
	gsumress.s	$$⊢\phi \to S\subseteq B$$
	gsumress.f	$$⊢\phi \to F:A⟶S$$
	gsumress.z	$$⊢\phi \to \underset{\dot{}}{0}\in S$$
	gsumress.c	$$⊢\left(\phi \wedge x\in B\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)$$
Assertion	gsumress	$$⊢\phi \to {\sum }_{G}F={\sum }_{H}F$$

Proof

Step	Hyp	Ref	Expression
1		gsumress.b	$$⊢B={\mathrm{Base}}_G$$
2		gsumress.o	$$⊢\underset{\dot{}}{+}={+}_G$$
3		gsumress.h	$$⊢H=G{\upharpoonright }_{𝑠}S$$
4		gsumress.g	$$⊢\phi \to G\in V$$
5		gsumress.a	$$⊢\phi \to A\in X$$
6		gsumress.s	$$⊢\phi \to S\subseteq B$$
7		gsumress.f	$$⊢\phi \to F:A⟶S$$
8		gsumress.z	$$⊢\phi \to \underset{\dot{}}{0}\in S$$
9		gsumress.c	$$⊢\left(\phi \wedge x\in B\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)$$
10		oveq1	$$⊢y=\underset{\dot{}}{0}\to y\underset{\dot{}}{+}x=\underset{\dot{}}{0}\underset{\dot{}}{+}x$$
11	10	eqeq1d	$$⊢y=\underset{\dot{}}{0}\to \left(y\underset{\dot{}}{+}x=x\leftrightarrow \underset{\dot{}}{0}\underset{\dot{}}{+}x=x\right)$$
12	11	ovanraleqv	$$⊢y=\underset{\dot{}}{0}\to \left(\forall x\in B\left(y\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}y=x\right)\leftrightarrow \forall x\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\right)$$
13	6 8	sseldd	$$⊢\phi \to \underset{\dot{}}{0}\in B$$
14	9	ralrimiva	$$⊢\phi \to \forall x\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)$$
15	12 13 14	elrabd	$$⊢\phi \to \underset{\dot{}}{0}\in \left\{y\in B|\forall x\in B\left(y\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}y=x\right)\right\}$$
16	15	snssd	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}\subseteq \left\{y\in B|\forall x\in B\left(y\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}y=x\right)\right\}$$
17		eqid	$$⊢0_G=0_G$$
18		eqid	$$⊢\left\{y\in B|\forall x\in B\left(y\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}y=x\right)\right\}=\left\{y\in B|\forall x\in B\left(y\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}y=x\right)\right\}$$
19	1 17 2 18	mgmidsssn0	$$⊢G\in V\to \left\{y\in B|\forall x\in B\left(y\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}y=x\right)\right\}\subseteq \left\{0_G\right\}$$
20	4 19	syl	$$⊢\phi \to \left\{y\in B|\forall x\in B\left(y\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}y=x\right)\right\}\subseteq \left\{0_G\right\}$$
21	20 15	sseldd	$$⊢\phi \to \underset{\dot{}}{0}\in \left\{0_G\right\}$$
22		elsni	$$⊢\underset{\dot{}}{0}\in \left\{0_G\right\}\to \underset{\dot{}}{0}=0_G$$
23	21 22	syl	$$⊢\phi \to \underset{\dot{}}{0}=0_G$$
24	23	sneqd	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}=\left\{0_G\right\}$$
25	20 24	sseqtrrd	$$⊢\phi \to \left\{y\in B|\forall x\in B\left(y\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}y=x\right)\right\}\subseteq \left\{\underset{\dot{}}{0}\right\}$$
26	16 25	eqssd	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}=\left\{y\in B|\forall x\in B\left(y\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}y=x\right)\right\}$$
27	11	ovanraleqv	$$⊢y=\underset{\dot{}}{0}\to \left(\forall x\in S\left(y\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}y=x\right)\leftrightarrow \forall x\in S\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\right)$$
28	6	sselda	$$⊢\left(\phi \wedge x\in S\right)\to x\in B$$
29	28 9	syldan	$$⊢\left(\phi \wedge x\in S\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)$$
30	29	ralrimiva	$$⊢\phi \to \forall x\in S\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)$$
31	27 8 30	elrabd	$$⊢\phi \to \underset{\dot{}}{0}\in \left\{y\in S|\forall x\in S\left(y\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}y=x\right)\right\}$$
32	3 1	ressbas2	$$⊢S\subseteq B\to S={\mathrm{Base}}_H$$
33	6 32	syl	$$⊢\phi \to S={\mathrm{Base}}_H$$
34		fvex	$$⊢{\mathrm{Base}}_H\in \mathrm{V}$$
35	33 34	eqeltrdi	$$⊢\phi \to S\in \mathrm{V}$$
36	3 2	ressplusg	$$⊢S\in \mathrm{V}\to \underset{\dot{}}{+}={+}_H$$
37	35 36	syl	$$⊢\phi \to \underset{\dot{}}{+}={+}_H$$
38	37	oveqd	$$⊢\phi \to y\underset{\dot{}}{+}x=y{+}_{H}x$$
39	38	eqeq1d	$$⊢\phi \to \left(y\underset{\dot{}}{+}x=x\leftrightarrow y{+}_{H}x=x\right)$$
40	37	oveqd	$$⊢\phi \to x\underset{\dot{}}{+}y=x{+}_{H}y$$
41	40	eqeq1d	$$⊢\phi \to \left(x\underset{\dot{}}{+}y=x\leftrightarrow x{+}_{H}y=x\right)$$
42	39 41	anbi12d	$$⊢\phi \to \left(\left(y\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}y=x\right)\leftrightarrow \left(y{+}_{H}x=x\wedge x{+}_{H}y=x\right)\right)$$
43	33 42	raleqbidv	$$⊢\phi \to \left(\forall x\in S\left(y\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}y=x\right)\leftrightarrow \forall x\in {\mathrm{Base}}_H\left(y{+}_{H}x=x\wedge x{+}_{H}y=x\right)\right)$$
44	33 43	rabeqbidv	$$⊢\phi \to \left\{y\in S|\forall x\in S\left(y\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}y=x\right)\right\}=\left\{y\in {\mathrm{Base}}_H|\forall x\in {\mathrm{Base}}_H\left(y{+}_{H}x=x\wedge x{+}_{H}y=x\right)\right\}$$
45	31 44	eleqtrd	$$⊢\phi \to \underset{\dot{}}{0}\in \left\{y\in {\mathrm{Base}}_H|\forall x\in {\mathrm{Base}}_H\left(y{+}_{H}x=x\wedge x{+}_{H}y=x\right)\right\}$$
46	45	snssd	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}\subseteq \left\{y\in {\mathrm{Base}}_H|\forall x\in {\mathrm{Base}}_H\left(y{+}_{H}x=x\wedge x{+}_{H}y=x\right)\right\}$$
47	3	ovexi	$$⊢H\in \mathrm{V}$$
48	47	a1i	$$⊢\phi \to H\in \mathrm{V}$$
49		eqid	$$⊢{\mathrm{Base}}_H={\mathrm{Base}}_H$$
50		eqid	$$⊢0_H=0_H$$
51		eqid	$$⊢{+}_H={+}_H$$
52		eqid	$$⊢\left\{y\in {\mathrm{Base}}_H|\forall x\in {\mathrm{Base}}_H\left(y{+}_{H}x=x\wedge x{+}_{H}y=x\right)\right\}=\left\{y\in {\mathrm{Base}}_H|\forall x\in {\mathrm{Base}}_H\left(y{+}_{H}x=x\wedge x{+}_{H}y=x\right)\right\}$$
53	49 50 51 52	mgmidsssn0	$$⊢H\in \mathrm{V}\to \left\{y\in {\mathrm{Base}}_H|\forall x\in {\mathrm{Base}}_H\left(y{+}_{H}x=x\wedge x{+}_{H}y=x\right)\right\}\subseteq \left\{0_H\right\}$$
54	48 53	syl	$$⊢\phi \to \left\{y\in {\mathrm{Base}}_H|\forall x\in {\mathrm{Base}}_H\left(y{+}_{H}x=x\wedge x{+}_{H}y=x\right)\right\}\subseteq \left\{0_H\right\}$$
55	54 45	sseldd	$$⊢\phi \to \underset{\dot{}}{0}\in \left\{0_H\right\}$$
56		elsni	$$⊢\underset{\dot{}}{0}\in \left\{0_H\right\}\to \underset{\dot{}}{0}=0_H$$
57	55 56	syl	$$⊢\phi \to \underset{\dot{}}{0}=0_H$$
58	57	sneqd	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}=\left\{0_H\right\}$$
59	54 58	sseqtrrd	$$⊢\phi \to \left\{y\in {\mathrm{Base}}_H|\forall x\in {\mathrm{Base}}_H\left(y{+}_{H}x=x\wedge x{+}_{H}y=x\right)\right\}\subseteq \left\{\underset{\dot{}}{0}\right\}$$
60	46 59	eqssd	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}=\left\{y\in {\mathrm{Base}}_H|\forall x\in {\mathrm{Base}}_H\left(y{+}_{H}x=x\wedge x{+}_{H}y=x\right)\right\}$$
61	26 60	eqtr3d	$$⊢\phi \to \left\{y\in B|\forall x\in B\left(y\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}y=x\right)\right\}=\left\{y\in {\mathrm{Base}}_H|\forall x\in {\mathrm{Base}}_H\left(y{+}_{H}x=x\wedge x{+}_{H}y=x\right)\right\}$$
62	61	sseq2d	$$⊢\phi \to \left(\mathrm{ran}F\subseteq \left\{y\in B|\forall x\in B\left(y\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}y=x\right)\right\}\leftrightarrow \mathrm{ran}F\subseteq \left\{y\in {\mathrm{Base}}_H|\forall x\in {\mathrm{Base}}_H\left(y{+}_{H}x=x\wedge x{+}_{H}y=x\right)\right\}\right)$$
63	23 57	eqtr3d	$$⊢\phi \to 0_G=0_H$$
64	37	seqeq2d	$$⊢\phi \to seqm\left(\underset{\dot{}}{+},F\right)=seqm\left({+}_H,F\right)$$
65	64	fveq1d	$$⊢\phi \to seqm\left(\underset{\dot{}}{+},F\right)\left(n\right)=seqm\left({+}_H,F\right)\left(n\right)$$
66	65	eqeq2d	$$⊢\phi \to \left(z=seqm\left(\underset{\dot{}}{+},F\right)\left(n\right)\leftrightarrow z=seqm\left({+}_H,F\right)\left(n\right)\right)$$
67	66	anbi2d	$$⊢\phi \to \left(\left(A=\left(m\dots n\right)\wedge z=seqm\left(\underset{\dot{}}{+},F\right)\left(n\right)\right)\leftrightarrow \left(A=\left(m\dots n\right)\wedge z=seqm\left({+}_H,F\right)\left(n\right)\right)\right)$$
68	67	rexbidv	$$⊢\phi \to \left(\exists n\in {\mathbb{Z}}_{\ge m}\left(A=\left(m\dots n\right)\wedge z=seqm\left(\underset{\dot{}}{+},F\right)\left(n\right)\right)\leftrightarrow \exists n\in {\mathbb{Z}}_{\ge m}\left(A=\left(m\dots n\right)\wedge z=seqm\left({+}_H,F\right)\left(n\right)\right)\right)$$
69	68	exbidv	$$⊢\phi \to \left(\exists m\exists n\in {\mathbb{Z}}_{\ge m}\left(A=\left(m\dots n\right)\wedge z=seqm\left(\underset{\dot{}}{+},F\right)\left(n\right)\right)\leftrightarrow \exists m\exists n\in {\mathbb{Z}}_{\ge m}\left(A=\left(m\dots n\right)\wedge z=seqm\left({+}_H,F\right)\left(n\right)\right)\right)$$
70	69	iotabidv	$$⊢\phi \to \left(\iota z|\exists m\exists n\in {\mathbb{Z}}_{\ge m}\left(A=\left(m\dots n\right)\wedge z=seqm\left(\underset{\dot{}}{+},F\right)\left(n\right)\right)\right)=\left(\iota z|\exists m\exists n\in {\mathbb{Z}}_{\ge m}\left(A=\left(m\dots n\right)\wedge z=seqm\left({+}_H,F\right)\left(n\right)\right)\right)$$
71	37	seqeq2d	$$⊢\phi \to seq1\left(\underset{\dot{}}{+},\left(F\circ f\right)\right)=seq1\left({+}_H,\left(F\circ f\right)\right)$$
72	71	fveq1d	$$⊢\phi \to seq1\left(\underset{\dot{}}{+},\left(F\circ f\right)\right)\left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)=seq1\left({+}_H,\left(F\circ f\right)\right)\left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)$$
73	72	eqeq2d	$$⊢\phi \to \left(z=seq1\left(\underset{\dot{}}{+},\left(F\circ f\right)\right)\left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\leftrightarrow z=seq1\left({+}_H,\left(F\circ f\right)\right)\left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\right)$$
74	73	anbi2d	$$⊢\phi \to \left(\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]\wedge z=seq1\left(\underset{\dot{}}{+},\left(F\circ f\right)\right)\left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\right)\leftrightarrow \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]\wedge z=seq1\left({+}_H,\left(F\circ f\right)\right)\left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\right)\right)$$
75	74	exbidv	$$⊢\phi \to \left(\exists f\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]\wedge z=seq1\left(\underset{\dot{}}{+},\left(F\circ f\right)\right)\left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\right)\leftrightarrow \exists f\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]\wedge z=seq1\left({+}_H,\left(F\circ f\right)\right)\left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\right)\right)$$
76	75	iotabidv	$$⊢\phi \to \left(\iota z|\exists f\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]\wedge z=seq1\left(\underset{\dot{}}{+},\left(F\circ f\right)\right)\left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\right)\right)=\left(\iota z|\exists f\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]\wedge z=seq1\left({+}_H,\left(F\circ f\right)\right)\left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\right)\right)$$
77	70 76	ifeq12d	$$⊢\phi \to if\left(A\in \mathrm{ran}\dots ,\left(\iota z|\exists m\exists n\in {\mathbb{Z}}_{\ge m}\left(A=\left(m\dots n\right)\wedge z=seqm\left(\underset{\dot{}}{+},F\right)\left(n\right)\right)\right),\left(\iota z|\exists f\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]\wedge z=seq1\left(\underset{\dot{}}{+},\left(F\circ f\right)\right)\left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\right)\right)\right)=if\left(A\in \mathrm{ran}\dots ,\left(\iota z|\exists m\exists n\in {\mathbb{Z}}_{\ge m}\left(A=\left(m\dots n\right)\wedge z=seqm\left({+}_H,F\right)\left(n\right)\right)\right),\left(\iota z|\exists f\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]\wedge z=seq1\left({+}_H,\left(F\circ f\right)\right)\left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\right)\right)\right)$$
78	62 63 77	ifbieq12d	$$⊢\phi \to if\left(\mathrm{ran}F\subseteq \left\{y\in B|\forall x\in B\left(y\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}y=x\right)\right\},0_G,if\left(A\in \mathrm{ran}\dots ,\left(\iota z|\exists m\exists n\in {\mathbb{Z}}_{\ge m}\left(A=\left(m\dots n\right)\wedge z=seqm\left(\underset{\dot{}}{+},F\right)\left(n\right)\right)\right),\left(\iota z|\exists f\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]\wedge z=seq1\left(\underset{\dot{}}{+},\left(F\circ f\right)\right)\left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\right)\right)\right)\right)=if\left(\mathrm{ran}F\subseteq \left\{y\in {\mathrm{Base}}_H|\forall x\in {\mathrm{Base}}_H\left(y{+}_{H}x=x\wedge x{+}_{H}y=x\right)\right\},0_H,if\left(A\in \mathrm{ran}\dots ,\left(\iota z|\exists m\exists n\in {\mathbb{Z}}_{\ge m}\left(A=\left(m\dots n\right)\wedge z=seqm\left({+}_H,F\right)\left(n\right)\right)\right),\left(\iota z|\exists f\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]\wedge z=seq1\left({+}_H,\left(F\circ f\right)\right)\left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\right)\right)\right)\right)$$
79	26	difeq2d	$$⊢\phi \to \mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}=\mathrm{V}\setminus \left\{y\in B|\forall x\in B\left(y\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}y=x\right)\right\}$$
80	79	imaeq2d	$$⊢\phi \to F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=F^{-1}\left[\mathrm{V}\setminus \left\{y\in B|\forall x\in B\left(y\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}y=x\right)\right\}\right]$$
81	7 6	fssd	$$⊢\phi \to F:A⟶B$$
82	1 17 2 18 80 4 5 81	gsumval	$$⊢\phi \to {\sum }_{G}F=if\left(\mathrm{ran}F\subseteq \left\{y\in B|\forall x\in B\left(y\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}y=x\right)\right\},0_G,if\left(A\in \mathrm{ran}\dots ,\left(\iota z|\exists m\exists n\in {\mathbb{Z}}_{\ge m}\left(A=\left(m\dots n\right)\wedge z=seqm\left(\underset{\dot{}}{+},F\right)\left(n\right)\right)\right),\left(\iota z|\exists f\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]\wedge z=seq1\left(\underset{\dot{}}{+},\left(F\circ f\right)\right)\left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\right)\right)\right)\right)$$
83	60	difeq2d	$$⊢\phi \to \mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}=\mathrm{V}\setminus \left\{y\in {\mathrm{Base}}_H|\forall x\in {\mathrm{Base}}_H\left(y{+}_{H}x=x\wedge x{+}_{H}y=x\right)\right\}$$
84	83	imaeq2d	$$⊢\phi \to F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=F^{-1}\left[\mathrm{V}\setminus \left\{y\in {\mathrm{Base}}_H|\forall x\in {\mathrm{Base}}_H\left(y{+}_{H}x=x\wedge x{+}_{H}y=x\right)\right\}\right]$$
85	33	feq3d	$$⊢\phi \to \left(F:A⟶S\leftrightarrow F:A⟶{\mathrm{Base}}_H\right)$$
86	7 85	mpbid	$$⊢\phi \to F:A⟶{\mathrm{Base}}_H$$
87	49 50 51 52 84 48 5 86	gsumval	$$⊢\phi \to {\sum }_{H}F=if\left(\mathrm{ran}F\subseteq \left\{y\in {\mathrm{Base}}_H|\forall x\in {\mathrm{Base}}_H\left(y{+}_{H}x=x\wedge x{+}_{H}y=x\right)\right\},0_H,if\left(A\in \mathrm{ran}\dots ,\left(\iota z|\exists m\exists n\in {\mathbb{Z}}_{\ge m}\left(A=\left(m\dots n\right)\wedge z=seqm\left({+}_H,F\right)\left(n\right)\right)\right),\left(\iota z|\exists f\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]\wedge z=seq1\left({+}_H,\left(F\circ f\right)\right)\left(\left|F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right|\right)\right)\right)\right)\right)$$
88	78 82 87	3eqtr4d	$$⊢\phi \to {\sum }_{G}F={\sum }_{H}F$$