Metamath Proof Explorer


Theorem oppcom

Description: Commutativity rule for "opposite" Theorem 9.2 of Schwabhauser p. 67. (Contributed by Thierry Arnoux, 19-Dec-2019)

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

Proof

Step Hyp Ref Expression
1 hpg.p
 |-  P = ( Base ` G )
2 hpg.d
 |-  .- = ( dist ` G )
3 hpg.i
 |-  I = ( Itv ` G )
4 hpg.o
 |-  O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
5 opphl.l
 |-  L = ( LineG ` G )
6 opphl.d
 |-  ( ph -> D e. ran L )
7 opphl.g
 |-  ( ph -> G e. TarskiG )
8 oppcom.a
 |-  ( ph -> A e. P )
9 oppcom.b
 |-  ( ph -> B e. P )
10 oppcom.o
 |-  ( ph -> A O B )
11 1 2 3 4 8 9 islnopp
 |-  ( ph -> ( A O B <-> ( ( -. A e. D /\ -. B e. D ) /\ E. t e. D t e. ( A I B ) ) ) )
12 10 11 mpbid
 |-  ( ph -> ( ( -. A e. D /\ -. B e. D ) /\ E. t e. D t e. ( A I B ) ) )
13 12 simpld
 |-  ( ph -> ( -. A e. D /\ -. B e. D ) )
14 13 simprd
 |-  ( ph -> -. B e. D )
15 13 simpld
 |-  ( ph -> -. A e. D )
16 12 simprd
 |-  ( ph -> E. t e. D t e. ( A I B ) )
17 7 ad2antrr
 |-  ( ( ( ph /\ t e. D ) /\ t e. ( A I B ) ) -> G e. TarskiG )
18 8 ad2antrr
 |-  ( ( ( ph /\ t e. D ) /\ t e. ( A I B ) ) -> A e. P )
19 7 adantr
 |-  ( ( ph /\ t e. D ) -> G e. TarskiG )
20 6 adantr
 |-  ( ( ph /\ t e. D ) -> D e. ran L )
21 simpr
 |-  ( ( ph /\ t e. D ) -> t e. D )
22 1 5 3 19 20 21 tglnpt
 |-  ( ( ph /\ t e. D ) -> t e. P )
23 22 adantr
 |-  ( ( ( ph /\ t e. D ) /\ t e. ( A I B ) ) -> t e. P )
24 9 ad2antrr
 |-  ( ( ( ph /\ t e. D ) /\ t e. ( A I B ) ) -> B e. P )
25 simpr
 |-  ( ( ( ph /\ t e. D ) /\ t e. ( A I B ) ) -> t e. ( A I B ) )
26 1 2 3 17 18 23 24 25 tgbtwncom
 |-  ( ( ( ph /\ t e. D ) /\ t e. ( A I B ) ) -> t e. ( B I A ) )
27 7 ad2antrr
 |-  ( ( ( ph /\ t e. D ) /\ t e. ( B I A ) ) -> G e. TarskiG )
28 9 ad2antrr
 |-  ( ( ( ph /\ t e. D ) /\ t e. ( B I A ) ) -> B e. P )
29 22 adantr
 |-  ( ( ( ph /\ t e. D ) /\ t e. ( B I A ) ) -> t e. P )
30 8 ad2antrr
 |-  ( ( ( ph /\ t e. D ) /\ t e. ( B I A ) ) -> A e. P )
31 simpr
 |-  ( ( ( ph /\ t e. D ) /\ t e. ( B I A ) ) -> t e. ( B I A ) )
32 1 2 3 27 28 29 30 31 tgbtwncom
 |-  ( ( ( ph /\ t e. D ) /\ t e. ( B I A ) ) -> t e. ( A I B ) )
33 26 32 impbida
 |-  ( ( ph /\ t e. D ) -> ( t e. ( A I B ) <-> t e. ( B I A ) ) )
34 33 rexbidva
 |-  ( ph -> ( E. t e. D t e. ( A I B ) <-> E. t e. D t e. ( B I A ) ) )
35 16 34 mpbid
 |-  ( ph -> E. t e. D t e. ( B I A ) )
36 14 15 35 jca31
 |-  ( ph -> ( ( -. B e. D /\ -. A e. D ) /\ E. t e. D t e. ( B I A ) ) )
37 1 2 3 4 9 8 islnopp
 |-  ( ph -> ( B O A <-> ( ( -. B e. D /\ -. A e. D ) /\ E. t e. D t e. ( B I A ) ) ) )
38 36 37 mpbird
 |-  ( ph -> B O A )