Theorem idlsrgmulrcl

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

	Ref	Expression
Hypotheses	idlsrgmulrval.1	⊢ 𝑆 = ( IDLsrg ‘ 𝑅 )
	idlsrgmulrval.2	⊢ 𝐵 = ( LIdeal ‘ 𝑅 )
	idlsrgmulrval.3	⊢ ⊗ = ( .r ‘ 𝑆 )
	idlsrgmulrcl.1	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	idlsrgmulrcl.2	⊢ ( 𝜑 → 𝐼 ∈ 𝐵 )
	idlsrgmulrcl.3	⊢ ( 𝜑 → 𝐽 ∈ 𝐵 )
Assertion	idlsrgmulrcl	⊢ ( 𝜑 → ( 𝐼 ⊗ 𝐽 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		idlsrgmulrval.1	⊢ 𝑆 = ( IDLsrg ‘ 𝑅 )
2		idlsrgmulrval.2	⊢ 𝐵 = ( LIdeal ‘ 𝑅 )
3		idlsrgmulrval.3	⊢ ⊗ = ( .r ‘ 𝑆 )
4		idlsrgmulrcl.1	⊢ ( 𝜑 → 𝑅 ∈ Ring )
5		idlsrgmulrcl.2	⊢ ( 𝜑 → 𝐼 ∈ 𝐵 )
6		idlsrgmulrcl.3	⊢ ( 𝜑 → 𝐽 ∈ 𝐵 )
7		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
8		eqid	⊢ ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) = ( LSSum ‘ ( mulGrp ‘ 𝑅 ) )
9	1 2 3 7 8 4 5 6	idlsrgmulrval	⊢ ( 𝜑 → ( 𝐼 ⊗ 𝐽 ) = ( ( RSpan ‘ 𝑅 ) ‘ ( 𝐼 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝐽 ) ) )
10		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11	10 2	lidlss	⊢ ( 𝐼 ∈ 𝐵 → 𝐼 ⊆ ( Base ‘ 𝑅 ) )
12	5 11	syl	⊢ ( 𝜑 → 𝐼 ⊆ ( Base ‘ 𝑅 ) )
13	10 2	lidlss	⊢ ( 𝐽 ∈ 𝐵 → 𝐽 ⊆ ( Base ‘ 𝑅 ) )
14	6 13	syl	⊢ ( 𝜑 → 𝐽 ⊆ ( Base ‘ 𝑅 ) )
15	10 7 8 4 12 14	ringlsmss	⊢ ( 𝜑 → ( 𝐼 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝐽 ) ⊆ ( Base ‘ 𝑅 ) )
16		eqid	⊢ ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 )
17	16 10 2	rspcl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐼 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝐽 ) ⊆ ( Base ‘ 𝑅 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ ( 𝐼 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝐽 ) ) ∈ 𝐵 )
18	4 15 17	syl2anc	⊢ ( 𝜑 → ( ( RSpan ‘ 𝑅 ) ‘ ( 𝐼 ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) 𝐽 ) ) ∈ 𝐵 )
19	9 18	eqeltrd	⊢ ( 𝜑 → ( 𝐼 ⊗ 𝐽 ) ∈ 𝐵 )