Metamath Proof Explorer

Theorem linerflx1

Description: Reflexivity law for line membership. Part of theorem 6.17 of Schwabhauser p. 45. (Contributed by Scott Fenton, 28-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion linerflx1 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ P ≠ Q → P ∈ P Line Q

Proof

Step Hyp Ref Expression
1 simpr1 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ P ≠ Q → P ∈ 𝔼 ⁡ N
2 colineartriv1 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N → P Colinear P Q
3 2 3adant3r3 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ P ≠ Q → P Colinear P Q
4 breq1 ⊢ x = P → x Colinear P Q ↔ P Colinear P Q
5 4 elrab ⊢ P ∈ x ∈ 𝔼 ⁡ N | x Colinear P Q ↔ P ∈ 𝔼 ⁡ N ∧ P Colinear P Q
6 1 3 5 sylanbrc ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ P ≠ Q → P ∈ x ∈ 𝔼 ⁡ N | x Colinear P Q
7 fvline2 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ P ≠ Q → P Line Q = x ∈ 𝔼 ⁡ N | x Colinear P Q
8 6 7 eleqtrrd ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ P ≠ Q → P ∈ P Line Q