Theorem elringlsmd

Description: Membership in a product of two subsets of a ring, one direction. (Contributed by Thierry Arnoux, 13-Apr-2024)

	Ref	Expression
Hypotheses	elringlsm.1	|- B = ( Base ` R )
	elringlsm.2	|- .x. = ( .r ` R )
	elringlsm.3	|- G = ( mulGrp ` R )
	elringlsm.4	|- .X. = ( LSSum ` G )
	elringlsm.6	|- ( ph -> E C_ B )
	elringlsm.7	|- ( ph -> F C_ B )
	elringlsmd.1	|- ( ph -> X e. E )
	elringlsmd.2	|- ( ph -> Y e. F )
Assertion	elringlsmd	|- ( ph -> ( X .x. Y ) e. ( E .X. F ) )

Proof

Step	Hyp	Ref	Expression
1		elringlsm.1	|- B = ( Base ` R )
2		elringlsm.2	|- .x. = ( .r ` R )
3		elringlsm.3	|- G = ( mulGrp ` R )
4		elringlsm.4	|- .X. = ( LSSum ` G )
5		elringlsm.6	|- ( ph -> E C_ B )
6		elringlsm.7	|- ( ph -> F C_ B )
7		elringlsmd.1	|- ( ph -> X e. E )
8		elringlsmd.2	|- ( ph -> Y e. F )
9		eqidd	|- ( ph -> ( X .x. Y ) = ( X .x. Y ) )
10		rspceov	|- ( ( X e. E /\ Y e. F /\ ( X .x. Y ) = ( X .x. Y ) ) -> E. x e. E E. y e. F ( X .x. Y ) = ( x .x. y ) )
11	7 8 9 10	syl3anc	|- ( ph -> E. x e. E E. y e. F ( X .x. Y ) = ( x .x. y ) )
12	1 2 3 4 5 6	elringlsm	|- ( ph -> ( ( X .x. Y ) e. ( E .X. F ) <-> E. x e. E E. y e. F ( X .x. Y ) = ( x .x. y ) ) )
13	11 12	mpbird	|- ( ph -> ( X .x. Y ) e. ( E .X. F ) )