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	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝐴 Line 𝐵 ) = { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑥 Colinear ⟨ 𝐴 , 𝐵 ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		fvline	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝐴 Line 𝐵 ) = { 𝑥 ∣ 𝑥 Colinear ⟨ 𝐴 , 𝐵 ⟩ } )
2		liness	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝐴 Line 𝐵 ) ⊆ ( 𝔼 ‘ 𝑁 ) )
3	1 2	eqsstrrd	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ) → { 𝑥 ∣ 𝑥 Colinear ⟨ 𝐴 , 𝐵 ⟩ } ⊆ ( 𝔼 ‘ 𝑁 ) )
4		df-ss	⊢ ( { 𝑥 ∣ 𝑥 Colinear ⟨ 𝐴 , 𝐵 ⟩ } ⊆ ( 𝔼 ‘ 𝑁 ) ↔ ( { 𝑥 ∣ 𝑥 Colinear ⟨ 𝐴 , 𝐵 ⟩ } ∩ ( 𝔼 ‘ 𝑁 ) ) = { 𝑥 ∣ 𝑥 Colinear ⟨ 𝐴 , 𝐵 ⟩ } )
5	3 4	sylib	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ) → ( { 𝑥 ∣ 𝑥 Colinear ⟨ 𝐴 , 𝐵 ⟩ } ∩ ( 𝔼 ‘ 𝑁 ) ) = { 𝑥 ∣ 𝑥 Colinear ⟨ 𝐴 , 𝐵 ⟩ } )
6	1 5	eqtr4d	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝐴 Line 𝐵 ) = ( { 𝑥 ∣ 𝑥 Colinear ⟨ 𝐴 , 𝐵 ⟩ } ∩ ( 𝔼 ‘ 𝑁 ) ) )
7		dfrab2	⊢ { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑥 Colinear ⟨ 𝐴 , 𝐵 ⟩ } = ( { 𝑥 ∣ 𝑥 Colinear ⟨ 𝐴 , 𝐵 ⟩ } ∩ ( 𝔼 ‘ 𝑁 ) )
8	6 7	eqtr4di	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝐴 Line 𝐵 ) = { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑥 Colinear ⟨ 𝐴 , 𝐵 ⟩ } )