Theorem linerflx2

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

Proof

Step	Hyp	Ref	Expression
1		necom	⊢ ( 𝑃 ≠ 𝑄 ↔ 𝑄 ≠ 𝑃 )
2	1	3anbi3i	⊢ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ↔ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ≠ 𝑃 ) )
3		3ancoma	⊢ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ≠ 𝑃 ) ↔ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ≠ 𝑃 ) )
4	2 3	bitri	⊢ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ↔ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ≠ 𝑃 ) )
5		linerflx1	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ≠ 𝑃 ) ) → 𝑄 ∈ ( 𝑄 Line 𝑃 ) )
6	4 5	sylan2b	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ) → 𝑄 ∈ ( 𝑄 Line 𝑃 ) )
7		linecom	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ) → ( 𝑃 Line 𝑄 ) = ( 𝑄 Line 𝑃 ) )
8	6 7	eleqtrrd	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ) → 𝑄 ∈ ( 𝑃 Line 𝑄 ) )