Metamath Proof Explorer

Theorem liness

Description: A line is a subset of the space its two points lie in. (Contributed by Scott Fenton, 25-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion liness ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → A Line B ⊆ 𝔼 ⁡ N

Proof

Step Hyp Ref Expression
1 fvline ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → A Line B = x | x Colinear A B
2 vex ⊢ x ∈ V
3 2 a1i ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → x ∈ V
4 simp1 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → A ∈ 𝔼 ⁡ N
5 simp2 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → B ∈ 𝔼 ⁡ N
6 3 4 5 3jca ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → x ∈ V ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N
7 colineardim1 ⊢ N ∈ ℕ ∧ x ∈ V ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → x Colinear A B → x ∈ 𝔼 ⁡ N
8 6 7 sylan2 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → x Colinear A B → x ∈ 𝔼 ⁡ N
9 8 abssdv ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → x | x Colinear A B ⊆ 𝔼 ⁡ N
10 1 9 eqsstrd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → A Line B ⊆ 𝔼 ⁡ N