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

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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
0ringidl.2 ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion 0ringidl ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ( LIdeal ‘ 𝑅 ) = { { 0 } } )

Proof

Step Hyp Ref Expression
1 0ringidl.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 0ringidl.2 ⊢ 0 = ( 0g ‘ 𝑅 )
3 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
4 1 3 lidlss ⊢ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) → 𝑖 ⊆ 𝐵 )
5 4 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑖 ⊆ 𝐵 )
6 1 2 0ring ⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → 𝐵 = { 0 } )
7 6 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝐵 = { 0 } )
8 5 7 sseqtrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑖 ⊆ { 0 } )
9 3 2 lidl0cl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) → 0 ∈ 𝑖 )
10 9 adantlr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) → 0 ∈ 𝑖 )
11 10 snssd ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) → { 0 } ⊆ 𝑖 )
12 8 11 eqssd ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑖 = { 0 } )
13 3 2 lidl0 ⊢ ( 𝑅 ∈ Ring → { 0 } ∈ ( LIdeal ‘ 𝑅 ) )
14 13 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → { 0 } ∈ ( LIdeal ‘ 𝑅 ) )
15 12 14 eqsnd ⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ( LIdeal ‘ 𝑅 ) = { { 0 } } )