Metamath Proof Explorer


Theorem ecopoveq

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)

Ref Expression
Hypothesis ecopopr.1 ˙ = x y | x S × S y S × S z w v u x = z w y = v u z + ˙ u = w + ˙ v
Assertion ecopoveq A S B S C S D S A B ˙ C D A + ˙ D = B + ˙ C

Proof

Step Hyp Ref Expression
1 ecopopr.1 ˙ = x y | x S × S y S × S z w v u x = z w y = v u z + ˙ u = w + ˙ v
2 oveq12 z = A u = D z + ˙ u = A + ˙ D
3 oveq12 w = B v = C w + ˙ v = B + ˙ C
4 2 3 eqeqan12d z = A u = D w = B v = C z + ˙ u = w + ˙ v A + ˙ D = B + ˙ C
5 4 an42s z = A w = B v = C u = D z + ˙ u = w + ˙ v A + ˙ D = B + ˙ C
6 5 1 opbrop A S B S C S D S A B ˙ C D A + ˙ D = B + ˙ C