Metamath Proof Explorer

Theorem tgbtwnconn3

Description: Inner connectivity law for betweenness. Theorem 5.3 of Schwabhauser p. 41. (Contributed by Thierry Arnoux, 17-May-2019)

Ref Expression
Hypotheses tgbtwnconn.p 
|- P = ( Base ` G )
tgbtwnconn.i 
|- I = ( Itv ` G )
tgbtwnconn.g 
|- ( ph -> G e. TarskiG )
tgbtwnconn.a 
|- ( ph -> A e. P )
tgbtwnconn.b 
|- ( ph -> B e. P )
tgbtwnconn.c 
|- ( ph -> C e. P )
tgbtwnconn.d 
|- ( ph -> D e. P )
tgbtwnconn3.1 
|- ( ph -> B e. ( A I D ) )
tgbtwnconn3.2 
|- ( ph -> C e. ( A I D ) )
Assertion tgbtwnconn3 
|- ( ph -> ( B e. ( A I C ) \/ C e. ( A I B ) ) )

Proof

Step Hyp Ref Expression
1 tgbtwnconn.p 
 |-  P = ( Base ` G )
2 tgbtwnconn.i 
 |-  I = ( Itv ` G )
3 tgbtwnconn.g 
 |-  ( ph -> G e. TarskiG )
4 tgbtwnconn.a 
 |-  ( ph -> A e. P )
5 tgbtwnconn.b 
 |-  ( ph -> B e. P )
6 tgbtwnconn.c 
 |-  ( ph -> C e. P )
7 tgbtwnconn.d 
 |-  ( ph -> D e. P )
8 tgbtwnconn3.1 
 |-  ( ph -> B e. ( A I D ) )
9 tgbtwnconn3.2 
 |-  ( ph -> C e. ( A I D ) )
10 eqid 
 |-  ( dist ` G ) = ( dist ` G )
11 3 adantr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> G e. TarskiG )
12 5 adantr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> B e. P )
13 4 adantr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> A e. P )
14 6 adantr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> C e. P )
15 simpr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> ( # ` P ) = 1 )
16 1 10 2 11 12 13 14 15 tgldim0itv 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> B e. ( A I C ) )
17 16 orcd 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> ( B e. ( A I C ) \/ C e. ( A I B ) ) )
18 3 ad3antrrr 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> G e. TarskiG )
19 simplr 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> p e. P )
20 4 ad3antrrr 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> A e. P )
21 5 ad3antrrr 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> B e. P )
22 6 ad3antrrr 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> C e. P )
23 simprr 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> A =/= p )
24 23 necomd 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> p =/= A )
25 7 ad3antrrr 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> D e. P )
26 8 ad3antrrr 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> B e. ( A I D ) )
27 simprl 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> A e. ( D I p ) )
28 1 10 2 18 25 20 19 27 tgbtwncom 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> A e. ( p I D ) )
29 1 10 2 18 21 20 19 25 26 28 tgbtwnintr 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> A e. ( B I p ) )
30 1 10 2 18 21 20 19 29 tgbtwncom 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> A e. ( p I B ) )
31 9 ad3antrrr 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> C e. ( A I D ) )
32 1 10 2 18 20 22 25 31 tgbtwncom 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> C e. ( D I A ) )
33 1 10 2 18 25 22 20 19 32 27 tgbtwnexch3 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> A e. ( C I p ) )
34 1 10 2 18 22 20 19 33 tgbtwncom 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> A e. ( p I C ) )
35 1 2 18 19 20 21 22 24 30 34 tgbtwnconn2 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> ( B e. ( A I C ) \/ C e. ( A I B ) ) )
36 3 adantr 
 |-  ( ( ph /\ 2 <_ ( # ` P ) ) -> G e. TarskiG )
37 7 adantr 
 |-  ( ( ph /\ 2 <_ ( # ` P ) ) -> D e. P )
38 4 adantr 
 |-  ( ( ph /\ 2 <_ ( # ` P ) ) -> A e. P )
39 simpr 
 |-  ( ( ph /\ 2 <_ ( # ` P ) ) -> 2 <_ ( # ` P ) )
40 1 10 2 36 37 38 39 tgbtwndiff 
 |-  ( ( ph /\ 2 <_ ( # ` P ) ) -> E. p e. P ( A e. ( D I p ) /\ A =/= p ) )
41 35 40 r19.29a 
 |-  ( ( ph /\ 2 <_ ( # ` P ) ) -> ( B e. ( A I C ) \/ C e. ( A I B ) ) )
42 1 4 tgldimor 
 |-  ( ph -> ( ( # ` P ) = 1 \/ 2 <_ ( # ` P ) ) )
43 17 41 42 mpjaodan 
 |-  ( ph -> ( B e. ( A I C ) \/ C e. ( A I B ) ) )