Theorem domnprodn0

Description: In a domain, a finite product of nonzero terms is nonzero. (Contributed by Thierry Arnoux, 6-Jun-2025)

	Ref	Expression
Hypotheses	domnprodn0.1	$$⊢B={\mathrm{Base}}_R$$
	domnprodn0.2	$$⊢M={\mathrm{mulGrp}}_R$$
	domnprodn0.3	$$⊢\underset{\dot{}}{0}=0_R$$
	domnprodn0.4	$$⊢\phi \to R\in \mathrm{Domn}$$
	domnprodn0.5	$$⊢\phi \to F\in \mathrm{Word}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
Assertion	domnprodn0	$$⊢\phi \to {\sum }_{M}F\ne \underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		domnprodn0.1	$$⊢B={\mathrm{Base}}_R$$
2		domnprodn0.2	$$⊢M={\mathrm{mulGrp}}_R$$
3		domnprodn0.3	$$⊢\underset{\dot{}}{0}=0_R$$
4		domnprodn0.4	$$⊢\phi \to R\in \mathrm{Domn}$$
5		domnprodn0.5	$$⊢\phi \to F\in \mathrm{Word}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
6		oveq2	$$⊢g=\varnothing \to {\sum }_{M}g={\sum }_M\varnothing$$
7	6	neeq1d	$$⊢g=\varnothing \to \left({\sum }_{M}g\ne \underset{\dot{}}{0}\leftrightarrow {\sum }_M\varnothing \ne \underset{\dot{}}{0}\right)$$
8	7	imbi2d	$$⊢g=\varnothing \to \left(\left(\phi \to {\sum }_{M}g\ne \underset{\dot{}}{0}\right)\leftrightarrow \left(\phi \to {\sum }_M\varnothing \ne \underset{\dot{}}{0}\right)\right)$$
9		oveq2	$$⊢g=f\to {\sum }_{M}g={\sum }_{M}f$$
10	9	neeq1d	$$⊢g=f\to \left({\sum }_{M}g\ne \underset{\dot{}}{0}\leftrightarrow {\sum }_{M}f\ne \underset{\dot{}}{0}\right)$$
11	10	imbi2d	$$⊢g=f\to \left(\left(\phi \to {\sum }_{M}g\ne \underset{\dot{}}{0}\right)\leftrightarrow \left(\phi \to {\sum }_{M}f\ne \underset{\dot{}}{0}\right)\right)$$
12		oveq2	$$⊢g=f\mathrm{++}⟨“x”⟩\to {\sum }_{M}g={\sum }_M\left(f\mathrm{++}⟨“x”⟩\right)$$
13	12	neeq1d	$$⊢g=f\mathrm{++}⟨“x”⟩\to \left({\sum }_{M}g\ne \underset{\dot{}}{0}\leftrightarrow {\sum }_M\left(f\mathrm{++}⟨“x”⟩\right)\ne \underset{\dot{}}{0}\right)$$
14	13	imbi2d	$$⊢g=f\mathrm{++}⟨“x”⟩\to \left(\left(\phi \to {\sum }_{M}g\ne \underset{\dot{}}{0}\right)\leftrightarrow \left(\phi \to {\sum }_M\left(f\mathrm{++}⟨“x”⟩\right)\ne \underset{\dot{}}{0}\right)\right)$$
15		oveq2	$$⊢g=F\to {\sum }_{M}g={\sum }_{M}F$$
16	15	neeq1d	$$⊢g=F\to \left({\sum }_{M}g\ne \underset{\dot{}}{0}\leftrightarrow {\sum }_{M}F\ne \underset{\dot{}}{0}\right)$$
17	16	imbi2d	$$⊢g=F\to \left(\left(\phi \to {\sum }_{M}g\ne \underset{\dot{}}{0}\right)\leftrightarrow \left(\phi \to {\sum }_{M}F\ne \underset{\dot{}}{0}\right)\right)$$
18		eqid	$$⊢1_R=1_R$$
19	2 18	ringidval	$$⊢1_R=0_M$$
20	19	gsum0	$$⊢{\sum }_M\varnothing =1_R$$
21	20	a1i	$$⊢\phi \to {\sum }_M\varnothing =1_R$$
22		domnnzr	$$⊢R\in \mathrm{Domn}\to R\in \mathrm{NzRing}$$
23	18 3	nzrnz	$$⊢R\in \mathrm{NzRing}\to 1_R\ne \underset{\dot{}}{0}$$
24	4 22 23	3syl	$$⊢\phi \to 1_R\ne \underset{\dot{}}{0}$$
25	21 24	eqnetrd	$$⊢\phi \to {\sum }_M\varnothing \ne \underset{\dot{}}{0}$$
26		domnring	$$⊢R\in \mathrm{Domn}\to R\in \mathrm{Ring}$$
27	2	ringmgp	$$⊢R\in \mathrm{Ring}\to M\in \mathrm{Mnd}$$
28	4 26 27	3syl	$$⊢\phi \to M\in \mathrm{Mnd}$$
29	28	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge f\in \mathrm{Word}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge {\sum }_{M}f\ne \underset{\dot{}}{0}\right)\to M\in \mathrm{Mnd}$$
30		difssd	$$⊢\phi \to B\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq B$$
31		sswrd	$$⊢B\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq B\to \mathrm{Word}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\subseteq \mathrm{Word}B$$
32	30 31	syl	$$⊢\phi \to \mathrm{Word}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\subseteq \mathrm{Word}B$$
33	32	sselda	$$⊢\left(\phi \wedge f\in \mathrm{Word}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to f\in \mathrm{Word}B$$
34	33	ad2antrr	$$⊢\left(\left(\left(\phi \wedge f\in \mathrm{Word}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge {\sum }_{M}f\ne \underset{\dot{}}{0}\right)\to f\in \mathrm{Word}B$$
35		simplr	$$⊢\left(\left(\left(\phi \wedge f\in \mathrm{Word}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge {\sum }_{M}f\ne \underset{\dot{}}{0}\right)\to x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
36	35	eldifad	$$⊢\left(\left(\left(\phi \wedge f\in \mathrm{Word}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge {\sum }_{M}f\ne \underset{\dot{}}{0}\right)\to x\in B$$
37	2 1	mgpbas	$$⊢B={\mathrm{Base}}_M$$
38		eqid	$$⊢{\cdot }_R={\cdot }_R$$
39	2 38	mgpplusg	$$⊢{\cdot }_R={+}_M$$
40	37 39	gsumccatsn	$$⊢\left(M\in \mathrm{Mnd}\wedge f\in \mathrm{Word}B\wedge x\in B\right)\to {\sum }_M\left(f\mathrm{++}⟨“x”⟩\right)=\left({\sum }_M,f\right){\cdot }_{R}x$$
41	29 34 36 40	syl3anc	$$⊢\left(\left(\left(\phi \wedge f\in \mathrm{Word}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge {\sum }_{M}f\ne \underset{\dot{}}{0}\right)\to {\sum }_M\left(f\mathrm{++}⟨“x”⟩\right)=\left({\sum }_M,f\right){\cdot }_{R}x$$
42	4	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge f\in \mathrm{Word}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge {\sum }_{M}f\ne \underset{\dot{}}{0}\right)\to R\in \mathrm{Domn}$$
43	37	gsumwcl	$$⊢\left(M\in \mathrm{Mnd}\wedge f\in \mathrm{Word}B\right)\to {\sum }_{M}f\in B$$
44	29 34 43	syl2anc	$$⊢\left(\left(\left(\phi \wedge f\in \mathrm{Word}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge {\sum }_{M}f\ne \underset{\dot{}}{0}\right)\to {\sum }_{M}f\in B$$
45		simpr	$$⊢\left(\left(\left(\phi \wedge f\in \mathrm{Word}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge {\sum }_{M}f\ne \underset{\dot{}}{0}\right)\to {\sum }_{M}f\ne \underset{\dot{}}{0}$$
46		eldifsni	$$⊢x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to x\ne \underset{\dot{}}{0}$$
47	35 46	syl	$$⊢\left(\left(\left(\phi \wedge f\in \mathrm{Word}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge {\sum }_{M}f\ne \underset{\dot{}}{0}\right)\to x\ne \underset{\dot{}}{0}$$
48	1 38 3	domnmuln0	$$⊢\left(R\in \mathrm{Domn}\wedge \left({\sum }_{M}f\in B\wedge {\sum }_{M}f\ne \underset{\dot{}}{0}\right)\wedge \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\right)\to \left({\sum }_M,f\right){\cdot }_{R}x\ne \underset{\dot{}}{0}$$
49	42 44 45 36 47 48	syl122anc	$$⊢\left(\left(\left(\phi \wedge f\in \mathrm{Word}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge {\sum }_{M}f\ne \underset{\dot{}}{0}\right)\to \left({\sum }_M,f\right){\cdot }_{R}x\ne \underset{\dot{}}{0}$$
50	41 49	eqnetrd	$$⊢\left(\left(\left(\phi \wedge f\in \mathrm{Word}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge {\sum }_{M}f\ne \underset{\dot{}}{0}\right)\to {\sum }_M\left(f\mathrm{++}⟨“x”⟩\right)\ne \underset{\dot{}}{0}$$
51	50	ex	$$⊢\left(\left(\phi \wedge f\in \mathrm{Word}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left({\sum }_{M}f\ne \underset{\dot{}}{0}\to {\sum }_M\left(f\mathrm{++}⟨“x”⟩\right)\ne \underset{\dot{}}{0}\right)$$
52	51	anasss	$$⊢\left(\phi \wedge \left(f\in \mathrm{Word}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\to \left({\sum }_{M}f\ne \underset{\dot{}}{0}\to {\sum }_M\left(f\mathrm{++}⟨“x”⟩\right)\ne \underset{\dot{}}{0}\right)$$
53	52	expcom	$$⊢\left(f\in \mathrm{Word}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(\phi \to \left({\sum }_{M}f\ne \underset{\dot{}}{0}\to {\sum }_M\left(f\mathrm{++}⟨“x”⟩\right)\ne \underset{\dot{}}{0}\right)\right)$$
54	53	a2d	$$⊢\left(f\in \mathrm{Word}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge x\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(\left(\phi \to {\sum }_{M}f\ne \underset{\dot{}}{0}\right)\to \left(\phi \to {\sum }_M\left(f\mathrm{++}⟨“x”⟩\right)\ne \underset{\dot{}}{0}\right)\right)$$
55	8 11 14 17 25 54	wrdind	$$⊢F\in \mathrm{Word}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to \left(\phi \to {\sum }_{M}F\ne \underset{\dot{}}{0}\right)$$
56	5 55	mpcom	$$⊢\phi \to {\sum }_{M}F\ne \underset{\dot{}}{0}$$