Metamath Proof Explorer

Theorem colhp

Description: Half-plane relation for colinear points. Theorem 9.19 of Schwabhauser p. 73. (Contributed by Thierry Arnoux, 3-Aug-2020)

Ref Expression
Hypotheses hpgid.p 
|- P = ( Base ` G )
hpgid.i 
|- I = ( Itv ` G )
hpgid.l 
|- L = ( LineG ` G )
hpgid.g 
|- ( ph -> G e. TarskiG )
hpgid.d 
|- ( ph -> D e. ran L )
hpgid.a 
|- ( ph -> A e. P )
hpgid.o 
|- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
colopp.b 
|- ( ph -> B e. P )
colopp.p 
|- ( ph -> C e. D )
colopp.1 
|- ( ph -> ( C e. ( A L B ) \/ A = B ) )
colhp.k 
|- K = ( hlG ` G )
Assertion colhp 
|- ( ph -> ( A ( ( hpG ` G ) ` D ) B <-> ( A ( K ` C ) B /\ -. A e. D ) ) )

Proof

Step Hyp Ref Expression
1 hpgid.p 
 |-  P = ( Base ` G )
2 hpgid.i 
 |-  I = ( Itv ` G )
3 hpgid.l 
 |-  L = ( LineG ` G )
4 hpgid.g 
 |-  ( ph -> G e. TarskiG )
5 hpgid.d 
 |-  ( ph -> D e. ran L )
6 hpgid.a 
 |-  ( ph -> A e. P )
7 hpgid.o 
 |-  O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
8 colopp.b 
 |-  ( ph -> B e. P )
9 colopp.p 
 |-  ( ph -> C e. D )
10 colopp.1 
 |-  ( ph -> ( C e. ( A L B ) \/ A = B ) )
11 colhp.k 
 |-  K = ( hlG ` G )
12 ancom 
 |-  ( ( A ( K ` C ) B /\ -. A e. D ) <-> ( -. A e. D /\ A ( K ` C ) B ) )
13 12 a1i 
 |-  ( ph -> ( ( A ( K ` C ) B /\ -. A e. D ) <-> ( -. A e. D /\ A ( K ` C ) B ) ) )
14 4 adantr 
 |-  ( ( ph /\ -. A e. D ) -> G e. TarskiG )
15 5 adantr 
 |-  ( ( ph /\ -. A e. D ) -> D e. ran L )
16 8 adantr 
 |-  ( ( ph /\ -. A e. D ) -> B e. P )
17 eqid 
 |-  ( dist ` G ) = ( dist ` G )
18 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
19 1 3 2 4 5 9 tglnpt 
 |-  ( ph -> C e. P )
20 eqid 
 |-  ( ( pInvG ` G ) ` C ) = ( ( pInvG ` G ) ` C )
21 1 17 2 3 18 4 19 20 6 mircl 
 |-  ( ph -> ( ( ( pInvG ` G ) ` C ) ` A ) e. P )
22 21 adantr 
 |-  ( ( ph /\ -. A e. D ) -> ( ( ( pInvG ` G ) ` C ) ` A ) e. P )
23 9 adantr 
 |-  ( ( ph /\ -. A e. D ) -> C e. D )
24 19 adantr 
 |-  ( ( ph /\ -. A e. D ) -> C e. P )
25 6 adantr 
 |-  ( ( ph /\ -. A e. D ) -> A e. P )
26 nelne2 
 |-  ( ( C e. D /\ -. A e. D ) -> C =/= A )
27 9 26 sylan 
 |-  ( ( ph /\ -. A e. D ) -> C =/= A )
28 27 necomd 
 |-  ( ( ph /\ -. A e. D ) -> A =/= C )
29 1 17 2 3 18 4 19 20 6 mirbtwn 
 |-  ( ph -> C e. ( ( ( ( pInvG ` G ) ` C ) ` A ) I A ) )
