Proof of Theorem ecovass
Step | Hyp | Ref
| Expression |
1 | | ecovass.1 |
. 2
⊢ 𝐷 = ((𝑆 × 𝑆) / ∼ ) |
2 | | oveq1 5860 |
. . . 4
⊢
([〈𝑥, 𝑦〉] ∼ = 𝐴 → ([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) = (𝐴 + [〈𝑧, 𝑤〉] ∼ )) |
3 | 2 | oveq1d 5868 |
. . 3
⊢
([〈𝑥, 𝑦〉] ∼ = 𝐴 → (([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) + [〈𝑣, 𝑢〉] ∼ ) = ((𝐴 + [〈𝑧, 𝑤〉] ∼ ) + [〈𝑣, 𝑢〉] ∼ )) |
4 | | oveq1 5860 |
. . 3
⊢
([〈𝑥, 𝑦〉] ∼ = 𝐴 → ([〈𝑥, 𝑦〉] ∼ + ([〈𝑧, 𝑤〉] ∼ + [〈𝑣, 𝑢〉] ∼ )) = (𝐴 + ([〈𝑧, 𝑤〉] ∼ + [〈𝑣, 𝑢〉] ∼
))) |
5 | 3, 4 | eqeq12d 2185 |
. 2
⊢
([〈𝑥, 𝑦〉] ∼ = 𝐴 → ((([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) + [〈𝑣, 𝑢〉] ∼ ) = ([〈𝑥, 𝑦〉] ∼ + ([〈𝑧, 𝑤〉] ∼ + [〈𝑣, 𝑢〉] ∼ )) ↔ ((𝐴 + [〈𝑧, 𝑤〉] ∼ ) + [〈𝑣, 𝑢〉] ∼ ) = (𝐴 + ([〈𝑧, 𝑤〉] ∼ + [〈𝑣, 𝑢〉] ∼
)))) |
6 | | oveq2 5861 |
. . . 4
⊢
([〈𝑧, 𝑤〉] ∼ = 𝐵 → (𝐴 + [〈𝑧, 𝑤〉] ∼ ) = (𝐴 + 𝐵)) |
7 | 6 | oveq1d 5868 |
. . 3
⊢
([〈𝑧, 𝑤〉] ∼ = 𝐵 → ((𝐴 + [〈𝑧, 𝑤〉] ∼ ) + [〈𝑣, 𝑢〉] ∼ ) = ((𝐴 + 𝐵) + [〈𝑣, 𝑢〉] ∼ )) |
8 | | oveq1 5860 |
. . . 4
⊢
([〈𝑧, 𝑤〉] ∼ = 𝐵 → ([〈𝑧, 𝑤〉] ∼ + [〈𝑣, 𝑢〉] ∼ ) = (𝐵 + [〈𝑣, 𝑢〉] ∼ )) |
9 | 8 | oveq2d 5869 |
. . 3
⊢
([〈𝑧, 𝑤〉] ∼ = 𝐵 → (𝐴 + ([〈𝑧, 𝑤〉] ∼ + [〈𝑣, 𝑢〉] ∼ )) = (𝐴 + (𝐵 + [〈𝑣, 𝑢〉] ∼
))) |
10 | 7, 9 | eqeq12d 2185 |
. 2
⊢
([〈𝑧, 𝑤〉] ∼ = 𝐵 → (((𝐴 + [〈𝑧, 𝑤〉] ∼ ) + [〈𝑣, 𝑢〉] ∼ ) = (𝐴 + ([〈𝑧, 𝑤〉] ∼ + [〈𝑣, 𝑢〉] ∼ )) ↔ ((𝐴 + 𝐵) + [〈𝑣, 𝑢〉] ∼ ) = (𝐴 + (𝐵 + [〈𝑣, 𝑢〉] ∼
)))) |
11 | | oveq2 5861 |
. . 3
⊢
([〈𝑣, 𝑢〉] ∼ = 𝐶 → ((𝐴 + 𝐵) + [〈𝑣, 𝑢〉] ∼ ) = ((𝐴 + 𝐵) + 𝐶)) |
12 | | oveq2 5861 |
. . . 4
⊢
([〈𝑣, 𝑢〉] ∼ = 𝐶 → (𝐵 + [〈𝑣, 𝑢〉] ∼ ) = (𝐵 + 𝐶)) |
13 | 12 | oveq2d 5869 |
. . 3
⊢
([〈𝑣, 𝑢〉] ∼ = 𝐶 → (𝐴 + (𝐵 + [〈𝑣, 𝑢〉] ∼ )) = (𝐴 + (𝐵 + 𝐶))) |
14 | 11, 13 | eqeq12d 2185 |
. 2
⊢
([〈𝑣, 𝑢〉] ∼ = 𝐶 → (((𝐴 + 𝐵) + [〈𝑣, 𝑢〉] ∼ ) = (𝐴 + (𝐵 + [〈𝑣, 𝑢〉] ∼ )) ↔ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))) |
15 | | ecovass.8 |
. . . 4
⊢ 𝐽 = 𝐿 |
16 | | ecovass.9 |
. . . 4
⊢ 𝐾 = 𝑀 |
17 | | opeq12 3767 |
. . . . 5
⊢ ((𝐽 = 𝐿 ∧ 𝐾 = 𝑀) → 〈𝐽, 𝐾〉 = 〈𝐿, 𝑀〉) |
18 | 17 | eceq1d 6549 |
. . . 4
⊢ ((𝐽 = 𝐿 ∧ 𝐾 = 𝑀) → [〈𝐽, 𝐾〉] ∼ = [〈𝐿, 𝑀〉] ∼ ) |
19 | 15, 16, 18 | mp2an 424 |
. . 3
⊢
[〈𝐽, 𝐾〉] ∼ = [〈𝐿, 𝑀〉] ∼ |
20 | | ecovass.2 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) = [〈𝐺, 𝐻〉] ∼ ) |
21 | 20 | oveq1d 5868 |
. . . . . 6
⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → (([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) + [〈𝑣, 𝑢〉] ∼ ) = ([〈𝐺, 𝐻〉] ∼ + [〈𝑣, 𝑢〉] ∼ )) |
22 | 21 | adantr 274 |
. . . . 5
⊢ ((((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) + [〈𝑣, 𝑢〉] ∼ ) = ([〈𝐺, 𝐻〉] ∼ + [〈𝑣, 𝑢〉] ∼ )) |
23 | | ecovass.6 |
. . . . . 6
⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → (𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆)) |
24 | | ecovass.4 |
. . . . . 6
⊢ (((𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([〈𝐺, 𝐻〉] ∼ + [〈𝑣, 𝑢〉] ∼ ) = [〈𝐽, 𝐾〉] ∼ ) |
25 | 23, 24 | sylan 281 |
. . . . 5
⊢ ((((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([〈𝐺, 𝐻〉] ∼ + [〈𝑣, 𝑢〉] ∼ ) = [〈𝐽, 𝐾〉] ∼ ) |
26 | 22, 25 | eqtrd 2203 |
. . . 4
⊢ ((((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) + [〈𝑣, 𝑢〉] ∼ ) = [〈𝐽, 𝐾〉] ∼ ) |
27 | 26 | 3impa 1189 |
. . 3
⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) + [〈𝑣, 𝑢〉] ∼ ) = [〈𝐽, 𝐾〉] ∼ ) |
28 | | ecovass.3 |
. . . . . . 7
⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([〈𝑧, 𝑤〉] ∼ + [〈𝑣, 𝑢〉] ∼ ) = [〈𝑁, 𝑄〉] ∼ ) |
29 | 28 | oveq2d 5869 |
. . . . . 6
⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ + ([〈𝑧, 𝑤〉] ∼ + [〈𝑣, 𝑢〉] ∼ )) = ([〈𝑥, 𝑦〉] ∼ + [〈𝑁, 𝑄〉] ∼ )) |
30 | 29 | adantl 275 |
. . . . 5
⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ ((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆))) → ([〈𝑥, 𝑦〉] ∼ + ([〈𝑧, 𝑤〉] ∼ + [〈𝑣, 𝑢〉] ∼ )) = ([〈𝑥, 𝑦〉] ∼ + [〈𝑁, 𝑄〉] ∼ )) |
31 | | ecovass.7 |
. . . . . 6
⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑁 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆)) |
32 | | ecovass.5 |
. . . . . 6
⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑁 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ + [〈𝑁, 𝑄〉] ∼ ) = [〈𝐿, 𝑀〉] ∼ ) |
33 | 31, 32 | sylan2 284 |
. . . . 5
⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ ((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆))) → ([〈𝑥, 𝑦〉] ∼ + [〈𝑁, 𝑄〉] ∼ ) = [〈𝐿, 𝑀〉] ∼ ) |
34 | 30, 33 | eqtrd 2203 |
. . . 4
⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ ((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆))) → ([〈𝑥, 𝑦〉] ∼ + ([〈𝑧, 𝑤〉] ∼ + [〈𝑣, 𝑢〉] ∼ )) = [〈𝐿, 𝑀〉] ∼ ) |
35 | 34 | 3impb 1194 |
. . 3
⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ + ([〈𝑧, 𝑤〉] ∼ + [〈𝑣, 𝑢〉] ∼ )) = [〈𝐿, 𝑀〉] ∼ ) |
36 | 19, 27, 35 | 3eqtr4a 2229 |
. 2
⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) + [〈𝑣, 𝑢〉] ∼ ) = ([〈𝑥, 𝑦〉] ∼ + ([〈𝑧, 𝑤〉] ∼ + [〈𝑣, 𝑢〉] ∼
))) |
37 | 1, 5, 10, 14, 36 | 3ecoptocl 6602 |
1
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |