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={\mathrm{Base}}_R$$
	elmgplsm.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	elmgplsm.g	$$⊢G={\mathrm{mulGrp}}_R$$
	elmgplsm.m	$$⊢\underset{\dot{}}{\times }=\mathrm{LSSum}\left(G\right)$$
	elmgplsm.e	$$⊢\phi \to E\subseteq B$$
	elmgplsm.f	$$⊢\phi \to F\subseteq B$$
	elmgplsmd.x	$$⊢\phi \to X\in E$$
	elmgplsmd.y	$$⊢\phi \to Y\in F$$
Assertion	elmgplsmd	$$⊢\phi \to X\underset{\dot{}}{·}Y\in \left(E\underset{\dot{}}{\times }F\right)$$

Proof

Step	Hyp	Ref	Expression
1		elmgplsm.b	$$⊢B={\mathrm{Base}}_R$$
2		elmgplsm.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		elmgplsm.g	$$⊢G={\mathrm{mulGrp}}_R$$
4		elmgplsm.m	$$⊢\underset{\dot{}}{\times }=\mathrm{LSSum}\left(G\right)$$
5		elmgplsm.e	$$⊢\phi \to E\subseteq B$$
6		elmgplsm.f	$$⊢\phi \to F\subseteq B$$
7		elmgplsmd.x	$$⊢\phi \to X\in E$$
8		elmgplsmd.y	$$⊢\phi \to Y\in F$$
9		eqidd	$$⊢\phi \to X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Y$$
10		rspceov	$$⊢\left(X\in E\wedge Y\in F\wedge X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Y\right)\to \exists x\in E\exists y\in FX\underset{\dot{}}{·}Y=x\underset{\dot{}}{·}y$$
11	7 8 9 10	syl3anc	$$⊢\phi \to \exists x\in E\exists y\in FX\underset{\dot{}}{·}Y=x\underset{\dot{}}{·}y$$
12	1 2 3 4 5 6	elmgplsm	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y\in \left(E\underset{\dot{}}{\times }F\right)\leftrightarrow \exists x\in E\exists y\in FX\underset{\dot{}}{·}Y=x\underset{\dot{}}{·}y\right)$$
13	11 12	mpbird	$$⊢\phi \to X\underset{\dot{}}{·}Y\in \left(E\underset{\dot{}}{\times }F\right)$$