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 syl5eq 
 |-  ( 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 )