Step | Hyp | Ref
| Expression |
1 | | dfcgra2.p |
. . . 4
⊢ 𝑃 = (Base‘𝐺) |
2 | | dfcgra2.i |
. . . 4
⊢ 𝐼 = (Itv‘𝐺) |
3 | | acopyeu.k |
. . . 4
⊢ 𝐾 = (hlG‘𝐺) |
4 | | acopyeu.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑃) |
5 | 4 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝑋 ∈ 𝑃) |
6 | 5 | ad3antrrr 762 |
. . . 4
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑋 ∈ 𝑃) |
7 | | simplr 788 |
. . . 4
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑦 ∈ 𝑃) |
8 | | acopyeu.y |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝑃) |
9 | 8 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝑌 ∈ 𝑃) |
10 | 9 | ad3antrrr 762 |
. . . 4
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑌 ∈ 𝑃) |
11 | | dfcgra2.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
12 | 11 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝐺 ∈ TarskiG) |
13 | 12 | ad3antrrr 762 |
. . . 4
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝐺 ∈ TarskiG) |
14 | | dfcgra2.e |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ 𝑃) |
15 | 14 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝐸 ∈ 𝑃) |
16 | 15 | ad3antrrr 762 |
. . . 4
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝐸 ∈ 𝑃) |
17 | | dfcgra2.m |
. . . . . . 7
⊢ − =
(dist‘𝐺) |
18 | | acopy.l |
. . . . . . 7
⊢ 𝐿 = (LineG‘𝐺) |
19 | | dfcgra2.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
20 | 19 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝐴 ∈ 𝑃) |
21 | 20 | ad3antrrr 762 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝐴 ∈ 𝑃) |
22 | | dfcgra2.b |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
23 | 22 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝐵 ∈ 𝑃) |
24 | 23 | ad3antrrr 762 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝐵 ∈ 𝑃) |
25 | | dfcgra2.c |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
26 | 25 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝐶 ∈ 𝑃) |
27 | 26 | ad3antrrr 762 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝐶 ∈ 𝑃) |
28 | | simplr 788 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝑑 ∈ 𝑃) |
29 | 28 | ad3antrrr 762 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑑 ∈ 𝑃) |
30 | | dfcgra2.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ 𝑃) |
31 | 30 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝐹 ∈ 𝑃) |
32 | 31 | ad3antrrr 762 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝐹 ∈ 𝑃) |
33 | | acopy.1 |
. . . . . . . . 9
⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) |
34 | 33 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) |
35 | 34 | ad3antrrr 762 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) |
36 | | dfcgra2.d |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
37 | 36 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝐷 ∈ 𝑃) |
38 | | acopy.2 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹)) |
39 | 38 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → ¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹)) |
40 | | simprl 790 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝑑(𝐾‘𝐸)𝐷) |
41 | 1, 2, 3, 28, 37, 15, 12, 18, 40 | hlln 25302 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝑑 ∈ (𝐷𝐿𝐸)) |
42 | 1, 2, 3, 28, 37, 15, 12, 40 | hlne1 25300 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝑑 ≠ 𝐸) |
43 | 1, 2, 18, 12, 37, 15, 31, 28, 39, 41, 42 | ncolncol 25341 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → ¬ (𝑑 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹)) |
44 | 43 | ad3antrrr 762 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → ¬ (𝑑 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹)) |
45 | | simprr 792 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → (𝐸 − 𝑑) = (𝐵 − 𝐴)) |
46 | 1, 17, 2, 12, 15, 28, 23, 20, 45 | tgcgrcomlr 25175 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → (𝑑 − 𝐸) = (𝐴 − 𝐵)) |
47 | 46 | eqcomd 2616 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → (𝐴 − 𝐵) = (𝑑 − 𝐸)) |
48 | 47 | ad3antrrr 762 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → (𝐴 − 𝐵) = (𝑑 − 𝐸)) |
49 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → 𝑢 = 𝑎) |
50 | 49 | eleq1d 2672 |
. . . . . . . . . 10
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (𝑢 ∈ (𝑃 ∖ (𝑑𝐿𝐸)) ↔ 𝑎 ∈ (𝑃 ∖ (𝑑𝐿𝐸)))) |
51 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → 𝑣 = 𝑏) |
52 | 51 | eleq1d 2672 |
. . . . . . . . . 10
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (𝑣 ∈ (𝑃 ∖ (𝑑𝐿𝐸)) ↔ 𝑏 ∈ (𝑃 ∖ (𝑑𝐿𝐸)))) |
53 | 50, 52 | anbi12d 743 |
. . . . . . . . 9
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → ((𝑢 ∈ (𝑃 ∖ (𝑑𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 ∖ (𝑑𝐿𝐸))) ↔ (𝑎 ∈ (𝑃 ∖ (𝑑𝐿𝐸)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑑𝐿𝐸))))) |
54 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) ∧ 𝑤 = 𝑡) → 𝑤 = 𝑡) |
55 | | simpll 786 |
. . . . . . . . . . . 12
⊢ (((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) ∧ 𝑤 = 𝑡) → 𝑢 = 𝑎) |
56 | | simplr 788 |
. . . . . . . . . . . 12
⊢ (((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) ∧ 𝑤 = 𝑡) → 𝑣 = 𝑏) |
57 | 55, 56 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) ∧ 𝑤 = 𝑡) → (𝑢𝐼𝑣) = (𝑎𝐼𝑏)) |
58 | 54, 57 | eleq12d 2682 |
. . . . . . . . . 10
⊢ (((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) ∧ 𝑤 = 𝑡) → (𝑤 ∈ (𝑢𝐼𝑣) ↔ 𝑡 ∈ (𝑎𝐼𝑏))) |
59 | 58 | cbvrexdva 3154 |
. . . . . . . . 9
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (∃𝑤 ∈ (𝑑𝐿𝐸)𝑤 ∈ (𝑢𝐼𝑣) ↔ ∃𝑡 ∈ (𝑑𝐿𝐸)𝑡 ∈ (𝑎𝐼𝑏))) |
60 | 53, 59 | anbi12d 743 |
. . . . . . . 8
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (((𝑢 ∈ (𝑃 ∖ (𝑑𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 ∖ (𝑑𝐿𝐸))) ∧ ∃𝑤 ∈ (𝑑𝐿𝐸)𝑤 ∈ (𝑢𝐼𝑣)) ↔ ((𝑎 ∈ (𝑃 ∖ (𝑑𝐿𝐸)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑑𝐿𝐸))) ∧ ∃𝑡 ∈ (𝑑𝐿𝐸)𝑡 ∈ (𝑎𝐼𝑏)))) |
61 | 60 | cbvopabv 4654 |
. . . . . . 7
⊢
{〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ (𝑃 ∖ (𝑑𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 ∖ (𝑑𝐿𝐸))) ∧ ∃𝑤 ∈ (𝑑𝐿𝐸)𝑤 ∈ (𝑢𝐼𝑣))} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ (𝑑𝐿𝐸)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑑𝐿𝐸))) ∧ ∃𝑡 ∈ (𝑑𝐿𝐸)𝑡 ∈ (𝑎𝐼𝑏))} |
62 | | simpllr 795 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑥 ∈ 𝑃) |
63 | | simprll 798 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉) |
64 | | simprrl 800 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉) |
65 | 1, 2, 18, 11, 36, 14, 30, 38 | ncolne1 25320 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐷 ≠ 𝐸) |
66 | 1, 2, 18, 11, 36, 14, 65 | tgelrnln 25325 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐷𝐿𝐸) ∈ ran 𝐿) |
67 | 66 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → (𝐷𝐿𝐸) ∈ ran 𝐿) |
68 | 1, 2, 18, 11, 36, 14, 65 | tglinerflx2 25329 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 ∈ (𝐷𝐿𝐸)) |
69 | 68 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝐸 ∈ (𝐷𝐿𝐸)) |
70 | 1, 2, 18, 12, 28, 15, 42, 42, 67, 41, 69 | tglinethru 25331 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → (𝐷𝐿𝐸) = (𝑑𝐿𝐸)) |
71 | 70, 67 | eqeltrrd 2689 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → (𝑑𝐿𝐸) ∈ ran 𝐿) |
72 | 71 | ad3antrrr 762 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → (𝑑𝐿𝐸) ∈ ran 𝐿) |
73 | 61 | eqcomi 2619 |
. . . . . . . 8
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ (𝑑𝐿𝐸)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑑𝐿𝐸))) ∧ ∃𝑡 ∈ (𝑑𝐿𝐸)𝑡 ∈ (𝑎𝐼𝑏))} = {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ (𝑃 ∖ (𝑑𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 ∖ (𝑑𝐿𝐸))) ∧ ∃𝑤 ∈ (𝑑𝐿𝐸)𝑤 ∈ (𝑢𝐼𝑣))} |
74 | 69, 70 | eleqtrd 2690 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝐸 ∈ (𝑑𝐿𝐸)) |
75 | 74 | ad3antrrr 762 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝐸 ∈ (𝑑𝐿𝐸)) |
76 | 37 | ad3antrrr 762 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝐷 ∈ 𝑃) |
77 | | acopyeu.1 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝑋”〉) |
78 | 1, 18, 2, 11, 22, 25, 19, 33 | ncolrot2 25258 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) |
79 | 1, 2, 17, 11, 19, 22, 25, 36, 14, 4, 77, 18, 78 | cgrancol 25520 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ¬ (𝑋 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸)) |
80 | 1, 18, 2, 11, 36, 14, 4, 79 | ncolcom 25256 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ¬ (𝑋 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷)) |
81 | 80 | ad5antr 766 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → ¬ (𝑋 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷)) |
82 | | simprlr 799 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑥(𝐾‘𝐸)𝑋) |
83 | 1, 2, 3, 62, 6, 16, 13, 18, 82 | hlln 25302 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑥 ∈ (𝑋𝐿𝐸)) |
84 | 1, 2, 3, 62, 6, 16, 13, 82 | hlne1 25300 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑥 ≠ 𝐸) |
85 | 1, 2, 18, 13, 6, 16, 76, 62, 81, 83, 84 | ncolncol 25341 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → ¬ (𝑥 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷)) |
86 | 1, 18, 2, 13, 16, 76, 62, 85 | ncolcom 25256 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → ¬ (𝑥 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸)) |
87 | | pm2.45 411 |
. . . . . . . . . . 11
⊢ (¬
(𝑥 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸) → ¬ 𝑥 ∈ (𝐷𝐿𝐸)) |
88 | 86, 87 | syl 17 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → ¬ 𝑥 ∈ (𝐷𝐿𝐸)) |
89 | 70 | ad3antrrr 762 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → (𝐷𝐿𝐸) = (𝑑𝐿𝐸)) |
90 | 89 | eleq2d 2673 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → (𝑥 ∈ (𝐷𝐿𝐸) ↔ 𝑥 ∈ (𝑑𝐿𝐸))) |
91 | 88, 90 | mtbid 313 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → ¬ 𝑥 ∈ (𝑑𝐿𝐸)) |
92 | 1, 2, 18, 13, 72, 16, 61, 3, 75, 62, 6, 91, 82 | hphl 25463 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑥((hpG‘𝐺)‘(𝑑𝐿𝐸))𝑋) |
93 | | acopyeu.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹) |
94 | 93 | ad5antr 766 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑋((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹) |
95 | 70 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → ((hpG‘𝐺)‘(𝐷𝐿𝐸)) = ((hpG‘𝐺)‘(𝑑𝐿𝐸))) |
96 | 95 | ad3antrrr 762 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → ((hpG‘𝐺)‘(𝐷𝐿𝐸)) = ((hpG‘𝐺)‘(𝑑𝐿𝐸))) |
97 | 96 | breqd 4594 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → (𝑋((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹 ↔ 𝑋((hpG‘𝐺)‘(𝑑𝐿𝐸))𝐹)) |
98 | 94, 97 | mpbid 221 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑋((hpG‘𝐺)‘(𝑑𝐿𝐸))𝐹) |
99 | 1, 2, 18, 13, 72, 62, 73, 6, 92, 32, 98 | hpgtr 25460 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑥((hpG‘𝐺)‘(𝑑𝐿𝐸))𝐹) |
100 | | acopyeu.2 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝑌”〉) |
101 | 1, 2, 17, 11, 19, 22, 25, 36, 14, 8, 100, 18, 78 | cgrancol 25520 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ¬ (𝑌 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸)) |
102 | 1, 18, 2, 11, 36, 14, 8, 101 | ncolcom 25256 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ¬ (𝑌 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷)) |
103 | 102 | ad5antr 766 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → ¬ (𝑌 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷)) |
104 | | simprrr 801 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑦(𝐾‘𝐸)𝑌) |
105 | 1, 2, 3, 7, 10, 16, 13, 18, 104 | hlln 25302 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑦 ∈ (𝑌𝐿𝐸)) |
106 | 1, 2, 3, 7, 10, 16, 13, 104 | hlne1 25300 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑦 ≠ 𝐸) |
107 | 1, 2, 18, 13, 10, 16, 76, 7, 103, 105, 106 | ncolncol 25341 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → ¬ (𝑦 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷)) |
108 | 1, 18, 2, 13, 16, 76, 7, 107 | ncolcom 25256 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → ¬ (𝑦 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸)) |
109 | | pm2.45 411 |
. . . . . . . . . . 11
⊢ (¬
(𝑦 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸) → ¬ 𝑦 ∈ (𝐷𝐿𝐸)) |
110 | 108, 109 | syl 17 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → ¬ 𝑦 ∈ (𝐷𝐿𝐸)) |
111 | 89 | eleq2d 2673 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → (𝑦 ∈ (𝐷𝐿𝐸) ↔ 𝑦 ∈ (𝑑𝐿𝐸))) |
112 | 110, 111 | mtbid 313 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → ¬ 𝑦 ∈ (𝑑𝐿𝐸)) |
113 | 1, 2, 18, 13, 72, 16, 61, 3, 75, 7, 10, 112, 104 | hphl 25463 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑦((hpG‘𝐺)‘(𝑑𝐿𝐸))𝑌) |
114 | | acopyeu.4 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹) |
115 | 114 | ad5antr 766 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑌((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹) |
116 | 96 | breqd 4594 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → (𝑌((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹 ↔ 𝑌((hpG‘𝐺)‘(𝑑𝐿𝐸))𝐹)) |
117 | 115, 116 | mpbid 221 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑌((hpG‘𝐺)‘(𝑑𝐿𝐸))𝐹) |
118 | 1, 2, 18, 13, 72, 7, 73, 10, 113, 32, 117 | hpgtr 25460 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑦((hpG‘𝐺)‘(𝑑𝐿𝐸))𝐹) |
119 | 1, 17, 2, 18, 3, 13, 21, 24, 27, 29, 16, 32, 35, 44, 48, 61, 62, 7, 63, 64, 99, 118 | trgcopyeulem 25497 |
. . . . . 6
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑥 = 𝑦) |
120 | 119, 82 | eqbrtrrd 4607 |
. . . . 5
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑦(𝐾‘𝐸)𝑋) |
121 | 1, 2, 3, 7, 6, 16,
13, 120 | hlcomd 25299 |
. . . 4
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑋(𝐾‘𝐸)𝑦) |
122 | 1, 2, 3, 6, 7, 10,
13, 16, 121, 104 | hltr 25305 |
. . 3
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑋(𝐾‘𝐸)𝑌) |
123 | 77 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝑋”〉) |
124 | 1, 2, 3, 12, 20, 23, 26, 37, 15, 5, 123, 28, 40 | cgrahl1 25508 |
. . . . 5
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝑑𝐸𝑋”〉) |
125 | 1, 2, 18, 11, 19, 22, 25, 33 | ncolne1 25320 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≠ 𝐵) |
126 | 125 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝐴 ≠ 𝐵) |
127 | 1, 2, 3, 12, 20, 23, 26, 28, 15, 5, 17, 126, 47 | iscgra1 25502 |
. . . . 5
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → (〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝑑𝐸𝑋”〉 ↔ ∃𝑥 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋))) |
128 | 124, 127 | mpbid 221 |
. . . 4
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → ∃𝑥 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋)) |
129 | 100 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝑌”〉) |
130 | 1, 2, 3, 12, 20, 23, 26, 37, 15, 9, 129, 28, 40 | cgrahl1 25508 |
. . . . 5
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝑑𝐸𝑌”〉) |
131 | 1, 2, 3, 12, 20, 23, 26, 28, 15, 9, 17, 126, 47 | iscgra1 25502 |
. . . . 5
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → (〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝑑𝐸𝑌”〉 ↔ ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) |
132 | 130, 131 | mpbid 221 |
. . . 4
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌)) |
133 | | reeanv 3086 |
. . . 4
⊢
(∃𝑥 ∈
𝑃 ∃𝑦 ∈ 𝑃 ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌)) ↔ (∃𝑥 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) |
134 | 128, 132,
133 | sylanbrc 695 |
. . 3
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) |
135 | 122, 134 | r19.29vva 3062 |
. 2
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝑋(𝐾‘𝐸)𝑌) |
136 | 125 | necomd 2837 |
. . 3
⊢ (𝜑 → 𝐵 ≠ 𝐴) |
137 | 1, 2, 3, 14, 22, 19, 11, 36, 17, 65, 136 | hlcgrex 25311 |
. 2
⊢ (𝜑 → ∃𝑑 ∈ 𝑃 (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) |
138 | 135, 137 | r19.29a 3060 |
1
⊢ (𝜑 → 𝑋(𝐾‘𝐸)𝑌) |