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 \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to P \in (P Line Q)$

Proof

Step	Hyp	Ref	Expression
1		simpr1	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to P \in 𝔼 (N)$
2		colineartriv1	$⊢ (N \in ℕ \land P \in 𝔼 (N) \land Q \in 𝔼 (N)) \to P Colinear ⟨P, Q⟩$
3	2	3adant3r3	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to P Colinear ⟨P, Q⟩$
4		breq1	$⊢ x = P \to (x Colinear ⟨P, Q⟩ \leftrightarrow P Colinear ⟨P, Q⟩)$
5	4	elrab	$⊢ P \in \{x \in 𝔼 (N) \| x Colinear ⟨P, Q⟩\} \leftrightarrow (P \in 𝔼 (N) \land P Colinear ⟨P, Q⟩)$
6	1 3 5	sylanbrc	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to P \in \{x \in 𝔼 (N) \| x Colinear ⟨P, Q⟩\}$
7		fvline2	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to P Line Q = \{x \in 𝔼 (N) \| x Colinear ⟨P, Q⟩\}$
8	6 7	eleqtrrd	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to P \in (P Line Q)$