Metamath Proof Explorer

Theorem hpgne2

Description: Points on the open half plane cannot lie on its border. (Contributed by Thierry Arnoux, 4-Mar-2020)

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

Proof

Step Hyp Ref Expression
1 ishpg.p 
 |-  P = ( Base ` G )
2 ishpg.i 
 |-  I = ( Itv ` G )
3 ishpg.l 
 |-  L = ( LineG ` G )
4 ishpg.o 
 |-  O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
5 ishpg.g 
 |-  ( ph -> G e. TarskiG )
6 ishpg.d 
 |-  ( ph -> D e. ran L )
7 hpgbr.a 
 |-  ( ph -> A e. P )
8 hpgbr.b 
 |-  ( ph -> B e. P )
9 hpgne1.1 
 |-  ( ph -> A ( ( hpG ` G ) ` D ) B )
10 eqid 
 |-  ( dist ` G ) = ( dist ` G )
11 6 ad2antrr 
 |-  ( ( ( ph /\ c e. P ) /\ ( A O c /\ B O c ) ) -> D e. ran L )
12 5 ad2antrr 
 |-  ( ( ( ph /\ c e. P ) /\ ( A O c /\ B O c ) ) -> G e. TarskiG )
13 8 ad2antrr 
 |-  ( ( ( ph /\ c e. P ) /\ ( A O c /\ B O c ) ) -> B e. P )
14 simplr 
 |-  ( ( ( ph /\ c e. P ) /\ ( A O c /\ B O c ) ) -> c e. P )
15 simprr 
 |-  ( ( ( ph /\ c e. P ) /\ ( A O c /\ B O c ) ) -> B O c )
16 1 10 2 4 3 11 12 13 14 15 oppne1 
 |-  ( ( ( ph /\ c e. P ) /\ ( A O c /\ B O c ) ) -> -. B e. D )
17 1 2 3 4 5 6 7 8 hpgbr 
 |-  ( ph -> ( A ( ( hpG ` G ) ` D ) B <-> E. c e. P ( A O c /\ B O c ) ) )
18 9 17 mpbid 
 |-  ( ph -> E. c e. P ( A O c /\ B O c ) )
19 16 18 r19.29a 
 |-  ( ph -> -. B e. D )