Metamath Proof Explorer

Theorem btwnexch3

Description: Exchange the first endpoint in betweenness. Left-hand side of Theorem 3.6 of Schwabhauser p. 30. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion btwnexch3 ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) → 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
2 simp3l ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
3 simp2l ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
4 simp3r ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
5 btwncom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ↔ 𝐶 Btwn ⟨ 𝐷 , 𝐴 ⟩ ) )
6 1 2 3 4 5 syl13anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ↔ 𝐶 Btwn ⟨ 𝐷 , 𝐴 ⟩ ) )
7 simp2r ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
8 btwncom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ↔ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ) )
9 1 7 3 2 8 syl13anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ↔ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ) )
10 6 9 anbi12d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) ↔ ( 𝐶 Btwn ⟨ 𝐷 , 𝐴 ⟩ ∧ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ) ) )
11 axpasch ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 Btwn ⟨ 𝐷 , 𝐴 ⟩ ∧ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑥 Btwn ⟨ 𝐶 , 𝐶 ⟩ ∧ 𝑥 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ) )
12 1 4 2 3 2 7 11 syl132anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 Btwn ⟨ 𝐷 , 𝐴 ⟩ ∧ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑥 Btwn ⟨ 𝐶 , 𝐶 ⟩ ∧ 𝑥 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ) )
13 10 12 sylbid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑥 Btwn ⟨ 𝐶 , 𝐶 ⟩ ∧ 𝑥 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ) )
14 13 ancomsd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑥 Btwn ⟨ 𝐶 , 𝐶 ⟩ ∧ 𝑥 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ) )
15 simpl1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
16 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) )
17 simpl3l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
18 axbtwnid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑥 Btwn ⟨ 𝐶 , 𝐶 ⟩ → 𝑥 = 𝐶 ) )
19 15 16 17 18 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑥 Btwn ⟨ 𝐶 , 𝐶 ⟩ → 𝑥 = 𝐶 ) )
20 breq1 ⊢ ( 𝑥 = 𝐶 → ( 𝑥 Btwn ⟨ 𝐵 , 𝐷 ⟩ ↔ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) )
21 20 biimpd ⊢ ( 𝑥 = 𝐶 → ( 𝑥 Btwn ⟨ 𝐵 , 𝐷 ⟩ → 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) )
22 19 21 syl6 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑥 Btwn ⟨ 𝐶 , 𝐶 ⟩ → ( 𝑥 Btwn ⟨ 𝐵 , 𝐷 ⟩ → 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ) )
23 22 impd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑥 Btwn ⟨ 𝐶 , 𝐶 ⟩ ∧ 𝑥 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) )
24 23 rexlimdva ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑥 Btwn ⟨ 𝐶 , 𝐶 ⟩ ∧ 𝑥 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) )
25 14 24 syld ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) → 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) )