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 } } )