rrx2linesl

Description: The line passing through the two different points X and Y in a real Euclidean space of dimension 2, expressed by the slope S between the two points ("point-slope form"), sometimes also written as ( ( p1 ) - ( X1 ) ) = ( S x. ( ( p0 ) - ( X0 ) ) ) . (Contributed by AV, 22-Jan-2023)

	Ref	Expression
Hypotheses	rrx2line.i	$⊢ I = (0 ..^2)$
	rrx2line.e	$⊢ E = I$
	rrx2line.b	$⊢ P = ℝ^{I}$
	rrx2line.l	$⊢ L = {Line}_{M} (E)$
	rrx2linesl.s	$⊢ S = \frac{Y (1) - X (1)}{Y (0) - X (0)}$
Assertion	rrx2linesl	$⊢ (X \in P \land Y \in P \land X (0) \neq Y (0)) \to X L Y = \{p \in P \| p (1) = S (p (0) - X (0)) + X (1)\}$

Proof

Step	Hyp	Ref	Expression
1		rrx2line.i	$⊢ I = (0 ..^2)$
2		rrx2line.e	$⊢ E = I$
3		rrx2line.b	$⊢ P = ℝ^{I}$
4		rrx2line.l	$⊢ L = {Line}_{M} (E)$
5		rrx2linesl.s	$⊢ S = \frac{Y (1) - X (1)}{Y (0) - X (0)}$
6		fveq1	$⊢ X = Y \to X (0) = Y (0)$
7	6	necon3i	$⊢ X (0) \neq Y (0) \to X \neq Y$
8	1 2 3 4	rrx2line	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X L Y = \{p \in P \| \exists t \in ℝ (p (0) = (1 - t) X (0) + t Y (0) \land p (1) = (1 - t) X (1) + t Y (1))\}$
9	7 8	syl3an3	$⊢ (X \in P \land Y \in P \land X (0) \neq Y (0)) \to X L Y = \{p \in P \| \exists t \in ℝ (p (0) = (1 - t) X (0) + t Y (0) \land p (1) = (1 - t) X (1) + t Y (1))\}$
10	1 3	rrx2pxel	$⊢ p \in P \to p (0) \in ℝ$
11	10	adantl	$⊢ ((X \in P \land Y \in P \land X (0) \neq Y (0)) \land p \in P) \to p (0) \in ℝ$
12	1 3	rrx2pxel	$⊢ X \in P \to X (0) \in ℝ$
13	12	3ad2ant1	$⊢ (X \in P \land Y \in P \land X (0) \neq Y (0)) \to X (0) \in ℝ$
14	13	adantr	$⊢ ((X \in P \land Y \in P \land X (0) \neq Y (0)) \land p \in P) \to X (0) \in ℝ$
15	1 3	rrx2pxel	$⊢ Y \in P \to Y (0) \in ℝ$
16	15	3ad2ant2	$⊢ (X \in P \land Y \in P \land X (0) \neq Y (0)) \to Y (0) \in ℝ$
17	16	adantr	$⊢ ((X \in P \land Y \in P \land X (0) \neq Y (0)) \land p \in P) \to Y (0) \in ℝ$
18		simpl3	$⊢ ((X \in P \land Y \in P \land X (0) \neq Y (0)) \land p \in P) \to X (0) \neq Y (0)$
19	1 3	rrx2pyel	$⊢ p \in P \to p (1) \in ℝ$
20	19	adantl	$⊢ ((X \in P \land Y \in P \land X (0) \neq Y (0)) \land p \in P) \to p (1) \in ℝ$
21	1 3	rrx2pyel	$⊢ X \in P \to X (1) \in ℝ$
22	21	3ad2ant1	$⊢ (X \in P \land Y \in P \land X (0) \neq Y (0)) \to X (1) \in ℝ$
23	22	adantr	$⊢ ((X \in P \land Y \in P \land X (0) \neq Y (0)) \land p \in P) \to X (1) \in ℝ$
24	1 3	rrx2pyel	$⊢ Y \in P \to Y (1) \in ℝ$
25	24	3ad2ant2	$⊢ (X \in P \land Y \in P \land X (0) \neq Y (0)) \to Y (1) \in ℝ$
26	25	adantr	$⊢ ((X \in P \land Y \in P \land X (0) \neq Y (0)) \land p \in P) \to Y (1) \in ℝ$
27	11 14 17 18 20 23 26 5	affinecomb1	$⊢ ((X \in P \land Y \in P \land X (0) \neq Y (0)) \land p \in P) \to (\exists t \in ℝ (p (0) = (1 - t) X (0) + t Y (0) \land p (1) = (1 - t) X (1) + t Y (1)) \leftrightarrow p (1) = S (p (0) - X (0)) + X (1))$
28	27	rabbidva	$⊢ (X \in P \land Y \in P \land X (0) \neq Y (0)) \to \{p \in P \| \exists t \in ℝ (p (0) = (1 - t) X (0) + t Y (0) \land p (1) = (1 - t) X (1) + t Y (1))\} = \{p \in P \| p (1) = S (p (0) - X (0)) + X (1)\}$
29	9 28	eqtrd	$⊢ (X \in P \land Y \in P \land X (0) \neq Y (0)) \to X L Y = \{p \in P \| p (1) = S (p (0) - X (0)) + X (1)\}$

Metamath Proof Explorer

Theorem rrx2linesl

Proof