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 ⊢ 𝑆 = ( IDLsrg ‘ 𝑅 )
idlsrgmulrss1.2 ⊢ 𝐵 = ( LIdeal ‘ 𝑅 )
idlsrgmulrss1.3 ⊢ ⊗ = ( .r ‘ 𝑆 )
idlsrgmulrss1.4 ⊢ · = ( .r ‘ 𝑅 )
idlsrgmulrss1.5 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
idlsrgmulrss1.6 ⊢ ( 𝜑 → 𝐼 ∈ 𝐵 )
idlsrgmulrss1.7 ⊢ ( 𝜑 → 𝐽 ∈ 𝐵 )
Assertion idlsrgmulrss1 ( 𝜑 → ( 𝐼 ⊗ 𝐽 ) ⊆ 𝐼 )

Proof

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