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 = ( IDLsrg ` R )
	idlsrgmulrval.2	|- B = ( LIdeal ` R )
	idlsrgmulrval.3	|- .(x) = ( .r ` S )
	idlsrgmulrcl.1	|- ( ph -> R e. Ring )
	idlsrgmulrcl.2	|- ( ph -> I e. B )
	idlsrgmulrcl.3	|- ( ph -> J e. B )
Assertion	idlsrgmulrcl	|- ( ph -> ( I .(x) J ) e. B )

Proof

Step	Hyp	Ref	Expression
1		idlsrgmulrval.1	|- S = ( IDLsrg ` R )
2		idlsrgmulrval.2	|- B = ( LIdeal ` R )
3		idlsrgmulrval.3	|- .(x) = ( .r ` S )
4		idlsrgmulrcl.1	|- ( ph -> R e. Ring )
5		idlsrgmulrcl.2	|- ( ph -> I e. B )
6		idlsrgmulrcl.3	|- ( ph -> J e. B )
7		eqid	|- ( mulGrp ` R ) = ( mulGrp ` R )
8		eqid	|- ( LSSum ` ( mulGrp ` R ) ) = ( LSSum ` ( mulGrp ` R ) )
9	1 2 3 7 8 4 5 6	idlsrgmulrval	|- ( ph -> ( I .(x) J ) = ( ( RSpan ` R ) ` ( I ( LSSum ` ( mulGrp ` R ) ) J ) ) )
10		eqid	|- ( Base ` R ) = ( Base ` R )
11	10 2	lidlss	|- ( I e. B -> I C_ ( Base ` R ) )
12	5 11	syl	|- ( ph -> I C_ ( Base ` R ) )
13	10 2	lidlss	|- ( J e. B -> J C_ ( Base ` R ) )
14	6 13	syl	|- ( ph -> J C_ ( Base ` R ) )
15	10 7 8 4 12 14	ringlsmss	|- ( ph -> ( I ( LSSum ` ( mulGrp ` R ) ) J ) C_ ( Base ` R ) )
16		eqid	|- ( RSpan ` R ) = ( RSpan ` R )
17	16 10 2	rspcl	|- ( ( R e. Ring /\ ( I ( LSSum ` ( mulGrp ` R ) ) J ) C_ ( Base ` R ) ) -> ( ( RSpan ` R ) ` ( I ( LSSum ` ( mulGrp ` R ) ) J ) ) e. B )
18	4 15 17	syl2anc	|- ( ph -> ( ( RSpan ` R ) ` ( I ( LSSum ` ( mulGrp ` R ) ) J ) ) e. B )
19	9 18	eqeltrd	|- ( ph -> ( I .(x) J ) e. B )