Metamath Proof Explorer

Theorem tgbtwnexch2

Description: Exchange the outer point of two betweenness statements. Right-hand side of Theorem 3.5 of Schwabhauser p. 30. (Contributed by Thierry Arnoux, 23-Mar-2019)

Ref Expression
Hypotheses tkgeom.p ⊢ P = Base G
tkgeom.d ⊢ - ˙ = dist ⁡ G
tkgeom.i ⊢ I = Itv ⁡ G
tkgeom.g ⊢ φ → G ∈ 𝒢 Tarski
tgbtwnintr.1 ⊢ φ → A ∈ P
tgbtwnintr.2 ⊢ φ → B ∈ P
tgbtwnintr.3 ⊢ φ → C ∈ P
tgbtwnintr.4 ⊢ φ → D ∈ P
tgbtwnexch2.1 ⊢ φ → B ∈ A I D
tgbtwnexch2.2 ⊢ φ → C ∈ B I D
Assertion tgbtwnexch2 ⊢ φ → C ∈ A I D

Proof

Step Hyp Ref Expression
1 tkgeom.p ⊢ P = Base G
2 tkgeom.d ⊢ - ˙ = dist ⁡ G
3 tkgeom.i ⊢ I = Itv ⁡ G
4 tkgeom.g ⊢ φ → G ∈ 𝒢 Tarski
5 tgbtwnintr.1 ⊢ φ → A ∈ P
6 tgbtwnintr.2 ⊢ φ → B ∈ P
7 tgbtwnintr.3 ⊢ φ → C ∈ P
8 tgbtwnintr.4 ⊢ φ → D ∈ P
9 tgbtwnexch2.1 ⊢ φ → B ∈ A I D
10 tgbtwnexch2.2 ⊢ φ → C ∈ B I D
11 simpr ⊢ φ ∧ B = C → B = C
12 9 adantr ⊢ φ ∧ B = C → B ∈ A I D
13 11 12 eqeltrrd ⊢ φ ∧ B = C → C ∈ A I D
14 4 adantr ⊢ φ ∧ B ≠ C → G ∈ 𝒢 Tarski
15 5 adantr ⊢ φ ∧ B ≠ C → A ∈ P
16 6 adantr ⊢ φ ∧ B ≠ C → B ∈ P
17 7 adantr ⊢ φ ∧ B ≠ C → C ∈ P
18 8 adantr ⊢ φ ∧ B ≠ C → D ∈ P
19 simpr ⊢ φ ∧ B ≠ C → B ≠ C
20 10 adantr ⊢ φ ∧ B ≠ C → C ∈ B I D
21 9 adantr ⊢ φ ∧ B ≠ C → B ∈ A I D
22 1 2 3 14 17 16 15 18 20 21 tgbtwnintr ⊢ φ ∧ B ≠ C → B ∈ C I A
23 1 2 3 14 17 16 15 22 tgbtwncom ⊢ φ ∧ B ≠ C → B ∈ A I C
24 1 2 3 14 15 16 17 18 19 23 20 tgbtwnouttr2 ⊢ φ ∧ B ≠ C → C ∈ A I D
25 13 24 pm2.61dane ⊢ φ → C ∈ A I D