Theorem elringlsm

Description: Membership in a product of two subsets of a ring. (Contributed by Thierry Arnoux, 20-Jan-2024)

	Ref	Expression
Hypotheses	elringlsm.1	$$⊢B={\mathrm{Base}}_R$$
	elringlsm.2	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	elringlsm.3	$$⊢G={\mathrm{mulGrp}}_R$$
	elringlsm.4	$$⊢\underset{\dot{}}{\times }=\mathrm{LSSum}\left(G\right)$$
	elringlsm.6	$$⊢\phi \to E\subseteq B$$
	elringlsm.7	$$⊢\phi \to F\subseteq B$$
Assertion	elringlsm	$$⊢\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		elringlsm.1	$$⊢B={\mathrm{Base}}_R$$
2		elringlsm.2	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		elringlsm.3	$$⊢G={\mathrm{mulGrp}}_R$$
4		elringlsm.4	$$⊢\underset{\dot{}}{\times }=\mathrm{LSSum}\left(G\right)$$
5		elringlsm.6	$$⊢\phi \to E\subseteq B$$
6		elringlsm.7	$$⊢\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)$$