![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ecovcom | GIF version |
Description: Lemma used to transfer a commutative law via an equivalence relation. Most uses will want ecovicom 6467 instead. (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 5713 | . . 3 ⊢ ([〈𝑥, 𝑦〉] ∼ = 𝐴 → ([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) = (𝐴 + [〈𝑧, 𝑤〉] ∼ )) | |
3 | oveq2 5714 | . . 3 ⊢ ([〈𝑥, 𝑦〉] ∼ = 𝐴 → ([〈𝑧, 𝑤〉] ∼ + [〈𝑥, 𝑦〉] ∼ ) = ([〈𝑧, 𝑤〉] ∼ + 𝐴)) | |
4 | 2, 3 | eqeq12d 2114 | . 2 ⊢ ([〈𝑥, 𝑦〉] ∼ = 𝐴 → (([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) = ([〈𝑧, 𝑤〉] ∼ + [〈𝑥, 𝑦〉] ∼ ) ↔ (𝐴 + [〈𝑧, 𝑤〉] ∼ ) = ([〈𝑧, 𝑤〉] ∼ + 𝐴))) |
5 | oveq2 5714 | . . 3 ⊢ ([〈𝑧, 𝑤〉] ∼ = 𝐵 → (𝐴 + [〈𝑧, 𝑤〉] ∼ ) = (𝐴 + 𝐵)) | |
6 | oveq1 5713 | . . 3 ⊢ ([〈𝑧, 𝑤〉] ∼ = 𝐵 → ([〈𝑧, 𝑤〉] ∼ + 𝐴) = (𝐵 + 𝐴)) | |
7 | 5, 6 | eqeq12d 2114 | . 2 ⊢ ([〈𝑧, 𝑤〉] ∼ = 𝐵 → ((𝐴 + [〈𝑧, 𝑤〉] ∼ ) = ([〈𝑧, 𝑤〉] ∼ + 𝐴) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴))) |
8 | ecovcom.4 | . . . 4 ⊢ 𝐷 = 𝐻 | |
9 | ecovcom.5 | . . . 4 ⊢ 𝐺 = 𝐽 | |
10 | opeq12 3654 | . . . . 5 ⊢ ((𝐷 = 𝐻 ∧ 𝐺 = 𝐽) → 〈𝐷, 𝐺〉 = 〈𝐻, 𝐽〉) | |
11 | 10 | eceq1d 6395 | . . . 4 ⊢ ((𝐷 = 𝐻 ∧ 𝐺 = 𝐽) → [〈𝐷, 𝐺〉] ∼ = [〈𝐻, 𝐽〉] ∼ ) |
12 | 8, 9, 11 | mp2an 420 | . . 3 ⊢ [〈𝐷, 𝐺〉] ∼ = [〈𝐻, 𝐽〉] ∼ |
13 | ecovcom.2 | . . 3 ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) = [〈𝐷, 𝐺〉] ∼ ) | |
14 | ecovcom.3 | . . . 4 ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ([〈𝑧, 𝑤〉] ∼ + [〈𝑥, 𝑦〉] ∼ ) = [〈𝐻, 𝐽〉] ∼ ) | |
15 | 14 | ancoms 266 | . . 3 ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([〈𝑧, 𝑤〉] ∼ + [〈𝑥, 𝑦〉] ∼ ) = [〈𝐻, 𝐽〉] ∼ ) |
16 | 12, 13, 15 | 3eqtr4a 2158 | . 2 ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) = ([〈𝑧, 𝑤〉] ∼ + [〈𝑥, 𝑦〉] ∼ )) |
17 | 1, 4, 7, 16 | 2ecoptocl 6447 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 = wceq 1299 ∈ wcel 1448 〈cop 3477 × cxp 4475 (class class class)co 5706 [cec 6357 / cqs 6358 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-14 1460 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 ax-sep 3986 ax-pow 4038 ax-pr 4069 |
This theorem depends on definitions: df-bi 116 df-3an 932 df-tru 1302 df-nf 1405 df-sb 1704 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-ral 2380 df-rex 2381 df-v 2643 df-un 3025 df-in 3027 df-ss 3034 df-pw 3459 df-sn 3480 df-pr 3481 df-op 3483 df-uni 3684 df-br 3876 df-opab 3930 df-xp 4483 df-cnv 4485 df-dm 4487 df-rn 4488 df-res 4489 df-ima 4490 df-iota 5024 df-fv 5067 df-ov 5709 df-ec 6361 df-qs 6365 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |