![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ecopoveq | Structured version Visualization version GIF version |
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 𝐹. (Contributed by NM, 16-Aug-1995.) |
Ref | Expression |
---|---|
ecopopr.1 | ⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} |
Ref | Expression |
---|---|
ecopoveq | ⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (〈𝐴, 𝐵〉 ∼ 〈𝐶, 𝐷〉 ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq12 7360 | . . . 4 ⊢ ((𝑧 = 𝐴 ∧ 𝑢 = 𝐷) → (𝑧 + 𝑢) = (𝐴 + 𝐷)) | |
2 | oveq12 7360 | . . . 4 ⊢ ((𝑤 = 𝐵 ∧ 𝑣 = 𝐶) → (𝑤 + 𝑣) = (𝐵 + 𝐶)) | |
3 | 1, 2 | eqeqan12d 2750 | . . 3 ⊢ (((𝑧 = 𝐴 ∧ 𝑢 = 𝐷) ∧ (𝑤 = 𝐵 ∧ 𝑣 = 𝐶)) → ((𝑧 + 𝑢) = (𝑤 + 𝑣) ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) |
4 | 3 | an42s 659 | . 2 ⊢ (((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) ∧ (𝑣 = 𝐶 ∧ 𝑢 = 𝐷)) → ((𝑧 + 𝑢) = (𝑤 + 𝑣) ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) |
5 | ecopopr.1 | . 2 ⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} | |
6 | 4, 5 | opbrop 5727 | 1 ⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (〈𝐴, 𝐵〉 ∼ 〈𝐶, 𝐷〉 ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∃wex 1781 ∈ wcel 2106 〈cop 4590 class class class wbr 5103 {copab 5165 × cxp 5629 (class class class)co 7351 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 ax-sep 5254 ax-nul 5261 ax-pr 5382 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-ral 3063 df-rex 3072 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-br 5104 df-opab 5166 df-xp 5637 df-iota 6445 df-fv 6501 df-ov 7354 |
This theorem is referenced by: ecopovsym 8716 ecopovtrn 8717 ecopover 8718 enqbreq 10813 enrbreq 10959 prsrlem1 10966 |
Copyright terms: Public domain | W3C validator |