30 1 17 2 4 21 19 6 29 tgbtwncom 
 |-  ( ph -> C e. ( A I ( ( ( pInvG ` G ) ` C ) ` A ) ) )
31 30 adantr 
 |-  ( ( ph /\ -. A e. D ) -> C e. ( A I ( ( ( pInvG ` G ) ` C ) ` A ) ) )
32 1 2 3 14 25 24 22 28 31 btwnlng3 
 |-  ( ( ph /\ -. A e. D ) -> ( ( ( pInvG ` G ) ` C ) ` A ) e. ( A L C ) )
33 1 3 2 4 6 8 19 10 colrot1 
 |-  ( ph -> ( A e. ( B L C ) \/ B = C ) )
34 1 3 2 4 8 19 6 33 colcom 
 |-  ( ph -> ( A e. ( C L B ) \/ C = B ) )
35 34 adantr 
 |-  ( ( ph /\ -. A e. D ) -> ( A e. ( C L B ) \/ C = B ) )
36 1 2 3 14 22 25 24 16 32 35 coltr 
 |-  ( ( ph /\ -. A e. D ) -> ( ( ( ( pInvG ` G ) ` C ) ` A ) e. ( C L B ) \/ C = B ) )
37 1 3 2 14 24 16 22 36 colrot1 
 |-  ( ( ph /\ -. A e. D ) -> ( C e. ( B L ( ( ( pInvG ` G ) ` C ) ` A ) ) \/ B = ( ( ( pInvG ` G ) ` C ) ` A ) ) )
38 1 2 3 14 15 16 7 22 23 37 colopp 
 |-  ( ( ph /\ -. A e. D ) -> ( B O ( ( ( pInvG ` G ) ` C ) ` A ) <-> ( C e. ( B I ( ( ( pInvG ` G ) ` C ) ` A ) ) /\ -. B e. D /\ -. ( ( ( pInvG ` G ) ` C ) ` A ) e. D ) ) )
39 simpr 
 |-  ( ( ph /\ -. A e. D ) -> -. A e. D )
40 1 17 2 3 18 4 19 20 6 mirmir 
 |-  ( ph -> ( ( ( pInvG ` G ) ` C ) ` ( ( ( pInvG ` G ) ` C ) ` A ) ) = A )
41 40 adantr 
 |-  ( ( ph /\ ( ( ( pInvG ` G ) ` C ) ` A ) e. D ) -> ( ( ( pInvG ` G ) ` C ) ` ( ( ( pInvG ` G ) ` C ) ` A ) ) = A )
42 4 adantr 
 |-  ( ( ph /\ ( ( ( pInvG ` G ) ` C ) ` A ) e. D ) -> G e. TarskiG )
43 5 adantr 
 |-  ( ( ph /\ ( ( ( pInvG ` G ) ` C ) ` A ) e. D ) -> D e. ran L )
44 9 adantr 
 |-  ( ( ph /\ ( ( ( pInvG ` G ) ` C ) ` A ) e. D ) -> C e. D )
45 simpr 
 |-  ( ( ph /\ ( ( ( pInvG ` G ) ` C ) ` A ) e. D ) -> ( ( ( pInvG ` G ) ` C ) ` A ) e. D )
46 1 17 2 3 18 42 20 43 44 45 mirln 
 |-  ( ( ph /\ ( ( ( pInvG ` G ) ` C ) ` A ) e. D ) -> ( ( ( pInvG ` G ) ` C ) ` ( ( ( pInvG ` G ) ` C ) ` A ) ) e. D )
