Proof of Theorem ecovidi
Step | Hyp | Ref
| Expression |
1 | | ecovidi.1 |
. 2
⊢ 𝐷 = ((𝑆 × 𝑆) / ∼ ) |
2 | | oveq1 5462 |
. . 3
⊢
([〈x, y〉] ∼ = A → ([〈x, y〉]
∼
·
([〈z, w〉] ∼ + [〈v, u〉]
∼
)) = (A · ([〈z, w〉]
∼
+
[〈v, u〉] ∼
))) |
3 | | oveq1 5462 |
. . . 4
⊢
([〈x, y〉] ∼ = A → ([〈x, y〉]
∼
·
[〈z, w〉] ∼ ) = (A · [〈z, w〉]
∼
)) |
4 | | oveq1 5462 |
. . . 4
⊢
([〈x, y〉] ∼ = A → ([〈x, y〉]
∼
·
[〈v, u〉] ∼ ) = (A · [〈v, u〉]
∼
)) |
5 | 3, 4 | oveq12d 5473 |
. . 3
⊢
([〈x, y〉] ∼ = A → (([〈x, y〉]
∼
·
[〈z, w〉] ∼ ) +
([〈x, y〉] ∼ · [〈v, u〉]
∼
)) = ((A · [〈z, w〉]
∼
) +
(A · [〈v, u〉]
∼
))) |
6 | 2, 5 | eqeq12d 2051 |
. 2
⊢
([〈x, y〉] ∼ = A → (([〈x, y〉]
∼
·
([〈z, w〉] ∼ + [〈v, u〉]
∼
)) = (([〈x, y〉] ∼ · [〈z, w〉]
∼
) +
([〈x, y〉] ∼ · [〈v, u〉]
∼
)) ↔ (A · ([〈z, w〉]
∼
+
[〈v, u〉] ∼ )) = ((A · [〈z, w〉]
∼
) +
(A · [〈v, u〉]
∼
)))) |
7 | | oveq1 5462 |
. . . 4
⊢
([〈z, w〉] ∼ = B → ([〈z, w〉]
∼
+
[〈v, u〉] ∼ ) = (B + [〈v, u〉]
∼
)) |
8 | 7 | oveq2d 5471 |
. . 3
⊢
([〈z, w〉] ∼ = B → (A
·
([〈z, w〉] ∼ + [〈v, u〉]
∼
)) = (A · (B + [〈v, u〉]
∼
))) |
9 | | oveq2 5463 |
. . . 4
⊢
([〈z, w〉] ∼ = B → (A
·
[〈z, w〉] ∼ ) = (A · B)) |
10 | 9 | oveq1d 5470 |
. . 3
⊢
([〈z, w〉] ∼ = B → ((A
·
[〈z, w〉] ∼ ) + (A · [〈v, u〉]
∼
)) = ((A · B) + (A · [〈v, u〉]
∼
))) |
11 | 8, 10 | eqeq12d 2051 |
. 2
⊢
([〈z, w〉] ∼ = B → ((A
·
([〈z, w〉] ∼ + [〈v, u〉]
∼
)) = ((A · [〈z, w〉]
∼
) +
(A · [〈v, u〉]
∼
)) ↔ (A · (B + [〈v, u〉]
∼
)) = ((A · B) + (A · [〈v, u〉]
∼
)))) |
12 | | oveq2 5463 |
. . . 4
⊢
([〈v, u〉] ∼ = 𝐶 → (B + [〈v, u〉]
∼
) = (B + 𝐶)) |
13 | 12 | oveq2d 5471 |
. . 3
⊢
([〈v, u〉] ∼ = 𝐶 → (A · (B + [〈v, u〉]
∼
)) = (A · (B + 𝐶))) |
14 | | oveq2 5463 |
. . . 4
⊢
([〈v, u〉] ∼ = 𝐶 → (A · [〈v, u〉]
∼
) = (A · 𝐶)) |
15 | 14 | oveq2d 5471 |
. . 3
⊢
([〈v, u〉] ∼ = 𝐶 → ((A · B) + (A · [〈v, u〉]
∼
)) = ((A · B) + (A · 𝐶))) |
16 | 13, 15 | eqeq12d 2051 |
. 2
⊢
([〈v, u〉] ∼ = 𝐶 → ((A · (B + [〈v, u〉]
∼
)) = ((A · B) + (A · [〈v, u〉]
∼
)) ↔ (A · (B + 𝐶)) = ((A
·
B) + (A · 𝐶)))) |
17 | | ecovidi.10 |
. . . 4
⊢
(((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → 𝐻 = 𝐾) |
18 | | ecovidi.11 |
. . . 4
⊢
(((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → 𝐽 = 𝐿) |
19 | | opeq12 3542 |
. . . . 5
⊢ ((𝐻 = 𝐾 ∧ 𝐽 = 𝐿) → 〈𝐻, 𝐽〉 = 〈𝐾, 𝐿〉) |
20 | 19 | eceq1d 6078 |
. . . 4
⊢ ((𝐻 = 𝐾 ∧ 𝐽 = 𝐿) → [〈𝐻, 𝐽〉] ∼ = [〈𝐾, 𝐿〉] ∼ ) |
21 | 17, 18, 20 | syl2anc 391 |
. . 3
⊢
(((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → [〈𝐻, 𝐽〉] ∼ = [〈𝐾, 𝐿〉] ∼ ) |
22 | | ecovidi.2 |
. . . . . . 7
⊢
(((z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → ([〈z, w〉]
∼
+
[〈v, u〉] ∼ ) = [〈𝑀, 𝑁〉] ∼ ) |
23 | 22 | oveq2d 5471 |
. . . . . 6
⊢
(((z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → ([〈x, y〉]
∼
·
([〈z, w〉] ∼ + [〈v, u〉]
∼
)) = ([〈x, y〉] ∼ · [〈𝑀, 𝑁〉] ∼ )) |
24 | 23 | adantl 262 |
. . . . 5
⊢
(((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ ((z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆))) → ([〈x, y〉]
∼
·
([〈z, w〉] ∼ + [〈v, u〉]
∼
)) = ([〈x, y〉] ∼ · [〈𝑀, 𝑁〉] ∼ )) |
25 | | ecovidi.7 |
. . . . . 6
⊢
(((z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) |
26 | | ecovidi.3 |
. . . . . 6
⊢
(((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) → ([〈x, y〉]
∼
·
[〈𝑀, 𝑁〉] ∼ ) = [〈𝐻, 𝐽〉] ∼ ) |
27 | 25, 26 | sylan2 270 |
. . . . 5
⊢
(((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ ((z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆))) → ([〈x, y〉]
∼
·
[〈𝑀, 𝑁〉] ∼ ) = [〈𝐻, 𝐽〉] ∼ ) |
28 | 24, 27 | eqtrd 2069 |
. . . 4
⊢
(((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ ((z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆))) → ([〈x, y〉]
∼
·
([〈z, w〉] ∼ + [〈v, u〉]
∼
)) = [〈𝐻, 𝐽〉] ∼ ) |
29 | 28 | 3impb 1099 |
. . 3
⊢
(((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → ([〈x, y〉]
∼
·
([〈z, w〉] ∼ + [〈v, u〉]
∼
)) = [〈𝐻, 𝐽〉] ∼ ) |
30 | | ecovidi.4 |
. . . . . 6
⊢
(((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆)) → ([〈x, y〉]
∼
·
[〈z, w〉] ∼ ) = [〈𝑊, 𝑋〉] ∼ ) |
31 | | ecovidi.5 |
. . . . . 6
⊢
(((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → ([〈x, y〉]
∼
·
[〈v, u〉] ∼ ) = [〈𝑌, 𝑍〉] ∼ ) |
32 | 30, 31 | oveqan12d 5474 |
. . . . 5
⊢
((((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆)) ∧ ((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆))) → (([〈x, y〉]
∼
·
[〈z, w〉] ∼ ) +
([〈x, y〉] ∼ · [〈v, u〉]
∼
)) = ([〈𝑊, 𝑋〉] ∼ + [〈𝑌, 𝑍〉] ∼ )) |
33 | | ecovidi.8 |
. . . . . 6
⊢
(((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆)) → (𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆)) |
34 | | ecovidi.9 |
. . . . . 6
⊢
(((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → (𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆)) |
35 | | ecovidi.6 |
. . . . . 6
⊢ (((𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆) ∧ (𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆)) → ([〈𝑊, 𝑋〉] ∼ + [〈𝑌, 𝑍〉] ∼ ) = [〈𝐾, 𝐿〉] ∼ ) |
36 | 33, 34, 35 | syl2an 273 |
. . . . 5
⊢
((((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆)) ∧ ((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆))) → ([〈𝑊, 𝑋〉] ∼ + [〈𝑌, 𝑍〉] ∼ ) = [〈𝐾, 𝐿〉] ∼ ) |
37 | 32, 36 | eqtrd 2069 |
. . . 4
⊢
((((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆)) ∧ ((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆))) → (([〈x, y〉]
∼
·
[〈z, w〉] ∼ ) +
([〈x, y〉] ∼ · [〈v, u〉]
∼
)) = [〈𝐾, 𝐿〉] ∼ ) |
38 | 37 | 3impdi 1189 |
. . 3
⊢
(((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → (([〈x, y〉]
∼
·
[〈z, w〉] ∼ ) +
([〈x, y〉] ∼ · [〈v, u〉]
∼
)) = [〈𝐾, 𝐿〉] ∼ ) |
39 | 21, 29, 38 | 3eqtr4d 2079 |
. 2
⊢
(((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → ([〈x, y〉]
∼
·
([〈z, w〉] ∼ + [〈v, u〉]
∼
)) = (([〈x, y〉] ∼ · [〈z, w〉]
∼
) +
([〈x, y〉] ∼ · [〈v, u〉]
∼
))) |
40 | 1, 6, 11, 16, 39 | 3ecoptocl 6131 |
1
⊢
((A ∈ 𝐷 ∧ B ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → (A · (B + 𝐶)) = ((A
·
B) + (A · 𝐶))) |