domnprodeq0

Description: A product over a domain is zero exactly when one of the factors is zero. Generalization of domneq0 for any number of factors. See also domnprodn0 . (Contributed by Thierry Arnoux, 15-Feb-2026)

	Ref	Expression
Hypotheses	domnprodeq0.m	$⊢ M = {mulGrp}_{R}$
	domnprodeq0.b	$⊢ B = {Base}_{R}$
	domnprodeq0.1	$⊢ \underset{˙}{0} = 0_{R}$
	domnprodeq0.r	$⊢ φ \to R \in IDomn$
	domnprodeq0.2	$⊢ φ \to A \in Fin$
	domnprodeq0.f	$⊢ φ \to F : A ⟶ B$
Assertion	domnprodeq0	$⊢ φ \to (\sum_{M} F = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \in ran F)$

Proof

Step	Hyp	Ref	Expression
1		domnprodeq0.m	$⊢ M = {mulGrp}_{R}$
2		domnprodeq0.b	$⊢ B = {Base}_{R}$
3		domnprodeq0.1	$⊢ \underset{˙}{0} = 0_{R}$
4		domnprodeq0.r	$⊢ φ \to R \in IDomn$
5		domnprodeq0.2	$⊢ φ \to A \in Fin$
6		domnprodeq0.f	$⊢ φ \to F : A ⟶ B$
7		mpteq1	$⊢ a = \emptyset \to (k \in a ⟼ F (k)) = (k \in \emptyset ⟼ F (k))$
8		mpt0	$⊢ (k \in \emptyset ⟼ F (k)) = \emptyset$
9	7 8	eqtrdi	$⊢ a = \emptyset \to (k \in a ⟼ F (k)) = \emptyset$
10	9	oveq2d	$⊢ a = \emptyset \to \underset{k \in a}{\sum_{M}} F (k) = \sum_{M} \emptyset$
11	10	eqeq1d	$⊢ a = \emptyset \to (\underset{k \in a}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow \sum_{M} \emptyset = \underset{˙}{0})$
12	9	rneqd	$⊢ a = \emptyset \to ran (k \in a ⟼ F (k)) = ran \emptyset$
13	12	eleq2d	$⊢ a = \emptyset \to (\underset{˙}{0} \in ran (k \in a ⟼ F (k)) \leftrightarrow \underset{˙}{0} \in ran \emptyset)$
14	11 13	bibi12d	$⊢ a = \emptyset \to ((\underset{k \in a}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \in ran (k \in a ⟼ F (k))) \leftrightarrow (\sum_{M} \emptyset = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \in ran \emptyset))$
15		mpteq1	$⊢ a = b \to (k \in a ⟼ F (k)) = (k \in b ⟼ F (k))$
16	15	oveq2d	$⊢ a = b \to \underset{k \in a}{\sum_{M}} F (k) = \underset{k \in b}{\sum_{M}} F (k)$
17	16	eqeq1d	$⊢ a = b \to (\underset{k \in a}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow \underset{k \in b}{\sum_{M}} F (k) = \underset{˙}{0})$
18	15	rneqd	$⊢ a = b \to ran (k \in a ⟼ F (k)) = ran (k \in b ⟼ F (k))$
19	18	eleq2d	$⊢ a = b \to (\underset{˙}{0} \in ran (k \in a ⟼ F (k)) \leftrightarrow \underset{˙}{0} \in ran (k \in b ⟼ F (k)))$
20	17 19	bibi12d	$⊢ a = b \to ((\underset{k \in a}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \in ran (k \in a ⟼ F (k))) \leftrightarrow (\underset{k \in b}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \in ran (k \in b ⟼ F (k))))$
21		mpteq1	$⊢ a = b \cup \{l\} \to (k \in a ⟼ F (k)) = (k \in (b \cup \{l\}) ⟼ F (k))$
22	21	oveq2d	$⊢ a = b \cup \{l\} \to \underset{k \in a}{\sum_{M}} F (k) = \underset{k \in b \cup \{l\}}{\sum_{M}} F (k)$
23	22	eqeq1d	$⊢ a = b \cup \{l\} \to (\underset{k \in a}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow \underset{k \in b \cup \{l\}}{\sum_{M}} F (k) = \underset{˙}{0})$
24	21	rneqd	$⊢ a = b \cup \{l\} \to ran (k \in a ⟼ F (k)) = ran (k \in (b \cup \{l\}) ⟼ F (k))$
25	24	eleq2d	$⊢ a = b \cup \{l\} \to (\underset{˙}{0} \in ran (k \in a ⟼ F (k)) \leftrightarrow \underset{˙}{0} \in ran (k \in (b \cup \{l\}) ⟼ F (k)))$
26	23 25	bibi12d	$⊢ a = b \cup \{l\} \to ((\underset{k \in a}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \in ran (k \in a ⟼ F (k))) \leftrightarrow (\underset{k \in b \cup \{l\}}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \in ran (k \in (b \cup \{l\}) ⟼ F (k))))$
27		mpteq1	$⊢ a = A \to (k \in a ⟼ F (k)) = (k \in A ⟼ F (k))$
28	27	oveq2d	$⊢ a = A \to \underset{k \in a}{\sum_{M}} F (k) = \underset{k \in A}{\sum_{M}} F (k)$
29	28	eqeq1d	$⊢ a = A \to (\underset{k \in a}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow \underset{k \in A}{\sum_{M}} F (k) = \underset{˙}{0})$
30	27	rneqd	$⊢ a = A \to ran (k \in a ⟼ F (k)) = ran (k \in A ⟼ F (k))$
31	30	eleq2d	$⊢ a = A \to (\underset{˙}{0} \in ran (k \in a ⟼ F (k)) \leftrightarrow \underset{˙}{0} \in ran (k \in A ⟼ F (k)))$
32	29 31	bibi12d	$⊢ a = A \to ((\underset{k \in a}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \in ran (k \in a ⟼ F (k))) \leftrightarrow (\underset{k \in A}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \in ran (k \in A ⟼ F (k))))$
33		eqid	$⊢ 1_{R} = 1_{R}$
34	1 33	ringidval	$⊢ 1_{R} = 0_{M}$
35	34	gsum0	$⊢ \sum_{M} \emptyset = 1_{R}$
36	35	a1i	$⊢ φ \to \sum_{M} \emptyset = 1_{R}$
37	4	idomdomd	$⊢ φ \to R \in Domn$
38		domnnzr	$⊢ R \in Domn \to R \in NzRing$
39	33 3	nzrnz	$⊢ R \in NzRing \to 1_{R} \neq \underset{˙}{0}$
40	37 38 39	3syl	$⊢ φ \to 1_{R} \neq \underset{˙}{0}$
41	36 40	eqnetrd	$⊢ φ \to \sum_{M} \emptyset \neq \underset{˙}{0}$
42	41	neneqd	$⊢ φ \to \neg \sum_{M} \emptyset = \underset{˙}{0}$
43		noel	$⊢ \neg \underset{˙}{0} \in \emptyset$
44		rn0	$⊢ ran \emptyset = \emptyset$
45	44	eleq2i	$⊢ \underset{˙}{0} \in ran \emptyset \leftrightarrow \underset{˙}{0} \in \emptyset$
46	43 45	mtbir	$⊢ \neg \underset{˙}{0} \in ran \emptyset$
47	46	a1i	$⊢ φ \to \neg \underset{˙}{0} \in ran \emptyset$
48	42 47	2falsed	$⊢ φ \to (\sum_{M} \emptyset = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \in ran \emptyset)$
49		simpr	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land (\underset{k \in b}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \in ran (k \in b ⟼ F (k)))) \to (\underset{k \in b}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \in ran (k \in b ⟼ F (k)))$
50	49	orbi1d	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land (\underset{k \in b}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \in ran (k \in b ⟼ F (k)))) \to ((\underset{k \in b}{\sum_{M}} F (k) = \underset{˙}{0} \lor F (l) = \underset{˙}{0}) \leftrightarrow (\underset{˙}{0} \in ran (k \in b ⟼ F (k)) \lor F (l) = \underset{˙}{0}))$
51	1 2	mgpbas	$⊢ B = {Base}_{M}$
52		eqid	$⊢ \cdot_{R} = \cdot_{R}$
53	1 52	mgpplusg	$⊢ \cdot_{R} = +_{M}$
54	4	idomcringd	$⊢ φ \to R \in CRing$
55	1	crngmgp	$⊢ R \in CRing \to M \in CMnd$
56	54 55	syl	$⊢ φ \to M \in CMnd$
57	56	ad2antrr	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to M \in CMnd$
58	5	ad2antrr	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to A \in Fin$
59		simplr	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to b \subseteq A$
60	58 59	ssfid	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to b \in Fin$
61	6	ad3antrrr	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land k \in b) \to F : A ⟶ B$
62	59	sselda	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land k \in b) \to k \in A$
63	61 62	ffvelcdmd	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land k \in b) \to F (k) \in B$
64		simpr	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to l \in (A ∖ b)$
65	64	eldifbd	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to \neg l \in b$
66	6	ad2antrr	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to F : A ⟶ B$
67	64	eldifad	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to l \in A$
68	66 67	ffvelcdmd	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to F (l) \in B$
69		fveq2	$⊢ k = l \to F (k) = F (l)$
70	51 53 57 60 63 64 65 68 69	gsumunsn	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to \underset{k \in b \cup \{l\}}{\sum_{M}} F (k) = (\underset{k \in b}{\sum_{M}}, F (k)) \cdot_{R} F (l)$
71	70	eqeq1d	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to (\underset{k \in b \cup \{l\}}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow (\underset{k \in b}{\sum_{M}}, F (k)) \cdot_{R} F (l) = \underset{˙}{0})$
72	37	ad2antrr	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to R \in Domn$
73	63	ralrimiva	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to \forall k \in b F (k) \in B$
74	51 57 60 73	gsummptcl	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to \underset{k \in b}{\sum_{M}} F (k) \in B$
75	2 52 3	domneq0	$⊢ (R \in Domn \land \underset{k \in b}{\sum_{M}} F (k) \in B \land F (l) \in B) \to ((\underset{k \in b}{\sum_{M}}, F (k)) \cdot_{R} F (l) = \underset{˙}{0} \leftrightarrow (\underset{k \in b}{\sum_{M}} F (k) = \underset{˙}{0} \lor F (l) = \underset{˙}{0}))$
76	72 74 68 75	syl3anc	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to ((\underset{k \in b}{\sum_{M}}, F (k)) \cdot_{R} F (l) = \underset{˙}{0} \leftrightarrow (\underset{k \in b}{\sum_{M}} F (k) = \underset{˙}{0} \lor F (l) = \underset{˙}{0}))$
77	71 76	bitrd	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to (\underset{k \in b \cup \{l\}}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow (\underset{k \in b}{\sum_{M}} F (k) = \underset{˙}{0} \lor F (l) = \underset{˙}{0}))$
78	77	adantr	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land (\underset{k \in b}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \in ran (k \in b ⟼ F (k)))) \to (\underset{k \in b \cup \{l\}}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow (\underset{k \in b}{\sum_{M}} F (k) = \underset{˙}{0} \lor F (l) = \underset{˙}{0}))$
79		eqid	$⊢ (k \in (b \cup \{l\}) ⟼ F (k)) = (k \in (b \cup \{l\}) ⟼ F (k))$
80		fvex	$⊢ F (k) \in V$
81	79 80	elrnmpti	$⊢ \underset{˙}{0} \in ran (k \in (b \cup \{l\}) ⟼ F (k)) \leftrightarrow \exists k \in (b \cup \{l\}) \underset{˙}{0} = F (k)$
82		rexun	$⊢ \exists k \in (b \cup \{l\}) \underset{˙}{0} = F (k) \leftrightarrow (\exists k \in b \underset{˙}{0} = F (k) \lor \exists k \in \{l\} \underset{˙}{0} = F (k))$
83		eqid	$⊢ (k \in b ⟼ F (k)) = (k \in b ⟼ F (k))$
84	83 80	elrnmpti	$⊢ \underset{˙}{0} \in ran (k \in b ⟼ F (k)) \leftrightarrow \exists k \in b \underset{˙}{0} = F (k)$
85	84	bicomi	$⊢ \exists k \in b \underset{˙}{0} = F (k) \leftrightarrow \underset{˙}{0} \in ran (k \in b ⟼ F (k))$
86		vex	$⊢ l \in V$
87	69	eqeq2d	$⊢ k = l \to (\underset{˙}{0} = F (k) \leftrightarrow \underset{˙}{0} = F (l))$
88		eqcom	$⊢ \underset{˙}{0} = F (l) \leftrightarrow F (l) = \underset{˙}{0}$
89	87 88	bitrdi	$⊢ k = l \to (\underset{˙}{0} = F (k) \leftrightarrow F (l) = \underset{˙}{0})$
90	86 89	rexsn	$⊢ \exists k \in \{l\} \underset{˙}{0} = F (k) \leftrightarrow F (l) = \underset{˙}{0}$
91	85 90	orbi12i	$⊢ (\exists k \in b \underset{˙}{0} = F (k) \lor \exists k \in \{l\} \underset{˙}{0} = F (k)) \leftrightarrow (\underset{˙}{0} \in ran (k \in b ⟼ F (k)) \lor F (l) = \underset{˙}{0})$
92	81 82 91	3bitri	$⊢ \underset{˙}{0} \in ran (k \in (b \cup \{l\}) ⟼ F (k)) \leftrightarrow (\underset{˙}{0} \in ran (k \in b ⟼ F (k)) \lor F (l) = \underset{˙}{0})$
93	92	a1i	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land (\underset{k \in b}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \in ran (k \in b ⟼ F (k)))) \to (\underset{˙}{0} \in ran (k \in (b \cup \{l\}) ⟼ F (k)) \leftrightarrow (\underset{˙}{0} \in ran (k \in b ⟼ F (k)) \lor F (l) = \underset{˙}{0}))$
94	50 78 93	3bitr4d	$⊢ (((φ \land b \subseteq A) \land l \in (A ∖ b)) \land (\underset{k \in b}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \in ran (k \in b ⟼ F (k)))) \to (\underset{k \in b \cup \{l\}}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \in ran (k \in (b \cup \{l\}) ⟼ F (k)))$
95	94	ex	$⊢ ((φ \land b \subseteq A) \land l \in (A ∖ b)) \to ((\underset{k \in b}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \in ran (k \in b ⟼ F (k))) \to (\underset{k \in b \cup \{l\}}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \in ran (k \in (b \cup \{l\}) ⟼ F (k))))$
96	95	anasss	$⊢ (φ \land (b \subseteq A \land l \in (A ∖ b))) \to ((\underset{k \in b}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \in ran (k \in b ⟼ F (k))) \to (\underset{k \in b \cup \{l\}}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \in ran (k \in (b \cup \{l\}) ⟼ F (k))))$
97	14 20 26 32 48 96 5	findcard2d	$⊢ φ \to (\underset{k \in A}{\sum_{M}} F (k) = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \in ran (k \in A ⟼ F (k)))$
98	6	feqmptd	$⊢ φ \to F = (k \in A ⟼ F (k))$
99	98	oveq2d	$⊢ φ \to \sum_{M} F = \underset{k \in A}{\sum_{M}} F (k)$
100	99	eqeq1d	$⊢ φ \to (\sum_{M} F = \underset{˙}{0} \leftrightarrow \underset{k \in A}{\sum_{M}} F (k) = \underset{˙}{0})$
101	98	rneqd	$⊢ φ \to ran F = ran (k \in A ⟼ F (k))$
102	101	eleq2d	$⊢ φ \to (\underset{˙}{0} \in ran F \leftrightarrow \underset{˙}{0} \in ran (k \in A ⟼ F (k)))$
103	97 100 102	3bitr4d	$⊢ φ \to (\sum_{M} F = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \in ran F)$

Metamath Proof Explorer

Theorem domnprodeq0

Proof