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

Metamath Proof Explorer

Theorem 0ringprmidl

Description: The trivial ring does not have any prime ideal. (Contributed by Thierry Arnoux, 30-Jun-2024)

Ref Expression
Hypothesis 0ringprmidl.1 
|- B = ( Base ` R )
Assertion 0ringprmidl 
|- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( PrmIdeal ` R ) = (/) )

Proof

Step Hyp Ref Expression
1 0ringprmidl.1 
 |-  B = ( Base ` R )
2 prmidlssidl 
 |-  ( R e. Ring -> ( PrmIdeal ` R ) C_ ( LIdeal ` R ) )
3 2 adantr 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( PrmIdeal ` R ) C_ ( LIdeal ` R ) )
4 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
5 1 4 0ringidl 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( LIdeal ` R ) = { { ( 0g ` R ) } } )
6 3 5 sseqtrd 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( PrmIdeal ` R ) C_ { { ( 0g ` R ) } } )
7 6 sselda 
 |-  ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> i e. { { ( 0g ` R ) } } )
8 elsni 
 |-  ( i e. { { ( 0g ` R ) } } -> i = { ( 0g ` R ) } )
9 7 8 syl 
 |-  ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> i = { ( 0g ` R ) } )
10 eqid 
 |-  ( .r ` R ) = ( .r ` R )
11 1 10 prmidlnr 
 |-  ( ( R e. Ring /\ i e. ( PrmIdeal ` R ) ) -> i =/= B )
12 11 adantlr 
 |-  ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> i =/= B )
13 1 4 0ring 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> B = { ( 0g ` R ) } )
14 13 adantr 
 |-  ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> B = { ( 0g ` R ) } )
15 12 14 neeqtrd 
 |-  ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> i =/= { ( 0g ` R ) } )
16 15 neneqd 
 |-  ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> -. i = { ( 0g ` R ) } )
17 9 16 pm2.65da 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> -. i e. ( PrmIdeal ` R ) )
18 17 eq0rdv 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( PrmIdeal ` R ) = (/) )