Metamath Proof Explorer


Theorem cgracgr

Description: First direction of proposition 11.4 of Schwabhauser p. 95. Again, this is "half" of the proposition, i.e. only two additional points are used, while Schwabhauser has four. (Contributed by Thierry Arnoux, 31-Jul-2020)

Ref Expression
Hypotheses iscgra.p P = Base G
iscgra.i I = Itv G
iscgra.k K = hl 𝒢 G
iscgra.g φ G 𝒢 Tarski
iscgra.a φ A P
iscgra.b φ B P
iscgra.c φ C P
iscgra.d φ D P
iscgra.e φ E P
iscgra.f φ F P
cgrahl1.2 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩
cgrahl1.x φ X P
cgracgr.m - ˙ = dist G
cgracgr.y φ Y P
cgracgr.1 φ X K B A
cgracgr.2 φ Y K B C
cgracgr.3 φ B - ˙ X = E - ˙ D
cgracgr.4 φ B - ˙ Y = E - ˙ F
Assertion cgracgr φ X - ˙ Y = D - ˙ F

Proof

Step Hyp Ref Expression
1 iscgra.p P = Base G
2 iscgra.i I = Itv G
3 iscgra.k K = hl 𝒢 G
4 iscgra.g φ G 𝒢 Tarski
5 iscgra.a φ A P
6 iscgra.b φ B P
7 iscgra.c φ C P
8 iscgra.d φ D P
9 iscgra.e φ E P
10 iscgra.f φ F P
11 cgrahl1.2 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩
12 cgrahl1.x φ X P
13 cgracgr.m - ˙ = dist G
14 cgracgr.y φ Y P
15 cgracgr.1 φ X K B A
16 cgracgr.2 φ Y K B C
17 cgracgr.3 φ B - ˙ X = E - ˙ D
18 cgracgr.4 φ B - ˙ Y = E - ˙ F
19 eqid Line 𝒢 G = Line 𝒢 G
20 4 ad3antrrr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F G 𝒢 Tarski
21 5 ad3antrrr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F A P
22 6 ad3antrrr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F B P
23 12 ad3antrrr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F X P
24 eqid 𝒢 G = 𝒢 G
25 simpllr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F x P
26 9 ad3antrrr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F E P
27 14 ad3antrrr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F Y P
28 8 ad3antrrr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F D P
29 10 ad3antrrr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F F P
30 1 2 3 12 5 6 4 15 hlne2 φ A B
31 30 necomd φ B A
32 1 2 3 12 5 6 4 19 15 hlln φ X A Line 𝒢 G B
33 1 2 19 4 6 5 12 31 32 lncom φ X B Line 𝒢 G A
34 33 orcd φ X B Line 𝒢 G A B = A
35 1 19 2 4 6 5 12 34 colrot1 φ B A Line 𝒢 G X A = X
36 35 ad3antrrr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F B A Line 𝒢 G X A = X
37 7 ad3antrrr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F C P
38 simplr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F y P
39 simpr1 φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩
40 1 13 2 24 20 21 22 37 25 26 38 39 cgr3simp1 φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F A - ˙ B = x - ˙ E
41 17 ad3antrrr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F B - ˙ X = E - ˙ D
42 eqid 𝒢 G = 𝒢 G
43 simpr2 φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F x K E D
44 1 2 3 25 28 26 20 ishlg φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F x K E D x E D E x E I D D E I x
45 43 44 mpbid φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F x E D E x E I D D E I x
46 45 simp3d φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F x E I D D E I x
47 1 2 3 12 5 6 4 ishlg φ X K B A X B A B X B I A A B I X
48 15 47 mpbid φ X B A B X B I A A B I X
49 48 simp3d φ X B I A A B I X
50 49 orcomd φ A B I X X B I A
51 50 ad3antrrr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F A B I X X B I A
52 40 eqcomd φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F x - ˙ E = A - ˙ B
53 1 13 2 20 25 26 21 22 52 tgcgrcomlr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F E - ˙ x = B - ˙ A
54 41 eqcomd φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F E - ˙ D = B - ˙ X
55 1 13 2 42 20 26 25 28 22 22 21 23 46 51 53 54 tgcgrsub2 φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F x - ˙ D = A - ˙ X
56 55 eqcomd φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F A - ˙ X = x - ˙ D
57 1 13 2 20 21 23 25 28 56 tgcgrcomlr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F X - ˙ A = D - ˙ x
58 1 13 24 20 21 22 23 25 26 28 40 41 57 trgcgr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F ⟨“ ABX ”⟩ 𝒢 G ⟨“ xED ”⟩
59 1 2 3 14 7 6 4 19 16 hlln φ Y C Line 𝒢 G B
60 59 orcd φ Y C Line 𝒢 G B C = B
61 1 19 2 4 7 6 14 60 colrot1 φ C B Line 𝒢 G Y B = Y
62 61 ad3antrrr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F C B Line 𝒢 G Y B = Y
63 1 13 2 24 20 21 22 37 25 26 38 39 cgr3simp2 φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F B - ˙ C = E - ˙ y
64 1 2 3 14 7 6 4 ishlg φ Y K B C Y B C B Y B I C C B I Y
65 16 64 mpbid φ Y B C B Y B I C C B I Y
66 65 simp3d φ Y B I C C B I Y
67 66 orcomd φ C B I Y Y B I C
68 67 ad3antrrr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F C B I Y Y B I C
69 simpr3 φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F y K E F
70 1 2 3 38 29 26 20 ishlg φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F y K E F y E F E y E I F F E I y
71 69 70 mpbid φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F y E F E y E I F F E I y
72 71 simp3d φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F y E I F F E I y
73 18 ad3antrrr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F B - ˙ Y = E - ˙ F
74 1 13 2 42 20 22 37 27 26 26 38 29 68 72 63 73 tgcgrsub2 φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F C - ˙ Y = y - ˙ F
75 1 13 2 20 22 27 26 29 73 tgcgrcomlr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F Y - ˙ B = F - ˙ E
76 1 13 24 20 22 37 27 26 38 29 63 74 75 trgcgr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F ⟨“ BCY ”⟩ 𝒢 G ⟨“ EyF ”⟩
77 53 eqcomd φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F B - ˙ A = E - ˙ x
78 1 13 2 24 20 21 22 37 25 26 38 39 cgr3simp3 φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F C - ˙ A = y - ˙ x
79 1 2 3 4 5 6 7 8 9 10 11 cgrane2 φ B C
80 79 ad3antrrr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F B C
81 1 19 2 20 22 37 27 24 26 38 13 21 29 25 62 76 77 78 80 tgfscgr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F Y - ˙ A = F - ˙ x
82 1 13 2 20 27 21 29 25 81 tgcgrcomlr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F A - ˙ Y = x - ˙ F
83 30 ad3antrrr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F A B
84 1 19 2 20 21 22 23 24 25 26 13 27 28 29 36 58 82 73 83 tgfscgr φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F X - ˙ Y = D - ˙ F
85 1 2 3 4 5 6 7 8 9 10 iscgra φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F
86 11 85 mpbid φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F
87 84 86 r19.29vva φ X - ˙ Y = D - ˙ F