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	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| ((x \in (S \times S) \land y \in (S \times S)) \land \exists z \exists w \exists v \exists u ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land z \underset{˙}{+} u = w \underset{˙}{+} v))\}$
	Assertion	ecopoveq	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to (⟨A, B⟩ \underset{˙}{\sim} ⟨C, D⟩ \leftrightarrow A \underset{˙}{+} D = B \underset{˙}{+} C)$

Proof

Step	Hyp	Ref	Expression
1		ecopopr.1	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| ((x \in (S \times S) \land y \in (S \times S)) \land \exists z \exists w \exists v \exists u ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land z \underset{˙}{+} u = w \underset{˙}{+} v))\}$
2		oveq12	$⊢ (z = A \land u = D) \to z \underset{˙}{+} u = A \underset{˙}{+} D$
3		oveq12	$⊢ (w = B \land v = C) \to w \underset{˙}{+} v = B \underset{˙}{+} C$
4	2 3	eqeqan12d	$⊢ ((z = A \land u = D) \land (w = B \land v = C)) \to (z \underset{˙}{+} u = w \underset{˙}{+} v \leftrightarrow A \underset{˙}{+} D = B \underset{˙}{+} C)$
5	4	an42s	$⊢ ((z = A \land w = B) \land (v = C \land u = D)) \to (z \underset{˙}{+} u = w \underset{˙}{+} v \leftrightarrow A \underset{˙}{+} D = B \underset{˙}{+} C)$
6	5 1	opbrop	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to (⟨A, B⟩ \underset{˙}{\sim} ⟨C, D⟩ \leftrightarrow A \underset{˙}{+} D = B \underset{˙}{+} C)$

Metamath Proof Explorer

Theorem ecopoveq

Proof