Theorem elmgplsm

Description: Membership in a product of two subsets of a multiplication group. (Contributed by Thierry Arnoux, 20-Jan-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 )
Assertion	elmgplsm	|- ( ph -> ( Z e. ( E .X. F ) <-> E. x e. E E. y e. F Z = ( x .x. y ) ) )

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	3	fvexi	|- G e. _V
8	3 1	mgpbas	|- B = ( Base ` G )
9	3 2	mgpplusg	|- .x. = ( +g ` G )
10	8 9 4	lsmelvalx	|- ( ( G e. _V /\ E C_ B /\ F C_ B ) -> ( Z e. ( E .X. F ) <-> E. x e. E E. y e. F Z = ( x .x. y ) ) )
11	7 5 6 10	mp3an2i	|- ( ph -> ( Z e. ( E .X. F ) <-> E. x e. E E. y e. F Z = ( x .x. y ) ) )