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 𝑆 = ( IDLsrg ‘ 𝑅 )
idlsrgmulrss2.2 𝐵 = ( LIdeal ‘ 𝑅 )
idlsrgmulrss2.3 = ( .r𝑆 )
idlsrgmulrss2.5 · = ( .r𝑅 )
idlsrgmulrss2.6 ( 𝜑𝑅 ∈ Ring )
idlsrgmulrss2.7 ( 𝜑𝐼𝐵 )
idlsrgmulrss2.8 ( 𝜑𝐽𝐵 )
Assertion idlsrgmulrss2 ( 𝜑 → ( 𝐼 𝐽 ) ⊆ 𝐽 )

Proof

Step Hyp Ref Expression
1 idlsrgmulrss2.1 𝑆 = ( IDLsrg ‘ 𝑅 )
2 idlsrgmulrss2.2 𝐵 = ( LIdeal ‘ 𝑅 )
3 idlsrgmulrss2.3 = ( .r𝑆 )
4 idlsrgmulrss2.5 · = ( .r𝑅 )
5 idlsrgmulrss2.6 ( 𝜑𝑅 ∈ Ring )
6 idlsrgmulrss2.7 ( 𝜑𝐼𝐵 )
7 idlsrgmulrss2.8 ( 𝜑𝐽𝐵 )
8 eqid ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
9 eqid ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) = ( LSSum ‘ ( mulGrp ‘ 𝑅 ) )
10 1 2 3 8 9 5 6 7 idlsrgmulrval ( 𝜑 → ( 𝐼 𝐽 ) = ( ( RSpan ‘ 𝑅 ) ‘ ( 𝐼 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝐽 ) ) )
11 rlmlmod ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )
12 5 11 syl ( 𝜑 → ( ringLMod ‘ 𝑅 ) ∈ LMod )
13 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
14 13 2 lidlss ( 𝐽𝐵𝐽 ⊆ ( Base ‘ 𝑅 ) )
15 7 14 syl ( 𝜑𝐽 ⊆ ( Base ‘ 𝑅 ) )
16 13 2 lidlss ( 𝐼𝐵𝐼 ⊆ ( Base ‘ 𝑅 ) )
17 6 16 syl ( 𝜑𝐼 ⊆ ( Base ‘ 𝑅 ) )
18 7 2 eleqtrdi ( 𝜑𝐽 ∈ ( LIdeal ‘ 𝑅 ) )
19 13 8 9 5 17 18 ringlsmss2 ( 𝜑 → ( 𝐼 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝐽 ) ⊆ 𝐽 )
20 rlmbas ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) )
21 rspval ( RSpan ‘ 𝑅 ) = ( LSpan ‘ ( ringLMod ‘ 𝑅 ) )
22 20 21 lspss ( ( ( ringLMod ‘ 𝑅 ) ∈ LMod ∧ 𝐽 ⊆ ( Base ‘ 𝑅 ) ∧ ( 𝐼 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝐽 ) ⊆ 𝐽 ) → ( ( RSpan ‘ 𝑅 ) ‘ ( 𝐼 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝐽 ) ) ⊆ ( ( RSpan ‘ 𝑅 ) ‘ 𝐽 ) )
23 12 15 19 22 syl3anc ( 𝜑 → ( ( RSpan ‘ 𝑅 ) ‘ ( 𝐼 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝐽 ) ) ⊆ ( ( RSpan ‘ 𝑅 ) ‘ 𝐽 ) )
24 eqid ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 )
25 24 2 rspidlid ( ( 𝑅 ∈ Ring ∧ 𝐽𝐵 ) → ( ( RSpan ‘ 𝑅 ) ‘ 𝐽 ) = 𝐽 )
26 5 7 25 syl2anc ( 𝜑 → ( ( RSpan ‘ 𝑅 ) ‘ 𝐽 ) = 𝐽 )
27 23 26 sseqtrd ( 𝜑 → ( ( RSpan ‘ 𝑅 ) ‘ ( 𝐼 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝐽 ) ) ⊆ 𝐽 )
28 10 27 eqsstrd ( 𝜑 → ( 𝐼 𝐽 ) ⊆ 𝐽 )