Metamath Proof Explorer

Theorem liness

Description: A line is a subset of the space its two points lie in. (Contributed by Scott Fenton, 25-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	liness	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B)) \to A Line B \subseteq 𝔼 (N)$

Proof

Step	Hyp	Ref	Expression
1		fvline	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B)) \to A Line B = \{x \| x Colinear ⟨A, B⟩\}$
2		vex	$⊢ x \in V$
3	2	a1i	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B) \to x \in V$
4		simp1	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B) \to A \in 𝔼 (N)$
5		simp2	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B) \to B \in 𝔼 (N)$
6	3 4 5	3jca	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B) \to (x \in V \land A \in 𝔼 (N) \land B \in 𝔼 (N))$
7		colineardim1	$⊢ (N \in ℕ \land (x \in V \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \to (x Colinear ⟨A, B⟩ \to x \in 𝔼 (N))$
8	6 7	sylan2	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B)) \to (x Colinear ⟨A, B⟩ \to x \in 𝔼 (N))$
9	8	abssdv	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B)) \to \{x \| x Colinear ⟨A, B⟩\} \subseteq 𝔼 (N)$
10	1 9	eqsstrd	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B)) \to A Line B \subseteq 𝔼 (N)$