Metamath Proof Explorer

Theorem lidlmcl

Description: An ideal is closed under left-multiplication by elements of the full ring. (Contributed by Stefan O'Rear, 3-Jan-2015)

Ref Expression
Hypotheses lidlcl.u ⊢U=LIdeal⁡R
lidlcl.b ⊢B=BaseR
lidlmcl.t ⊢·˙=⋅R
Assertion lidlmcl ⊢R∈Ring∧I∈U∧X∈B∧Y∈I→X·˙Y∈I

Proof

Step Hyp Ref Expression
1 lidlcl.u ⊢U=LIdeal⁡R
2 lidlcl.b ⊢B=BaseR
3 lidlmcl.t ⊢·˙=⋅R
4 rlmvsca ⊢⋅R=⋅ringLMod⁡R
5 3 4 eqtri ⊢·˙=⋅ringLMod⁡R
6 5 oveqi ⊢X·˙Y=X⋅ringLMod⁡RY
7 rlmlmod ⊢R∈Ring→ringLMod⁡R∈LMod
8 7 ad2antrr ⊢R∈Ring∧I∈U∧X∈B∧Y∈I→ringLMod⁡R∈LMod
9 simpr ⊢R∈Ring∧I∈U→I∈U
10 lidlval ⊢LIdeal⁡R=LSubSp⁡ringLMod⁡R
11 1 10 eqtri ⊢U=LSubSp⁡ringLMod⁡R
12 9 11 eleqtrdi ⊢R∈Ring∧I∈U→I∈LSubSp⁡ringLMod⁡R
13 12 adantr ⊢R∈Ring∧I∈U∧X∈B∧Y∈I→I∈LSubSp⁡ringLMod⁡R
14 rlmsca ⊢R∈Ring→R=Scalar⁡ringLMod⁡R
15 14 fveq2d ⊢R∈Ring→BaseR=BaseScalar⁡ringLMod⁡R
16 2 15 eqtrid ⊢R∈Ring→B=BaseScalar⁡ringLMod⁡R
17 16 eleq2d ⊢R∈Ring→X∈B↔X∈BaseScalar⁡ringLMod⁡R
18 17 biimpa ⊢R∈Ring∧X∈B→X∈BaseScalar⁡ringLMod⁡R
19 18 ad2ant2r ⊢R∈Ring∧I∈U∧X∈B∧Y∈I→X∈BaseScalar⁡ringLMod⁡R
20 simprr ⊢R∈Ring∧I∈U∧X∈B∧Y∈I→Y∈I
21 eqid ⊢Scalar⁡ringLMod⁡R=Scalar⁡ringLMod⁡R
22 eqid ⊢⋅ringLMod⁡R=⋅ringLMod⁡R
23 eqid ⊢BaseScalar⁡ringLMod⁡R=BaseScalar⁡ringLMod⁡R
24 eqid ⊢LSubSp⁡ringLMod⁡R=LSubSp⁡ringLMod⁡R
25 21 22 23 24 lssvscl ⊢ringLMod⁡R∈LMod∧I∈LSubSp⁡ringLMod⁡R∧X∈BaseScalar⁡ringLMod⁡R∧Y∈I→X⋅ringLMod⁡RY∈I
26 8 13 19 20 25 syl22anc ⊢R∈Ring∧I∈U∧X∈B∧Y∈I→X⋅ringLMod⁡RY∈I
27 6 26 eqeltrid ⊢R∈Ring∧I∈U∧X∈B∧Y∈I→X·˙Y∈I