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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	domnprodn0.2	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
	domnprodn0.3	⊢ 0 = ( 0g ‘ 𝑅 )
	domnprodn0.4	⊢ ( 𝜑 → 𝑅 ∈ Domn )
	domnprodn0.5	⊢ ( 𝜑 → 𝐹 ∈ Word ( 𝐵 ∖ { 0 } ) )
Assertion	domnprodn0	⊢ ( 𝜑 → ( 𝑀 Σg 𝐹 ) ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		domnprodn0.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		domnprodn0.2	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
3		domnprodn0.3	⊢ 0 = ( 0g ‘ 𝑅 )
4		domnprodn0.4	⊢ ( 𝜑 → 𝑅 ∈ Domn )
5		domnprodn0.5	⊢ ( 𝜑 → 𝐹 ∈ Word ( 𝐵 ∖ { 0 } ) )
6		oveq2	⊢ ( 𝑔 = ∅ → ( 𝑀 Σg 𝑔 ) = ( 𝑀 Σg ∅ ) )
7	6	neeq1d	⊢ ( 𝑔 = ∅ → ( ( 𝑀 Σg 𝑔 ) ≠ 0 ↔ ( 𝑀 Σg ∅ ) ≠ 0 ) )
8	7	imbi2d	⊢ ( 𝑔 = ∅ → ( ( 𝜑 → ( 𝑀 Σg 𝑔 ) ≠ 0 ) ↔ ( 𝜑 → ( 𝑀 Σg ∅ ) ≠ 0 ) ) )
9		oveq2	⊢ ( 𝑔 = 𝑓 → ( 𝑀 Σg 𝑔 ) = ( 𝑀 Σg 𝑓 ) )
10	9	neeq1d	⊢ ( 𝑔 = 𝑓 → ( ( 𝑀 Σg 𝑔 ) ≠ 0 ↔ ( 𝑀 Σg 𝑓 ) ≠ 0 ) )
11	10	imbi2d	⊢ ( 𝑔 = 𝑓 → ( ( 𝜑 → ( 𝑀 Σg 𝑔 ) ≠ 0 ) ↔ ( 𝜑 → ( 𝑀 Σg 𝑓 ) ≠ 0 ) ) )
12		oveq2	⊢ ( 𝑔 = ( 𝑓 ++ ⟨“ 𝑥 ”⟩ ) → ( 𝑀 Σg 𝑔 ) = ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑥 ”⟩ ) ) )
13	12	neeq1d	⊢ ( 𝑔 = ( 𝑓 ++ ⟨“ 𝑥 ”⟩ ) → ( ( 𝑀 Σg 𝑔 ) ≠ 0 ↔ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑥 ”⟩ ) ) ≠ 0 ) )
14	13	imbi2d	⊢ ( 𝑔 = ( 𝑓 ++ ⟨“ 𝑥 ”⟩ ) → ( ( 𝜑 → ( 𝑀 Σg 𝑔 ) ≠ 0 ) ↔ ( 𝜑 → ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑥 ”⟩ ) ) ≠ 0 ) ) )
15		oveq2	⊢ ( 𝑔 = 𝐹 → ( 𝑀 Σg 𝑔 ) = ( 𝑀 Σg 𝐹 ) )
16	15	neeq1d	⊢ ( 𝑔 = 𝐹 → ( ( 𝑀 Σg 𝑔 ) ≠ 0 ↔ ( 𝑀 Σg 𝐹 ) ≠ 0 ) )
17	16	imbi2d	⊢ ( 𝑔 = 𝐹 → ( ( 𝜑 → ( 𝑀 Σg 𝑔 ) ≠ 0 ) ↔ ( 𝜑 → ( 𝑀 Σg 𝐹 ) ≠ 0 ) ) )
18		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
19	2 18	ringidval	⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑀 )
20	19	gsum0	⊢ ( 𝑀 Σg ∅ ) = ( 1r ‘ 𝑅 )
21	20	a1i	⊢ ( 𝜑 → ( 𝑀 Σg ∅ ) = ( 1r ‘ 𝑅 ) )
22		domnnzr	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
23	18 3	nzrnz	⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ 0 )
24	4 22 23	3syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ≠ 0 )
25	21 24	eqnetrd	⊢ ( 𝜑 → ( 𝑀 Σg ∅ ) ≠ 0 )
26		domnring	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Ring )
27	2	ringmgp	⊢ ( 𝑅 ∈ Ring → 𝑀 ∈ Mnd )
28	4 26 27	3syl	⊢ ( 𝜑 → 𝑀 ∈ Mnd )
29	28	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ Word ( 𝐵 ∖ { 0 } ) ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → 𝑀 ∈ Mnd )
30		difssd	⊢ ( 𝜑 → ( 𝐵 ∖ { 0 } ) ⊆ 𝐵 )
31		sswrd	⊢ ( ( 𝐵 ∖ { 0 } ) ⊆ 𝐵 → Word ( 𝐵 ∖ { 0 } ) ⊆ Word 𝐵 )
32	30 31	syl	⊢ ( 𝜑 → Word ( 𝐵 ∖ { 0 } ) ⊆ Word 𝐵 )
33	32	sselda	⊢ ( ( 𝜑 ∧ 𝑓 ∈ Word ( 𝐵 ∖ { 0 } ) ) → 𝑓 ∈ Word 𝐵 )
34	33	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ Word ( 𝐵 ∖ { 0 } ) ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → 𝑓 ∈ Word 𝐵 )
35		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ Word ( 𝐵 ∖ { 0 } ) ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → 𝑥 ∈ ( 𝐵 ∖ { 0 } ) )
36	35	eldifad	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ Word ( 𝐵 ∖ { 0 } ) ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → 𝑥 ∈ 𝐵 )
37	2 1	mgpbas	⊢ 𝐵 = ( Base ‘ 𝑀 )
38		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
39	2 38	mgpplusg	⊢ ( .r ‘ 𝑅 ) = ( +g ‘ 𝑀 )
40	37 39	gsumccatsn	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑓 ∈ Word 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑥 ”⟩ ) ) = ( ( 𝑀 Σg 𝑓 ) ( .r ‘ 𝑅 ) 𝑥 ) )
41	29 34 36 40	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ Word ( 𝐵 ∖ { 0 } ) ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑥 ”⟩ ) ) = ( ( 𝑀 Σg 𝑓 ) ( .r ‘ 𝑅 ) 𝑥 ) )
42	4	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ Word ( 𝐵 ∖ { 0 } ) ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → 𝑅 ∈ Domn )
43	37	gsumwcl	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑓 ∈ Word 𝐵 ) → ( 𝑀 Σg 𝑓 ) ∈ 𝐵 )
44	29 34 43	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ Word ( 𝐵 ∖ { 0 } ) ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ( 𝑀 Σg 𝑓 ) ∈ 𝐵 )
45		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ Word ( 𝐵 ∖ { 0 } ) ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ( 𝑀 Σg 𝑓 ) ≠ 0 )
46		eldifsni	⊢ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) → 𝑥 ≠ 0 )
47	35 46	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ Word ( 𝐵 ∖ { 0 } ) ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → 𝑥 ≠ 0 )
48	1 38 3	domnmuln0	⊢ ( ( 𝑅 ∈ Domn ∧ ( ( 𝑀 Σg 𝑓 ) ∈ 𝐵 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( ( 𝑀 Σg 𝑓 ) ( .r ‘ 𝑅 ) 𝑥 ) ≠ 0 )
49	42 44 45 36 47 48	syl122anc	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ Word ( 𝐵 ∖ { 0 } ) ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ( ( 𝑀 Σg 𝑓 ) ( .r ‘ 𝑅 ) 𝑥 ) ≠ 0 )
50	41 49	eqnetrd	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ Word ( 𝐵 ∖ { 0 } ) ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑥 ”⟩ ) ) ≠ 0 )
51	50	ex	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ Word ( 𝐵 ∖ { 0 } ) ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( 𝑀 Σg 𝑓 ) ≠ 0 → ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑥 ”⟩ ) ) ≠ 0 ) )
52	51	anasss	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ Word ( 𝐵 ∖ { 0 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( ( 𝑀 Σg 𝑓 ) ≠ 0 → ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑥 ”⟩ ) ) ≠ 0 ) )
53	52	expcom	⊢ ( ( 𝑓 ∈ Word ( 𝐵 ∖ { 0 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝜑 → ( ( 𝑀 Σg 𝑓 ) ≠ 0 → ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑥 ”⟩ ) ) ≠ 0 ) ) )
54	53	a2d	⊢ ( ( 𝑓 ∈ Word ( 𝐵 ∖ { 0 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( 𝜑 → ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ( 𝜑 → ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑥 ”⟩ ) ) ≠ 0 ) ) )
55	8 11 14 17 25 54	wrdind	⊢ ( 𝐹 ∈ Word ( 𝐵 ∖ { 0 } ) → ( 𝜑 → ( 𝑀 Σg 𝐹 ) ≠ 0 ) )
56	5 55	mpcom	⊢ ( 𝜑 → ( 𝑀 Σg 𝐹 ) ≠ 0 )