Metamath Proof Explorer

Theorem hpgerlem

Description: Lemma for the proof that the half-plane relation is an equivalence relation. Lemma 9.10 of Schwabhauser p. 72. (Contributed by Thierry Arnoux, 4-Mar-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 ) ) }
hpgid.1 
|- ( ph -> -. A e. D )
Assertion hpgerlem 
|- ( ph -> E. c e. P A O c )

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 hpgid.1 
 |-  ( ph -> -. A e. D )
9 3 4 5 tglnne0 
 |-  ( ph -> D =/= (/) )
10 n0 
 |-  ( D =/= (/) <-> E. x x e. D )
11 9 10 sylib 
 |-  ( ph -> E. x x e. D )
12 eqid 
 |-  ( dist ` G ) = ( dist ` G )
13 4 adantr 
 |-  ( ( ph /\ x e. D ) -> G e. TarskiG )
14 6 adantr 
 |-  ( ( ph /\ x e. D ) -> A e. P )
15 5 adantr 
 |-  ( ( ph /\ x e. D ) -> D e. ran L )
16 simpr 
 |-  ( ( ph /\ x e. D ) -> x e. D )
17 1 3 2 13 15 16 tglnpt 
 |-  ( ( ph /\ x e. D ) -> x e. P )
18 5 adantr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> D e. ran L )
19 4 adantr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> G e. TarskiG )
20 simpr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> ( # ` P ) = 1 )
21 1 2 3 19 20 tglndim0 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> -. D e. ran L )
22 18 21 pm2.65da 
 |-  ( ph -> -. ( # ` P ) = 1 )
23 1 6 tgldimor 
 |-  ( ph -> ( ( # ` P ) = 1 \/ 2 <_ ( # ` P ) ) )
24 23 ord 
 |-  ( ph -> ( -. ( # ` P ) = 1 -> 2 <_ ( # ` P ) ) )
25 22 24 mpd 
 |-  ( ph -> 2 <_ ( # ` P ) )
26 25 adantr 
 |-  ( ( ph /\ x e. D ) -> 2 <_ ( # ` P ) )
27 1 12 2 13 14 17 26 tgbtwndiff 
 |-  ( ( ph /\ x e. D ) -> E. c e. P ( x e. ( A I c ) /\ x =/= c ) )
28 8 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ c e. P ) /\ x e. ( A I c ) ) /\ x =/= c ) -> -. A e. D )
29 13 ad4antr 
 |-  ( ( ( ( ( ( ph /\ x e. D ) /\ c e. P ) /\ x e. ( A I c ) ) /\ x =/= c ) /\ c e. D ) -> G e. TarskiG )
30 17 ad4antr 
 |-  ( ( ( ( ( ( ph /\ x e. D ) /\ c e. P ) /\ x e. ( A I c ) ) /\ x =/= c ) /\ c e. D ) -> x e. P )
31 simpr 
 |-  ( ( ( ph /\ x e. D ) /\ c e. P ) -> c e. P )
32 31 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ x e. D ) /\ c e. P ) /\ x e. ( A I c ) ) /\ x =/= c ) /\ c e. D ) -> c e. P )
33 14 ad4antr 
 |-  ( ( ( ( ( ( ph /\ x e. D ) /\ c e. P ) /\ x e. ( A I c ) ) /\ x =/= c ) /\ c e. D ) -> A e. P )
34 simplr 
 |-  ( ( ( ( ( ( ph /\ x e. D ) /\ c e. P ) /\ x e. ( A I c ) ) /\ x =/= c ) /\ c e. D ) -> x =/= c )
35 simplr 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ c e. P ) /\ x e. ( A I c ) ) /\ x =/= c ) -> x e. ( A I c ) )
36 35 adantr 
 |-  ( ( ( ( ( ( ph /\ x e. D ) /\ c e. P ) /\ x e. ( A I c ) ) /\ x =/= c ) /\ c e. D ) -> x e. ( A I c ) )
