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 = Base R
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 = Base R
3 lidlmcl.t ⊢ · ˙ = ⋅ R
4 rlmvsca ⊢ ⋅ R = ⋅ ringLMod ⁡ R
5 3 4 eqtri ⊢ · ˙ = ⋅ ringLMod ⁡ R
6 5 oveqi ⊢ X · ˙ Y = X ⋅ ringLMod ⁡ R Y
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 → Base R = Base Scalar ⁡ ringLMod ⁡ R
16 2 15 eqtrid ⊢ R ∈ Ring → B = Base Scalar ⁡ ringLMod ⁡ R
17 16 eleq2d ⊢ R ∈ Ring → X ∈ B ↔ X ∈ Base Scalar ⁡ ringLMod ⁡ R
18 17 biimpa ⊢ R ∈ Ring ∧ X ∈ B → X ∈ Base Scalar ⁡ ringLMod ⁡ R
19 18 ad2ant2r ⊢ R ∈ Ring ∧ I ∈ U ∧ X ∈ B ∧ Y ∈ I → X ∈ Base Scalar ⁡ 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 ⊢ Base Scalar ⁡ ringLMod ⁡ R = Base Scalar ⁡ ringLMod ⁡ R
24 eqid ⊢ LSubSp ⁡ ringLMod ⁡ R = LSubSp ⁡ ringLMod ⁡ R
25 21 22 23 24 lssvscl ⊢ ringLMod ⁡ R ∈ LMod ∧ I ∈ LSubSp ⁡ ringLMod ⁡ R ∧ X ∈ Base Scalar ⁡ ringLMod ⁡ R ∧ Y ∈ I → X ⋅ ringLMod ⁡ R Y ∈ I
26 8 13 19 20 25 syl22anc ⊢ R ∈ Ring ∧ I ∈ U ∧ X ∈ B ∧ Y ∈ I → X ⋅ ringLMod ⁡ R Y ∈ I
27 6 26 eqeltrid ⊢ R ∈ Ring ∧ I ∈ U ∧ X ∈ B ∧ Y ∈ I → X · ˙ Y ∈ I