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