Metamath Proof Explorer

Theorem btwnouttr

Description: Outer transitivity law for betweenness. Right-hand side of Theorem 3.7 of Schwabhauser p. 30. (Contributed by Scott Fenton, 14-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
2 simp2r ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
3 simp3r ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
4 simp2l ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
5 necom ⊢ ( 𝐵 ≠ 𝐶 ↔ 𝐶 ≠ 𝐵 )
6 5 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 ≠ 𝐶 ↔ 𝐶 ≠ 𝐵 ) )
7 simp3l ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
8 btwncom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ↔ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ) )
9 1 2 4 7 8 syl13anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ↔ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ) )
10 btwncom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ↔ 𝐶 Btwn ⟨ 𝐷 , 𝐵 ⟩ ) )
11 1 7 2 3 10 syl13anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ↔ 𝐶 Btwn ⟨ 𝐷 , 𝐵 ⟩ ) )
12 6 9 11 3anbi123d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ↔ ( 𝐶 ≠ 𝐵 ∧ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∧ 𝐶 Btwn ⟨ 𝐷 , 𝐵 ⟩ ) ) )
13 3ancomb ⊢ ( ( 𝐶 ≠ 𝐵 ∧ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∧ 𝐶 Btwn ⟨ 𝐷 , 𝐵 ⟩ ) ↔ ( 𝐶 ≠ 𝐵 ∧ 𝐶 Btwn ⟨ 𝐷 , 𝐵 ⟩ ∧ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ) )
14 12 13 bitrdi ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ↔ ( 𝐶 ≠ 𝐵 ∧ 𝐶 Btwn ⟨ 𝐷 , 𝐵 ⟩ ∧ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ) ) )
15 14 biimpa ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ) → ( 𝐶 ≠ 𝐵 ∧ 𝐶 Btwn ⟨ 𝐷 , 𝐵 ⟩ ∧ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ) )
16 btwnouttr2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 ≠ 𝐵 ∧ 𝐶 Btwn ⟨ 𝐷 , 𝐵 ⟩ ∧ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ) → 𝐵 Btwn ⟨ 𝐷 , 𝐴 ⟩ ) )
17 1 3 7 2 4 16 syl122anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 ≠ 𝐵 ∧ 𝐶 Btwn ⟨ 𝐷 , 𝐵 ⟩ ∧ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ) → 𝐵 Btwn ⟨ 𝐷 , 𝐴 ⟩ ) )
18 17 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ) → ( ( 𝐶 ≠ 𝐵 ∧ 𝐶 Btwn ⟨ 𝐷 , 𝐵 ⟩ ∧ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ) → 𝐵 Btwn ⟨ 𝐷 , 𝐴 ⟩ ) )
19 15 18 mpd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ) → 𝐵 Btwn ⟨ 𝐷 , 𝐴 ⟩ )
20 1 2 3 4 19 btwncomand ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ) → 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ )
21 20 ex ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) )