Theorem ringlsmss

Description: Closure of the product of two subsets of a ring. (Contributed by Thierry Arnoux, 20-Jan-2024)

	Ref	Expression
Hypotheses	ringlsmss.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
	ringlsmss.2	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
	ringlsmss.3	⊢ × = ( LSSum ‘ 𝐺 )
	ringlsmss.4	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	ringlsmss.5	⊢ ( 𝜑 → 𝐸 ⊆ 𝐵 )
	ringlsmss.6	⊢ ( 𝜑 → 𝐹 ⊆ 𝐵 )
Assertion	ringlsmss	⊢ ( 𝜑 → ( 𝐸 × 𝐹 ) ⊆ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ringlsmss.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		ringlsmss.2	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
3		ringlsmss.3	⊢ × = ( LSSum ‘ 𝐺 )
4		ringlsmss.4	⊢ ( 𝜑 → 𝑅 ∈ Ring )
5		ringlsmss.5	⊢ ( 𝜑 → 𝐸 ⊆ 𝐵 )
6		ringlsmss.6	⊢ ( 𝜑 → 𝐹 ⊆ 𝐵 )
7	2	ringmgp	⊢ ( 𝑅 ∈ Ring → 𝐺 ∈ Mnd )
8	4 7	syl	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
9	2 1	mgpbas	⊢ 𝐵 = ( Base ‘ 𝐺 )
10	9 3	lsmssv	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐸 ⊆ 𝐵 ∧ 𝐹 ⊆ 𝐵 ) → ( 𝐸 × 𝐹 ) ⊆ 𝐵 )
11	8 5 6 10	syl3anc	⊢ ( 𝜑 → ( 𝐸 × 𝐹 ) ⊆ 𝐵 )