47 41 46 eqeltrrd 
 |-  ( ( ph /\ ( ( ( pInvG ` G ) ` C ) ` A ) e. D ) -> A e. D )
48 47 stoic1a 
 |-  ( ( ph /\ -. A e. D ) -> -. ( ( ( pInvG ` G ) ` C ) ` A ) e. D )
49 simpr 
 |-  ( ( ph /\ t = C ) -> t = C )
50 49 eleq1d 
 |-  ( ( ph /\ t = C ) -> ( t e. ( A I ( ( ( pInvG ` G ) ` C ) ` A ) ) <-> C e. ( A I ( ( ( pInvG ` G ) ` C ) ` A ) ) ) )
51 9 50 30 rspcedvd 
 |-  ( ph -> E. t e. D t e. ( A I ( ( ( pInvG ` G ) ` C ) ` A ) ) )
52 51 adantr 
 |-  ( ( ph /\ -. A e. D ) -> E. t e. D t e. ( A I ( ( ( pInvG ` G ) ` C ) ` A ) ) )
53 39 48 52 jca31 
 |-  ( ( ph /\ -. A e. D ) -> ( ( -. A e. D /\ -. ( ( ( pInvG ` G ) ` C ) ` A ) e. D ) /\ E. t e. D t e. ( A I ( ( ( pInvG ` G ) ` C ) ` A ) ) ) )
54 1 17 2 7 25 22 islnopp 
 |-  ( ( ph /\ -. A e. D ) -> ( A O ( ( ( pInvG ` G ) ` C ) ` A ) <-> ( ( -. A e. D /\ -. ( ( ( pInvG ` G ) ` C ) ` A ) e. D ) /\ E. t e. D t e. ( A I ( ( ( pInvG ` G ) ` C ) ` A ) ) ) ) )
55 53 54 mpbird 
 |-  ( ( ph /\ -. A e. D ) -> A O ( ( ( pInvG ` G ) ` C ) ` A ) )
56 1 2 3 7 14 15 25 16 22 55 lnopp2hpgb 
 |-  ( ( ph /\ -. A e. D ) -> ( B O ( ( ( pInvG ` G ) ` C ) ` A ) <-> A ( ( hpG ` G ) ` D ) B ) )
57 8 ad2antrr 
 |-  ( ( ( ph /\ -. A e. D ) /\ ( C e. ( B I ( ( ( pInvG ` G ) ` C ) ` A ) ) /\ -. B e. D ) ) -> B e. P )
58 6 ad2antrr 
 |-  ( ( ( ph /\ -. A e. D ) /\ ( C e. ( B I ( ( ( pInvG ` G ) ` C ) ` A ) ) /\ -. B e. D ) ) -> A e. P )
59 19 ad2antrr 
 |-  ( ( ( ph /\ -. A e. D ) /\ ( C e. ( B I ( ( ( pInvG ` G ) ` C ) ` A ) ) /\ -. B e. D ) ) -> C e. P )
60 4 ad2antrr 
 |-  ( ( ( ph /\ -. A e. D ) /\ ( C e. ( B I ( ( ( pInvG ` G ) ` C ) ` A ) ) /\ -. B e. D ) ) -> G e. TarskiG )
61 9 ad2antrr 
 |-  ( ( ( ph /\ -. A e. D ) /\ ( C e. ( B I ( ( ( pInvG ` G ) ` C ) ` A ) ) /\ -. B e. D ) ) -> C e. D )
62 simprr 
 |-  ( ( ( ph /\ -. A e. D ) /\ ( C e. ( B I ( ( ( pInvG ` G ) ` C ) ` A ) ) /\ -. B e. D ) ) -> -. B e. D )
63 nelne2 
 |-  ( ( C e. D /\ -. B e. D ) -> C =/= B )
64 63 necomd 
 |-  ( ( C e. D /\ -. B e. D ) -> B =/= C )
65 61 62 64 syl2anc 
 |-  ( ( ( ph /\ -. A e. D ) /\ ( C e. ( B I ( ( ( pInvG ` G ) ` C ) ` A ) ) /\ -. B e. D ) ) -> B =/= C )
