Metamath Proof Explorer

Theorem idlsrgmulrss2

Description: The product of two ideals is a subset of the second one. (Contributed by Thierry Arnoux, 2-Jun-2024)

Ref Expression
Hypotheses idlsrgmulrss2.1 
|- S = ( IDLsrg ` R )
idlsrgmulrss2.2 
|- B = ( LIdeal ` R )
idlsrgmulrss2.3 
|- .(x) = ( .r ` S )
idlsrgmulrss2.5 
|- .x. = ( .r ` R )
idlsrgmulrss2.6 
|- ( ph -> R e. Ring )
idlsrgmulrss2.7 
|- ( ph -> I e. B )
idlsrgmulrss2.8 
|- ( ph -> J e. B )
Assertion idlsrgmulrss2 
|- ( ph -> ( I .(x) J ) C_ J )

Proof

Step Hyp Ref Expression
1 idlsrgmulrss2.1 
 |-  S = ( IDLsrg ` R )
2 idlsrgmulrss2.2 
 |-  B = ( LIdeal ` R )
3 idlsrgmulrss2.3 
 |-  .(x) = ( .r ` S )
4 idlsrgmulrss2.5 
 |-  .x. = ( .r ` R )
5 idlsrgmulrss2.6 
 |-  ( ph -> R e. Ring )
6 idlsrgmulrss2.7 
 |-  ( ph -> I e. B )
7 idlsrgmulrss2.8 
 |-  ( ph -> J e. B )
8 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
9 eqid 
 |-  ( LSSum ` ( mulGrp ` R ) ) = ( LSSum ` ( mulGrp ` R ) )
10 1 2 3 8 9 5 6 7 idlsrgmulrval 
 |-  ( ph -> ( I .(x) J ) = ( ( RSpan ` R ) ` ( I ( LSSum ` ( mulGrp ` R ) ) J ) ) )
11 rlmlmod 
 |-  ( R e. Ring -> ( ringLMod ` R ) e. LMod )
12 5 11 syl 
 |-  ( ph -> ( ringLMod ` R ) e. LMod )
13 eqid 
 |-  ( Base ` R ) = ( Base ` R )
14 13 2 lidlss 
 |-  ( J e. B -> J C_ ( Base ` R ) )
15 7 14 syl 
 |-  ( ph -> J C_ ( Base ` R ) )
16 13 2 lidlss 
 |-  ( I e. B -> I C_ ( Base ` R ) )
17 6 16 syl 
 |-  ( ph -> I C_ ( Base ` R ) )
18 7 2 eleqtrdi 
 |-  ( ph -> J e. ( LIdeal ` R ) )
19 13 8 9 5 17 18 ringlsmss2 
 |-  ( ph -> ( I ( LSSum ` ( mulGrp ` R ) ) J ) C_ J )
20 rlmbas 
 |-  ( Base ` R ) = ( Base ` ( ringLMod ` R ) )
21 rspval 
 |-  ( RSpan ` R ) = ( LSpan ` ( ringLMod ` R ) )
22 20 21 lspss 
 |-  ( ( ( ringLMod ` R ) e. LMod /\ J C_ ( Base ` R ) /\ ( I ( LSSum ` ( mulGrp ` R ) ) J ) C_ J ) -> ( ( RSpan ` R ) ` ( I ( LSSum ` ( mulGrp ` R ) ) J ) ) C_ ( ( RSpan ` R ) ` J ) )
23 12 15 19 22 syl3anc 
 |-  ( ph -> ( ( RSpan ` R ) ` ( I ( LSSum ` ( mulGrp ` R ) ) J ) ) C_ ( ( RSpan ` R ) ` J ) )
24 eqid 
 |-  ( RSpan ` R ) = ( RSpan ` R )
25 24 2 rspidlid 
 |-  ( ( R e. Ring /\ J e. B ) -> ( ( RSpan ` R ) ` J ) = J )
26 5 7 25 syl2anc 
 |-  ( ph -> ( ( RSpan ` R ) ` J ) = J )
27 23 26 sseqtrd 
 |-  ( ph -> ( ( RSpan ` R ) ` ( I ( LSSum ` ( mulGrp ` R ) ) J ) ) C_ J )
28 10 27 eqsstrd 
 |-  ( ph -> ( I .(x) J ) C_ J )