# Metamath Proof Explorer

## Theorem lidl0cl

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

Ref Expression
Hypotheses lidlcl.u ${⊢}{U}=\mathrm{LIdeal}\left({R}\right)$
lidl0cl.z
Assertion lidl0cl

### Proof

Step Hyp Ref Expression
1 lidlcl.u ${⊢}{U}=\mathrm{LIdeal}\left({R}\right)$
2 lidl0cl.z
3 rlm0 ${⊢}{0}_{{R}}={0}_{\mathrm{ringLMod}\left({R}\right)}$
4 2 3 eqtri
5 rlmlmod ${⊢}{R}\in \mathrm{Ring}\to \mathrm{ringLMod}\left({R}\right)\in \mathrm{LMod}$
6 simpr ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {U}\right)\to {I}\in {U}$
7 lidlval ${⊢}\mathrm{LIdeal}\left({R}\right)=\mathrm{LSubSp}\left(\mathrm{ringLMod}\left({R}\right)\right)$
8 1 7 eqtri ${⊢}{U}=\mathrm{LSubSp}\left(\mathrm{ringLMod}\left({R}\right)\right)$
9 6 8 eleqtrdi ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {U}\right)\to {I}\in \mathrm{LSubSp}\left(\mathrm{ringLMod}\left({R}\right)\right)$
10 eqid ${⊢}{0}_{\mathrm{ringLMod}\left({R}\right)}={0}_{\mathrm{ringLMod}\left({R}\right)}$
11 eqid ${⊢}\mathrm{LSubSp}\left(\mathrm{ringLMod}\left({R}\right)\right)=\mathrm{LSubSp}\left(\mathrm{ringLMod}\left({R}\right)\right)$
12 10 11 lss0cl ${⊢}\left(\mathrm{ringLMod}\left({R}\right)\in \mathrm{LMod}\wedge {I}\in \mathrm{LSubSp}\left(\mathrm{ringLMod}\left({R}\right)\right)\right)\to {0}_{\mathrm{ringLMod}\left({R}\right)}\in {I}$
13 5 9 12 syl2an2r ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {U}\right)\to {0}_{\mathrm{ringLMod}\left({R}\right)}\in {I}$
14 4 13 eqeltrid