Metamath Proof Explorer


Theorem acopyeu

Description: Angle construction. Theorem 11.15 of Schwabhauser p. 98. This is Hilbert's axiom III.4 for geometry. Akin to a uniqueness theorem, this states that if two points X and Y both fulfill the conditions, then they are on the same half-line. (Contributed by Thierry Arnoux, 9-Aug-2020)

Ref Expression
Hypotheses dfcgra2.p P = Base G
dfcgra2.i I = Itv G
dfcgra2.m - ˙ = dist G
dfcgra2.g φ G 𝒢 Tarski
dfcgra2.a φ A P
dfcgra2.b φ B P
dfcgra2.c φ C P
dfcgra2.d φ D P
dfcgra2.e φ E P
dfcgra2.f φ F P
acopy.l L = Line 𝒢 G
acopy.1 φ ¬ A B L C B = C
acopy.2 φ ¬ D E L F E = F
acopyeu.x φ X P
acopyeu.y φ Y P
acopyeu.k K = hl 𝒢 G
acopyeu.1 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEX ”⟩
acopyeu.2 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEY ”⟩
acopyeu.3 φ X hp 𝒢 G D L E F
acopyeu.4 φ Y hp 𝒢 G D L E F
Assertion acopyeu φ X K E Y

Proof

Step Hyp Ref Expression
1 dfcgra2.p P = Base G
2 dfcgra2.i I = Itv G
3 dfcgra2.m - ˙ = dist G
4 dfcgra2.g φ G 𝒢 Tarski
5 dfcgra2.a φ A P
6 dfcgra2.b φ B P
7 dfcgra2.c φ C P
8 dfcgra2.d φ D P
9 dfcgra2.e φ E P
10 dfcgra2.f φ F P
11 acopy.l L = Line 𝒢 G
12 acopy.1 φ ¬ A B L C B = C
13 acopy.2 φ ¬ D E L F E = F
14 acopyeu.x φ X P
15 acopyeu.y φ Y P
16 acopyeu.k K = hl 𝒢 G
17 acopyeu.1 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEX ”⟩
18 acopyeu.2 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEY ”⟩
19 acopyeu.3 φ X hp 𝒢 G D L E F
20 acopyeu.4 φ Y hp 𝒢 G D L E F
21 14 ad2antrr φ d P d K E D E - ˙ d = B - ˙ A X P
22 21 ad3antrrr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y X P
23 simplr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y y P
24 15 ad2antrr φ d P d K E D E - ˙ d = B - ˙ A Y P
25 24 ad3antrrr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y Y P
26 4 ad2antrr φ d P d K E D E - ˙ d = B - ˙ A G 𝒢 Tarski
27 26 ad3antrrr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y G 𝒢 Tarski
28 9 ad2antrr φ d P d K E D E - ˙ d = B - ˙ A E P
29 28 ad3antrrr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y E P
30 5 ad2antrr φ d P d K E D E - ˙ d = B - ˙ A A P
31 30 ad3antrrr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y A P
32 6 ad2antrr φ d P d K E D E - ˙ d = B - ˙ A B P
33 32 ad3antrrr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y B P
34 7 ad2antrr φ d P d K E D E - ˙ d = B - ˙ A C P
35 34 ad3antrrr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y C P
36 simplr φ d P d K E D E - ˙ d = B - ˙ A d P
37 36 ad3antrrr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y d P
38 10 ad2antrr φ d P d K E D E - ˙ d = B - ˙ A F P
39 38 ad3antrrr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y F P
40 12 ad2antrr φ d P d K E D E - ˙ d = B - ˙ A ¬ A B L C B = C
41 40 ad3antrrr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y ¬ A B L C B = C
42 8 ad2antrr φ d P d K E D E - ˙ d = B - ˙ A D P
43 13 ad2antrr φ d P d K E D E - ˙ d = B - ˙ A ¬ D E L F E = F
44 simprl φ d P d K E D E - ˙ d = B - ˙ A d K E D
45 1 2 16 36 42 28 26 11 44 hlln φ d P d K E D E - ˙ d = B - ˙ A d D L E
46 1 2 16 36 42 28 26 44 hlne1 φ d P d K E D E - ˙ d = B - ˙ A d E
47 1 2 11 26 42 28 38 36 43 45 46 ncolncol φ d P d K E D E - ˙ d = B - ˙ A ¬ d E L F E = F
48 47 ad3antrrr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y ¬ d E L F E = F
49 simprr φ d P d K E D E - ˙ d = B - ˙ A E - ˙ d = B - ˙ A
50 1 3 2 26 28 36 32 30 49 tgcgrcomlr φ d P d K E D E - ˙ d = B - ˙ A d - ˙ E = A - ˙ B
51 50 eqcomd φ d P d K E D E - ˙ d = B - ˙ A A - ˙ B = d - ˙ E
52 51 ad3antrrr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y A - ˙ B = d - ˙ E
53 simpl u = a v = b u = a
54 53 eleq1d u = a v = b u P d L E a P d L E
55 simpr u = a v = b v = b
56 55 eleq1d u = a v = b v P d L E b P d L E
57 54 56 anbi12d u = a v = b u P d L E v P d L E a P d L E b P d L E
58 simpr u = a v = b w = t w = t
59 simpll u = a v = b w = t u = a
60 simplr u = a v = b w = t v = b
61 59 60 oveq12d u = a v = b w = t u I v = a I b
62 58 61 eleq12d u = a v = b w = t w u I v t a I b
63 62 cbvrexdva u = a v = b w d L E w u I v t d L E t a I b
64 57 63 anbi12d u = a v = b u P d L E v P d L E w d L E w u I v a P d L E b P d L E t d L E t a I b
65 64 cbvopabv u v | u P d L E v P d L E w d L E w u I v = a b | a P d L E b P d L E t d L E t a I b
66 simpllr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y x P
67 simprll φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩
68 simprrl φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩
69 1 2 11 26 36 28 46 tgelrnln φ d P d K E D E - ˙ d = B - ˙ A d L E ran L
70 69 ad3antrrr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y d L E ran L
71 1 2 11 26 36 28 46 tglinerflx2 φ d P d K E D E - ˙ d = B - ˙ A E d L E
72 71 ad3antrrr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y E d L E
73 42 ad3antrrr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y D P
74 1 11 2 4 6 7 5 12 ncolrot2 φ ¬ C A L B A = B
75 1 2 3 4 5 6 7 8 9 14 17 11 74 cgrancol φ ¬ X D L E D = E
76 1 11 2 4 8 9 14 75 ncolcom φ ¬ X E L D E = D
77 76 ad5antr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y ¬ X E L D E = D
78 simprlr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y x K E X
79 1 2 16 66 22 29 27 11 78 hlln φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y x X L E
80 1 2 16 66 22 29 27 78 hlne1 φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y x E
81 1 2 11 27 22 29 73 66 77 79 80 ncolncol φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y ¬ x E L D E = D
82 1 11 2 27 29 73 66 81 ncolcom φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y ¬ x D L E D = E
83 pm2.45 ¬ x D L E D = E ¬ x D L E
84 82 83 syl φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y ¬ x D L E
85 1 2 11 4 8 9 10 13 ncolne1 φ D E
86 1 2 11 4 8 9 85 tgelrnln φ D L E ran L
87 86 ad2antrr φ d P d K E D E - ˙ d = B - ˙ A D L E ran L
88 1 2 11 4 8 9 85 tglinerflx2 φ E D L E
89 88 ad2antrr φ d P d K E D E - ˙ d = B - ˙ A E D L E
90 1 2 11 26 36 28 46 46 87 45 89 tglinethru φ d P d K E D E - ˙ d = B - ˙ A D L E = d L E
91 90 ad3antrrr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y D L E = d L E
92 84 91 neleqtrd φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y ¬ x d L E
93 1 2 11 27 70 29 65 16 72 66 22 92 78 hphl φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y x hp 𝒢 G d L E X
94 90 fveq2d φ d P d K E D E - ˙ d = B - ˙ A hp 𝒢 G D L E = hp 𝒢 G d L E
95 94 ad3antrrr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y hp 𝒢 G D L E = hp 𝒢 G d L E
96 19 ad5antr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y X hp 𝒢 G D L E F
97 95 96 breqdi φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y X hp 𝒢 G d L E F
98 1 2 11 27 70 66 65 22 93 39 97 hpgtr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y x hp 𝒢 G d L E F
99 1 2 3 4 5 6 7 8 9 15 18 11 74 cgrancol φ ¬ Y D L E D = E
100 1 11 2 4 8 9 15 99 ncolcom φ ¬ Y E L D E = D
101 100 ad5antr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y ¬ Y E L D E = D
102 simprrr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y y K E Y
103 1 2 16 23 25 29 27 11 102 hlln φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y y Y L E
104 1 2 16 23 25 29 27 102 hlne1 φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y y E
105 1 2 11 27 25 29 73 23 101 103 104 ncolncol φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y ¬ y E L D E = D
106 1 11 2 27 29 73 23 105 ncolcom φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y ¬ y D L E D = E
107 pm2.45 ¬ y D L E D = E ¬ y D L E
108 106 107 syl φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y ¬ y D L E
109 108 91 neleqtrd φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y ¬ y d L E
110 1 2 11 27 70 29 65 16 72 23 25 109 102 hphl φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y y hp 𝒢 G d L E Y
111 20 ad5antr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y Y hp 𝒢 G D L E F
112 95 111 breqdi φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y Y hp 𝒢 G d L E F
113 1 2 11 27 70 23 65 25 110 39 112 hpgtr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y y hp 𝒢 G d L E F
114 1 3 2 11 16 27 31 33 35 37 29 39 41 48 52 65 66 23 67 68 98 113 trgcopyeulem φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y x = y
115 114 78 eqbrtrrd φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y y K E X
116 1 2 16 23 22 29 27 115 hlcomd φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y X K E y
117 1 2 16 22 23 25 27 29 116 102 hltr φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y X K E Y
118 17 ad2antrr φ d P d K E D E - ˙ d = B - ˙ A ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEX ”⟩
119 1 2 16 26 30 32 34 42 28 21 118 36 44 cgrahl1 φ d P d K E D E - ˙ d = B - ˙ A ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEX ”⟩
120 1 2 11 4 5 6 7 12 ncolne1 φ A B
121 120 ad2antrr φ d P d K E D E - ˙ d = B - ˙ A A B
122 1 2 16 26 30 32 34 36 28 21 3 121 51 iscgra1 φ d P d K E D E - ˙ d = B - ˙ A ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEX ”⟩ x P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X
123 119 122 mpbid φ d P d K E D E - ˙ d = B - ˙ A x P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X
124 18 ad2antrr φ d P d K E D E - ˙ d = B - ˙ A ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEY ”⟩
125 1 2 16 26 30 32 34 42 28 24 124 36 44 cgrahl1 φ d P d K E D E - ˙ d = B - ˙ A ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEY ”⟩
126 1 2 16 26 30 32 34 36 28 24 3 121 51 iscgra1 φ d P d K E D E - ˙ d = B - ˙ A ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEY ”⟩ y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y
127 125 126 mpbid φ d P d K E D E - ˙ d = B - ˙ A y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y
128 reeanv x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y x P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y
129 123 127 128 sylanbrc φ d P d K E D E - ˙ d = B - ˙ A x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEx ”⟩ x K E X ⟨“ ABC ”⟩ 𝒢 G ⟨“ dEy ”⟩ y K E Y
130 117 129 r19.29vva φ d P d K E D E - ˙ d = B - ˙ A X K E Y
131 120 necomd φ B A
132 1 2 16 9 6 5 4 8 3 85 131 hlcgrex φ d P d K E D E - ˙ d = B - ˙ A
133 130 132 r19.29a φ X K E Y