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
|- .x. = ( .r ` R )
Assertion lidlmcl
|- ( ( ( R e. Ring /\ I e. U ) /\ ( X e. B /\ Y e. I ) ) -> ( X .x. Y ) e. I )

Proof

Step Hyp Ref Expression
1 lidlcl.u
 |-  U = ( LIdeal ` R )
2 lidlcl.b
 |-  B = ( Base ` R )
3 lidlmcl.t
 |-  .x. = ( .r ` R )
4 rlmvsca
 |-  ( .r ` R ) = ( .s ` ( ringLMod ` R ) )
5 3 4 eqtri
 |-  .x. = ( .s ` ( ringLMod ` R ) )
6 5 oveqi
 |-  ( X .x. Y ) = ( X ( .s ` ( ringLMod ` R ) ) Y )
7 rlmlmod
 |-  ( R e. Ring -> ( ringLMod ` R ) e. LMod )
8 7 ad2antrr
 |-  ( ( ( R e. Ring /\ I e. U ) /\ ( X e. B /\ Y e. I ) ) -> ( ringLMod ` R ) e. LMod )
9 simpr
 |-  ( ( R e. Ring /\ I e. U ) -> I e. U )
10 lidlval
 |-  ( LIdeal ` R ) = ( LSubSp ` ( ringLMod ` R ) )
11 1 10 eqtri
 |-  U = ( LSubSp ` ( ringLMod ` R ) )
12 9 11 eleqtrdi
 |-  ( ( R e. Ring /\ I e. U ) -> I e. ( LSubSp ` ( ringLMod ` R ) ) )
13 12 adantr
 |-  ( ( ( R e. Ring /\ I e. U ) /\ ( X e. B /\ Y e. I ) ) -> I e. ( LSubSp ` ( ringLMod ` R ) ) )
14 rlmsca
 |-  ( R e. Ring -> R = ( Scalar ` ( ringLMod ` R ) ) )
15 14 fveq2d
 |-  ( R e. Ring -> ( Base ` R ) = ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) )
16 2 15 eqtrid
 |-  ( R e. Ring -> B = ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) )
17 16 eleq2d
 |-  ( R e. Ring -> ( X e. B <-> X e. ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) ) )
18 17 biimpa
 |-  ( ( R e. Ring /\ X e. B ) -> X e. ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) )
19 18 ad2ant2r
 |-  ( ( ( R e. Ring /\ I e. U ) /\ ( X e. B /\ Y e. I ) ) -> X e. ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) )
20 simprr
 |-  ( ( ( R e. Ring /\ I e. U ) /\ ( X e. B /\ Y e. I ) ) -> Y e. I )
21 eqid
 |-  ( Scalar ` ( ringLMod ` R ) ) = ( Scalar ` ( ringLMod ` R ) )
22 eqid
 |-  ( .s ` ( ringLMod ` R ) ) = ( .s ` ( 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 ) e. LMod /\ I e. ( LSubSp ` ( ringLMod ` R ) ) ) /\ ( X e. ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) /\ Y e. I ) ) -> ( X ( .s ` ( ringLMod ` R ) ) Y ) e. I )
26 8 13 19 20 25 syl22anc
 |-  ( ( ( R e. Ring /\ I e. U ) /\ ( X e. B /\ Y e. I ) ) -> ( X ( .s ` ( ringLMod ` R ) ) Y ) e. I )
27 6 26 eqeltrid
 |-  ( ( ( R e. Ring /\ I e. U ) /\ ( X e. B /\ Y e. I ) ) -> ( X .x. Y ) e. I )