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 = {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$
Assertion	elringlsm	$⊢ φ \to (Z \in (E \underset{˙}{\times} F) \leftrightarrow \exists x \in E \exists y \in F Z = x \underset{˙}{\cdot} y)$

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	3	fvexi	$⊢ G \in V$
8	3 1	mgpbas	$⊢ B = {Base}_{G}$
9	3 2	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{G}$
10	8 9 4	lsmelvalx	$⊢ (G \in V \land E \subseteq B \land F \subseteq B) \to (Z \in (E \underset{˙}{\times} F) \leftrightarrow \exists x \in E \exists y \in F Z = x \underset{˙}{\cdot} y)$
11	7 5 6 10	mp3an2i	$⊢ φ \to (Z \in (E \underset{˙}{\times} F) \leftrightarrow \exists x \in E \exists y \in F Z = x \underset{˙}{\cdot} y)$

Metamath Proof Explorer