Theorem 2idl0

Description: Every ring contains a zero two-sided ideal. (Contributed by AV, 13-Feb-2025)

	Ref	Expression
Hypotheses	2idl0.u	⊢ 𝐼 = ( 2Ideal ‘ 𝑅 )
	2idl0.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	2idl0	⊢ ( 𝑅 ∈ Ring → { 0 } ∈ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		2idl0.u	⊢ 𝐼 = ( 2Ideal ‘ 𝑅 )
2		2idl0.z	⊢ 0 = ( 0g ‘ 𝑅 )
3		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
4	3 2	lidl0	⊢ ( 𝑅 ∈ Ring → { 0 } ∈ ( LIdeal ‘ 𝑅 ) )
5		eqid	⊢ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) = ( LIdeal ‘ ( oppr ‘ 𝑅 ) )
6	5 2	ridl0	⊢ ( 𝑅 ∈ Ring → { 0 } ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) )
7	4 6	elind	⊢ ( 𝑅 ∈ Ring → { 0 } ∈ ( ( LIdeal ‘ 𝑅 ) ∩ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) )
8		eqid	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
9	3 8 5 1	2idlval	⊢ 𝐼 = ( ( LIdeal ‘ 𝑅 ) ∩ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) )
10	7 9	eleqtrrdi	⊢ ( 𝑅 ∈ Ring → { 0 } ∈ 𝐼 )