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 Could not format assertion : No typesetting found for |- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( PrmIdeal ` R ) = (/) ) with typecode |-

Proof

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