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

Proof

Step	Hyp	Ref	Expression
1		idlsrgmulrss1.1	Could not format S = ( IDLsrg ` R ) : No typesetting found for |- S = ( IDLsrg ` R ) with typecode |-
2		idlsrgmulrss1.2	$$⊢B=\mathrm{LIdeal}\left(R\right)$$
3		idlsrgmulrss1.3	$$⊢\underset{\dot{}}{\otimes }={\cdot }_S$$
4		idlsrgmulrss1.4	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
5		idlsrgmulrss1.5	$$⊢\phi \to R\in \mathrm{CRing}$$
6		idlsrgmulrss1.6	$$⊢\phi \to I\in B$$
7		idlsrgmulrss1.7	$$⊢\phi \to J\in B$$
8		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
9		eqid	$$⊢\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)=\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)$$
10	1 2 3 8 9 5 6 7	idlsrgmulrval	$$⊢\phi \to I\underset{\dot{}}{\otimes }J=\mathrm{RSpan}\left(R\right)\left(I\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)J\right)$$
11		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
12		rlmlmod	$$⊢R\in \mathrm{Ring}\to \mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}$$
13	5 11 12	3syl	$$⊢\phi \to \mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}$$
14		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
15	14 2	lidlss	$$⊢I\in B\to I\subseteq {\mathrm{Base}}_R$$
16	6 15	syl	$$⊢\phi \to I\subseteq {\mathrm{Base}}_R$$
17	14 2	lidlss	$$⊢J\in B\to J\subseteq {\mathrm{Base}}_R$$
18	7 17	syl	$$⊢\phi \to J\subseteq {\mathrm{Base}}_R$$
19	6 2	eleqtrdi	$$⊢\phi \to I\in \mathrm{LIdeal}\left(R\right)$$
20	14 8 9 5 18 19	ringlsmss1	$$⊢\phi \to I\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)J\subseteq I$$
21		rlmbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{ringLMod}\left(R\right)}$$
22		rspval	$$⊢\mathrm{RSpan}\left(R\right)=\mathrm{LSpan}\left(\mathrm{ringLMod}\left(R\right)\right)$$
23	21 22	lspss	$$⊢\left(\mathrm{ringLMod}\left(R\right)\in \mathrm{LMod}\wedge I\subseteq {\mathrm{Base}}_R\wedge I\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)J\subseteq I\right)\to \mathrm{RSpan}\left(R\right)\left(I\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)J\right)\subseteq \mathrm{RSpan}\left(R\right)\left(I\right)$$
24	13 16 20 23	syl3anc	$$⊢\phi \to \mathrm{RSpan}\left(R\right)\left(I\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)J\right)\subseteq \mathrm{RSpan}\left(R\right)\left(I\right)$$
25	5 11	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
26		eqid	$$⊢\mathrm{RSpan}\left(R\right)=\mathrm{RSpan}\left(R\right)$$
27	26 2	rspidlid	$$⊢\left(R\in \mathrm{Ring}\wedge I\in B\right)\to \mathrm{RSpan}\left(R\right)\left(I\right)=I$$
28	25 6 27	syl2anc	$$⊢\phi \to \mathrm{RSpan}\left(R\right)\left(I\right)=I$$
29	24 28	sseqtrd	$$⊢\phi \to \mathrm{RSpan}\left(R\right)\left(I\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)J\right)\subseteq I$$
30	10 29	eqsstrd	$$⊢\phi \to I\underset{\dot{}}{\otimes }J\subseteq I$$