Metamath Proof Explorer


Theorem tgbtwnouttr

Description: Outer transitivity law for betweenness. Right-hand side of Theorem 3.7 of Schwabhauser p. 30. (Contributed by Thierry Arnoux, 23-Mar-2019)

Ref Expression
Hypotheses tkgeom.p 𝑃 = ( Base ‘ 𝐺 )
tkgeom.d = ( dist ‘ 𝐺 )
tkgeom.i 𝐼 = ( Itv ‘ 𝐺 )
tkgeom.g ( 𝜑𝐺 ∈ TarskiG )
tgbtwnintr.1 ( 𝜑𝐴𝑃 )
tgbtwnintr.2 ( 𝜑𝐵𝑃 )
tgbtwnintr.3 ( 𝜑𝐶𝑃 )
tgbtwnintr.4 ( 𝜑𝐷𝑃 )
tgbtwnouttr.1 ( 𝜑𝐵𝐶 )
tgbtwnouttr.2 ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
tgbtwnouttr.3 ( 𝜑𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )
Assertion tgbtwnouttr ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐷 ) )

Proof

Step Hyp Ref Expression
1 tkgeom.p 𝑃 = ( Base ‘ 𝐺 )
2 tkgeom.d = ( dist ‘ 𝐺 )
3 tkgeom.i 𝐼 = ( Itv ‘ 𝐺 )
4 tkgeom.g ( 𝜑𝐺 ∈ TarskiG )
5 tgbtwnintr.1 ( 𝜑𝐴𝑃 )
6 tgbtwnintr.2 ( 𝜑𝐵𝑃 )
7 tgbtwnintr.3 ( 𝜑𝐶𝑃 )
8 tgbtwnintr.4 ( 𝜑𝐷𝑃 )
9 tgbtwnouttr.1 ( 𝜑𝐵𝐶 )
10 tgbtwnouttr.2 ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
11 tgbtwnouttr.3 ( 𝜑𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )
12 9 necomd ( 𝜑𝐶𝐵 )
13 1 2 3 4 6 7 8 11 tgbtwncom ( 𝜑𝐶 ∈ ( 𝐷 𝐼 𝐵 ) )
14 1 2 3 4 5 6 7 10 tgbtwncom ( 𝜑𝐵 ∈ ( 𝐶 𝐼 𝐴 ) )
15 1 2 3 4 8 7 6 5 12 13 14 tgbtwnouttr2 ( 𝜑𝐵 ∈ ( 𝐷 𝐼 𝐴 ) )
16 1 2 3 4 8 6 5 15 tgbtwncom ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐷 ) )