Theorem elmgplsmd

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

	Ref	Expression
Hypotheses	elmgplsm.b	|- B = ( Base ` R )
	elmgplsm.t	|- .x. = ( .r ` R )
	elmgplsm.g	|- G = ( mulGrp ` R )
	elmgplsm.m	|- .X. = ( LSSum ` G )
	elmgplsm.e	|- ( ph -> E C_ B )
	elmgplsm.f	|- ( ph -> F C_ B )
	elmgplsmd.x	|- ( ph -> X e. E )
	elmgplsmd.y	|- ( ph -> Y e. F )
Assertion	elmgplsmd	|- ( ph -> ( X .x. Y ) e. ( E .X. F ) )

Proof

Step	Hyp	Ref	Expression
1		elmgplsm.b	|- B = ( Base ` R )
2		elmgplsm.t	|- .x. = ( .r ` R )
3		elmgplsm.g	|- G = ( mulGrp ` R )
4		elmgplsm.m	|- .X. = ( LSSum ` G )
5		elmgplsm.e	|- ( ph -> E C_ B )
6		elmgplsm.f	|- ( ph -> F C_ B )
7		elmgplsmd.x	|- ( ph -> X e. E )
8		elmgplsmd.y	|- ( 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	elmgplsm	|- ( 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 ) )