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	No typesetting found for |- S = ( IDLsrg ` R ) with typecode |-
	idlsrgmulrssin.2	$$⊢B=\mathrm{LIdeal}\left(R\right)$$
	idlsrgmulrssin.3	$$⊢\underset{\dot{}}{\otimes }={\cdot }_S$$
	idlsrgmulrssin.4	$$⊢\phi \to R\in \mathrm{CRing}$$
	idlsrgmulrssin.5	$$⊢\phi \to I\in B$$
	idlsrgmulrssin.6	$$⊢\phi \to J\in B$$
Assertion	idlsrgmulrssin	$$⊢\phi \to I\underset{\dot{}}{\otimes }J\subseteq I\cap J$$

Proof

Step	Hyp	Ref	Expression
1		idlsrgmulrssin.1	Could not format S = ( IDLsrg ` R ) : No typesetting found for |- S = ( IDLsrg ` R ) with typecode |-
2		idlsrgmulrssin.2	$$⊢B=\mathrm{LIdeal}\left(R\right)$$
3		idlsrgmulrssin.3	$$⊢\underset{\dot{}}{\otimes }={\cdot }_S$$
4		idlsrgmulrssin.4	$$⊢\phi \to R\in \mathrm{CRing}$$
5		idlsrgmulrssin.5	$$⊢\phi \to I\in B$$
6		idlsrgmulrssin.6	$$⊢\phi \to J\in B$$
7		eqid	$$⊢{\cdot }_R={\cdot }_R$$
8	1 2 3 7 4 5 6	idlsrgmulrss1	$$⊢\phi \to I\underset{\dot{}}{\otimes }J\subseteq I$$
9	4	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
10	1 2 3 7 9 5 6	idlsrgmulrss2	$$⊢\phi \to I\underset{\dot{}}{\otimes }J\subseteq J$$
11	8 10	ssind	$$⊢\phi \to I\underset{\dot{}}{\otimes }J\subseteq I\cap J$$