37 1 2 3 29 30 32 33 34 36 btwnlng2 
 |-  ( ( ( ( ( ( ph /\ x e. D ) /\ c e. P ) /\ x e. ( A I c ) ) /\ x =/= c ) /\ c e. D ) -> A e. ( x L c ) )
38 15 ad4antr 
 |-  ( ( ( ( ( ( ph /\ x e. D ) /\ c e. P ) /\ x e. ( A I c ) ) /\ x =/= c ) /\ c e. D ) -> D e. ran L )
39 16 ad4antr 
 |-  ( ( ( ( ( ( ph /\ x e. D ) /\ c e. P ) /\ x e. ( A I c ) ) /\ x =/= c ) /\ c e. D ) -> x e. D )
40 simpr 
 |-  ( ( ( ( ( ( ph /\ x e. D ) /\ c e. P ) /\ x e. ( A I c ) ) /\ x =/= c ) /\ c e. D ) -> c e. D )
41 1 2 3 29 30 32 34 34 38 39 40 tglinethru 
 |-  ( ( ( ( ( ( ph /\ x e. D ) /\ c e. P ) /\ x e. ( A I c ) ) /\ x =/= c ) /\ c e. D ) -> D = ( x L c ) )
42 37 41 eleqtrrd 
 |-  ( ( ( ( ( ( ph /\ x e. D ) /\ c e. P ) /\ x e. ( A I c ) ) /\ x =/= c ) /\ c e. D ) -> A e. D )
43 28 42 mtand 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ c e. P ) /\ x e. ( A I c ) ) /\ x =/= c ) -> -. c e. D )
44 eleq1w 
 |-  ( t = x -> ( t e. ( A I c ) <-> x e. ( A I c ) ) )
45 44 rspcev 
 |-  ( ( x e. D /\ x e. ( A I c ) ) -> E. t e. D t e. ( A I c ) )
46 45 ad5ant24 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ c e. P ) /\ x e. ( A I c ) ) /\ x =/= c ) -> E. t e. D t e. ( A I c ) )
47 28 43 46 jca31 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ c e. P ) /\ x e. ( A I c ) ) /\ x =/= c ) -> ( ( -. A e. D /\ -. c e. D ) /\ E. t e. D t e. ( A I c ) ) )
48 47 anasss 
 |-  ( ( ( ( ph /\ x e. D ) /\ c e. P ) /\ ( x e. ( A I c ) /\ x =/= c ) ) -> ( ( -. A e. D /\ -. c e. D ) /\ E. t e. D t e. ( A I c ) ) )
49 14 adantr 
 |-  ( ( ( ph /\ x e. D ) /\ c e. P ) -> A e. P )
50 1 12 2 7 49 31 islnopp 
 |-  ( ( ( ph /\ x e. D ) /\ c e. P ) -> ( A O c <-> ( ( -. A e. D /\ -. c e. D ) /\ E. t e. D t e. ( A I c ) ) ) )
51 50 adantr 
 |-  ( ( ( ( ph /\ x e. D ) /\ c e. P ) /\ ( x e. ( A I c ) /\ x =/= c ) ) -> ( A O c <-> ( ( -. A e. D /\ -. c e. D ) /\ E. t e. D t e. ( A I c ) ) ) )
52 48 51 mpbird 
 |-  ( ( ( ( ph /\ x e. D ) /\ c e. P ) /\ ( x e. ( A I c ) /\ x =/= c ) ) -> A O c )
53 52 ex 
 |-  ( ( ( ph /\ x e. D ) /\ c e. P ) -> ( ( x e. ( A I c ) /\ x =/= c ) -> A O c ) )
54 53 reximdva 
 |-  ( ( ph /\ x e. D ) -> ( E. c e. P ( x e. ( A I c ) /\ x =/= c ) -> E. c e. P A O c ) )
55 27 54 mpd 
 |-  ( ( ph /\ x e. D ) -> E. c e. P A O c )
56 11 55 exlimddv 
 |-  ( ph -> E. c e. P A O c )