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	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ) → 𝑃 ∈ ( 𝑃 Line 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		simpr1	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
2		colineartriv1	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑃 Colinear ⟨ 𝑃 , 𝑄 ⟩ )
3	2	3adant3r3	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ) → 𝑃 Colinear ⟨ 𝑃 , 𝑄 ⟩ )
4		breq1	⊢ ( 𝑥 = 𝑃 → ( 𝑥 Colinear ⟨ 𝑃 , 𝑄 ⟩ ↔ 𝑃 Colinear ⟨ 𝑃 , 𝑄 ⟩ ) )
5	4	elrab	⊢ ( 𝑃 ∈ { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑥 Colinear ⟨ 𝑃 , 𝑄 ⟩ } ↔ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 Colinear ⟨ 𝑃 , 𝑄 ⟩ ) )
6	1 3 5	sylanbrc	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ) → 𝑃 ∈ { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑥 Colinear ⟨ 𝑃 , 𝑄 ⟩ } )
7		fvline2	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ) → ( 𝑃 Line 𝑄 ) = { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑥 Colinear ⟨ 𝑃 , 𝑄 ⟩ } )
8	6 7	eleqtrrd	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ) → 𝑃 ∈ ( 𝑃 Line 𝑄 ) )