Metamath Proof Explorer

Theorem tgbtwnconn2

Description: Another connectivity law for betweenness. Theorem 5.2 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 )
tgbtwnconn2.1 
|- ( ph -> A =/= B )
tgbtwnconn2.2 
|- ( ph -> B e. ( A I C ) )
tgbtwnconn2.3 
|- ( ph -> B e. ( A I D ) )
Assertion tgbtwnconn2 
|- ( ph -> ( C e. ( B I D ) \/ D e. ( B I C ) ) )

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 tgbtwnconn2.1 
 |-  ( ph -> A =/= B )
9 tgbtwnconn2.2 
 |-  ( ph -> B e. ( A I C ) )
10 tgbtwnconn2.3 
 |-  ( ph -> B e. ( A I D ) )
11 eqid 
 |-  ( dist ` G ) = ( dist ` G )
12 3 adantr 
 |-  ( ( ph /\ C e. ( A I D ) ) -> G e. TarskiG )
13 4 adantr 
 |-  ( ( ph /\ C e. ( A I D ) ) -> A e. P )
14 5 adantr 
 |-  ( ( ph /\ C e. ( A I D ) ) -> B e. P )
15 6 adantr 
 |-  ( ( ph /\ C e. ( A I D ) ) -> C e. P )
16 7 adantr 
 |-  ( ( ph /\ C e. ( A I D ) ) -> D e. P )
17 9 adantr 
 |-  ( ( ph /\ C e. ( A I D ) ) -> B e. ( A I C ) )
18 simpr 
 |-  ( ( ph /\ C e. ( A I D ) ) -> C e. ( A I D ) )
19 1 11 2 12 13 14 15 16 17 18 tgbtwnexch3 
 |-  ( ( ph /\ C e. ( A I D ) ) -> C e. ( B I D ) )
20 19 orcd 
 |-  ( ( ph /\ C e. ( A I D ) ) -> ( C e. ( B I D ) \/ D e. ( B I C ) ) )
21 3 adantr 
 |-  ( ( ph /\ D e. ( A I C ) ) -> G e. TarskiG )
22 4 adantr 
 |-  ( ( ph /\ D e. ( A I C ) ) -> A e. P )
23 5 adantr 
 |-  ( ( ph /\ D e. ( A I C ) ) -> B e. P )
24 7 adantr 
 |-  ( ( ph /\ D e. ( A I C ) ) -> D e. P )
25 6 adantr 
 |-  ( ( ph /\ D e. ( A I C ) ) -> C e. P )
26 10 adantr 
 |-  ( ( ph /\ D e. ( A I C ) ) -> B e. ( A I D ) )
27 simpr 
 |-  ( ( ph /\ D e. ( A I C ) ) -> D e. ( A I C ) )
28 1 11 2 21 22 23 24 25 26 27 tgbtwnexch3 
 |-  ( ( ph /\ D e. ( A I C ) ) -> D e. ( B I C ) )
29 28 olcd 
 |-  ( ( ph /\ D e. ( A I C ) ) -> ( C e. ( B I D ) \/ D e. ( B I C ) ) )
30 1 2 3 4 5 6 7 8 9 10 tgbtwnconn1 
 |-  ( ph -> ( C e. ( A I D ) \/ D e. ( A I C ) ) )
31 20 29 30 mpjaodan 
 |-  ( ph -> ( C e. ( B I D ) \/ D e. ( B I C ) ) )