Theorem 2idl1

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

	Ref	Expression
Hypotheses	2idl0.u	⊢ 𝐼 = ( 2Ideal ‘ 𝑅 )
	2idl1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	2idl1	⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		2idl0.u	⊢ 𝐼 = ( 2Ideal ‘ 𝑅 )
2		2idl1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
4	3 2	lidl1	⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ ( LIdeal ‘ 𝑅 ) )
5		eqid	⊢ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) = ( LIdeal ‘ ( oppr ‘ 𝑅 ) )
6	5 2	ridl1	⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) )
7	4 6	elind	⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ ( ( LIdeal ‘ 𝑅 ) ∩ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) )
8		eqid	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
9	3 8 5 1	2idlval	⊢ 𝐼 = ( ( LIdeal ‘ 𝑅 ) ∩ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) )
10	7 9	eleqtrrdi	⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ 𝐼 )