Step | Hyp | Ref
| Expression |
1 | | cgraid.p |
. . . . . . . 8
⊢ 𝑃 = (Base‘𝐺) |
2 | | eqid 2622 |
. . . . . . . 8
⊢
(dist‘𝐺) =
(dist‘𝐺) |
3 | | cgraid.i |
. . . . . . . 8
⊢ 𝐼 = (Itv‘𝐺) |
4 | | cgraid.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
5 | 4 | ad3antrrr 766 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → 𝐺 ∈ TarskiG) |
6 | | cgraid.b |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
7 | 6 | ad3antrrr 766 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → 𝐵 ∈ 𝑃) |
8 | | simpllr 799 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → 𝑥 ∈ 𝑃) |
9 | | cgraid.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
10 | 9 | ad3antrrr 766 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → 𝐴 ∈ 𝑃) |
11 | | simprlr 803 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) |
12 | 1, 2, 3, 5, 7, 8, 7, 10, 11 | tgcgrcomlr 25375 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → (𝑥(dist‘𝐺)𝐵) = (𝐴(dist‘𝐺)𝐵)) |
13 | 12 | eqcomd 2628 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → (𝐴(dist‘𝐺)𝐵) = (𝑥(dist‘𝐺)𝐵)) |
14 | | simprrr 805 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)) |
15 | 14 | eqcomd 2628 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → (𝐵(dist‘𝐺)𝐶) = (𝐵(dist‘𝐺)𝑦)) |
16 | | simplr 792 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → 𝑦 ∈ 𝑃) |
17 | | cgraid.c |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
18 | 17 | ad3antrrr 766 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → 𝐶 ∈ 𝑃) |
19 | | eqid 2622 |
. . . . . . . . 9
⊢
(LineG‘𝐺) =
(LineG‘𝐺) |
20 | | eqid 2622 |
. . . . . . . . 9
⊢
(cgrG‘𝐺) =
(cgrG‘𝐺) |
21 | | cgraid.k |
. . . . . . . . . . . 12
⊢ 𝐾 = (hlG‘𝐺) |
22 | | simprll 802 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → 𝑥(𝐾‘𝐵)𝐶) |
23 | 1, 3, 21, 8, 18, 7, 5, 19, 22 | hlln 25502 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → 𝑥 ∈ (𝐶(LineG‘𝐺)𝐵)) |
24 | 23 | orcd 407 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → (𝑥 ∈ (𝐶(LineG‘𝐺)𝐵) ∨ 𝐶 = 𝐵)) |
25 | 1, 19, 3, 5, 18, 7,
8, 24 | colrot1 25454 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → (𝐶 ∈ (𝐵(LineG‘𝐺)𝑥) ∨ 𝐵 = 𝑥)) |
26 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(≤G‘𝐺) =
(≤G‘𝐺) |
27 | 1, 3, 21, 8, 18, 7, 5 | ishlg 25497 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → (𝑥(𝐾‘𝐵)𝐶 ↔ (𝑥 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ (𝑥 ∈ (𝐵𝐼𝐶) ∨ 𝐶 ∈ (𝐵𝐼𝑥))))) |
28 | 22, 27 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → (𝑥 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ (𝑥 ∈ (𝐵𝐼𝐶) ∨ 𝐶 ∈ (𝐵𝐼𝑥)))) |
29 | 28 | simp3d 1075 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → (𝑥 ∈ (𝐵𝐼𝐶) ∨ 𝐶 ∈ (𝐵𝐼𝑥))) |
30 | 29 | orcomd 403 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → (𝐶 ∈ (𝐵𝐼𝑥) ∨ 𝑥 ∈ (𝐵𝐼𝐶))) |
31 | | simprrl 804 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → 𝑦(𝐾‘𝐵)𝐴) |
32 | 1, 3, 21, 16, 10, 7, 5 | ishlg 25497 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → (𝑦(𝐾‘𝐵)𝐴 ↔ (𝑦 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ (𝑦 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝑦))))) |
33 | 31, 32 | mpbid 222 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → (𝑦 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ (𝑦 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝑦)))) |
34 | 33 | simp3d 1075 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → (𝑦 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝑦))) |
35 | 1, 2, 3, 26, 5, 7,
18, 8, 7, 7, 16, 10, 30, 34, 15, 11 | tgcgrsub2 25490 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → (𝐶(dist‘𝐺)𝑥) = (𝑦(dist‘𝐺)𝐴)) |
36 | 1, 2, 20, 5, 7, 18, 8, 7, 16, 10, 15, 35, 12 | trgcgr 25411 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → 〈“𝐵𝐶𝑥”〉(cgrG‘𝐺)〈“𝐵𝑦𝐴”〉) |
37 | 1, 2, 3, 5, 18, 16 | axtgcgrrflx 25361 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → (𝐶(dist‘𝐺)𝑦) = (𝑦(dist‘𝐺)𝐶)) |
38 | | cgraid.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ≠ 𝐶) |
39 | 38 | ad3antrrr 766 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → 𝐵 ≠ 𝐶) |
40 | 1, 19, 3, 5, 7, 18,
8, 20, 7, 16, 2, 16, 10, 18, 25, 36, 14, 37, 39 | tgfscgr 25463 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → (𝑥(dist‘𝐺)𝑦) = (𝐴(dist‘𝐺)𝐶)) |
41 | 1, 2, 3, 5, 8, 16,
10, 18, 40 | tgcgrcomlr 25375 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → (𝑦(dist‘𝐺)𝑥) = (𝐶(dist‘𝐺)𝐴)) |
42 | 41 | eqcomd 2628 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → (𝐶(dist‘𝐺)𝐴) = (𝑦(dist‘𝐺)𝑥)) |
43 | 13, 15, 42 | 3jca 1242 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → ((𝐴(dist‘𝐺)𝐵) = (𝑥(dist‘𝐺)𝐵) ∧ (𝐵(dist‘𝐺)𝐶) = (𝐵(dist‘𝐺)𝑦) ∧ (𝐶(dist‘𝐺)𝐴) = (𝑦(dist‘𝐺)𝑥))) |
44 | 4 | 3ad2ant1 1082 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃) → 𝐺 ∈ TarskiG) |
45 | 9 | 3ad2ant1 1082 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃) → 𝐴 ∈ 𝑃) |
46 | 6 | 3ad2ant1 1082 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃) → 𝐵 ∈ 𝑃) |
47 | 17 | 3ad2ant1 1082 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃) → 𝐶 ∈ 𝑃) |
48 | | simp2 1062 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃) → 𝑥 ∈ 𝑃) |
49 | | simp3 1063 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃) → 𝑦 ∈ 𝑃) |
50 | 1, 2, 20, 44, 45, 46, 47, 48, 46, 49 | trgcgrg 25410 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃) → (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐵𝑦”〉 ↔ ((𝐴(dist‘𝐺)𝐵) = (𝑥(dist‘𝐺)𝐵) ∧ (𝐵(dist‘𝐺)𝐶) = (𝐵(dist‘𝐺)𝑦) ∧ (𝐶(dist‘𝐺)𝐴) = (𝑦(dist‘𝐺)𝑥)))) |
51 | 50 | 3expa 1265 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) → (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐵𝑦”〉 ↔ ((𝐴(dist‘𝐺)𝐵) = (𝑥(dist‘𝐺)𝐵) ∧ (𝐵(dist‘𝐺)𝐶) = (𝐵(dist‘𝐺)𝑦) ∧ (𝐶(dist‘𝐺)𝐴) = (𝑦(dist‘𝐺)𝑥)))) |
52 | 51 | adantr 481 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐵𝑦”〉 ↔ ((𝐴(dist‘𝐺)𝐵) = (𝑥(dist‘𝐺)𝐵) ∧ (𝐵(dist‘𝐺)𝐶) = (𝐵(dist‘𝐺)𝑦) ∧ (𝐶(dist‘𝐺)𝐴) = (𝑦(dist‘𝐺)𝑥)))) |
53 | 43, 52 | mpbird 247 |
. . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐵𝑦”〉) |
54 | 53, 22, 31 | 3jca 1242 |
. . 3
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) → (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐵𝑦”〉 ∧ 𝑥(𝐾‘𝐵)𝐶 ∧ 𝑦(𝐾‘𝐵)𝐴)) |
55 | 38 | necomd 2849 |
. . . . 5
⊢ (𝜑 → 𝐶 ≠ 𝐵) |
56 | | cgraid.1 |
. . . . . 6
⊢ (𝜑 → 𝐴 ≠ 𝐵) |
57 | 56 | necomd 2849 |
. . . . 5
⊢ (𝜑 → 𝐵 ≠ 𝐴) |
58 | 1, 3, 21, 6, 6, 9,
4, 17, 2, 55, 57 | hlcgrex 25511 |
. . . 4
⊢ (𝜑 → ∃𝑥 ∈ 𝑃 (𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴))) |
59 | 1, 3, 21, 6, 6, 17, 4, 9, 2,
56, 38 | hlcgrex 25511 |
. . . 4
⊢ (𝜑 → ∃𝑦 ∈ 𝑃 (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶))) |
60 | | reeanv 3107 |
. . . 4
⊢
(∃𝑥 ∈
𝑃 ∃𝑦 ∈ 𝑃 ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶))) ↔ (∃𝑥 ∈ 𝑃 (𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ ∃𝑦 ∈ 𝑃 (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) |
61 | 58, 59, 60 | sylanbrc 698 |
. . 3
⊢ (𝜑 → ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ((𝑥(𝐾‘𝐵)𝐶 ∧ (𝐵(dist‘𝐺)𝑥) = (𝐵(dist‘𝐺)𝐴)) ∧ (𝑦(𝐾‘𝐵)𝐴 ∧ (𝐵(dist‘𝐺)𝑦) = (𝐵(dist‘𝐺)𝐶)))) |
62 | 54, 61 | reximddv2 3020 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐵𝑦”〉 ∧ 𝑥(𝐾‘𝐵)𝐶 ∧ 𝑦(𝐾‘𝐵)𝐴)) |
63 | 1, 3, 21, 4, 9, 6,
17, 17, 6, 9 | iscgra 25701 |
. 2
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐶𝐵𝐴”〉 ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐵𝑦”〉 ∧ 𝑥(𝐾‘𝐵)𝐶 ∧ 𝑦(𝐾‘𝐵)𝐴))) |
64 | 62, 63 | mpbird 247 |
1
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐶𝐵𝐴”〉) |