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 ⊢ ( 𝜑 → ( 𝐼 ⊗ 𝐽 ) ⊆ 𝐽 )