66 28 adantr 
 |-  ( ( ( ph /\ -. A e. D ) /\ ( C e. ( B I ( ( ( pInvG ` G ) ` C ) ` A ) ) /\ -. B e. D ) ) -> A =/= C )
67 simprl 
 |-  ( ( ( ph /\ -. A e. D ) /\ ( C e. ( B I ( ( ( pInvG ` G ) ` C ) ` A ) ) /\ -. B e. D ) ) -> C e. ( B I ( ( ( pInvG ` G ) ` C ) ` A ) ) )
68 1 17 2 3 18 60 20 11 59 57 58 58 65 66 67 mirhl2 
 |-  ( ( ( ph /\ -. A e. D ) /\ ( C e. ( B I ( ( ( pInvG ` G ) ` C ) ` A ) ) /\ -. B e. D ) ) -> B ( K ` C ) A )
69 1 2 11 57 58 59 60 68 hlcomd 
 |-  ( ( ( ph /\ -. A e. D ) /\ ( C e. ( B I ( ( ( pInvG ` G ) ` C ) ` A ) ) /\ -. B e. D ) ) -> A ( K ` C ) B )
70 69 3adantr3 
 |-  ( ( ( ph /\ -. A e. D ) /\ ( C e. ( B I ( ( ( pInvG ` G ) ` C ) ` A ) ) /\ -. B e. D /\ -. ( ( ( pInvG ` G ) ` C ) ` A ) e. D ) ) -> A ( K ` C ) B )
71 6 ad2antrr 
 |-  ( ( ( ph /\ -. A e. D ) /\ A ( K ` C ) B ) -> A e. P )
72 8 ad2antrr 
 |-  ( ( ( ph /\ -. A e. D ) /\ A ( K ` C ) B ) -> B e. P )
73 21 ad2antrr 
 |-  ( ( ( ph /\ -. A e. D ) /\ A ( K ` C ) B ) -> ( ( ( pInvG ` G ) ` C ) ` A ) e. P )
74 4 ad2antrr 
 |-  ( ( ( ph /\ -. A e. D ) /\ A ( K ` C ) B ) -> G e. TarskiG )
75 19 ad2antrr 
 |-  ( ( ( ph /\ -. A e. D ) /\ A ( K ` C ) B ) -> C e. P )
76 simpr 
 |-  ( ( ( ph /\ -. A e. D ) /\ A ( K ` C ) B ) -> A ( K ` C ) B )
77 30 ad2antrr 
 |-  ( ( ( ph /\ -. A e. D ) /\ A ( K ` C ) B ) -> C e. ( A I ( ( ( pInvG ` G ) ` C ) ` A ) ) )
78 1 2 11 71 72 73 74 75 76 77 btwnhl 
 |-  ( ( ( ph /\ -. A e. D ) /\ A ( K ` C ) B ) -> C e. ( B I ( ( ( pInvG ` G ) ` C ) ` A ) ) )
79 1 2 11 71 72 75 74 3 76 hlln 
 |-  ( ( ( ph /\ -. A e. D ) /\ A ( K ` C ) B ) -> A e. ( B L C ) )
80 79 adantr 
 |-  ( ( ( ( ph /\ -. A e. D ) /\ A ( K ` C ) B ) /\ B e. D ) -> A e. ( B L C ) )
81 14 ad2antrr 
 |-  ( ( ( ( ph /\ -. A e. D ) /\ A ( K ` C ) B ) /\ B e. D ) -> G e. TarskiG )
82 16 ad2antrr 
 |-  ( ( ( ( ph /\ -. A e. D ) /\ A ( K ` C ) B ) /\ B e. D ) -> B e. P )
83 75 adantr 
 |-  ( ( ( ( ph /\ -. A e. D ) /\ A ( K ` C ) B ) /\ B e. D ) -> C e. P )
84 25 ad2antrr 
 |-  ( ( ( ( ph /\ -. A e. D ) /\ A ( K ` C ) B ) /\ B e. D ) -> A e. P )
