Metamath Proof Explorer


Theorem hpgcom

Description: The half-plane relation commutes. Theorem 9.12 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 )
Assertion hpgcom
|- ( ph -> B ( ( 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 hpgcom.b
 |-  ( ph -> B e. P )
9 hpgcom.1
 |-  ( ph -> A ( ( hpG ` G ) ` D ) B )
10 ancom
 |-  ( ( A O c /\ B O c ) <-> ( B O c /\ A O c ) )
11 10 a1i
 |-  ( ph -> ( ( A O c /\ B O c ) <-> ( B O c /\ A O c ) ) )
12 11 rexbidv
 |-  ( ph -> ( E. c e. P ( A O c /\ B O c ) <-> E. c e. P ( B O c /\ A O c ) ) )
13 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 ) ) )
14 1 2 3 7 4 5 8 6 hpgbr
 |-  ( ph -> ( B ( ( hpG ` G ) ` D ) A <-> E. c e. P ( B O c /\ A O c ) ) )
15 12 13 14 3bitr4d
 |-  ( ph -> ( A ( ( hpG ` G ) ` D ) B <-> B ( ( hpG ` G ) ` D ) A ) )
16 9 15 mpbid
 |-  ( ph -> B ( ( hpG ` G ) ` D ) A )