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 = ( LineG ` G )
colperpex.g 
|- ( ph -> G e. TarskiG )
colperpexlem.s 
|- S = ( pInvG ` G )
colperpexlem.m 
|- M = ( S ` A )
colperpexlem.n 
|- N = ( S ` B )
colperpexlem.k 
|- K = ( S ` Q )
colperpexlem.a 
|- ( ph -> A e. P )
colperpexlem.b 
|- ( ph -> B e. P )
colperpexlem.c 
|- ( ph -> C e. P )
colperpexlem.q 
|- ( ph -> Q e. P )
colperpexlem.1 
|- ( ph -> <" A B C "> e. ( raG ` G ) )
colperpexlem.2 
|- ( ph -> ( K ` ( M ` C ) ) = ( N ` C ) )
Assertion colperpexlem1 
|- ( ph -> <" B A Q "> e. ( raG ` 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 = ( LineG ` G )
5 colperpex.g 
 |-  ( ph -> G e. TarskiG )
6 colperpexlem.s 
 |-  S = ( pInvG ` G )
7 colperpexlem.m 
 |-  M = ( S ` A )
8 colperpexlem.n 
 |-  N = ( S ` B )
9 colperpexlem.k 
 |-  K = ( S ` Q )
10 colperpexlem.a 
 |-  ( ph -> A e. P )
11 colperpexlem.b 
 |-  ( ph -> B e. P )
12 colperpexlem.c 
 |-  ( ph -> C e. P )
13 colperpexlem.q 
 |-  ( ph -> Q e. P )
14 colperpexlem.1 
 |-  ( ph -> <" A B C "> e. ( raG ` G ) )
15 colperpexlem.2 
 |-  ( ph -> ( K ` ( M ` C ) ) = ( N ` C ) )
16 1 2 3 4 6 5 10 7 13 mircl 
 |-  ( ph -> ( M ` Q ) e. P )
17 1 2 3 4 6 5 10 7 12 mircl 
 |-  ( ph -> ( M ` C ) e. P )
18 eqid 
 |-  ( S ` B ) = ( S ` B )
19 1 2 3 4 6 5 11 18 12 mircl 
 |-  ( ph -> ( ( S ` B ) ` C ) e. P )
20 1 2 3 4 6 5 10 7 19 mircl 
 |-  ( ph -> ( M ` ( ( S ` B ) ` C ) ) e. P )
21 1 2 3 4 6 5 11 8 12 mircl 
 |-  ( ph -> ( N ` C ) e. P )
22 15 21 eqeltrd 
 |-  ( ph -> ( K ` ( M ` C ) ) e. P )
23 1 2 3 4 6 5 13 9 17 mirbtwn 
 |-  ( ph -> Q e. ( ( K ` ( M ` C ) ) I ( M ` C ) ) )
24 1 2 3 5 22 13 17 23 tgbtwncom 
 |-  ( ph -> Q e. ( ( M ` C ) I ( K ` ( M ` C ) ) ) )
25 8 fveq1i 
 |-  ( N ` C ) = ( ( S ` B ) ` C )
26 15 25 eqtrdi 
 |-  ( ph -> ( K ` ( M ` C ) ) = ( ( S ` B ) ` C ) )
27 26 oveq2d 
 |-  ( ph -> ( ( M ` C ) I ( K ` ( M ` C ) ) ) = ( ( M ` C ) I ( ( S ` B ) ` C ) ) )
28 24 27 eleqtrd 
 |-  ( ph -> Q e. ( ( M ` C ) I ( ( S ` B ) ` C ) ) )
29 1 2 3 5 17 13 19 28 tgbtwncom 
 |-  ( ph -> Q e. ( ( ( S ` B ) ` C ) I ( M ` C ) ) )
30 1 2 3 4 6 5 10 7 19 13 17 29 mirbtwni 
 |-  ( ph -> ( M ` Q ) e. ( ( M ` ( ( S ` B ) ` C ) ) I ( M ` ( M ` C ) ) ) )
31 1 2 3 4 6 5 10 7 12 mirmir 
 |-  ( ph -> ( M ` ( M ` C ) ) = C )
32 31 oveq2d 
 |-  ( ph -> ( ( M ` ( ( S ` B ) ` C ) ) I ( M ` ( M ` C ) ) ) = ( ( M ` ( ( S ` B ) ` C ) ) I C ) )
33 30 32 eleqtrd 
 |-  ( ph -> ( M ` Q ) e. ( ( M ` ( ( S ` B ) ` C ) ) I C ) )
34 1 2 3 5 17 19 axtgcgrrflx 
 |-  ( ph -> ( ( M ` C ) .- ( ( S ` B ) ` C ) ) = ( ( ( S ` B ) ` C ) .- ( M ` C ) ) )
35 1 2 3 4 6 5 10 7 19 17 miriso 
 |-  ( ph -> ( ( M ` ( ( S ` B ) ` C ) ) .- ( M ` ( M ` C ) ) ) = ( ( ( S ` B ) ` C ) .- ( M ` C ) ) )
36 31 oveq2d 
 |-  ( ph -> ( ( M ` ( ( S ` B ) ` C ) ) .- ( M ` ( M ` C ) ) ) = ( ( M ` ( ( S ` B ) ` C ) ) .- C ) )
37 34 35 36 3eqtr2d 
 |-  ( ph -> ( ( M ` C ) .- ( ( S ` B ) ` C ) ) = ( ( M ` ( ( S ` B ) ` C ) ) .- C ) )
38 26 oveq2d 
 |-  ( ph -> ( Q .- ( K ` ( M ` C ) ) ) = ( Q .- ( ( S ` B ) ` C ) ) )
39 1 2 3 4 6 5 13 9 17 mircgr 
 |-  ( ph -> ( Q .- ( K ` ( M ` C ) ) ) = ( Q .- ( M ` C ) ) )
40 38 39 eqtr3d 
 |-  ( ph -> ( Q .- ( ( S ` B ) ` C ) ) = ( Q .- ( M ` C ) ) )
