Step | Hyp | Ref
| Expression |
1 | | oveq1 7278 |
. . . . 5
⊢ (𝑎 = 𝐴 → (𝑎𝐼𝑐) = (𝐴𝐼𝑐)) |
2 | 1 | eleq2d 2826 |
. . . 4
⊢ (𝑎 = 𝐴 → (𝑏 ∈ (𝑎𝐼𝑐) ↔ 𝑏 ∈ (𝐴𝐼𝑐))) |
3 | 2 | anbi1d 630 |
. . 3
⊢ (𝑎 = 𝐴 → ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ (𝑏 ∈ (𝐴𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)))) |
4 | | oveq1 7278 |
. . . . 5
⊢ (𝑎 = 𝐴 → (𝑎 − 𝑏) = (𝐴 − 𝑏)) |
5 | 4 | eqeq1d 2742 |
. . . 4
⊢ (𝑎 = 𝐴 → ((𝑎 − 𝑏) = (𝑥 − 𝑦) ↔ (𝐴 − 𝑏) = (𝑥 − 𝑦))) |
6 | 5 | anbi1d 630 |
. . 3
⊢ (𝑎 = 𝐴 → (((𝑎 − 𝑏) = (𝑥 − 𝑦) ∧ (𝑏 − 𝑐) = (𝑦 − 𝑧)) ↔ ((𝐴 − 𝑏) = (𝑥 − 𝑦) ∧ (𝑏 − 𝑐) = (𝑦 − 𝑧)))) |
7 | | oveq1 7278 |
. . . . 5
⊢ (𝑎 = 𝐴 → (𝑎 − 𝑑) = (𝐴 − 𝑑)) |
8 | 7 | eqeq1d 2742 |
. . . 4
⊢ (𝑎 = 𝐴 → ((𝑎 − 𝑑) = (𝑥 − 𝑤) ↔ (𝐴 − 𝑑) = (𝑥 − 𝑤))) |
9 | 8 | anbi1d 630 |
. . 3
⊢ (𝑎 = 𝐴 → (((𝑎 − 𝑑) = (𝑥 − 𝑤) ∧ (𝑏 − 𝑑) = (𝑦 − 𝑤)) ↔ ((𝐴 − 𝑑) = (𝑥 − 𝑤) ∧ (𝑏 − 𝑑) = (𝑦 − 𝑤)))) |
10 | 3, 6, 9 | 3anbi123d 1435 |
. 2
⊢ (𝑎 = 𝐴 → (((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 − 𝑏) = (𝑥 − 𝑦) ∧ (𝑏 − 𝑐) = (𝑦 − 𝑧)) ∧ ((𝑎 − 𝑑) = (𝑥 − 𝑤) ∧ (𝑏 − 𝑑) = (𝑦 − 𝑤))) ↔ ((𝑏 ∈ (𝐴𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝐴 − 𝑏) = (𝑥 − 𝑦) ∧ (𝑏 − 𝑐) = (𝑦 − 𝑧)) ∧ ((𝐴 − 𝑑) = (𝑥 − 𝑤) ∧ (𝑏 − 𝑑) = (𝑦 − 𝑤))))) |
11 | | eleq1 2828 |
. . . 4
⊢ (𝑏 = 𝐵 → (𝑏 ∈ (𝐴𝐼𝑐) ↔ 𝐵 ∈ (𝐴𝐼𝑐))) |
12 | 11 | anbi1d 630 |
. . 3
⊢ (𝑏 = 𝐵 → ((𝑏 ∈ (𝐴𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ (𝐵 ∈ (𝐴𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)))) |
13 | | oveq2 7279 |
. . . . 5
⊢ (𝑏 = 𝐵 → (𝐴 − 𝑏) = (𝐴 − 𝐵)) |
14 | 13 | eqeq1d 2742 |
. . . 4
⊢ (𝑏 = 𝐵 → ((𝐴 − 𝑏) = (𝑥 − 𝑦) ↔ (𝐴 − 𝐵) = (𝑥 − 𝑦))) |
15 | | oveq1 7278 |
. . . . 5
⊢ (𝑏 = 𝐵 → (𝑏 − 𝑐) = (𝐵 − 𝑐)) |
16 | 15 | eqeq1d 2742 |
. . . 4
⊢ (𝑏 = 𝐵 → ((𝑏 − 𝑐) = (𝑦 − 𝑧) ↔ (𝐵 − 𝑐) = (𝑦 − 𝑧))) |
17 | 14, 16 | anbi12d 631 |
. . 3
⊢ (𝑏 = 𝐵 → (((𝐴 − 𝑏) = (𝑥 − 𝑦) ∧ (𝑏 − 𝑐) = (𝑦 − 𝑧)) ↔ ((𝐴 − 𝐵) = (𝑥 − 𝑦) ∧ (𝐵 − 𝑐) = (𝑦 − 𝑧)))) |
18 | | oveq1 7278 |
. . . . 5
⊢ (𝑏 = 𝐵 → (𝑏 − 𝑑) = (𝐵 − 𝑑)) |
19 | 18 | eqeq1d 2742 |
. . . 4
⊢ (𝑏 = 𝐵 → ((𝑏 − 𝑑) = (𝑦 − 𝑤) ↔ (𝐵 − 𝑑) = (𝑦 − 𝑤))) |
20 | 19 | anbi2d 629 |
. . 3
⊢ (𝑏 = 𝐵 → (((𝐴 − 𝑑) = (𝑥 − 𝑤) ∧ (𝑏 − 𝑑) = (𝑦 − 𝑤)) ↔ ((𝐴 − 𝑑) = (𝑥 − 𝑤) ∧ (𝐵 − 𝑑) = (𝑦 − 𝑤)))) |
21 | 12, 17, 20 | 3anbi123d 1435 |
. 2
⊢ (𝑏 = 𝐵 → (((𝑏 ∈ (𝐴𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝐴 − 𝑏) = (𝑥 − 𝑦) ∧ (𝑏 − 𝑐) = (𝑦 − 𝑧)) ∧ ((𝐴 − 𝑑) = (𝑥 − 𝑤) ∧ (𝑏 − 𝑑) = (𝑦 − 𝑤))) ↔ ((𝐵 ∈ (𝐴𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝐴 − 𝐵) = (𝑥 − 𝑦) ∧ (𝐵 − 𝑐) = (𝑦 − 𝑧)) ∧ ((𝐴 − 𝑑) = (𝑥 − 𝑤) ∧ (𝐵 − 𝑑) = (𝑦 − 𝑤))))) |
22 | | oveq2 7279 |
. . . . 5
⊢ (𝑐 = 𝐶 → (𝐴𝐼𝑐) = (𝐴𝐼𝐶)) |
23 | 22 | eleq2d 2826 |
. . . 4
⊢ (𝑐 = 𝐶 → (𝐵 ∈ (𝐴𝐼𝑐) ↔ 𝐵 ∈ (𝐴𝐼𝐶))) |
24 | 23 | anbi1d 630 |
. . 3
⊢ (𝑐 = 𝐶 → ((𝐵 ∈ (𝐴𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ (𝐵 ∈ (𝐴𝐼𝐶) ∧ 𝑦 ∈ (𝑥𝐼𝑧)))) |
25 | | oveq2 7279 |
. . . . 5
⊢ (𝑐 = 𝐶 → (𝐵 − 𝑐) = (𝐵 − 𝐶)) |
26 | 25 | eqeq1d 2742 |
. . . 4
⊢ (𝑐 = 𝐶 → ((𝐵 − 𝑐) = (𝑦 − 𝑧) ↔ (𝐵 − 𝐶) = (𝑦 − 𝑧))) |
27 | 26 | anbi2d 629 |
. . 3
⊢ (𝑐 = 𝐶 → (((𝐴 − 𝐵) = (𝑥 − 𝑦) ∧ (𝐵 − 𝑐) = (𝑦 − 𝑧)) ↔ ((𝐴 − 𝐵) = (𝑥 − 𝑦) ∧ (𝐵 − 𝐶) = (𝑦 − 𝑧)))) |
28 | 24, 27 | 3anbi12d 1436 |
. 2
⊢ (𝑐 = 𝐶 → (((𝐵 ∈ (𝐴𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝐴 − 𝐵) = (𝑥 − 𝑦) ∧ (𝐵 − 𝑐) = (𝑦 − 𝑧)) ∧ ((𝐴 − 𝑑) = (𝑥 − 𝑤) ∧ (𝐵 − 𝑑) = (𝑦 − 𝑤))) ↔ ((𝐵 ∈ (𝐴𝐼𝐶) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝐴 − 𝐵) = (𝑥 − 𝑦) ∧ (𝐵 − 𝐶) = (𝑦 − 𝑧)) ∧ ((𝐴 − 𝑑) = (𝑥 − 𝑤) ∧ (𝐵 − 𝑑) = (𝑦 − 𝑤))))) |
29 | | oveq2 7279 |
. . . . 5
⊢ (𝑑 = 𝐷 → (𝐴 − 𝑑) = (𝐴 − 𝐷)) |
30 | 29 | eqeq1d 2742 |
. . . 4
⊢ (𝑑 = 𝐷 → ((𝐴 − 𝑑) = (𝑥 − 𝑤) ↔ (𝐴 − 𝐷) = (𝑥 − 𝑤))) |
31 | | oveq2 7279 |
. . . . 5
⊢ (𝑑 = 𝐷 → (𝐵 − 𝑑) = (𝐵 − 𝐷)) |
32 | 31 | eqeq1d 2742 |
. . . 4
⊢ (𝑑 = 𝐷 → ((𝐵 − 𝑑) = (𝑦 − 𝑤) ↔ (𝐵 − 𝐷) = (𝑦 − 𝑤))) |
33 | 30, 32 | anbi12d 631 |
. . 3
⊢ (𝑑 = 𝐷 → (((𝐴 − 𝑑) = (𝑥 − 𝑤) ∧ (𝐵 − 𝑑) = (𝑦 − 𝑤)) ↔ ((𝐴 − 𝐷) = (𝑥 − 𝑤) ∧ (𝐵 − 𝐷) = (𝑦 − 𝑤)))) |
34 | 33 | 3anbi3d 1441 |
. 2
⊢ (𝑑 = 𝐷 → (((𝐵 ∈ (𝐴𝐼𝐶) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝐴 − 𝐵) = (𝑥 − 𝑦) ∧ (𝐵 − 𝐶) = (𝑦 − 𝑧)) ∧ ((𝐴 − 𝑑) = (𝑥 − 𝑤) ∧ (𝐵 − 𝑑) = (𝑦 − 𝑤))) ↔ ((𝐵 ∈ (𝐴𝐼𝐶) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝐴 − 𝐵) = (𝑥 − 𝑦) ∧ (𝐵 − 𝐶) = (𝑦 − 𝑧)) ∧ ((𝐴 − 𝐷) = (𝑥 − 𝑤) ∧ (𝐵 − 𝐷) = (𝑦 − 𝑤))))) |
35 | | oveq1 7278 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑥𝐼𝑧) = (𝑋𝐼𝑧)) |
36 | 35 | eleq2d 2826 |
. . . 4
⊢ (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑋𝐼𝑧))) |
37 | 36 | anbi2d 629 |
. . 3
⊢ (𝑥 = 𝑋 → ((𝐵 ∈ (𝐴𝐼𝐶) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ (𝐵 ∈ (𝐴𝐼𝐶) ∧ 𝑦 ∈ (𝑋𝐼𝑧)))) |
38 | | oveq1 7278 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑥 − 𝑦) = (𝑋 − 𝑦)) |
39 | 38 | eqeq2d 2751 |
. . . 4
⊢ (𝑥 = 𝑋 → ((𝐴 − 𝐵) = (𝑥 − 𝑦) ↔ (𝐴 − 𝐵) = (𝑋 − 𝑦))) |
40 | 39 | anbi1d 630 |
. . 3
⊢ (𝑥 = 𝑋 → (((𝐴 − 𝐵) = (𝑥 − 𝑦) ∧ (𝐵 − 𝐶) = (𝑦 − 𝑧)) ↔ ((𝐴 − 𝐵) = (𝑋 − 𝑦) ∧ (𝐵 − 𝐶) = (𝑦 − 𝑧)))) |
41 | | oveq1 7278 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑥 − 𝑤) = (𝑋 − 𝑤)) |
42 | 41 | eqeq2d 2751 |
. . . 4
⊢ (𝑥 = 𝑋 → ((𝐴 − 𝐷) = (𝑥 − 𝑤) ↔ (𝐴 − 𝐷) = (𝑋 − 𝑤))) |
43 | 42 | anbi1d 630 |
. . 3
⊢ (𝑥 = 𝑋 → (((𝐴 − 𝐷) = (𝑥 − 𝑤) ∧ (𝐵 − 𝐷) = (𝑦 − 𝑤)) ↔ ((𝐴 − 𝐷) = (𝑋 − 𝑤) ∧ (𝐵 − 𝐷) = (𝑦 − 𝑤)))) |
44 | 37, 40, 43 | 3anbi123d 1435 |
. 2
⊢ (𝑥 = 𝑋 → (((𝐵 ∈ (𝐴𝐼𝐶) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝐴 − 𝐵) = (𝑥 − 𝑦) ∧ (𝐵 − 𝐶) = (𝑦 − 𝑧)) ∧ ((𝐴 − 𝐷) = (𝑥 − 𝑤) ∧ (𝐵 − 𝐷) = (𝑦 − 𝑤))) ↔ ((𝐵 ∈ (𝐴𝐼𝐶) ∧ 𝑦 ∈ (𝑋𝐼𝑧)) ∧ ((𝐴 − 𝐵) = (𝑋 − 𝑦) ∧ (𝐵 − 𝐶) = (𝑦 − 𝑧)) ∧ ((𝐴 − 𝐷) = (𝑋 − 𝑤) ∧ (𝐵 − 𝐷) = (𝑦 − 𝑤))))) |
45 | | eleq1 2828 |
. . . 4
⊢ (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑧))) |
46 | 45 | anbi2d 629 |
. . 3
⊢ (𝑦 = 𝑌 → ((𝐵 ∈ (𝐴𝐼𝐶) ∧ 𝑦 ∈ (𝑋𝐼𝑧)) ↔ (𝐵 ∈ (𝐴𝐼𝐶) ∧ 𝑌 ∈ (𝑋𝐼𝑧)))) |
47 | | oveq2 7279 |
. . . . 5
⊢ (𝑦 = 𝑌 → (𝑋 − 𝑦) = (𝑋 − 𝑌)) |
48 | 47 | eqeq2d 2751 |
. . . 4
⊢ (𝑦 = 𝑌 → ((𝐴 − 𝐵) = (𝑋 − 𝑦) ↔ (𝐴 − 𝐵) = (𝑋 − 𝑌))) |
49 | | oveq1 7278 |
. . . . 5
⊢ (𝑦 = 𝑌 → (𝑦 − 𝑧) = (𝑌 − 𝑧)) |
50 | 49 | eqeq2d 2751 |
. . . 4
⊢ (𝑦 = 𝑌 → ((𝐵 − 𝐶) = (𝑦 − 𝑧) ↔ (𝐵 − 𝐶) = (𝑌 − 𝑧))) |
51 | 48, 50 | anbi12d 631 |
. . 3
⊢ (𝑦 = 𝑌 → (((𝐴 − 𝐵) = (𝑋 − 𝑦) ∧ (𝐵 − 𝐶) = (𝑦 − 𝑧)) ↔ ((𝐴 − 𝐵) = (𝑋 − 𝑌) ∧ (𝐵 − 𝐶) = (𝑌 − 𝑧)))) |
52 | | oveq1 7278 |
. . . . 5
⊢ (𝑦 = 𝑌 → (𝑦 − 𝑤) = (𝑌 − 𝑤)) |
53 | 52 | eqeq2d 2751 |
. . . 4
⊢ (𝑦 = 𝑌 → ((𝐵 − 𝐷) = (𝑦 − 𝑤) ↔ (𝐵 − 𝐷) = (𝑌 − 𝑤))) |
54 | 53 | anbi2d 629 |
. . 3
⊢ (𝑦 = 𝑌 → (((𝐴 − 𝐷) = (𝑋 − 𝑤) ∧ (𝐵 − 𝐷) = (𝑦 − 𝑤)) ↔ ((𝐴 − 𝐷) = (𝑋 − 𝑤) ∧ (𝐵 − 𝐷) = (𝑌 − 𝑤)))) |
55 | 46, 51, 54 | 3anbi123d 1435 |
. 2
⊢ (𝑦 = 𝑌 → (((𝐵 ∈ (𝐴𝐼𝐶) ∧ 𝑦 ∈ (𝑋𝐼𝑧)) ∧ ((𝐴 − 𝐵) = (𝑋 − 𝑦) ∧ (𝐵 − 𝐶) = (𝑦 − 𝑧)) ∧ ((𝐴 − 𝐷) = (𝑋 − 𝑤) ∧ (𝐵 − 𝐷) = (𝑦 − 𝑤))) ↔ ((𝐵 ∈ (𝐴𝐼𝐶) ∧ 𝑌 ∈ (𝑋𝐼𝑧)) ∧ ((𝐴 − 𝐵) = (𝑋 − 𝑌) ∧ (𝐵 − 𝐶) = (𝑌 − 𝑧)) ∧ ((𝐴 − 𝐷) = (𝑋 − 𝑤) ∧ (𝐵 − 𝐷) = (𝑌 − 𝑤))))) |
56 | | oveq2 7279 |
. . . . 5
⊢ (𝑧 = 𝑍 → (𝑋𝐼𝑧) = (𝑋𝐼𝑍)) |
57 | 56 | eleq2d 2826 |
. . . 4
⊢ (𝑧 = 𝑍 → (𝑌 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑍))) |
58 | 57 | anbi2d 629 |
. . 3
⊢ (𝑧 = 𝑍 → ((𝐵 ∈ (𝐴𝐼𝐶) ∧ 𝑌 ∈ (𝑋𝐼𝑧)) ↔ (𝐵 ∈ (𝐴𝐼𝐶) ∧ 𝑌 ∈ (𝑋𝐼𝑍)))) |
59 | | oveq2 7279 |
. . . . 5
⊢ (𝑧 = 𝑍 → (𝑌 − 𝑧) = (𝑌 − 𝑍)) |
60 | 59 | eqeq2d 2751 |
. . . 4
⊢ (𝑧 = 𝑍 → ((𝐵 − 𝐶) = (𝑌 − 𝑧) ↔ (𝐵 − 𝐶) = (𝑌 − 𝑍))) |
61 | 60 | anbi2d 629 |
. . 3
⊢ (𝑧 = 𝑍 → (((𝐴 − 𝐵) = (𝑋 − 𝑌) ∧ (𝐵 − 𝐶) = (𝑌 − 𝑧)) ↔ ((𝐴 − 𝐵) = (𝑋 − 𝑌) ∧ (𝐵 − 𝐶) = (𝑌 − 𝑍)))) |
62 | 58, 61 | 3anbi12d 1436 |
. 2
⊢ (𝑧 = 𝑍 → (((𝐵 ∈ (𝐴𝐼𝐶) ∧ 𝑌 ∈ (𝑋𝐼𝑧)) ∧ ((𝐴 − 𝐵) = (𝑋 − 𝑌) ∧ (𝐵 − 𝐶) = (𝑌 − 𝑧)) ∧ ((𝐴 − 𝐷) = (𝑋 − 𝑤) ∧ (𝐵 − 𝐷) = (𝑌 − 𝑤))) ↔ ((𝐵 ∈ (𝐴𝐼𝐶) ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ ((𝐴 − 𝐵) = (𝑋 − 𝑌) ∧ (𝐵 − 𝐶) = (𝑌 − 𝑍)) ∧ ((𝐴 − 𝐷) = (𝑋 − 𝑤) ∧ (𝐵 − 𝐷) = (𝑌 − 𝑤))))) |
63 | | oveq2 7279 |
. . . . 5
⊢ (𝑤 = 𝑊 → (𝑋 − 𝑤) = (𝑋 − 𝑊)) |
64 | 63 | eqeq2d 2751 |
. . . 4
⊢ (𝑤 = 𝑊 → ((𝐴 − 𝐷) = (𝑋 − 𝑤) ↔ (𝐴 − 𝐷) = (𝑋 − 𝑊))) |
65 | | oveq2 7279 |
. . . . 5
⊢ (𝑤 = 𝑊 → (𝑌 − 𝑤) = (𝑌 − 𝑊)) |
66 | 65 | eqeq2d 2751 |
. . . 4
⊢ (𝑤 = 𝑊 → ((𝐵 − 𝐷) = (𝑌 − 𝑤) ↔ (𝐵 − 𝐷) = (𝑌 − 𝑊))) |
67 | 64, 66 | anbi12d 631 |
. . 3
⊢ (𝑤 = 𝑊 → (((𝐴 − 𝐷) = (𝑋 − 𝑤) ∧ (𝐵 − 𝐷) = (𝑌 − 𝑤)) ↔ ((𝐴 − 𝐷) = (𝑋 − 𝑊) ∧ (𝐵 − 𝐷) = (𝑌 − 𝑊)))) |
68 | 67 | 3anbi3d 1441 |
. 2
⊢ (𝑤 = 𝑊 → (((𝐵 ∈ (𝐴𝐼𝐶) ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ ((𝐴 − 𝐵) = (𝑋 − 𝑌) ∧ (𝐵 − 𝐶) = (𝑌 − 𝑍)) ∧ ((𝐴 − 𝐷) = (𝑋 − 𝑤) ∧ (𝐵 − 𝐷) = (𝑌 − 𝑤))) ↔ ((𝐵 ∈ (𝐴𝐼𝐶) ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ ((𝐴 − 𝐵) = (𝑋 − 𝑌) ∧ (𝐵 − 𝐶) = (𝑌 − 𝑍)) ∧ ((𝐴 − 𝐷) = (𝑋 − 𝑊) ∧ (𝐵 − 𝐷) = (𝑌 − 𝑊))))) |
69 | | brafs.o |
. . 3
⊢ 𝑂 = (AFS‘𝐺) |
70 | | brafs.p |
. . . 4
⊢ 𝑃 = (Base‘𝐺) |
71 | | brafs.d |
. . . 4
⊢ − =
(dist‘𝐺) |
72 | | brafs.i |
. . . 4
⊢ 𝐼 = (Itv‘𝐺) |
73 | | brafs.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
74 | 70, 71, 72, 73 | afsval 32647 |
. . 3
⊢ (𝜑 → (AFS‘𝐺) = {〈𝑒, 𝑓〉 ∣ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ∃𝑤 ∈ 𝑃 (𝑒 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑓 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 − 𝑏) = (𝑥 − 𝑦) ∧ (𝑏 − 𝑐) = (𝑦 − 𝑧)) ∧ ((𝑎 − 𝑑) = (𝑥 − 𝑤) ∧ (𝑏 − 𝑑) = (𝑦 − 𝑤))))}) |
75 | 69, 74 | eqtrid 2792 |
. 2
⊢ (𝜑 → 𝑂 = {〈𝑒, 𝑓〉 ∣ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ∃𝑤 ∈ 𝑃 (𝑒 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑓 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 ∈ (𝑎𝐼𝑐) ∧ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ((𝑎 − 𝑏) = (𝑥 − 𝑦) ∧ (𝑏 − 𝑐) = (𝑦 − 𝑧)) ∧ ((𝑎 − 𝑑) = (𝑥 − 𝑤) ∧ (𝑏 − 𝑑) = (𝑦 − 𝑤))))}) |
76 | | brafs.1 |
. 2
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
77 | | brafs.2 |
. 2
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
78 | | brafs.3 |
. 2
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
79 | | brafs.4 |
. 2
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
80 | | brafs.5 |
. 2
⊢ (𝜑 → 𝑋 ∈ 𝑃) |
81 | | brafs.6 |
. 2
⊢ (𝜑 → 𝑌 ∈ 𝑃) |
82 | | brafs.7 |
. 2
⊢ (𝜑 → 𝑍 ∈ 𝑃) |
83 | | brafs.8 |
. 2
⊢ (𝜑 → 𝑊 ∈ 𝑃) |
84 | 10, 21, 28, 34, 44, 55, 62, 68, 75, 76, 77, 78, 79, 80, 81, 82, 83 | br8d 30946 |
1
⊢ (𝜑 → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉𝑂〈〈𝑋, 𝑌〉, 〈𝑍, 𝑊〉〉 ↔ ((𝐵 ∈ (𝐴𝐼𝐶) ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ ((𝐴 − 𝐵) = (𝑋 − 𝑌) ∧ (𝐵 − 𝐶) = (𝑌 − 𝑍)) ∧ ((𝐴 − 𝐷) = (𝑋 − 𝑊) ∧ (𝐵 − 𝐷) = (𝑌 − 𝑊))))) |