Metamath Proof Explorer


Theorem colperpexlem1

Description: Lemma for colperp . First part of lemma 8.20 of Schwabhauser p. 62. (Contributed by Thierry Arnoux, 27-Oct-2019)

Ref Expression
Hypotheses colperpex.p P = Base G
colperpex.d - ˙ = dist G
colperpex.i I = Itv G
colperpex.l L = Line 𝒢 G
colperpex.g φ G 𝒢 Tarski
colperpexlem.s S = pInv 𝒢 G
colperpexlem.m M = S A
colperpexlem.n N = S B
colperpexlem.k K = S Q
colperpexlem.a φ A P
colperpexlem.b φ B P
colperpexlem.c φ C P
colperpexlem.q φ Q P
colperpexlem.1 φ ⟨“ ABC ”⟩ 𝒢 G
colperpexlem.2 φ K M C = N C
Assertion colperpexlem1 φ ⟨“ BAQ ”⟩ 𝒢 G

Proof

Step Hyp Ref Expression
1 colperpex.p P = Base G
2 colperpex.d - ˙ = dist G
3 colperpex.i I = Itv G
4 colperpex.l L = Line 𝒢 G
5 colperpex.g φ G 𝒢 Tarski
6 colperpexlem.s S = pInv 𝒢 G
7 colperpexlem.m M = S A
8 colperpexlem.n N = S B
9 colperpexlem.k K = S Q
10 colperpexlem.a φ A P
11 colperpexlem.b φ B P
12 colperpexlem.c φ C P
13 colperpexlem.q φ Q P
14 colperpexlem.1 φ ⟨“ ABC ”⟩ 𝒢 G
15 colperpexlem.2 φ K M C = N C
16 1 2 3 4 6 5 10 7 13 mircl φ M Q P
17 1 2 3 4 6 5 10 7 12 mircl φ M C P
18 eqid S B = S B
19 1 2 3 4 6 5 11 18 12 mircl φ S B C P
20 1 2 3 4 6 5 10 7 19 mircl φ M S B C P
21 1 2 3 4 6 5 11 8 12 mircl φ N C P
22 15 21 eqeltrd φ K M C P
23 1 2 3 4 6 5 13 9 17 mirbtwn φ Q K M C I M C
24 1 2 3 5 22 13 17 23 tgbtwncom φ Q M C I K M C
25 8 fveq1i N C = S B C
26 15 25 syl6eq φ K M C = S B C
27 26 oveq2d φ M C I K M C = M C I S B C
28 24 27 eleqtrd φ Q M C I S B C
29 1 2 3 5 17 13 19 28 tgbtwncom φ Q S B C I M C
30 1 2 3 4 6 5 10 7 19 13 17 29 mirbtwni φ M Q M S B C I M M C
31 1 2 3 4 6 5 10 7 12 mirmir φ M M C = C
32 31 oveq2d φ M S B C I M M C = M S B C I C
33 30 32 eleqtrd φ M Q M S B C I C
34 1 2 3 5 17 19 axtgcgrrflx φ M C - ˙ S B C = S B C - ˙ M C
35 1 2 3 4 6 5 10 7 19 17 miriso φ M S B C - ˙ M M C = S B C - ˙ M C
36 31 oveq2d φ M S B C - ˙ M M C = M S B C - ˙ C
37 34 35 36 3eqtr2d φ M C - ˙ S B C = M S B C - ˙ C
38 26 oveq2d φ Q - ˙ K M C = Q - ˙ S B C
39 1 2 3 4 6 5 13 9 17 mircgr φ Q - ˙ K M C = Q - ˙ M C
40 38 39 eqtr3d φ Q - ˙ S B C = Q - ˙ M C
41 1 2 3 4 6 5 10 7 13 17 miriso φ M Q - ˙ M M C = Q - ˙ M C
42 31 oveq2d φ M Q - ˙ M M C = M Q - ˙ C
43 40 41 42 3eqtr2d φ Q - ˙ S B C = M Q - ˙ C
44 1 2 3 4 6 5 10 7 11 mirmir φ M M B = B
45 eqidd φ M B = M B
46 eqidd φ M C = M C
47 44 45 46 s3eqd φ ⟨“ M M B M B M C ”⟩ = ⟨“ B M B M C ”⟩
48 1 2 3 4 6 5 10 7 11 mircl φ M B P
49 simpr φ A = B A = B
50 49 fveq2d φ A = B M A = M B
51 5 adantr φ A = B G 𝒢 Tarski
52 10 adantr φ A = B A P
53 1 2 3 4 6 51 52 7 mircinv φ A = B M A = A
54 50 53 eqtr3d φ A = B M B = A
55 eqidd φ A = B B = B
56 eqidd φ A = B C = C
57 54 55 56 s3eqd φ A = B ⟨“ M B BC ”⟩ = ⟨“ ABC ”⟩
58 14 adantr φ A = B ⟨“ ABC ”⟩ 𝒢 G
59 57 58 eqeltrd φ A = B ⟨“ M B BC ”⟩ 𝒢 G
60 5 adantr φ A B G 𝒢 Tarski
61 10 adantr φ A B A P
62 11 adantr φ A B B P
63 12 adantr φ A B C P
64 1 2 3 4 6 60 61 7 62 mircl φ A B M B P
65 14 adantr φ A B ⟨“ ABC ”⟩ 𝒢 G
66 simpr φ A B A B
67 1 2 3 4 6 60 61 7 62 mirbtwn φ A B A M B I B
68 1 4 3 60 64 62 61 67 btwncolg1 φ A B A M B L B M B = B
69 1 4 3 60 64 62 61 68 colcom φ A B A B L M B B = M B
70 1 2 3 4 6 60 61 62 63 64 65 66 69 ragcol φ A B ⟨“ M B BC ”⟩ 𝒢 G
71 59 70 pm2.61dane φ ⟨“ M B BC ”⟩ 𝒢 G
72 1 2 3 4 6 5 48 11 12 71 7 10 mirrag φ ⟨“ M M B M B M C ”⟩ 𝒢 G
73 47 72 eqeltrrd φ ⟨“ B M B M C ”⟩ 𝒢 G
74 1 2 3 4 6 5 11 48 17 israg φ ⟨“ B M B M C ”⟩ 𝒢 G B - ˙ M C = B - ˙ S M B M C
75 73 74 mpbid φ B - ˙ M C = B - ˙ S M B M C
76 1 2 3 4 6 5 10 7 12 11 mirmir2 φ M S B C = S M B M C
77 76 oveq2d φ B - ˙ M S B C = B - ˙ S M B M C
78 75 77 eqtr4d φ B - ˙ M C = B - ˙ M S B C
79 1 2 3 5 11 17 11 20 78 tgcgrcomlr φ M C - ˙ B = M S B C - ˙ B
80 1 2 3 4 6 5 11 18 12 mircgr φ B - ˙ S B C = B - ˙ C
81 1 2 3 5 11 19 11 12 80 tgcgrcomlr φ S B C - ˙ B = C - ˙ B
82 1 2 3 5 17 13 19 11 20 16 12 11 28 33 37 43 79 81 tgifscgr φ Q - ˙ B = M Q - ˙ B
83 1 2 3 5 13 11 16 11 82 tgcgrcomlr φ B - ˙ Q = B - ˙ M Q
84 7 fveq1i M Q = S A Q
85 84 oveq2i B - ˙ M Q = B - ˙ S A Q
86 83 85 syl6eq φ B - ˙ Q = B - ˙ S A Q
87 1 2 3 4 6 5 11 10 13 israg φ ⟨“ BAQ ”⟩ 𝒢 G B - ˙ Q = B - ˙ S A Q
88 86 87 mpbird φ ⟨“ BAQ ”⟩ 𝒢 G