Database
ELEMENTARY GEOMETRY
Tarskian Geometry
Congruence
tgbtwnexch
Metamath Proof Explorer
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
⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐷 ) )