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 ) = (/) )