Database
ELEMENTARY GEOMETRY
Tarskian Geometry
Congruence
tgbtwnexch3
Metamath Proof Explorer
Description: Exchange the first endpoint in betweenness. Left-hand side of Theorem
3.6 of Schwabhauser p. 30. (Contributed by Thierry Arnoux , 18-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
⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
tgbtwnexch3.5
⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
tgbtwnexch3.6
⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 𝐷 ) )
Assertion
tgbtwnexch3
⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )
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
tgbtwnexch3.5
⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
10
tgbtwnexch3.6
⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 𝐷 ) )
11
1 2 3 4 5 6 7 9
tgbtwncom
⊢ ( 𝜑 → 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) )
12
1 2 3 4 5 7 8 10
tgbtwncom
⊢ ( 𝜑 → 𝐶 ∈ ( 𝐷 𝐼 𝐴 ) )
13
1 2 3 4 6 7 8 5 11 12
tgbtwnintr
⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )