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	|- B = ( Base ` R )
	ringlsmss.2	|- G = ( mulGrp ` R )
	ringlsmss.3	|- .X. = ( LSSum ` G )
	ringlsmss.4	|- ( ph -> R e. Ring )
	ringlsmss.5	|- ( ph -> E C_ B )
	ringlsmss.6	|- ( ph -> F C_ B )
Assertion	ringlsmss	|- ( ph -> ( E .X. F ) C_ B )

Proof

Step	Hyp	Ref	Expression
1		ringlsmss.1	|- B = ( Base ` R )
2		ringlsmss.2	|- G = ( mulGrp ` R )
3		ringlsmss.3	|- .X. = ( LSSum ` G )
4		ringlsmss.4	|- ( ph -> R e. Ring )
5		ringlsmss.5	|- ( ph -> E C_ B )
6		ringlsmss.6	|- ( ph -> F C_ B )
7	2	ringmgp	|- ( R e. Ring -> G e. Mnd )
8	4 7	syl	|- ( ph -> G e. Mnd )
9	2 1	mgpbas	|- B = ( Base ` G )
10	9 3	lsmssv	|- ( ( G e. Mnd /\ E C_ B /\ F C_ B ) -> ( E .X. F ) C_ B )
11	8 5 6 10	syl3anc	|- ( ph -> ( E .X. F ) C_ B )