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 = ( Base ` R )
	elringlsm.2	|- .x. = ( .r ` R )
	elringlsm.3	|- G = ( mulGrp ` R )
	elringlsm.4	|- .X. = ( LSSum ` G )
	elringlsm.6	|- ( ph -> E C_ B )
	elringlsm.7	|- ( ph -> F C_ B )
Assertion	elringlsm	|- ( ph -> ( Z e. ( E .X. F ) <-> E. x e. E E. y e. F Z = ( x .x. y ) ) )

Proof

Step	Hyp	Ref	Expression
1		elringlsm.1	|- B = ( Base ` R )
2		elringlsm.2	|- .x. = ( .r ` R )
3		elringlsm.3	|- G = ( mulGrp ` R )
4		elringlsm.4	|- .X. = ( LSSum ` G )
5		elringlsm.6	|- ( ph -> E C_ B )
6		elringlsm.7	|- ( ph -> F C_ B )
7	3	fvexi	|- G e. _V
8	3 1	mgpbas	|- B = ( Base ` G )
9	3 2	mgpplusg	|- .x. = ( +g ` G )
10	8 9 4	lsmelvalx	|- ( ( G e. _V /\ E C_ B /\ F C_ B ) -> ( Z e. ( E .X. F ) <-> E. x e. E E. y e. F Z = ( x .x. y ) ) )
11	7 5 6 10	mp3an2i	|- ( ph -> ( Z e. ( E .X. F ) <-> E. x e. E E. y e. F Z = ( x .x. y ) ) )