Metamath Proof Explorer

Theorem fvline2

Description: Alternate definition of a line. (Contributed by Scott Fenton, 25-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion fvline2 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → A Line B = x ∈ 𝔼 ⁡ N | x Colinear A B

Proof

Step Hyp Ref Expression
1 fvline ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → A Line B = x | x Colinear A B
2 liness ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → A Line B ⊆ 𝔼 ⁡ N
3 1 2 eqsstrrd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → x | x Colinear A B ⊆ 𝔼 ⁡ N
4 dfss2 ⊢ x | x Colinear A B ⊆ 𝔼 ⁡ N ↔ x | x Colinear A B ∩ 𝔼 ⁡ N = x | x Colinear A B
5 3 4 sylib ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → x | x Colinear A B ∩ 𝔼 ⁡ N = x | x Colinear A B
6 1 5 eqtr4d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → A Line B = x | x Colinear A B ∩ 𝔼 ⁡ N
7 dfrab2 ⊢ x ∈ 𝔼 ⁡ N | x Colinear A B = x | x Colinear A B ∩ 𝔼 ⁡ N
8 6 7 eqtr4di ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → A Line B = x ∈ 𝔼 ⁡ N | x Colinear A B