Metamath Proof Explorer

Theorem rprmnz

Description: A ring prime is nonzero. (Contributed by Thierry Arnoux, 18-May-2025)

Ref Expression
Hypotheses rprmnz.p ⊢ 𝑃 = ( RPrime ‘ 𝑅 )
rprmnz.0 ⊢ 0 = ( 0g ‘ 𝑅 )
rprmnz.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
rprmnz.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
Assertion rprmnz ( 𝜑 → 𝑄 ≠ 0 )

Proof

Step Hyp Ref Expression
1 rprmnz.p ⊢ 𝑃 = ( RPrime ‘ 𝑅 )
2 rprmnz.0 ⊢ 0 = ( 0g ‘ 𝑅 )
3 rprmnz.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
4 rprmnz.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
5 eqidd ⊢ ( 𝜑 → ( ( Unit ‘ 𝑅 ) ∪ { 0 } ) = ( ( Unit ‘ 𝑅 ) ∪ { 0 } ) )
6 4 1 eleqtrdi ⊢ ( 𝜑 → 𝑄 ∈ ( RPrime ‘ 𝑅 ) )
7 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
9 eqid ⊢ ( ∥r ‘ 𝑅 ) = ( ∥r ‘ 𝑅 )
10 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
11 7 8 2 9 10 isrprm ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑄 ∈ ( RPrime ‘ 𝑅 ) ↔ ( 𝑄 ∈ ( ( Base ‘ 𝑅 ) ∖ ( ( Unit ‘ 𝑅 ) ∪ { 0 } ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑄 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) → ( 𝑄 ( ∥r ‘ 𝑅 ) 𝑥 ∨ 𝑄 ( ∥r ‘ 𝑅 ) 𝑦 ) ) ) ) )
12 11 simprbda ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑄 ∈ ( RPrime ‘ 𝑅 ) ) → 𝑄 ∈ ( ( Base ‘ 𝑅 ) ∖ ( ( Unit ‘ 𝑅 ) ∪ { 0 } ) ) )
13 3 6 12 syl2anc ⊢ ( 𝜑 → 𝑄 ∈ ( ( Base ‘ 𝑅 ) ∖ ( ( Unit ‘ 𝑅 ) ∪ { 0 } ) ) )
14 13 eldifbd ⊢ ( 𝜑 → ¬ 𝑄 ∈ ( ( Unit ‘ 𝑅 ) ∪ { 0 } ) )
15 nelun ⊢ ( ( ( Unit ‘ 𝑅 ) ∪ { 0 } ) = ( ( Unit ‘ 𝑅 ) ∪ { 0 } ) → ( ¬ 𝑄 ∈ ( ( Unit ‘ 𝑅 ) ∪ { 0 } ) ↔ ( ¬ 𝑄 ∈ ( Unit ‘ 𝑅 ) ∧ ¬ 𝑄 ∈ { 0 } ) ) )
16 15 simplbda ⊢ ( ( ( ( Unit ‘ 𝑅 ) ∪ { 0 } ) = ( ( Unit ‘ 𝑅 ) ∪ { 0 } ) ∧ ¬ 𝑄 ∈ ( ( Unit ‘ 𝑅 ) ∪ { 0 } ) ) → ¬ 𝑄 ∈ { 0 } )
17 5 14 16 syl2anc ⊢ ( 𝜑 → ¬ 𝑄 ∈ { 0 } )
18 elsng ⊢ ( 𝑄 ∈ 𝑃 → ( 𝑄 ∈ { 0 } ↔ 𝑄 = 0 ) )
19 4 18 syl ⊢ ( 𝜑 → ( 𝑄 ∈ { 0 } ↔ 𝑄 = 0 ) )
20 19 necon3bbid ⊢ ( 𝜑 → ( ¬ 𝑄 ∈ { 0 } ↔ 𝑄 ≠ 0 ) )
21 17 20 mpbid ⊢ ( 𝜑 → 𝑄 ≠ 0 )