Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ecovcom | Structured version Visualization version GIF version |
Description: Lemma used to transfer a commutative law via an equivalence relation. (Contributed by NM, 29-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.) |
Ref | Expression |
---|---|
ecovcom.1 | ⊢ 𝐶 = ((𝑆 × 𝑆) / ∼ ) |
ecovcom.2 | ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) = [〈𝐷, 𝐺〉] ∼ ) |
ecovcom.3 | ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ([〈𝑧, 𝑤〉] ∼ + [〈𝑥, 𝑦〉] ∼ ) = [〈𝐻, 𝐽〉] ∼ ) |
ecovcom.4 | ⊢ 𝐷 = 𝐻 |
ecovcom.5 | ⊢ 𝐺 = 𝐽 |
Ref | Expression |
---|---|
ecovcom | ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ecovcom.1 | . 2 ⊢ 𝐶 = ((𝑆 × 𝑆) / ∼ ) | |
2 | oveq1 7163 | . . 3 ⊢ ([〈𝑥, 𝑦〉] ∼ = 𝐴 → ([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) = (𝐴 + [〈𝑧, 𝑤〉] ∼ )) | |
3 | oveq2 7164 | . . 3 ⊢ ([〈𝑥, 𝑦〉] ∼ = 𝐴 → ([〈𝑧, 𝑤〉] ∼ + [〈𝑥, 𝑦〉] ∼ ) = ([〈𝑧, 𝑤〉] ∼ + 𝐴)) | |
4 | 2, 3 | eqeq12d 2837 | . 2 ⊢ ([〈𝑥, 𝑦〉] ∼ = 𝐴 → (([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) = ([〈𝑧, 𝑤〉] ∼ + [〈𝑥, 𝑦〉] ∼ ) ↔ (𝐴 + [〈𝑧, 𝑤〉] ∼ ) = ([〈𝑧, 𝑤〉] ∼ + 𝐴))) |
5 | oveq2 7164 | . . 3 ⊢ ([〈𝑧, 𝑤〉] ∼ = 𝐵 → (𝐴 + [〈𝑧, 𝑤〉] ∼ ) = (𝐴 + 𝐵)) | |
6 | oveq1 7163 | . . 3 ⊢ ([〈𝑧, 𝑤〉] ∼ = 𝐵 → ([〈𝑧, 𝑤〉] ∼ + 𝐴) = (𝐵 + 𝐴)) | |
7 | 5, 6 | eqeq12d 2837 | . 2 ⊢ ([〈𝑧, 𝑤〉] ∼ = 𝐵 → ((𝐴 + [〈𝑧, 𝑤〉] ∼ ) = ([〈𝑧, 𝑤〉] ∼ + 𝐴) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴))) |
8 | ecovcom.4 | . . . 4 ⊢ 𝐷 = 𝐻 | |
9 | ecovcom.5 | . . . 4 ⊢ 𝐺 = 𝐽 | |
10 | opeq12 4805 | . . . . 5 ⊢ ((𝐷 = 𝐻 ∧ 𝐺 = 𝐽) → 〈𝐷, 𝐺〉 = 〈𝐻, 𝐽〉) | |
11 | 10 | eceq1d 8328 | . . . 4 ⊢ ((𝐷 = 𝐻 ∧ 𝐺 = 𝐽) → [〈𝐷, 𝐺〉] ∼ = [〈𝐻, 𝐽〉] ∼ ) |
12 | 8, 9, 11 | mp2an 690 | . . 3 ⊢ [〈𝐷, 𝐺〉] ∼ = [〈𝐻, 𝐽〉] ∼ |
13 | ecovcom.2 | . . 3 ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) = [〈𝐷, 𝐺〉] ∼ ) | |
14 | ecovcom.3 | . . . 4 ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ([〈𝑧, 𝑤〉] ∼ + [〈𝑥, 𝑦〉] ∼ ) = [〈𝐻, 𝐽〉] ∼ ) | |
15 | 14 | ancoms 461 | . . 3 ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([〈𝑧, 𝑤〉] ∼ + [〈𝑥, 𝑦〉] ∼ ) = [〈𝐻, 𝐽〉] ∼ ) |
16 | 12, 13, 15 | 3eqtr4a 2882 | . 2 ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) = ([〈𝑧, 𝑤〉] ∼ + [〈𝑥, 𝑦〉] ∼ )) |
17 | 1, 4, 7, 16 | 2ecoptocl 8388 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1537 ∈ wcel 2114 〈cop 4573 × cxp 5553 (class class class)co 7156 [cec 8287 / cqs 8288 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pr 5330 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3496 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4839 df-br 5067 df-opab 5129 df-xp 5561 df-cnv 5563 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-iota 6314 df-fv 6363 df-ov 7159 df-ec 8291 df-qs 8295 |
This theorem is referenced by: addcomsr 10509 mulcomsr 10511 axmulcom 10577 |
Copyright terms: Public domain | W3C validator |