Theorem dprdfeq0

Description: The zero function is the only function that sums to zero in a direct product. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 14-Jul-2019)

	Ref	Expression
Hypotheses	eldprdi.0	$$⊢\underset{\dot{}}{0}=0_G$$
	eldprdi.w	$$⊢W=\left\{h\in \underset{i\in I}{⨉}S\left(i\right)|{finSupp}_{\underset{\dot{}}{0}}\left(h\right)\right\}$$
	eldprdi.1	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$
	eldprdi.2	$$⊢\phi \to \mathrm{dom}S=I$$
	eldprdi.3	$$⊢\phi \to F\in W$$
Assertion	dprdfeq0	$$⊢\phi \to \left({\sum }_{G}F=\underset{\dot{}}{0}\leftrightarrow F=\left(x\in I⟼\underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eldprdi.0	$$⊢\underset{\dot{}}{0}=0_G$$
2		eldprdi.w	$$⊢W=\left\{h\in \underset{i\in I}{⨉}S\left(i\right)|{finSupp}_{\underset{\dot{}}{0}}\left(h\right)\right\}$$
3		eldprdi.1	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$
4		eldprdi.2	$$⊢\phi \to \mathrm{dom}S=I$$
5		eldprdi.3	$$⊢\phi \to F\in W$$
6		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
7	2 3 4 5 6	dprdff	$$⊢\phi \to F:I⟶{\mathrm{Base}}_G$$
8	7	feqmptd	$$⊢\phi \to F=\left(x\in I⟼F\left(x\right)\right)$$
9	8	adantr	$$⊢\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\to F=\left(x\in I⟼F\left(x\right)\right)$$
10	2 3 4 5	dprdfcl	$$⊢\left(\phi \wedge x\in I\right)\to F\left(x\right)\in S\left(x\right)$$
11	10	adantlr	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to F\left(x\right)\in S\left(x\right)$$
12	3	ad2antrr	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to G\mathrm{dom}\mathrm{DProd}S$$
13	4	ad2antrr	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to \mathrm{dom}S=I$$
14		simpr	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to x\in I$$
15		eqid	$$⊢\left(y\in I⟼if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right)\right)=\left(y\in I⟼if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right)\right)$$
16	1 2 12 13 14 11 15	dprdfid	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to \left(\left(y\in I⟼if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right)\right)\in W\wedge \underset{y\in I}{{\sum }_G}if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right)=F\left(x\right)\right)$$
17	16	simpld	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to \left(y\in I⟼if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right)\right)\in W$$
18	5	ad2antrr	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to F\in W$$
19		eqid	$$⊢{-}_G={-}_G$$
20	1 2 12 13 17 18 19	dprdfsub	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to \left(\left(y\in I⟼if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right)\right){{-}_G}_{f}F\in W\wedge {\sum }_G\left(\left(y\in I⟼if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right)\right){{-}_G}_{f}F\right)=\left(\underset{y\in I}{{\sum }_G},if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right)\right){-}_G\left({\sum }_G,F\right)\right)$$
21	20	simprd	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to {\sum }_G\left(\left(y\in I⟼if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right)\right){{-}_G}_{f}F\right)=\left(\underset{y\in I}{{\sum }_G},if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right)\right){-}_G\left({\sum }_G,F\right)$$
22	3 4	dprddomcld	$$⊢\phi \to I\in \mathrm{V}$$
23	22	ad2antrr	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to I\in \mathrm{V}$$
24		fvex	$$⊢F\left(x\right)\in \mathrm{V}$$
25	1	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
26	24 25	ifex	$$⊢if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right)\in \mathrm{V}$$
27	26	a1i	$$⊢\left(\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\wedge y\in I\right)\to if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right)\in \mathrm{V}$$
28		fvexd	$$⊢\left(\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\wedge y\in I\right)\to F\left(y\right)\in \mathrm{V}$$
29		eqidd	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to \left(y\in I⟼if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right)\right)=\left(y\in I⟼if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right)\right)$$
30	7	ad2antrr	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to F:I⟶{\mathrm{Base}}_G$$
31	30	feqmptd	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to F=\left(y\in I⟼F\left(y\right)\right)$$
32	23 27 28 29 31	offval2	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to \left(y\in I⟼if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right)\right){{-}_G}_{f}F=\left(y\in I⟼if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right){-}_{G}F\left(y\right)\right)$$
33	32	oveq2d	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to {\sum }_G\left(\left(y\in I⟼if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right)\right){{-}_G}_{f}F\right)=\underset{y\in I}{{\sum }_G}\left(if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right){-}_{G}F\left(y\right)\right)$$
34	16	simprd	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to \underset{y\in I}{{\sum }_G}if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right)=F\left(x\right)$$
35		simplr	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to {\sum }_{G}F=\underset{\dot{}}{0}$$
36	34 35	oveq12d	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to \left(\underset{y\in I}{{\sum }_G},if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right)\right){-}_G\left({\sum }_G,F\right)=F\left(x\right){-}_G\underset{\dot{}}{0}$$
37		dprdgrp	$$⊢G\mathrm{dom}\mathrm{DProd}S\to G\in \mathrm{Grp}$$
38	12 37	syl	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to G\in \mathrm{Grp}$$
39	30 14	ffvelcdmd	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to F\left(x\right)\in {\mathrm{Base}}_G$$
40	6 1 19	grpsubid1	$$⊢\left(G\in \mathrm{Grp}\wedge F\left(x\right)\in {\mathrm{Base}}_G\right)\to F\left(x\right){-}_G\underset{\dot{}}{0}=F\left(x\right)$$
41	38 39 40	syl2anc	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to F\left(x\right){-}_G\underset{\dot{}}{0}=F\left(x\right)$$
42	36 41	eqtrd	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to \left(\underset{y\in I}{{\sum }_G},if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right)\right){-}_G\left({\sum }_G,F\right)=F\left(x\right)$$
43	21 33 42	3eqtr3d	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to \underset{y\in I}{{\sum }_G}\left(if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right){-}_{G}F\left(y\right)\right)=F\left(x\right)$$
44		eqid	$$⊢\mathrm{Cntz}\left(G\right)=\mathrm{Cntz}\left(G\right)$$
45		grpmnd	$$⊢G\in \mathrm{Grp}\to G\in \mathrm{Mnd}$$
46	3 37 45	3syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
47	46	ad2antrr	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to G\in \mathrm{Mnd}$$
48	6	subgacs	$$⊢G\in \mathrm{Grp}\to \mathrm{SubGrp}\left(G\right)\in \mathrm{ACS}\left({\mathrm{Base}}_G\right)$$
49		acsmre	$$⊢\mathrm{SubGrp}\left(G\right)\in \mathrm{ACS}\left({\mathrm{Base}}_G\right)\to \mathrm{SubGrp}\left(G\right)\in \mathrm{Moore}\left({\mathrm{Base}}_G\right)$$
50	38 48 49	3syl	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to \mathrm{SubGrp}\left(G\right)\in \mathrm{Moore}\left({\mathrm{Base}}_G\right)$$
51		imassrn	$$⊢S\left[I\setminus \left\{x\right\}\right]\subseteq \mathrm{ran}S$$
52	3 4	dprdf2	$$⊢\phi \to S:I⟶\mathrm{SubGrp}\left(G\right)$$
53	52	ad2antrr	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to S:I⟶\mathrm{SubGrp}\left(G\right)$$
54	53	frnd	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to \mathrm{ran}S\subseteq \mathrm{SubGrp}\left(G\right)$$
55		mresspw	$$⊢\mathrm{SubGrp}\left(G\right)\in \mathrm{Moore}\left({\mathrm{Base}}_G\right)\to \mathrm{SubGrp}\left(G\right)\subseteq 𝒫{\mathrm{Base}}_G$$
56	50 55	syl	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to \mathrm{SubGrp}\left(G\right)\subseteq 𝒫{\mathrm{Base}}_G$$
57	54 56	sstrd	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to \mathrm{ran}S\subseteq 𝒫{\mathrm{Base}}_G$$
58	51 57	sstrid	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to S\left[I\setminus \left\{x\right\}\right]\subseteq 𝒫{\mathrm{Base}}_G$$
59		sspwuni	$$⊢S\left[I\setminus \left\{x\right\}\right]\subseteq 𝒫{\mathrm{Base}}_G\leftrightarrow \bigcup S\left[I\setminus \left\{x\right\}\right]\subseteq {\mathrm{Base}}_G$$
60	58 59	sylib	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to \bigcup S\left[I\setminus \left\{x\right\}\right]\subseteq {\mathrm{Base}}_G$$
61		eqid	$$⊢\mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)=\mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)$$
62	61	mrccl	$$⊢\left(\mathrm{SubGrp}\left(G\right)\in \mathrm{Moore}\left({\mathrm{Base}}_G\right)\wedge \bigcup S\left[I\setminus \left\{x\right\}\right]\subseteq {\mathrm{Base}}_G\right)\to \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)\in \mathrm{SubGrp}\left(G\right)$$
63	50 60 62	syl2anc	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)\in \mathrm{SubGrp}\left(G\right)$$
64		subgsubm	$$⊢\mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)\in \mathrm{SubGrp}\left(G\right)\to \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)\in \mathrm{SubMnd}\left(G\right)$$
65	63 64	syl	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)\in \mathrm{SubMnd}\left(G\right)$$
66		oveq1	$$⊢F\left(x\right)=if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right)\to F\left(x\right){-}_{G}F\left(y\right)=if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right){-}_{G}F\left(y\right)$$
67	66	eleq1d	$$⊢F\left(x\right)=if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right)\to \left(F\left(x\right){-}_{G}F\left(y\right)\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)\leftrightarrow if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right){-}_{G}F\left(y\right)\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)\right)$$
68		oveq1	$$⊢\underset{\dot{}}{0}=if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right)\to \underset{\dot{}}{0}{-}_{G}F\left(y\right)=if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right){-}_{G}F\left(y\right)$$
69	68	eleq1d	$$⊢\underset{\dot{}}{0}=if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right)\to \left(\underset{\dot{}}{0}{-}_{G}F\left(y\right)\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)\leftrightarrow if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right){-}_{G}F\left(y\right)\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)\right)$$
70		simpr	$$⊢\left(\left(\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\wedge y\in I\right)\wedge y=x\right)\to y=x$$
71	70	fveq2d	$$⊢\left(\left(\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\wedge y\in I\right)\wedge y=x\right)\to F\left(y\right)=F\left(x\right)$$
72	71	oveq2d	$$⊢\left(\left(\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\wedge y\in I\right)\wedge y=x\right)\to F\left(x\right){-}_{G}F\left(y\right)=F\left(x\right){-}_{G}F\left(x\right)$$
73	6 1 19	grpsubid	$$⊢\left(G\in \mathrm{Grp}\wedge F\left(x\right)\in {\mathrm{Base}}_G\right)\to F\left(x\right){-}_{G}F\left(x\right)=\underset{\dot{}}{0}$$
74	38 39 73	syl2anc	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to F\left(x\right){-}_{G}F\left(x\right)=\underset{\dot{}}{0}$$
75	1	subg0cl	$$⊢\mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)\in \mathrm{SubGrp}\left(G\right)\to \underset{\dot{}}{0}\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)$$
76	63 75	syl	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to \underset{\dot{}}{0}\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)$$
77	74 76	eqeltrd	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to F\left(x\right){-}_{G}F\left(x\right)\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)$$
78	77	ad2antrr	$$⊢\left(\left(\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\wedge y\in I\right)\wedge y=x\right)\to F\left(x\right){-}_{G}F\left(x\right)\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)$$
79	72 78	eqeltrd	$$⊢\left(\left(\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\wedge y\in I\right)\wedge y=x\right)\to F\left(x\right){-}_{G}F\left(y\right)\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)$$
80	63	ad2antrr	$$⊢\left(\left(\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\wedge y\in I\right)\wedge \neg y=x\right)\to \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)\in \mathrm{SubGrp}\left(G\right)$$
81	80 75	syl	$$⊢\left(\left(\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\wedge y\in I\right)\wedge \neg y=x\right)\to \underset{\dot{}}{0}\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)$$
82	50 61 60	mrcssidd	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to \bigcup S\left[I\setminus \left\{x\right\}\right]\subseteq \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)$$
83	82	ad2antrr	$$⊢\left(\left(\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\wedge y\in I\right)\wedge \neg y=x\right)\to \bigcup S\left[I\setminus \left\{x\right\}\right]\subseteq \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)$$
84	2 12 13 18	dprdfcl	$$⊢\left(\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\wedge y\in I\right)\to F\left(y\right)\in S\left(y\right)$$
85	84	adantr	$$⊢\left(\left(\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\wedge y\in I\right)\wedge \neg y=x\right)\to F\left(y\right)\in S\left(y\right)$$
86	53	ffnd	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to SFnI$$
87	86	ad2antrr	$$⊢\left(\left(\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\wedge y\in I\right)\wedge \neg y=x\right)\to SFnI$$
88		difssd	$$⊢\left(\left(\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\wedge y\in I\right)\wedge \neg y=x\right)\to I\setminus \left\{x\right\}\subseteq I$$
89		df-ne	$$⊢y\ne x\leftrightarrow \neg y=x$$
90		eldifsn	$$⊢y\in \left(I\setminus \left\{x\right\}\right)\leftrightarrow \left(y\in I\wedge y\ne x\right)$$
91	90	biimpri	$$⊢\left(y\in I\wedge y\ne x\right)\to y\in \left(I\setminus \left\{x\right\}\right)$$
92	89 91	sylan2br	$$⊢\left(y\in I\wedge \neg y=x\right)\to y\in \left(I\setminus \left\{x\right\}\right)$$
93	92	adantll	$$⊢\left(\left(\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\wedge y\in I\right)\wedge \neg y=x\right)\to y\in \left(I\setminus \left\{x\right\}\right)$$
94		fnfvima	$$⊢\left(SFnI\wedge I\setminus \left\{x\right\}\subseteq I\wedge y\in \left(I\setminus \left\{x\right\}\right)\right)\to S\left(y\right)\in S\left[I\setminus \left\{x\right\}\right]$$
95	87 88 93 94	syl3anc	$$⊢\left(\left(\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\wedge y\in I\right)\wedge \neg y=x\right)\to S\left(y\right)\in S\left[I\setminus \left\{x\right\}\right]$$
96		elunii	$$⊢\left(F\left(y\right)\in S\left(y\right)\wedge S\left(y\right)\in S\left[I\setminus \left\{x\right\}\right]\right)\to F\left(y\right)\in \bigcup S\left[I\setminus \left\{x\right\}\right]$$
97	85 95 96	syl2anc	$$⊢\left(\left(\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\wedge y\in I\right)\wedge \neg y=x\right)\to F\left(y\right)\in \bigcup S\left[I\setminus \left\{x\right\}\right]$$
98	83 97	sseldd	$$⊢\left(\left(\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\wedge y\in I\right)\wedge \neg y=x\right)\to F\left(y\right)\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)$$
99	19	subgsubcl	$$⊢\left(\mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)\in \mathrm{SubGrp}\left(G\right)\wedge \underset{\dot{}}{0}\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)\wedge F\left(y\right)\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)\right)\to \underset{\dot{}}{0}{-}_{G}F\left(y\right)\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)$$
100	80 81 98 99	syl3anc	$$⊢\left(\left(\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\wedge y\in I\right)\wedge \neg y=x\right)\to \underset{\dot{}}{0}{-}_{G}F\left(y\right)\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)$$
101	67 69 79 100	ifbothda	$$⊢\left(\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\wedge y\in I\right)\to if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right){-}_{G}F\left(y\right)\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)$$
102	101	fmpttd	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to \left(y\in I⟼if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right){-}_{G}F\left(y\right)\right):I⟶\mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)$$
103	20	simpld	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to \left(y\in I⟼if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right)\right){{-}_G}_{f}F\in W$$
104	32 103	eqeltrrd	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to \left(y\in I⟼if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right){-}_{G}F\left(y\right)\right)\in W$$
105	2 12 13 104 44	dprdfcntz	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to \mathrm{ran}\left(y\in I⟼if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right){-}_{G}F\left(y\right)\right)\subseteq \mathrm{Cntz}\left(G\right)\left(\mathrm{ran}\left(y\in I⟼if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right){-}_{G}F\left(y\right)\right)\right)$$
106	2 12 13 104	dprdffsupp	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to {finSupp}_{\underset{\dot{}}{0}}\left(\left(y\in I⟼if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right){-}_{G}F\left(y\right)\right)\right)$$
107	1 44 47 23 65 102 105 106	gsumzsubmcl	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to \underset{y\in I}{{\sum }_G}\left(if\left(y=x,F\left(x\right),\underset{\dot{}}{0}\right){-}_{G}F\left(y\right)\right)\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)$$
108	43 107	eqeltrrd	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to F\left(x\right)\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)$$
109	11 108	elind	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to F\left(x\right)\in \left(S\left(x\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)\right)$$
110	12 13 14 1 61	dprddisj	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to S\left(x\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left(G\right)\right)\left(\bigcup S\left[I\setminus \left\{x\right\}\right]\right)=\left\{\underset{\dot{}}{0}\right\}$$
111	109 110	eleqtrd	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to F\left(x\right)\in \left\{\underset{\dot{}}{0}\right\}$$
112		elsni	$$⊢F\left(x\right)\in \left\{\underset{\dot{}}{0}\right\}\to F\left(x\right)=\underset{\dot{}}{0}$$
113	111 112	syl	$$⊢\left(\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\wedge x\in I\right)\to F\left(x\right)=\underset{\dot{}}{0}$$
114	113	mpteq2dva	$$⊢\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\to \left(x\in I⟼F\left(x\right)\right)=\left(x\in I⟼\underset{\dot{}}{0}\right)$$
115	9 114	eqtrd	$$⊢\left(\phi \wedge {\sum }_{G}F=\underset{\dot{}}{0}\right)\to F=\left(x\in I⟼\underset{\dot{}}{0}\right)$$
116	115	ex	$$⊢\phi \to \left({\sum }_{G}F=\underset{\dot{}}{0}\to F=\left(x\in I⟼\underset{\dot{}}{0}\right)\right)$$
117	1	gsumz	$$⊢\left(G\in \mathrm{Mnd}\wedge I\in \mathrm{V}\right)\to \underset{x\in I}{{\sum }_G}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
118	46 22 117	syl2anc	$$⊢\phi \to \underset{x\in I}{{\sum }_G}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
119		oveq2	$$⊢F=\left(x\in I⟼\underset{\dot{}}{0}\right)\to {\sum }_{G}F=\underset{x\in I}{{\sum }_G}\underset{\dot{}}{0}$$
120	119	eqeq1d	$$⊢F=\left(x\in I⟼\underset{\dot{}}{0}\right)\to \left({\sum }_{G}F=\underset{\dot{}}{0}\leftrightarrow \underset{x\in I}{{\sum }_G}\underset{\dot{}}{0}=\underset{\dot{}}{0}\right)$$
121	118 120	syl5ibrcom	$$⊢\phi \to \left(F=\left(x\in I⟼\underset{\dot{}}{0}\right)\to {\sum }_{G}F=\underset{\dot{}}{0}\right)$$
122	116 121	impbid	$$⊢\phi \to \left({\sum }_{G}F=\underset{\dot{}}{0}\leftrightarrow F=\left(x\in I⟼\underset{\dot{}}{0}\right)\right)$$