Metamath Proof Explorer

Theorem idlsrgmulrss1

Description: In a commutative ring, the product of two ideals is a subset of the first one. (Contributed by Thierry Arnoux, 16-Jun-2024)

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

Proof

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