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

Metamath Proof Explorer

Theorem lidl0cl

Description: An ideal contains 0. (Contributed by Stefan O'Rear, 3-Jan-2015)

Ref Expression
Hypotheses lidlcl.u ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
lidl0cl.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion lidl0cl ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 0 ∈ 𝐼 )

Proof

Step Hyp Ref Expression
1 lidlcl.u ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
2 lidl0cl.z ⊢ 0 = ( 0g ‘ 𝑅 )
3 rlm0 ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ ( ringLMod ‘ 𝑅 ) )
4 2 3 eqtri ⊢ 0 = ( 0g ‘ ( ringLMod ‘ 𝑅 ) )
5 rlmlmod ⊢ ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )
6 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 𝐼 ∈ 𝑈 )
7 lidlval ⊢ ( LIdeal ‘ 𝑅 ) = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
8 1 7 eqtri ⊢ 𝑈 = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
9 6 8 eleqtrdi ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 𝐼 ∈ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) )
10 eqid ⊢ ( 0g ‘ ( ringLMod ‘ 𝑅 ) ) = ( 0g ‘ ( ringLMod ‘ 𝑅 ) )
11 eqid ⊢ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
12 10 11 lss0cl ⊢ ( ( ( ringLMod ‘ 𝑅 ) ∈ LMod ∧ 𝐼 ∈ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) ) → ( 0g ‘ ( ringLMod ‘ 𝑅 ) ) ∈ 𝐼 )
13 5 9 12 syl2an2r ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( 0g ‘ ( ringLMod ‘ 𝑅 ) ) ∈ 𝐼 )
14 4 13 eqeltrid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 0 ∈ 𝐼 )