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 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝑆 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑆 × 𝑆 ) ) ∧ ∃ 𝑧𝑤𝑣𝑢 ( ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ ( 𝑧 + 𝑢 ) = ( 𝑤 + 𝑣 ) ) ) }
Assertion ecopoveq ( ( ( 𝐴𝑆𝐵𝑆 ) ∧ ( 𝐶𝑆𝐷𝑆 ) ) → ( ⟨ 𝐴 , 𝐵𝐶 , 𝐷 ⟩ ↔ ( 𝐴 + 𝐷 ) = ( 𝐵 + 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 ecopopr.1 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝑆 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑆 × 𝑆 ) ) ∧ ∃ 𝑧𝑤𝑣𝑢 ( ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ ( 𝑧 + 𝑢 ) = ( 𝑤 + 𝑣 ) ) ) }
2 oveq12 ( ( 𝑧 = 𝐴𝑢 = 𝐷 ) → ( 𝑧 + 𝑢 ) = ( 𝐴 + 𝐷 ) )
3 oveq12 ( ( 𝑤 = 𝐵𝑣 = 𝐶 ) → ( 𝑤 + 𝑣 ) = ( 𝐵 + 𝐶 ) )
4 2 3 eqeqan12d ( ( ( 𝑧 = 𝐴𝑢 = 𝐷 ) ∧ ( 𝑤 = 𝐵𝑣 = 𝐶 ) ) → ( ( 𝑧 + 𝑢 ) = ( 𝑤 + 𝑣 ) ↔ ( 𝐴 + 𝐷 ) = ( 𝐵 + 𝐶 ) ) )
5 4 an42s ( ( ( 𝑧 = 𝐴𝑤 = 𝐵 ) ∧ ( 𝑣 = 𝐶𝑢 = 𝐷 ) ) → ( ( 𝑧 + 𝑢 ) = ( 𝑤 + 𝑣 ) ↔ ( 𝐴 + 𝐷 ) = ( 𝐵 + 𝐶 ) ) )
6 5 1 opbrop ( ( ( 𝐴𝑆𝐵𝑆 ) ∧ ( 𝐶𝑆𝐷𝑆 ) ) → ( ⟨ 𝐴 , 𝐵𝐶 , 𝐷 ⟩ ↔ ( 𝐴 + 𝐷 ) = ( 𝐵 + 𝐶 ) ) )