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 ) ) )