This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = ( 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 )
elringlsmd.1 
|- ( ph -> X e. E )
elringlsmd.2 
|- ( ph -> Y e. F )
Assertion elringlsmd 
|- ( ph -> ( X .x. Y ) e. ( E .X. F ) )

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 elringlsmd.1 
 |-  ( ph -> X e. E )
8 elringlsmd.2 
 |-  ( ph -> Y e. F )
9 eqidd 
 |-  ( ph -> ( X .x. Y ) = ( X .x. Y ) )
10 rspceov 
 |-  ( ( X e. E /\ Y e. F /\ ( X .x. Y ) = ( X .x. Y ) ) -> E. x e. E E. y e. F ( X .x. Y ) = ( x .x. y ) )
11 7 8 9 10 syl3anc 
 |-  ( ph -> E. x e. E E. y e. F ( X .x. Y ) = ( x .x. y ) )
12 1 2 3 4 5 6 elringlsm 
 |-  ( ph -> ( ( X .x. Y ) e. ( E .X. F ) <-> E. x e. E E. y e. F ( X .x. Y ) = ( x .x. y ) ) )
13 11 12 mpbird 
 |-  ( ph -> ( X .x. Y ) e. ( E .X. F ) )