Metamath Proof Explorer

Theorem hpgbr

Description: Half-planes : property for points A and B to belong to the same open half plane delimited by line D . Definition 9.7 of Schwabhauser p. 71. (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 )
Assertion hpgbr 
|- ( ph -> ( A ( ( hpG ` G ) ` D ) B <-> E. c e. P ( A O c /\ B O c ) ) )

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 1 2 3 4 5 6 ishpg 
 |-  ( ph -> ( ( hpG ` G ) ` D ) = { <. a , b >. | E. c e. P ( a O c /\ b O c ) } )
10 simpl 
 |-  ( ( a = u /\ b = v ) -> a = u )
11 10 breq1d 
 |-  ( ( a = u /\ b = v ) -> ( a O c <-> u O c ) )
12 simpr 
 |-  ( ( a = u /\ b = v ) -> b = v )
13 12 breq1d 
 |-  ( ( a = u /\ b = v ) -> ( b O c <-> v O c ) )
14 11 13 anbi12d 
 |-  ( ( a = u /\ b = v ) -> ( ( a O c /\ b O c ) <-> ( u O c /\ v O c ) ) )
15 14 rexbidv 
 |-  ( ( a = u /\ b = v ) -> ( E. c e. P ( a O c /\ b O c ) <-> E. c e. P ( u O c /\ v O c ) ) )
16 15 cbvopabv 
 |-  { <. a , b >. | E. c e. P ( a O c /\ b O c ) } = { <. u , v >. | E. c e. P ( u O c /\ v O c ) }
17 9 16 eqtrdi 
 |-  ( ph -> ( ( hpG ` G ) ` D ) = { <. u , v >. | E. c e. P ( u O c /\ v O c ) } )
18 17 breqd 
 |-  ( ph -> ( A ( ( hpG ` G ) ` D ) B <-> A { <. u , v >. | E. c e. P ( u O c /\ v O c ) } B ) )
19 simpl 
 |-  ( ( u = A /\ v = B ) -> u = A )
20 19 breq1d 
 |-  ( ( u = A /\ v = B ) -> ( u O c <-> A O c ) )
21 simpr 
 |-  ( ( u = A /\ v = B ) -> v = B )
22 21 breq1d 
 |-  ( ( u = A /\ v = B ) -> ( v O c <-> B O c ) )
23 20 22 anbi12d 
 |-  ( ( u = A /\ v = B ) -> ( ( u O c /\ v O c ) <-> ( A O c /\ B O c ) ) )
24 23 rexbidv 
 |-  ( ( u = A /\ v = B ) -> ( E. c e. P ( u O c /\ v O c ) <-> E. c e. P ( A O c /\ B O c ) ) )
25 eqid 
 |-  { <. u , v >. | E. c e. P ( u O c /\ v O c ) } = { <. u , v >. | E. c e. P ( u O c /\ v O c ) }
26 24 25 brabga 
 |-  ( ( A e. P /\ B e. P ) -> ( A { <. u , v >. | E. c e. P ( u O c /\ v O c ) } B <-> E. c e. P ( A O c /\ B O c ) ) )
27 7 8 26 syl2anc 
 |-  ( ph -> ( A { <. u , v >. | E. c e. P ( u O c /\ v O c ) } B <-> E. c e. P ( A O c /\ B O c ) ) )
28 18 27 bitrd 
 |-  ( ph -> ( A ( ( hpG ` G ) ` D ) B <-> E. c e. P ( A O c /\ B O c ) ) )