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 = {Base}_{R}$
	elringlsm.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	elringlsm.3	$⊢ G = {mulGrp}_{R}$
	elringlsm.4	$⊢ \underset{˙}{\times} = LSSum (G)$
	elringlsm.6	$⊢ φ \to E \subseteq B$
	elringlsm.7	$⊢ φ \to F \subseteq B$
	elringlsmd.1	$⊢ φ \to X \in E$
	elringlsmd.2	$⊢ φ \to Y \in F$
Assertion	elringlsmd	$⊢ φ \to X \underset{˙}{\cdot} Y \in (E \underset{˙}{\times} F)$

Step	Hyp	Ref	Expression
1		elringlsm.1	$⊢ B = {Base}_{R}$
2		elringlsm.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		elringlsm.3	$⊢ G = {mulGrp}_{R}$
4		elringlsm.4	$⊢ \underset{˙}{\times} = LSSum (G)$
5		elringlsm.6	$⊢ φ \to E \subseteq B$
6		elringlsm.7	$⊢ φ \to F \subseteq B$
7		elringlsmd.1	$⊢ φ \to X \in E$
8		elringlsmd.2	$⊢ φ \to Y \in F$
9		eqidd	$⊢ φ \to X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} Y$
10		rspceov	$⊢ (X \in E \land Y \in F \land X \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} Y) \to \exists x \in E \exists y \in F X \underset{˙}{\cdot} Y = x \underset{˙}{\cdot} y$
11	7 8 9 10	syl3anc	$⊢ φ \to \exists x \in E \exists y \in F X \underset{˙}{\cdot} Y = x \underset{˙}{\cdot} y$
12	1 2 3 4 5 6	elringlsm	$⊢ φ \to (X \underset{˙}{\cdot} Y \in (E \underset{˙}{\times} F) \leftrightarrow \exists x \in E \exists y \in F X \underset{˙}{\cdot} Y = x \underset{˙}{\cdot} y)$
13	11 12	mpbird	$⊢ φ \to X \underset{˙}{\cdot} Y \in (E \underset{˙}{\times} F)$

Metamath Proof Explorer