Metamath Proof Explorer


Theorem tgbtwnexch2

Description: Exchange the outer point of two betweenness statements. Right-hand side of Theorem 3.5 of Schwabhauser p. 30. (Contributed by Thierry Arnoux, 23-Mar-2019)

Ref Expression
Hypotheses tkgeom.p
|- P = ( Base ` G )
tkgeom.d
|- .- = ( dist ` G )
tkgeom.i
|- I = ( Itv ` G )
tkgeom.g
|- ( ph -> G e. TarskiG )
tgbtwnintr.1
|- ( ph -> A e. P )
tgbtwnintr.2
|- ( ph -> B e. P )
tgbtwnintr.3
|- ( ph -> C e. P )
tgbtwnintr.4
|- ( ph -> D e. P )
tgbtwnexch2.1
|- ( ph -> B e. ( A I D ) )
tgbtwnexch2.2
|- ( ph -> C e. ( B I D ) )
Assertion tgbtwnexch2
|- ( ph -> C e. ( A I D ) )

Proof

Step Hyp Ref Expression
1 tkgeom.p
 |-  P = ( Base ` G )
2 tkgeom.d
 |-  .- = ( dist ` G )
3 tkgeom.i
 |-  I = ( Itv ` G )
4 tkgeom.g
 |-  ( ph -> G e. TarskiG )
5 tgbtwnintr.1
 |-  ( ph -> A e. P )
6 tgbtwnintr.2
 |-  ( ph -> B e. P )
7 tgbtwnintr.3
 |-  ( ph -> C e. P )
8 tgbtwnintr.4
 |-  ( ph -> D e. P )
9 tgbtwnexch2.1
 |-  ( ph -> B e. ( A I D ) )
10 tgbtwnexch2.2
 |-  ( ph -> C e. ( B I D ) )
11 simpr
 |-  ( ( ph /\ B = C ) -> B = C )
12 9 adantr
 |-  ( ( ph /\ B = C ) -> B e. ( A I D ) )
13 11 12 eqeltrrd
 |-  ( ( ph /\ B = C ) -> C e. ( A I D ) )
14 4 adantr
 |-  ( ( ph /\ B =/= C ) -> G e. TarskiG )
15 5 adantr
 |-  ( ( ph /\ B =/= C ) -> A e. P )
16 6 adantr
 |-  ( ( ph /\ B =/= C ) -> B e. P )
17 7 adantr
 |-  ( ( ph /\ B =/= C ) -> C e. P )
18 8 adantr
 |-  ( ( ph /\ B =/= C ) -> D e. P )
19 simpr
 |-  ( ( ph /\ B =/= C ) -> B =/= C )
20 10 adantr
 |-  ( ( ph /\ B =/= C ) -> C e. ( B I D ) )
21 9 adantr
 |-  ( ( ph /\ B =/= C ) -> B e. ( A I D ) )
22 1 2 3 14 17 16 15 18 20 21 tgbtwnintr
 |-  ( ( ph /\ B =/= C ) -> B e. ( C I A ) )
23 1 2 3 14 17 16 15 22 tgbtwncom
 |-  ( ( ph /\ B =/= C ) -> B e. ( A I C ) )
24 1 2 3 14 15 16 17 18 19 23 20 tgbtwnouttr2
 |-  ( ( ph /\ B =/= C ) -> C e. ( A I D ) )
25 13 24 pm2.61dane
 |-  ( ph -> C e. ( A I D ) )