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	|- S = ( IDLsrg ` R )
	idlsrgmulrssin.2	|- B = ( LIdeal ` R )
	idlsrgmulrssin.3	|- .(x) = ( .r ` S )
	idlsrgmulrssin.4	|- ( ph -> R e. CRing )
	idlsrgmulrssin.5	|- ( ph -> I e. B )
	idlsrgmulrssin.6	|- ( ph -> J e. B )
Assertion	idlsrgmulrssin	|- ( ph -> ( I .(x) J ) C_ ( I i^i J ) )

Proof

Step	Hyp	Ref	Expression
1		idlsrgmulrssin.1	|- S = ( IDLsrg ` R )
2		idlsrgmulrssin.2	|- B = ( LIdeal ` R )
3		idlsrgmulrssin.3	|- .(x) = ( .r ` S )
4		idlsrgmulrssin.4	|- ( ph -> R e. CRing )
5		idlsrgmulrssin.5	|- ( ph -> I e. B )
6		idlsrgmulrssin.6	|- ( ph -> J e. B )
7		eqid	|- ( .r ` R ) = ( .r ` R )
8	1 2 3 7 4 5 6	idlsrgmulrss1	|- ( ph -> ( I .(x) J ) C_ I )
9	4	crngringd	|- ( ph -> R e. Ring )
10	1 2 3 7 9 5 6	idlsrgmulrss2	|- ( ph -> ( I .(x) J ) C_ J )
11	8 10	ssind	|- ( ph -> ( I .(x) J ) C_ ( I i^i J ) )