This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )