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

Metamath Proof Explorer

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