Step | Hyp | Ref
| Expression |
1 | | simprr 763 |
. . 3
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → (𝐸 − 𝑓) = (𝐵 − 𝐶)) |
2 | | tgsas.p |
. . . . 5
⊢ 𝑃 = (Base‘𝐺) |
3 | | tgsas.i |
. . . . 5
⊢ 𝐼 = (Itv‘𝐺) |
4 | | tgasa.l |
. . . . 5
⊢ 𝐿 = (LineG‘𝐺) |
5 | | tgsas.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
6 | 5 | ad2antrr 716 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐺 ∈ TarskiG) |
7 | | tgsas.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ 𝑃) |
8 | 7 | ad2antrr 716 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐹 ∈ 𝑃) |
9 | | tgsas.d |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
10 | 9 | ad2antrr 716 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐷 ∈ 𝑃) |
11 | | tgsas.e |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ 𝑃) |
12 | 11 | ad2antrr 716 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐸 ∈ 𝑃) |
13 | | tgsas.m |
. . . . . . 7
⊢ − =
(dist‘𝐺) |
14 | | tgsas.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
15 | | tgsas.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
16 | | tgsas.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
17 | | tgasa.3 |
. . . . . . 7
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) |
18 | | tgasa.1 |
. . . . . . 7
⊢ (𝜑 → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) |
19 | 2, 3, 13, 5, 14, 15, 16, 9, 11, 7, 17, 4, 18 | cgrancol 26181 |
. . . . . 6
⊢ (𝜑 → ¬ (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸)) |
20 | 19 | ad2antrr 716 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → ¬ (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸)) |
21 | | eqid 2778 |
. . . . . 6
⊢
(hlG‘𝐺) =
(hlG‘𝐺) |
22 | | simplr 759 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝑓 ∈ 𝑃) |
23 | 16 | ad2antrr 716 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐶 ∈ 𝑃) |
24 | 14 | ad2antrr 716 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐴 ∈ 𝑃) |
25 | 15 | ad2antrr 716 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐵 ∈ 𝑃) |
26 | 18 | ad2antrr 716 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) |
27 | 6 | adantr 474 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → 𝐺 ∈ TarskiG) |
28 | 10 | adantr 474 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → 𝐷 ∈ 𝑃) |
29 | 12 | adantr 474 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → 𝐸 ∈ 𝑃) |
30 | 8 | adantr 474 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → 𝐹 ∈ 𝑃) |
31 | 24 | adantr 474 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → 𝐴 ∈ 𝑃) |
32 | 25 | adantr 474 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → 𝐵 ∈ 𝑃) |
33 | 23 | adantr 474 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → 𝐶 ∈ 𝑃) |
34 | 2, 3, 5, 21, 14, 15, 16, 9, 11, 7, 17 | cgracom 26174 |
. . . . . . . . . 10
⊢ (𝜑 → 〈“𝐷𝐸𝐹”〉(cgrA‘𝐺)〈“𝐴𝐵𝐶”〉) |
35 | 34 | ad3antrrr 720 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → 〈“𝐷𝐸𝐹”〉(cgrA‘𝐺)〈“𝐴𝐵𝐶”〉) |
36 | | simpr 479 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) |
37 | 2, 4, 3, 27, 28, 30, 29, 36 | colcom 25913 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → (𝐸 ∈ (𝐹𝐿𝐷) ∨ 𝐹 = 𝐷)) |
38 | 2, 4, 3, 27, 30, 28, 29, 37 | colrot1 25914 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸)) |
39 | 2, 3, 13, 27, 28, 29, 30, 31, 32, 33, 35, 4, 38 | cgracol 26180 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) |
40 | 26 | adantr 474 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) |
41 | 39, 40 | pm2.65da 807 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → ¬ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) |
42 | | eqid 2778 |
. . . . . . . . . 10
⊢
(cgrG‘𝐺) =
(cgrG‘𝐺) |
43 | 17 | ad2antrr 716 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) |
44 | | simprl 761 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝑓((hlG‘𝐺)‘𝐸)𝐹) |
45 | 2, 3, 21, 6, 24, 25, 23, 10, 12, 8, 43, 22, 44 | cgrahl2 26169 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝑓”〉) |
46 | 2, 3, 21, 5, 14, 15, 16, 9, 11, 7, 17 | cgrane1 26164 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ≠ 𝐵) |
47 | 2, 3, 21, 14, 14, 15, 5, 46 | hlid 25964 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴((hlG‘𝐺)‘𝐵)𝐴) |
48 | 47 | ad2antrr 716 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐴((hlG‘𝐺)‘𝐵)𝐴) |
49 | 2, 3, 21, 5, 14, 15, 16, 9, 11, 7, 17 | cgrane2 26165 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ≠ 𝐶) |
50 | 49 | necomd 3024 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ≠ 𝐵) |
51 | 2, 3, 21, 16, 14, 15, 5, 50 | hlid 25964 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶((hlG‘𝐺)‘𝐵)𝐶) |
52 | 51 | ad2antrr 716 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐶((hlG‘𝐺)‘𝐵)𝐶) |
53 | | tgasa.2 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) |
54 | 2, 13, 3, 5, 14, 15, 9, 11, 53 | tgcgrcomlr 25835 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵 − 𝐴) = (𝐸 − 𝐷)) |
55 | 54 | ad2antrr 716 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → (𝐵 − 𝐴) = (𝐸 − 𝐷)) |
56 | 1 | eqcomd 2784 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → (𝐵 − 𝐶) = (𝐸 − 𝑓)) |
57 | 2, 3, 21, 6, 24, 25, 23, 10, 12, 22, 45, 24, 13, 23, 48, 52, 55, 56 | cgracgr 26170 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → (𝐴 − 𝐶) = (𝐷 − 𝑓)) |
58 | 2, 13, 3, 6, 24, 23, 10, 22, 57 | tgcgrcomlr 25835 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → (𝐶 − 𝐴) = (𝑓 − 𝐷)) |
59 | 53 | ad2antrr 716 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → (𝐴 − 𝐵) = (𝐷 − 𝐸)) |
60 | 2, 13, 42, 6, 23, 24, 25, 22, 10, 12, 58, 59, 56 | trgcgr 25871 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 〈“𝐶𝐴𝐵”〉(cgrG‘𝐺)〈“𝑓𝐷𝐸”〉) |
61 | 2, 3, 4, 5, 16, 14, 15, 18 | ncolne1 25980 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ≠ 𝐴) |
62 | 61 | ad2antrr 716 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐶 ≠ 𝐴) |
63 | 2, 13, 3, 6, 23, 24, 22, 10, 58, 62 | tgcgrneq 25838 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝑓 ≠ 𝐷) |
64 | 2, 3, 21, 22, 8, 10, 6, 63 | hlid 25964 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝑓((hlG‘𝐺)‘𝐷)𝑓) |
65 | 2, 3, 21, 5, 9, 11, 7, 14, 15, 16, 34 | cgrane1 26164 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐷 ≠ 𝐸) |
66 | 65 | necomd 3024 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ≠ 𝐷) |
67 | 2, 3, 21, 11, 14, 9, 5, 66 | hlid 25964 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸((hlG‘𝐺)‘𝐷)𝐸) |
68 | 67 | ad2antrr 716 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐸((hlG‘𝐺)‘𝐷)𝐸) |
69 | 2, 3, 21, 6, 23, 24, 25, 22, 10, 12, 22, 12, 60, 64, 68 | iscgrad 26163 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 〈“𝐶𝐴𝐵”〉(cgrA‘𝐺)〈“𝑓𝐷𝐸”〉) |
70 | 65 | ad2antrr 716 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐷 ≠ 𝐸) |
71 | 2, 3, 6, 21, 22, 10, 12, 63, 70 | cgraswap 26172 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 〈“𝑓𝐷𝐸”〉(cgrA‘𝐺)〈“𝐸𝐷𝑓”〉) |
72 | 2, 3, 6, 21, 23, 24, 25, 22, 10, 12, 69, 12, 10, 22, 71 | cgratr 26175 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 〈“𝐶𝐴𝐵”〉(cgrA‘𝐺)〈“𝐸𝐷𝑓”〉) |
73 | | tgasa.4 |
. . . . . . . . 9
⊢ (𝜑 → 〈“𝐶𝐴𝐵”〉(cgrA‘𝐺)〈“𝐹𝐷𝐸”〉) |
74 | 2, 3, 21, 5, 16, 14, 15, 7, 9, 11, 73 | cgrane3 26166 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ≠ 𝐹) |
75 | 74 | necomd 3024 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ≠ 𝐷) |
76 | 2, 3, 5, 21, 7, 9,
11, 75, 65 | cgraswap 26172 |
. . . . . . . . 9
⊢ (𝜑 → 〈“𝐹𝐷𝐸”〉(cgrA‘𝐺)〈“𝐸𝐷𝐹”〉) |
77 | 2, 3, 5, 21, 16, 14, 15, 7, 9, 11, 73, 11, 9, 7, 76 | cgratr 26175 |
. . . . . . . 8
⊢ (𝜑 → 〈“𝐶𝐴𝐵”〉(cgrA‘𝐺)〈“𝐸𝐷𝐹”〉) |
78 | 77 | ad2antrr 716 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 〈“𝐶𝐴𝐵”〉(cgrA‘𝐺)〈“𝐸𝐷𝐹”〉) |
79 | 2, 3, 4, 5, 11, 9,
66 | tgelrnln 25985 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸𝐿𝐷) ∈ ran 𝐿) |
80 | 79 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → (𝐸𝐿𝐷) ∈ ran 𝐿) |
81 | | simpl 476 |
. . . . . . . . . . . 12
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → 𝑎 = 𝑢) |
82 | | eqidd 2779 |
. . . . . . . . . . . 12
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (𝑃 ∖ (𝐸𝐿𝐷)) = (𝑃 ∖ (𝐸𝐿𝐷))) |
83 | 81, 82 | eleq12d 2853 |
. . . . . . . . . . 11
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (𝑎 ∈ (𝑃 ∖ (𝐸𝐿𝐷)) ↔ 𝑢 ∈ (𝑃 ∖ (𝐸𝐿𝐷)))) |
84 | | simpr 479 |
. . . . . . . . . . . 12
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → 𝑏 = 𝑣) |
85 | 84, 82 | eleq12d 2853 |
. . . . . . . . . . 11
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (𝑏 ∈ (𝑃 ∖ (𝐸𝐿𝐷)) ↔ 𝑣 ∈ (𝑃 ∖ (𝐸𝐿𝐷)))) |
86 | 83, 85 | anbi12d 624 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → ((𝑎 ∈ (𝑃 ∖ (𝐸𝐿𝐷)) ∧ 𝑏 ∈ (𝑃 ∖ (𝐸𝐿𝐷))) ↔ (𝑢 ∈ (𝑃 ∖ (𝐸𝐿𝐷)) ∧ 𝑣 ∈ (𝑃 ∖ (𝐸𝐿𝐷))))) |
87 | | simpr 479 |
. . . . . . . . . . . 12
⊢ (((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) ∧ 𝑡 = 𝑤) → 𝑡 = 𝑤) |
88 | | simpll 757 |
. . . . . . . . . . . . 13
⊢ (((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) ∧ 𝑡 = 𝑤) → 𝑎 = 𝑢) |
89 | | simplr 759 |
. . . . . . . . . . . . 13
⊢ (((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) ∧ 𝑡 = 𝑤) → 𝑏 = 𝑣) |
90 | 88, 89 | oveq12d 6942 |
. . . . . . . . . . . 12
⊢ (((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) ∧ 𝑡 = 𝑤) → (𝑎𝐼𝑏) = (𝑢𝐼𝑣)) |
91 | 87, 90 | eleq12d 2853 |
. . . . . . . . . . 11
⊢ (((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) ∧ 𝑡 = 𝑤) → (𝑡 ∈ (𝑎𝐼𝑏) ↔ 𝑤 ∈ (𝑢𝐼𝑣))) |
92 | 91 | cbvrexdva 3374 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (∃𝑡 ∈ (𝐸𝐿𝐷)𝑡 ∈ (𝑎𝐼𝑏) ↔ ∃𝑤 ∈ (𝐸𝐿𝐷)𝑤 ∈ (𝑢𝐼𝑣))) |
93 | 86, 92 | anbi12d 624 |
. . . . . . . . 9
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (((𝑎 ∈ (𝑃 ∖ (𝐸𝐿𝐷)) ∧ 𝑏 ∈ (𝑃 ∖ (𝐸𝐿𝐷))) ∧ ∃𝑡 ∈ (𝐸𝐿𝐷)𝑡 ∈ (𝑎𝐼𝑏)) ↔ ((𝑢 ∈ (𝑃 ∖ (𝐸𝐿𝐷)) ∧ 𝑣 ∈ (𝑃 ∖ (𝐸𝐿𝐷))) ∧ ∃𝑤 ∈ (𝐸𝐿𝐷)𝑤 ∈ (𝑢𝐼𝑣)))) |
94 | 93 | cbvopabv 4960 |
. . . . . . . 8
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ (𝐸𝐿𝐷)) ∧ 𝑏 ∈ (𝑃 ∖ (𝐸𝐿𝐷))) ∧ ∃𝑡 ∈ (𝐸𝐿𝐷)𝑡 ∈ (𝑎𝐼𝑏))} = {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ (𝑃 ∖ (𝐸𝐿𝐷)) ∧ 𝑣 ∈ (𝑃 ∖ (𝐸𝐿𝐷))) ∧ ∃𝑤 ∈ (𝐸𝐿𝐷)𝑤 ∈ (𝑢𝐼𝑣))} |
95 | 2, 3, 4, 5, 11, 9,
66 | tglinerflx1 25988 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ (𝐸𝐿𝐷)) |
96 | 95 | ad2antrr 716 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐸 ∈ (𝐸𝐿𝐷)) |
97 | 2, 4, 3, 5, 9, 11,
7, 19 | ncolcom 25916 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ (𝐹 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷)) |
98 | | pm2.45 868 |
. . . . . . . . . . 11
⊢ (¬
(𝐹 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷) → ¬ 𝐹 ∈ (𝐸𝐿𝐷)) |
99 | 97, 98 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ 𝐹 ∈ (𝐸𝐿𝐷)) |
100 | 99 | ad2antrr 716 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → ¬ 𝐹 ∈ (𝐸𝐿𝐷)) |
101 | 2, 3, 21, 22, 8, 12, 6, 44 | hlcomd 25959 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐹((hlG‘𝐺)‘𝐸)𝑓) |
102 | 2, 3, 4, 6, 80, 12, 94, 21, 96, 8, 22, 100, 101 | hphl 26123 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐹((hpG‘𝐺)‘(𝐸𝐿𝐷))𝑓) |
103 | 2, 3, 4, 6, 80, 8,
94, 22, 102 | hpgcom 26119 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝑓((hpG‘𝐺)‘(𝐸𝐿𝐷))𝐹) |
104 | 2, 3, 4, 5, 79, 7,
94, 99 | hpgid 26118 |
. . . . . . . 8
⊢ (𝜑 → 𝐹((hpG‘𝐺)‘(𝐸𝐿𝐷))𝐹) |
105 | 104 | ad2antrr 716 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐹((hpG‘𝐺)‘(𝐸𝐿𝐷))𝐹) |
106 | 2, 3, 13, 6, 23, 24, 25, 12, 10, 8, 4, 26, 41, 22, 8, 21, 72, 78, 103, 105 | acopyeu 26187 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝑓((hlG‘𝐺)‘𝐷)𝐹) |
107 | 2, 3, 21, 22, 8, 10, 6, 4, 106 | hlln 25962 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝑓 ∈ (𝐹𝐿𝐷)) |
108 | 2, 3, 4, 5, 7, 9, 75 | tglinerflx1 25988 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝐹𝐿𝐷)) |
109 | 108 | ad2antrr 716 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐹 ∈ (𝐹𝐿𝐷)) |
110 | 2, 3, 21, 5, 14, 15, 16, 9, 11, 7, 17 | cgrane4 26167 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ≠ 𝐹) |
111 | 110 | ad2antrr 716 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐸 ≠ 𝐹) |
112 | 2, 3, 21, 22, 8, 12, 6, 4, 44 | hlln 25962 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝑓 ∈ (𝐹𝐿𝐸)) |
113 | 2, 3, 4, 6, 12, 8,
22, 111, 112 | lncom 25977 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝑓 ∈ (𝐸𝐿𝐹)) |
114 | 2, 3, 4, 6, 12, 8,
111 | tglinerflx2 25989 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐹 ∈ (𝐸𝐿𝐹)) |
115 | 2, 3, 4, 6, 8, 10,
12, 8, 20, 107, 109, 113, 114 | tglineinteq 26000 |
. . . 4
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝑓 = 𝐹) |
116 | 115 | oveq2d 6940 |
. . 3
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → (𝐸 − 𝑓) = (𝐸 − 𝐹)) |
117 | 1, 116 | eqtr3d 2816 |
. 2
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → (𝐵 − 𝐶) = (𝐸 − 𝐹)) |
118 | 110 | necomd 3024 |
. . 3
⊢ (𝜑 → 𝐹 ≠ 𝐸) |
119 | 2, 3, 21, 11, 15, 16, 5, 7, 13, 118, 49 | hlcgrex 25971 |
. 2
⊢ (𝜑 → ∃𝑓 ∈ 𝑃 (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) |
120 | 117, 119 | r19.29a 3264 |
1
⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) |