Metamath Proof Explorer


Theorem tgbtwnexch

Description: Outer transitivity law for betweenness. Right-hand side of Theorem 3.6 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 ( 𝜑𝐷𝑃 )
tgbtwnexch.1 ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
tgbtwnexch.2 ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐷 ) )
Assertion tgbtwnexch ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐷 ) )

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 tgbtwnexch.1 ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
10 tgbtwnexch.2 ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐷 ) )
11 1 2 3 4 5 7 8 10 tgbtwncom ( 𝜑𝐶 ∈ ( 𝐷 𝐼 𝐴 ) )
12 1 2 3 4 5 6 7 9 tgbtwncom ( 𝜑𝐵 ∈ ( 𝐶 𝐼 𝐴 ) )
13 1 2 3 4 8 7 6 5 11 12 tgbtwnexch2 ( 𝜑𝐵 ∈ ( 𝐷 𝐼 𝐴 ) )
14 1 2 3 4 8 6 5 13 tgbtwncom ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐷 ) )