Metamath Proof Explorer

Theorem tgbtwnouttr2

Description: Outer transitivity law for betweenness. Left-hand side of Theorem 3.7 of Schwabhauser p. 30. (Contributed by Thierry Arnoux, 18-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 )
tgbtwnouttr2.1 
|- ( ph -> B =/= C )
tgbtwnouttr2.2 
|- ( ph -> B e. ( A I C ) )
tgbtwnouttr2.3 
|- ( ph -> C e. ( B I D ) )
Assertion tgbtwnouttr2 
|- ( 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 tgbtwnouttr2.1 
 |-  ( ph -> B =/= C )
10 tgbtwnouttr2.2 
 |-  ( ph -> B e. ( A I C ) )
11 tgbtwnouttr2.3 
 |-  ( ph -> C e. ( B I D ) )
12 simprl 
 |-  ( ( ( ph /\ x e. P ) /\ ( C e. ( A I x ) /\ ( C .- x ) = ( C .- D ) ) ) -> C e. ( A I x ) )
13 4 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ ( C e. ( A I x ) /\ ( C .- x ) = ( C .- D ) ) ) -> G e. TarskiG )
14 7 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ ( C e. ( A I x ) /\ ( C .- x ) = ( C .- D ) ) ) -> C e. P )
15 8 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ ( C e. ( A I x ) /\ ( C .- x ) = ( C .- D ) ) ) -> D e. P )
16 6 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ ( C e. ( A I x ) /\ ( C .- x ) = ( C .- D ) ) ) -> B e. P )
17 simplr 
 |-  ( ( ( ph /\ x e. P ) /\ ( C e. ( A I x ) /\ ( C .- x ) = ( C .- D ) ) ) -> x e. P )
18 9 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ ( C e. ( A I x ) /\ ( C .- x ) = ( C .- D ) ) ) -> B =/= C )
19 5 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ ( C e. ( A I x ) /\ ( C .- x ) = ( C .- D ) ) ) -> A e. P )
20 10 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ ( C e. ( A I x ) /\ ( C .- x ) = ( C .- D ) ) ) -> B e. ( A I C ) )
21 1 2 3 13 19 16 14 17 20 12 tgbtwnexch3 
 |-  ( ( ( ph /\ x e. P ) /\ ( C e. ( A I x ) /\ ( C .- x ) = ( C .- D ) ) ) -> C e. ( B I x ) )
22 11 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ ( C e. ( A I x ) /\ ( C .- x ) = ( C .- D ) ) ) -> C e. ( B I D ) )
23 simprr 
 |-  ( ( ( ph /\ x e. P ) /\ ( C e. ( A I x ) /\ ( C .- x ) = ( C .- D ) ) ) -> ( C .- x ) = ( C .- D ) )
24 eqidd 
 |-  ( ( ( ph /\ x e. P ) /\ ( C e. ( A I x ) /\ ( C .- x ) = ( C .- D ) ) ) -> ( C .- D ) = ( C .- D ) )
25 1 2 3 13 14 14 15 16 17 15 18 21 22 23 24 tgsegconeq 
 |-  ( ( ( ph /\ x e. P ) /\ ( C e. ( A I x ) /\ ( C .- x ) = ( C .- D ) ) ) -> x = D )
26 25 oveq2d 
 |-  ( ( ( ph /\ x e. P ) /\ ( C e. ( A I x ) /\ ( C .- x ) = ( C .- D ) ) ) -> ( A I x ) = ( A I D ) )
27 12 26 eleqtrd 
 |-  ( ( ( ph /\ x e. P ) /\ ( C e. ( A I x ) /\ ( C .- x ) = ( C .- D ) ) ) -> C e. ( A I D ) )
28 1 2 3 4 5 7 7 8 axtgsegcon 
 |-  ( ph -> E. x e. P ( C e. ( A I x ) /\ ( C .- x ) = ( C .- D ) ) )
29 27 28 r19.29a 
 |-  ( ph -> C e. ( A I D ) )