Metamath Proof Explorer

Theorem rprmnz

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

Ref Expression
Hypotheses rprmnz.p 
|- P = ( RPrime ` R )
rprmnz.0 
|- .0. = ( 0g ` R )
rprmnz.r 
|- ( ph -> R e. V )
rprmnz.q 
|- ( ph -> Q e. P )
Assertion rprmnz 
|- ( ph -> Q =/= .0. )

Proof

Step Hyp Ref Expression
1 rprmnz.p 
 |-  P = ( RPrime ` R )
2 rprmnz.0 
 |-  .0. = ( 0g ` R )
3 rprmnz.r 
 |-  ( ph -> R e. V )
4 rprmnz.q 
 |-  ( ph -> Q e. P )
5 eqidd 
 |-  ( ph -> ( ( Unit ` R ) u. { .0. } ) = ( ( Unit ` R ) u. { .0. } ) )
6 4 1 eleqtrdi 
 |-  ( ph -> Q e. ( RPrime ` R ) )
7 eqid 
 |-  ( Base ` R ) = ( Base ` R )
8 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
9 eqid 
 |-  ( ||r ` R ) = ( ||r ` R )
10 eqid 
 |-  ( .r ` R ) = ( .r ` R )
11 7 8 2 9 10 isrprm 
 |-  ( R e. V -> ( Q e. ( RPrime ` R ) <-> ( Q e. ( ( Base ` R ) \ ( ( Unit ` R ) u. { .0. } ) ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( Q ( ||r ` R ) ( x ( .r ` R ) y ) -> ( Q ( ||r ` R ) x \/ Q ( ||r ` R ) y ) ) ) ) )
12 11 simprbda 
 |-  ( ( R e. V /\ Q e. ( RPrime ` R ) ) -> Q e. ( ( Base ` R ) \ ( ( Unit ` R ) u. { .0. } ) ) )
13 3 6 12 syl2anc 
 |-  ( ph -> Q e. ( ( Base ` R ) \ ( ( Unit ` R ) u. { .0. } ) ) )
14 13 eldifbd 
 |-  ( ph -> -. Q e. ( ( Unit ` R ) u. { .0. } ) )
15 nelun 
 |-  ( ( ( Unit ` R ) u. { .0. } ) = ( ( Unit ` R ) u. { .0. } ) -> ( -. Q e. ( ( Unit ` R ) u. { .0. } ) <-> ( -. Q e. ( Unit ` R ) /\ -. Q e. { .0. } ) ) )
16 15 simplbda 
 |-  ( ( ( ( Unit ` R ) u. { .0. } ) = ( ( Unit ` R ) u. { .0. } ) /\ -. Q e. ( ( Unit ` R ) u. { .0. } ) ) -> -. Q e. { .0. } )
17 5 14 16 syl2anc 
 |-  ( ph -> -. Q e. { .0. } )
18 elsng 
 |-  ( Q e. P -> ( Q e. { .0. } <-> Q = .0. ) )
19 4 18 syl 
 |-  ( ph -> ( Q e. { .0. } <-> Q = .0. ) )
20 19 necon3bbid 
 |-  ( ph -> ( -. Q e. { .0. } <-> Q =/= .0. ) )
21 17 20 mpbid 
 |-  ( ph -> Q =/= .0. )