85 76 adantr 
 |-  ( ( ( ( ph /\ -. A e. D ) /\ A ( K ` C ) B ) /\ B e. D ) -> A ( K ` C ) B )
86 1 2 11 84 82 83 81 85 hlne2 
 |-  ( ( ( ( ph /\ -. A e. D ) /\ A ( K ` C ) B ) /\ B e. D ) -> B =/= C )
87 15 ad2antrr 
 |-  ( ( ( ( ph /\ -. A e. D ) /\ A ( K ` C ) B ) /\ B e. D ) -> D e. ran L )
88 simpr 
 |-  ( ( ( ( ph /\ -. A e. D ) /\ A ( K ` C ) B ) /\ B e. D ) -> B e. D )
89 9 ad3antrrr 
 |-  ( ( ( ( ph /\ -. A e. D ) /\ A ( K ` C ) B ) /\ B e. D ) -> C e. D )
90 1 2 3 81 82 83 86 86 87 88 89 tglinethru 
 |-  ( ( ( ( ph /\ -. A e. D ) /\ A ( K ` C ) B ) /\ B e. D ) -> D = ( B L C ) )
91 80 90 eleqtrrd 
 |-  ( ( ( ( ph /\ -. A e. D ) /\ A ( K ` C ) B ) /\ B e. D ) -> A e. D )
92 39 ad2antrr 
 |-  ( ( ( ( ph /\ -. A e. D ) /\ A ( K ` C ) B ) /\ B e. D ) -> -. A e. D )
93 91 92 pm2.65da 
 |-  ( ( ( ph /\ -. A e. D ) /\ A ( K ` C ) B ) -> -. B e. D )
94 48 adantr 
 |-  ( ( ( ph /\ -. A e. D ) /\ A ( K ` C ) B ) -> -. ( ( ( pInvG ` G ) ` C ) ` A ) e. D )
95 78 93 94 3jca 
 |-  ( ( ( ph /\ -. A e. D ) /\ A ( K ` C ) B ) -> ( C e. ( B I ( ( ( pInvG ` G ) ` C ) ` A ) ) /\ -. B e. D /\ -. ( ( ( pInvG ` G ) ` C ) ` A ) e. D ) )
96 70 95 impbida 
 |-  ( ( ph /\ -. A e. D ) -> ( ( C e. ( B I ( ( ( pInvG ` G ) ` C ) ` A ) ) /\ -. B e. D /\ -. ( ( ( pInvG ` G ) ` C ) ` A ) e. D ) <-> A ( K ` C ) B ) )
97 38 56 96 3bitr3d 
 |-  ( ( ph /\ -. A e. D ) -> ( A ( ( hpG ` G ) ` D ) B <-> A ( K ` C ) B ) )
98 97 pm5.32da 
 |-  ( ph -> ( ( -. A e. D /\ A ( ( hpG ` G ) ` D ) B ) <-> ( -. A e. D /\ A ( K ` C ) B ) ) )
99 simprr 
 |-  ( ( ph /\ ( -. A e. D /\ A ( ( hpG ` G ) ` D ) B ) ) -> A ( ( hpG ` G ) ` D ) B )
100 4 adantr 
 |-  ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) -> G e. TarskiG )
101 5 adantr 
 |-  ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) -> D e. ran L )
102 6 adantr 
 |-  ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) -> A e. P )
103 8 adantr 
 |-  ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) -> B e. P )
104 simpr 
 |-  ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) -> A ( ( hpG ` G ) ` D ) B )
105 1 2 3 7 100 101 102 103 104 hpgne1 
 |-  ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) -> -. A e. D )
106 105 104 jca 
 |-  ( ( ph /\ A ( ( hpG ` G ) ` D ) B ) -> ( -. A e. D /\ A ( ( hpG ` G ) ` D ) B ) )
107 99 106 impbida 
 |-  ( ph -> ( ( -. A e. D /\ A ( ( hpG ` G ) ` D ) B ) <-> A ( ( hpG ` G ) ` D ) B ) )
108 13 98 107 3bitr2rd 
 |-  ( ph -> ( A ( ( hpG ` G ) ` D ) B <-> ( A ( K ` C ) B /\ -. A e. D ) ) )