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 )