Metamath Proof Explorer

Theorem prmringnzring

Description: A prime ring is a nonzero ring. (Contributed by AV, 26-Jun-2026)

Ref Expression
Assertion prmringnzring 
|- ( R e. PrmRing -> R e. NzRing )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
2 eqid 
 |-  ( PrmIdeal ` R ) = ( PrmIdeal ` R )
3 1 2 isprmrng 
 |-  ( R e. PrmRing <-> ( R e. Ring /\ { ( 0g ` R ) } e. ( PrmIdeal ` R ) ) )
4 eqid 
 |-  ( Base ` R ) = ( Base ` R )
5 4 0ringprmidl 
 |-  ( ( R e. Ring /\ ( # ` ( Base ` R ) ) = 1 ) -> ( PrmIdeal ` R ) = (/) )
6 eleq2 
 |-  ( ( PrmIdeal ` R ) = (/) -> ( { ( 0g ` R ) } e. ( PrmIdeal ` R ) <-> { ( 0g ` R ) } e. (/) ) )
7 noel 
 |-  -. { ( 0g ` R ) } e. (/)
8 7 pm2.21i 
 |-  ( { ( 0g ` R ) } e. (/) -> R e. NzRing )
9 6 8 biimtrdi 
 |-  ( ( PrmIdeal ` R ) = (/) -> ( { ( 0g ` R ) } e. ( PrmIdeal ` R ) -> R e. NzRing ) )
10 5 9 syl 
 |-  ( ( R e. Ring /\ ( # ` ( Base ` R ) ) = 1 ) -> ( { ( 0g ` R ) } e. ( PrmIdeal ` R ) -> R e. NzRing ) )
11 10 ex 
 |-  ( R e. Ring -> ( ( # ` ( Base ` R ) ) = 1 -> ( { ( 0g ` R ) } e. ( PrmIdeal ` R ) -> R e. NzRing ) ) )
12 0ringnnzr 
 |-  ( R e. Ring -> ( ( # ` ( Base ` R ) ) = 1 <-> -. R e. NzRing ) )
13 12 bicomd 
 |-  ( R e. Ring -> ( -. R e. NzRing <-> ( # ` ( Base ` R ) ) = 1 ) )
14 13 con1bid 
 |-  ( R e. Ring -> ( -. ( # ` ( Base ` R ) ) = 1 <-> R e. NzRing ) )
15 ax1w 
 |-  ( R e. Ring -> ( R e. NzRing -> ( { ( 0g ` R ) } e. ( PrmIdeal ` R ) -> R e. NzRing ) ) )
16 14 15 sylbid 
 |-  ( R e. Ring -> ( -. ( # ` ( Base ` R ) ) = 1 -> ( { ( 0g ` R ) } e. ( PrmIdeal ` R ) -> R e. NzRing ) ) )
17 11 16 pm2.61d 
 |-  ( R e. Ring -> ( { ( 0g ` R ) } e. ( PrmIdeal ` R ) -> R e. NzRing ) )
18 17 imp 
 |-  ( ( R e. Ring /\ { ( 0g ` R ) } e. ( PrmIdeal ` R ) ) -> R e. NzRing )
19 3 18 sylbi 
 |-  ( R e. PrmRing -> R e. NzRing )