Metamath Proof Explorer

Theorem 0ringirng

Description: A zero ring R has no integral elements. (Contributed by Thierry Arnoux, 5-Feb-2025)

Ref Expression
Hypotheses irngval.o 
|- O = ( R evalSub1 S )
irngval.u 
|- U = ( R |`s S )
irngval.b 
|- B = ( Base ` R )
irngval.0 
|- .0. = ( 0g ` R )
elirng.r 
|- ( ph -> R e. CRing )
elirng.s 
|- ( ph -> S e. ( SubRing ` R ) )
0ringirng.1 
|- ( ph -> -. R e. NzRing )
Assertion 0ringirng 
|- ( ph -> ( R IntgRing S ) = (/) )

Proof

Step Hyp Ref Expression
1 irngval.o 
 |-  O = ( R evalSub1 S )
2 irngval.u 
 |-  U = ( R |`s S )
3 irngval.b 
 |-  B = ( Base ` R )
4 irngval.0 
 |-  .0. = ( 0g ` R )
5 elirng.r 
 |-  ( ph -> R e. CRing )
6 elirng.s 
 |-  ( ph -> S e. ( SubRing ` R ) )
7 0ringirng.1 
 |-  ( ph -> -. R e. NzRing )
8 rex0 
 |-  -. E. p e. (/) ( ( O ` p ) ` x ) = .0.
9 eqid 
 |-  ( Monic1p ` U ) = ( Monic1p ` U )
10 eqid 
 |-  ( Base ` U ) = ( Base ` U )
11 2 subrgring 
 |-  ( S e. ( SubRing ` R ) -> U e. Ring )
12 6 11 syl 
 |-  ( ph -> U e. Ring )
13 5 crngringd 
 |-  ( ph -> R e. Ring )
14 3 fveq2i 
 |-  ( # ` B ) = ( # ` ( Base ` R ) )
15 0ringnnzr 
 |-  ( R e. Ring -> ( ( # ` ( Base ` R ) ) = 1 <-> -. R e. NzRing ) )
16 15 biimpar 
 |-  ( ( R e. Ring /\ -. R e. NzRing ) -> ( # ` ( Base ` R ) ) = 1 )
17 13 7 16 syl2anc 
 |-  ( ph -> ( # ` ( Base ` R ) ) = 1 )
18 14 17 eqtrid 
 |-  ( ph -> ( # ` B ) = 1 )
19 3 subrgss 
 |-  ( S e. ( SubRing ` R ) -> S C_ B )
20 2 3 ressbas2 
 |-  ( S C_ B -> S = ( Base ` U ) )
21 6 19 20 3syl 
 |-  ( ph -> S = ( Base ` U ) )
22 21 6 eqeltrrd 
 |-  ( ph -> ( Base ` U ) e. ( SubRing ` R ) )
23 3 13 18 22 0ringsubrg 
 |-  ( ph -> ( # ` ( Base ` U ) ) = 1 )
24 9 10 12 23 0ringmon1p 
 |-  ( ph -> ( Monic1p ` U ) = (/) )
25 24 rexeqdv 
 |-  ( ph -> ( E. p e. ( Monic1p ` U ) ( ( O ` p ) ` x ) = .0. <-> E. p e. (/) ( ( O ` p ) ` x ) = .0. ) )
26 8 25 mtbiri 
 |-  ( ph -> -. E. p e. ( Monic1p ` U ) ( ( O ` p ) ` x ) = .0. )
27 1 2 3 4 5 6 elirng 
 |-  ( ph -> ( x e. ( R IntgRing S ) <-> ( x e. B /\ E. p e. ( Monic1p ` U ) ( ( O ` p ) ` x ) = .0. ) ) )
28 27 simplbda 
 |-  ( ( ph /\ x e. ( R IntgRing S ) ) -> E. p e. ( Monic1p ` U ) ( ( O ` p ) ` x ) = .0. )
29 26 28 mtand 
 |-  ( ph -> -. x e. ( R IntgRing S ) )
30 29 eq0rdv 
 |-  ( ph -> ( R IntgRing S ) = (/) )