41 1 2 3 4 6 5 10 7 13 17 miriso 
 |-  ( ph -> ( ( M ` Q ) .- ( M ` ( M ` C ) ) ) = ( Q .- ( M ` C ) ) )
42 31 oveq2d 
 |-  ( ph -> ( ( M ` Q ) .- ( M ` ( M ` C ) ) ) = ( ( M ` Q ) .- C ) )
43 40 41 42 3eqtr2d 
 |-  ( ph -> ( Q .- ( ( S ` B ) ` C ) ) = ( ( M ` Q ) .- C ) )
44 1 2 3 4 6 5 10 7 11 mirmir 
 |-  ( ph -> ( M ` ( M ` B ) ) = B )
45 eqidd 
 |-  ( ph -> ( M ` B ) = ( M ` B ) )
46 eqidd 
 |-  ( ph -> ( M ` C ) = ( M ` C ) )
47 44 45 46 s3eqd 
 |-  ( ph -> <" ( M ` ( M ` B ) ) ( M ` B ) ( M ` C ) "> = <" B ( M ` B ) ( M ` C ) "> )
48 1 2 3 4 6 5 10 7 11 mircl 
 |-  ( ph -> ( M ` B ) e. P )
49 simpr 
 |-  ( ( ph /\ A = B ) -> A = B )
50 49 fveq2d 
 |-  ( ( ph /\ A = B ) -> ( M ` A ) = ( M ` B ) )
51 5 adantr 
 |-  ( ( ph /\ A = B ) -> G e. TarskiG )
52 10 adantr 
 |-  ( ( ph /\ A = B ) -> A e. P )
53 1 2 3 4 6 51 52 7 mircinv 
 |-  ( ( ph /\ A = B ) -> ( M ` A ) = A )
54 50 53 eqtr3d 
 |-  ( ( ph /\ A = B ) -> ( M ` B ) = A )
55 eqidd 
 |-  ( ( ph /\ A = B ) -> B = B )
56 eqidd 
 |-  ( ( ph /\ A = B ) -> C = C )
57 54 55 56 s3eqd 
 |-  ( ( ph /\ A = B ) -> <" ( M ` B ) B C "> = <" A B C "> )
58 14 adantr 
 |-  ( ( ph /\ A = B ) -> <" A B C "> e. ( raG ` G ) )
59 57 58 eqeltrd 
 |-  ( ( ph /\ A = B ) -> <" ( M ` B ) B C "> e. ( raG ` G ) )
60 5 adantr 
 |-  ( ( ph /\ A =/= B ) -> G e. TarskiG )
61 10 adantr 
 |-  ( ( ph /\ A =/= B ) -> A e. P )
62 11 adantr 
 |-  ( ( ph /\ A =/= B ) -> B e. P )
63 12 adantr 
 |-  ( ( ph /\ A =/= B ) -> C e. P )
64 1 2 3 4 6 60 61 7 62 mircl 
 |-  ( ( ph /\ A =/= B ) -> ( M ` B ) e. P )
65 14 adantr 
 |-  ( ( ph /\ A =/= B ) -> <" A B C "> e. ( raG ` G ) )
66 simpr 
 |-  ( ( ph /\ A =/= B ) -> A =/= B )
67 1 2 3 4 6 60 61 7 62 mirbtwn 
 |-  ( ( ph /\ A =/= B ) -> A e. ( ( M ` B ) I B ) )
68 1 4 3 60 64 62 61 67 btwncolg1 
 |-  ( ( ph /\ A =/= B ) -> ( A e. ( ( M ` B ) L B ) \/ ( M ` B ) = B ) )
69 1 4 3 60 64 62 61 68 colcom 
 |-  ( ( ph /\ A =/= B ) -> ( A e. ( B L ( M ` B ) ) \/ B = ( M ` B ) ) )
70 1 2 3 4 6 60 61 62 63 64 65 66 69 ragcol 
 |-  ( ( ph /\ A =/= B ) -> <" ( M ` B ) B C "> e. ( raG ` G ) )
71 59 70 pm2.61dane 
 |-  ( ph -> <" ( M ` B ) B C "> e. ( raG ` G ) )
72 1 2 3 4 6 5 48 11 12 71 7 10 mirrag 
 |-  ( ph -> <" ( M ` ( M ` B ) ) ( M ` B ) ( M ` C ) "> e. ( raG ` G ) )
73 47 72 eqeltrrd 
 |-  ( ph -> <" B ( M ` B ) ( M ` C ) "> e. ( raG ` G ) )
74 1 2 3 4 6 5 11 48 17 israg 
 |-  ( ph -> ( <" B ( M ` B ) ( M ` C ) "> e. ( raG ` G ) <-> ( B .- ( M ` C ) ) = ( B .- ( ( S ` ( M ` B ) ) ` ( M ` C ) ) ) ) )
75 73 74 mpbid 
 |-  ( ph -> ( B .- ( M ` C ) ) = ( B .- ( ( S ` ( M ` B ) ) ` ( M ` C ) ) ) )
76 1 2 3 4 6 5 10 7 12 11 mirmir2 
 |-  ( ph -> ( M ` ( ( S ` B ) ` C ) ) = ( ( S ` ( M ` B ) ) ` ( M ` C ) ) )
77 76 oveq2d 
 |-  ( ph -> ( B .- ( M ` ( ( S ` B ) ` C ) ) ) = ( B .- ( ( S ` ( M ` B ) ) ` ( M ` C ) ) ) )
78 75 77 eqtr4d 
 |-  ( ph -> ( B .- ( M ` C ) ) = ( B .- ( M ` ( ( S ` B ) ` C ) ) ) )
79 1 2 3 5 11 17 11 20 78 tgcgrcomlr 
 |-  ( ph -> ( ( M ` C ) .- B ) = ( ( M ` ( ( S ` B ) ` C ) ) .- B ) )
80 1 2 3 4 6 5 11 18 12 mircgr 
 |-  ( ph -> ( B .- ( ( S ` B ) ` C ) ) = ( B .- C ) )
81 1 2 3 5 11 19 11 12 80 tgcgrcomlr 
 |-  ( ph -> ( ( ( 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 
 |-  ( ph -> ( Q .- B ) = ( ( M ` Q ) .- B ) )
83 1 2 3 5 13 11 16 11 82 tgcgrcomlr 
 |-  ( ph -> ( 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 eqtrdi 
 |-  ( ph -> ( B .- Q ) = ( B .- ( ( S ` A ) ` Q ) ) )
87 1 2 3 4 6 5 11 10 13 israg 
 |-  ( ph -> ( <" B A Q "> e. ( raG ` G ) <-> ( B .- Q ) = ( B .- ( ( S ` A ) ` Q ) ) ) )
88 86 87 mpbird 
 |-  ( ph -> <" B A Q "> e. ( raG ` G ) )