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{˙}{0} = 0_{G}$
	eldprdi.w	$⊢ W = \{h \in \underset{i \in I}{⨉} S (i) \| {finSupp}_{\underset{˙}{0}} (h)\}$
	eldprdi.1	$⊢ φ \to G dom DProd S$
	eldprdi.2	$⊢ φ \to dom S = I$
	eldprdi.3	$⊢ φ \to F \in W$
Assertion	dprdfeq0	$⊢ φ \to (\sum_{G} F = \underset{˙}{0} \leftrightarrow F = (x \in I ⟼ \underset{˙}{0}))$

Proof

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

Metamath Proof Explorer

Theorem dprdfeq0

Proof