MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ecopoveq Unicode version

Theorem ecopoveq 6802
Description: This is the first of several theorems about equivalence relations of the kind used in construction of fractions and signed reals, involving operations on equivalent classes of ordered pairs. This theorem expresses the relation 
.~ (specified by the hypothesis) in terms of its operation  F. (Contributed by NM, 16-Aug-1995.)
Hypothesis
Ref Expression
ecopopr.1  |-  .~  =  { <. x ,  y
>.  |  ( (
x  e.  ( S  X.  S )  /\  y  e.  ( S  X.  S ) )  /\  E. z E. w E. v E. u ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z 
.+  u )  =  ( w  .+  v
) ) ) }
Assertion
Ref Expression
ecopoveq  |-  ( ( ( A  e.  S  /\  B  e.  S
)  /\  ( C  e.  S  /\  D  e.  S ) )  -> 
( <. A ,  B >.  .~  <. C ,  D >.  <-> 
( A  .+  D
)  =  ( B 
.+  C ) ) )
Distinct variable groups:    x, y,
z, w, v, u, 
.+    x, S, y, z, w, v, u    x, A, y, z, w, v, u    x, B, y, z, w, v, u   
x, C, y, z, w, v, u    x, D, y, z, w, v, u
Allowed substitution hints:    .~ ( x, y, z, w, v, u)

Proof of Theorem ecopoveq
StepHypRef Expression
1 oveq12 5909 . . . 4  |-  ( ( z  =  A  /\  u  =  D )  ->  ( z  .+  u
)  =  ( A 
.+  D ) )
2 oveq12 5909 . . . 4  |-  ( ( w  =  B  /\  v  =  C )  ->  ( w  .+  v
)  =  ( B 
.+  C ) )
31, 2eqeqan12d 2331 . . 3  |-  ( ( ( z  =  A  /\  u  =  D )  /\  ( w  =  B  /\  v  =  C ) )  -> 
( ( z  .+  u )  =  ( w  .+  v )  <-> 
( A  .+  D
)  =  ( B 
.+  C ) ) )
43an42s 800 . 2  |-  ( ( ( z  =  A  /\  w  =  B )  /\  ( v  =  C  /\  u  =  D ) )  -> 
( ( z  .+  u )  =  ( w  .+  v )  <-> 
( A  .+  D
)  =  ( B 
.+  C ) ) )
5 ecopopr.1 . 2  |-  .~  =  { <. x ,  y
>.  |  ( (
x  e.  ( S  X.  S )  /\  y  e.  ( S  X.  S ) )  /\  E. z E. w E. v E. u ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z 
.+  u )  =  ( w  .+  v
) ) ) }
64, 5opbrop 4804 1  |-  ( ( ( A  e.  S  /\  B  e.  S
)  /\  ( C  e.  S  /\  D  e.  S ) )  -> 
( <. A ,  B >.  .~  <. C ,  D >.  <-> 
( A  .+  D
)  =  ( B 
.+  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   E.wex 1532    = wceq 1633    e. wcel 1701   <.cop 3677   class class class wbr 4060   {copab 4113    X. cxp 4724  (class class class)co 5900
This theorem is referenced by:  ecopovsym  6803  ecopovtrn  6804  ecopover  6805  enqbreq  8588  enrbreq  8734
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pr 4251
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-opab 4115  df-xp 4732  df-iota 5256  df-fv 5300  df-ov 5903
  Copyright terms: Public domain W3C validator