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 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 | ecopoveq | |- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( <. A , B >. .~ <. C , D >. <-> ( A .+ D ) = ( B .+ C ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 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 ) ) ) } |
|
| 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 e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( <. A , B >. .~ <. C , D >. <-> ( A .+ D ) = ( B .+ C ) ) ) |