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 ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
lidlcl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
lidlmcl.t ⊢ · = ( .r ‘ 𝑅 )
Assertion lidlmcl ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝐼 )

Proof

Step Hyp Ref Expression
1 lidlcl.u ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
2 lidlcl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 lidlmcl.t ⊢ · = ( .r ‘ 𝑅 )
4 rlmvsca ⊢ ( .r ‘ 𝑅 ) = ( ·𝑠 ‘ ( ringLMod ‘ 𝑅 ) )
5 3 4 eqtri ⊢ · = ( ·𝑠 ‘ ( ringLMod ‘ 𝑅 ) )
6 5 oveqi ⊢ ( 𝑋 · 𝑌 ) = ( 𝑋 ( ·𝑠 ‘ ( ringLMod ‘ 𝑅 ) ) 𝑌 )
7 rlmlmod ⊢ ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )
8 7 ad2antrr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → ( ringLMod ‘ 𝑅 ) ∈ LMod )
9 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 𝐼 ∈ 𝑈 )
10 lidlval ⊢ ( LIdeal ‘ 𝑅 ) = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
11 1 10 eqtri ⊢ 𝑈 = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
12 9 11 eleqtrdi ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 𝐼 ∈ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) )
13 12 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → 𝐼 ∈ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) )
14 rlmsca ⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
15 14 fveq2d ⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) )
16 2 15 syl5eq ⊢ ( 𝑅 ∈ Ring → 𝐵 = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) )
17 16 eleq2d ⊢ ( 𝑅 ∈ Ring → ( 𝑋 ∈ 𝐵 ↔ 𝑋 ∈ ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) ) )
18 17 biimpa ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) )
19 18 ad2ant2r ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → 𝑋 ∈ ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) )
20 simprr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → 𝑌 ∈ 𝐼 )
21 eqid ⊢ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) )
22 eqid ⊢ ( ·𝑠 ‘ ( ringLMod ‘ 𝑅 ) ) = ( ·𝑠 ‘ ( ringLMod ‘ 𝑅 ) )
23 eqid ⊢ ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
24 eqid ⊢ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
25 21 22 23 24 lssvscl ⊢ ( ( ( ( ringLMod ‘ 𝑅 ) ∈ LMod ∧ 𝐼 ∈ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) ) ∧ ( 𝑋 ∈ ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 ( ·𝑠 ‘ ( ringLMod ‘ 𝑅 ) ) 𝑌 ) ∈ 𝐼 )
26 8 13 19 20 25 syl22anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 ( ·𝑠 ‘ ( ringLMod ‘ 𝑅 ) ) 𝑌 ) ∈ 𝐼 )
27 6 26 eqeltrid ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝐼 )