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 ˙ = 0 R
Assertion 0ringidl R Ring B = 1 LIdeal R = 0 ˙

Proof

Step Hyp Ref Expression
1 0ringidl.1 B = Base R
2 0ringidl.2 0 ˙ = 0 R
3 eqid LIdeal R = LIdeal R
4 1 3 lidlss i LIdeal R i B
5 4 adantl R Ring B = 1 i LIdeal R i B
6 1 2 0ring R Ring B = 1 B = 0 ˙
7 6 adantr R Ring B = 1 i LIdeal R B = 0 ˙
8 5 7 sseqtrd R Ring B = 1 i LIdeal R i 0 ˙
9 3 2 lidl0cl R Ring i LIdeal R 0 ˙ i
10 9 adantlr R Ring B = 1 i LIdeal R 0 ˙ i
11 10 snssd R Ring B = 1 i LIdeal R 0 ˙ i
12 8 11 eqssd R Ring B = 1 i LIdeal R i = 0 ˙
13 3 2 lidl0 R Ring 0 ˙ LIdeal R
14 13 adantr R Ring B = 1 0 ˙ LIdeal R
15 12 14 eqsnd R Ring B = 1 LIdeal R = 0 ˙