ringlsmss

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

	Ref	Expression
Hypotheses	ringlsmss.1	$⊢ B = {Base}_{R}$
	ringlsmss.2	$⊢ G = {mulGrp}_{R}$
	ringlsmss.3	$⊢ \underset{˙}{\times} = LSSum (G)$
	ringlsmss.4	$⊢ φ \to R \in Ring$
	ringlsmss.5	$⊢ φ \to E \subseteq B$
	ringlsmss.6	$⊢ φ \to F \subseteq B$
Assertion	ringlsmss	$⊢ φ \to E \underset{˙}{\times} F \subseteq B$

Step	Hyp	Ref	Expression
1		ringlsmss.1	$⊢ B = {Base}_{R}$
2		ringlsmss.2	$⊢ G = {mulGrp}_{R}$
3		ringlsmss.3	$⊢ \underset{˙}{\times} = LSSum (G)$
4		ringlsmss.4	$⊢ φ \to R \in Ring$
5		ringlsmss.5	$⊢ φ \to E \subseteq B$
6		ringlsmss.6	$⊢ φ \to F \subseteq B$
7	2	ringmgp	$⊢ R \in Ring \to G \in Mnd$
8	4 7	syl	$⊢ φ \to G \in Mnd$
9	2 1	mgpbas	$⊢ B = {Base}_{G}$
10	9 3	lsmssv	$⊢ (G \in Mnd \land E \subseteq B \land F \subseteq B) \to E \underset{˙}{\times} F \subseteq B$
11	8 5 6 10	syl3anc	$⊢ φ \to E \underset{˙}{\times} F \subseteq B$

Metamath Proof Explorer