Metamath Proof Explorer


Theorem hpgid

Description: The half-plane relation is reflexive. Theorem 9.11 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 hpgid
|- ( ph -> A ( ( hpG ` G ) ` D ) A )

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 simprr
 |-  ( ( ph /\ ( c e. P /\ A O c ) ) -> A O c )
10 9 9 jca
 |-  ( ( ph /\ ( c e. P /\ A O c ) ) -> ( A O c /\ A O c ) )
11 1 2 3 4 5 6 7 8 hpgerlem
 |-  ( ph -> E. c e. P A O c )
12 10 11 reximddv
 |-  ( ph -> E. c e. P ( A O c /\ A O c ) )
13 1 2 3 7 4 5 6 6 hpgbr
 |-  ( ph -> ( A ( ( hpG ` G ) ` D ) A <-> E. c e. P ( A O c /\ A O c ) ) )
14 12 13 mpbird
 |-  ( ph -> A ( ( hpG ` G ) ` D ) A )