Theorem idlsrgmulrssin

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

	Ref	Expression
Hypotheses	idlsrgmulrssin.1	⊢ 𝑆 = ( IDLsrg ‘ 𝑅 )
	idlsrgmulrssin.2	⊢ 𝐵 = ( LIdeal ‘ 𝑅 )
	idlsrgmulrssin.3	⊢ ⊗ = ( .r ‘ 𝑆 )
	idlsrgmulrssin.4	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	idlsrgmulrssin.5	⊢ ( 𝜑 → 𝐼 ∈ 𝐵 )
	idlsrgmulrssin.6	⊢ ( 𝜑 → 𝐽 ∈ 𝐵 )
Assertion	idlsrgmulrssin	⊢ ( 𝜑 → ( 𝐼 ⊗ 𝐽 ) ⊆ ( 𝐼 ∩ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		idlsrgmulrssin.1	⊢ 𝑆 = ( IDLsrg ‘ 𝑅 )
2		idlsrgmulrssin.2	⊢ 𝐵 = ( LIdeal ‘ 𝑅 )
3		idlsrgmulrssin.3	⊢ ⊗ = ( .r ‘ 𝑆 )
4		idlsrgmulrssin.4	⊢ ( 𝜑 → 𝑅 ∈ CRing )
5		idlsrgmulrssin.5	⊢ ( 𝜑 → 𝐼 ∈ 𝐵 )
6		idlsrgmulrssin.6	⊢ ( 𝜑 → 𝐽 ∈ 𝐵 )
7		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
8	1 2 3 7 4 5 6	idlsrgmulrss1	⊢ ( 𝜑 → ( 𝐼 ⊗ 𝐽 ) ⊆ 𝐼 )
9	4	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
10	1 2 3 7 9 5 6	idlsrgmulrss2	⊢ ( 𝜑 → ( 𝐼 ⊗ 𝐽 ) ⊆ 𝐽 )
11	8 10	ssind	⊢ ( 𝜑 → ( 𝐼 ⊗ 𝐽 ) ⊆ ( 𝐼 ∩ 𝐽 ) )