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={\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$$
Assertion	elmgplsm	$$⊢\phi \to \left(Z\in \left(E\underset{\dot{}}{\times }F\right)\leftrightarrow \exists x\in E\exists y\in FZ=x\underset{\dot{}}{·}y\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	3	fvexi	$$⊢G\in \mathrm{V}$$
8	3 1	mgpbas	$$⊢B={\mathrm{Base}}_G$$
9	3 2	mgpplusg	$$⊢\underset{\dot{}}{·}={+}_G$$
10	8 9 4	lsmelvalx	$$⊢\left(G\in \mathrm{V}\wedge E\subseteq B\wedge F\subseteq B\right)\to \left(Z\in \left(E\underset{\dot{}}{\times }F\right)\leftrightarrow \exists x\in E\exists y\in FZ=x\underset{\dot{}}{·}y\right)$$
11	7 5 6 10	mp3an2i	$$⊢\phi \to \left(Z\in \left(E\underset{\dot{}}{\times }F\right)\leftrightarrow \exists x\in E\exists y\in FZ=x\underset{\dot{}}{·}y\right)$$