Metamath Proof Explorer

Theorem 0ringidl

Description: The zero ideal is the only ideal of the trivial ring. (Contributed by Thierry Arnoux, 1-Jul-2024)

Ref Expression
Hypotheses 0ringidl.1 
|- B = ( Base ` R )
0ringidl.2 
|- .0. = ( 0g ` R )
Assertion 0ringidl 
|- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( LIdeal ` R ) = { { .0. } } )

Proof

Step Hyp Ref Expression
1 0ringidl.1 
 |-  B = ( Base ` R )
2 0ringidl.2 
 |-  .0. = ( 0g ` R )
3 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
4 1 3 lidlss 
 |-  ( i e. ( LIdeal ` R ) -> i C_ B )
5 4 adantl 
 |-  ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( LIdeal ` R ) ) -> i C_ B )
6 1 2 0ring 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> B = { .0. } )
7 6 adantr 
 |-  ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( LIdeal ` R ) ) -> B = { .0. } )
8 5 7 sseqtrd 
 |-  ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( LIdeal ` R ) ) -> i C_ { .0. } )
9 3 2 lidl0cl 
 |-  ( ( R e. Ring /\ i e. ( LIdeal ` R ) ) -> .0. e. i )
10 9 adantlr 
 |-  ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( LIdeal ` R ) ) -> .0. e. i )
11 10 snssd 
 |-  ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( LIdeal ` R ) ) -> { .0. } C_ i )
12 8 11 eqssd 
 |-  ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( LIdeal ` R ) ) -> i = { .0. } )
13 3 2 lidl0 
 |-  ( R e. Ring -> { .0. } e. ( LIdeal ` R ) )
14 13 adantr 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> { .0. } e. ( LIdeal ` R ) )
15 12 14 eqsnd 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( LIdeal ` R ) = { { .0. } } )