Theorem elringlsmd

Description: Membership in a product of two subsets of a ring, one direction. (Contributed by Thierry Arnoux, 13-Apr-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$$
	elringlsmd.1	$$⊢\phi \to X\in E$$
	elringlsmd.2	$$⊢\phi \to Y\in F$$
Assertion	elringlsmd	$$⊢\phi \to X\underset{\dot{}}{·}Y\in \left(E\underset{\dot{}}{\times }F\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		elringlsmd.1	$$⊢\phi \to X\in E$$
8		elringlsmd.2	$$⊢\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	elringlsm	$$⊢\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)$$