Metamath Proof Explorer

Theorem lidl0cl

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

Ref Expression
Hypotheses lidlcl.u ⊢ U = LIdeal ⁡ R
lidl0cl.z ⊢ 0 ˙ = 0 R
Assertion lidl0cl ⊢ R ∈ Ring ∧ I ∈ U → 0 ˙ ∈ I

Proof

Step Hyp Ref Expression
1 lidlcl.u ⊢ U = LIdeal ⁡ R
2 lidl0cl.z ⊢ 0 ˙ = 0 R
3 rlm0 ⊢ 0 R = 0 ringLMod ⁡ R
4 2 3 eqtri ⊢ 0 ˙ = 0 ringLMod ⁡ R
5 rlmlmod ⊢ R ∈ Ring → ringLMod ⁡ R ∈ LMod
6 simpr ⊢ R ∈ Ring ∧ I ∈ U → I ∈ U
7 lidlval ⊢ LIdeal ⁡ R = LSubSp ⁡ ringLMod ⁡ R
8 1 7 eqtri ⊢ U = LSubSp ⁡ ringLMod ⁡ R
9 6 8 eleqtrdi ⊢ R ∈ Ring ∧ I ∈ U → I ∈ LSubSp ⁡ ringLMod ⁡ R
10 eqid ⊢ 0 ringLMod ⁡ R = 0 ringLMod ⁡ R
11 eqid ⊢ LSubSp ⁡ ringLMod ⁡ R = LSubSp ⁡ ringLMod ⁡ R
12 10 11 lss0cl ⊢ ringLMod ⁡ R ∈ LMod ∧ I ∈ LSubSp ⁡ ringLMod ⁡ R → 0 ringLMod ⁡ R ∈ I
13 5 9 12 syl2an2r ⊢ R ∈ Ring ∧ I ∈ U → 0 ringLMod ⁡ R ∈ I
14 4 13 eqeltrid ⊢ R ∈ Ring ∧ I ∈ U → 0 ˙ ∈ I