Theorem idlsrgmulrss2

Description: The product of two ideals is a subset of the second one. (Contributed by Thierry Arnoux, 2-Jun-2024)

	Ref	Expression
Hypotheses	idlsrgmulrss2.1	No typesetting found for |- S = ( IDLsrg ` R ) with typecode |-
	idlsrgmulrss2.2	$$⊢B=\mathrm{LIdeal}\left(R\right)$$
	idlsrgmulrss2.3	$$⊢\underset{\dot{}}{\otimes }={\cdot }_S$$
	idlsrgmulrss2.5	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	idlsrgmulrss2.6	$$⊢\phi \to R\in \mathrm{Ring}$$
	idlsrgmulrss2.7	$$⊢\phi \to I\in B$$
	idlsrgmulrss2.8	$$⊢\phi \to J\in B$$
Assertion	idlsrgmulrss2	$$⊢\phi \to I\underset{\dot{}}{\otimes }J\subseteq J$$

Proof

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