Theorem idlsrgmulrcl

Description: Ideals of a ring R are closed under multiplication. (Contributed by Thierry Arnoux, 1-Jun-2024)

	Ref	Expression
Hypotheses	idlsrgmulrval.1	$$⊢S=\mathrm{IDLsrg}\left(R\right)$$
	idlsrgmulrval.2	$$⊢B=\mathrm{LIdeal}\left(R\right)$$
	idlsrgmulrval.3	$$⊢\underset{\dot{}}{\otimes }={\cdot }_S$$
	idlsrgmulrcl.1	$$⊢\phi \to R\in \mathrm{Ring}$$
	idlsrgmulrcl.2	$$⊢\phi \to I\in B$$
	idlsrgmulrcl.3	$$⊢\phi \to J\in B$$
Assertion	idlsrgmulrcl	$$⊢\phi \to I\underset{\dot{}}{\otimes }J\in B$$

Proof

Step	Hyp	Ref	Expression
1		idlsrgmulrval.1	$$⊢S=\mathrm{IDLsrg}\left(R\right)$$
2		idlsrgmulrval.2	$$⊢B=\mathrm{LIdeal}\left(R\right)$$
3		idlsrgmulrval.3	$$⊢\underset{\dot{}}{\otimes }={\cdot }_S$$
4		idlsrgmulrcl.1	$$⊢\phi \to R\in \mathrm{Ring}$$
5		idlsrgmulrcl.2	$$⊢\phi \to I\in B$$
6		idlsrgmulrcl.3	$$⊢\phi \to J\in B$$
7		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
8		eqid	$$⊢\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)=\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)$$
9	1 2 3 7 8 4 5 6	idlsrgmulrval	$$⊢\phi \to I\underset{\dot{}}{\otimes }J=\mathrm{RSpan}\left(R\right)\left(I\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)J\right)$$
10		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
11	10 2	lidlss	$$⊢I\in B\to I\subseteq {\mathrm{Base}}_R$$
12	5 11	syl	$$⊢\phi \to I\subseteq {\mathrm{Base}}_R$$
13	10 2	lidlss	$$⊢J\in B\to J\subseteq {\mathrm{Base}}_R$$
14	6 13	syl	$$⊢\phi \to J\subseteq {\mathrm{Base}}_R$$
15	10 7 8 4 12 14	ringlsmss	$$⊢\phi \to I\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)J\subseteq {\mathrm{Base}}_R$$
16		eqid	$$⊢\mathrm{RSpan}\left(R\right)=\mathrm{RSpan}\left(R\right)$$
17	16 10 2	rspcl	$$⊢\left(R\in \mathrm{Ring}\wedge I\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)J\subseteq {\mathrm{Base}}_R\right)\to \mathrm{RSpan}\left(R\right)\left(I\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)J\right)\in B$$
18	4 15 17	syl2anc	$$⊢\phi \to \mathrm{RSpan}\left(R\right)\left(I\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)J\right)\in B$$
19	9 18	eqeltrd	$$⊢\phi \to I\underset{\dot{}}{\otimes }J\in B$$