Metamath Proof Explorer

Theorem hpgtr

Description: The half-plane relation is transitive. Theorem 9.13 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 ) ) }
hpgcom.b 
|- ( ph -> B e. P )
hpgcom.1 
|- ( ph -> A ( ( hpG ` G ) ` D ) B )
hpgtr.c 
|- ( ph -> C e. P )
hpgtr.1 
|- ( ph -> B ( ( hpG ` G ) ` D ) C )
Assertion hpgtr 
|- ( ph -> A ( ( hpG ` G ) ` D ) 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 hpgcom.b 
 |-  ( ph -> B e. P )
9 hpgcom.1 
 |-  ( ph -> A ( ( hpG ` G ) ` D ) B )
10 hpgtr.c 
 |-  ( ph -> C e. P )
11 hpgtr.1 
 |-  ( ph -> B ( ( hpG ` G ) ` D ) C )
12 1 2 3 7 4 5 6 8 hpgbr 
 |-  ( ph -> ( A ( ( hpG ` G ) ` D ) B <-> E. c e. P ( A O c /\ B O c ) ) )
13 9 12 mpbid 
 |-  ( ph -> E. c e. P ( A O c /\ B O c ) )
14 simprl 
 |-  ( ( ( ph /\ c e. P ) /\ ( A O c /\ B O c ) ) -> A O c )
15 11 ad2antrr 
 |-  ( ( ( ph /\ c e. P ) /\ ( A O c /\ B O c ) ) -> B ( ( hpG ` G ) ` D ) C )
16 4 ad2antrr 
 |-  ( ( ( ph /\ c e. P ) /\ ( A O c /\ B O c ) ) -> G e. TarskiG )
17 5 ad2antrr 
 |-  ( ( ( ph /\ c e. P ) /\ ( A O c /\ B O c ) ) -> D e. ran L )
18 8 ad2antrr 
 |-  ( ( ( ph /\ c e. P ) /\ ( A O c /\ B O c ) ) -> B e. P )
19 10 ad2antrr 
 |-  ( ( ( ph /\ c e. P ) /\ ( A O c /\ B O c ) ) -> C e. P )
20 simplr 
 |-  ( ( ( ph /\ c e. P ) /\ ( A O c /\ B O c ) ) -> c e. P )
21 simprr 
 |-  ( ( ( ph /\ c e. P ) /\ ( A O c /\ B O c ) ) -> B O c )
22 1 2 3 7 16 17 18 19 20 21 lnopp2hpgb 
 |-  ( ( ( ph /\ c e. P ) /\ ( A O c /\ B O c ) ) -> ( C O c <-> B ( ( hpG ` G ) ` D ) C ) )
23 15 22 mpbird 
 |-  ( ( ( ph /\ c e. P ) /\ ( A O c /\ B O c ) ) -> C O c )
24 14 23 jca 
 |-  ( ( ( ph /\ c e. P ) /\ ( A O c /\ B O c ) ) -> ( A O c /\ C O c ) )
25 24 ex 
 |-  ( ( ph /\ c e. P ) -> ( ( A O c /\ B O c ) -> ( A O c /\ C O c ) ) )
26 25 reximdva 
 |-  ( ph -> ( E. c e. P ( A O c /\ B O c ) -> E. c e. P ( A O c /\ C O c ) ) )
27 13 26 mpd 
 |-  ( ph -> E. c e. P ( A O c /\ C O c ) )
28 1 2 3 7 4 5 6 10 hpgbr 
 |-  ( ph -> ( A ( ( hpG ` G ) ` D ) C <-> E. c e. P ( A O c /\ C O c ) ) )
29 27 28 mpbird 
 |-  ( ph -> A ( ( hpG ` G ) ` D ) C )