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 ( ( p2 ) - ( X2 ) ) = ( S x. ( ( p1 ) - ( X1 ) ) ) . (Contributed by AV, 22-Jan-2023)

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

Proof

Step	Hyp	Ref	Expression
1		rrx2line.i	$⊢ I = \{1, 2\}$
2		rrx2line.e	$⊢ E = I$
3		rrx2line.b	$⊢ P = ℝ^{I}$
4		rrx2line.l	$⊢ L = {Line}_{M} (E)$
5		rrx2linesl.s	$⊢ S = \frac{Y (2) - X (2)}{Y (1) - X (1)}$
6		fveq1	$⊢ X = Y \to X (1) = Y (1)$
7	6	necon3i	$⊢ X (1) \neq Y (1) \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 (1) = (1 - t) X (1) + t Y (1) \land p (2) = (1 - t) X (2) + t Y (2))\}$
9	7 8	syl3an3	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to X L Y = \{p \in P \| \exists t \in ℝ (p (1) = (1 - t) X (1) + t Y (1) \land p (2) = (1 - t) X (2) + t Y (2))\}$
10		reex	$⊢ ℝ \in V$
11		prex	$⊢ \{1, 2\} \in V$
12	1 11	eqeltri	$⊢ I \in V$
13	10 12	elmap	$⊢ p \in (ℝ^{I}) \leftrightarrow p : I ⟶ ℝ$
14		id	$⊢ p : I ⟶ ℝ \to p : I ⟶ ℝ$
15		1ex	$⊢ 1 \in V$
16	15	prid1	$⊢ 1 \in \{1, 2\}$
17	16 1	eleqtrri	$⊢ 1 \in I$
18	17	a1i	$⊢ p : I ⟶ ℝ \to 1 \in I$
19	14 18	ffvelrnd	$⊢ p : I ⟶ ℝ \to p (1) \in ℝ$
20	13 19	sylbi	$⊢ p \in (ℝ^{I}) \to p (1) \in ℝ$
21	20 3	eleq2s	$⊢ p \in P \to p (1) \in ℝ$
22	21	adantl	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land p \in P) \to p (1) \in ℝ$
23	10 12	elmap	$⊢ X \in (ℝ^{I}) \leftrightarrow X : I ⟶ ℝ$
24		id	$⊢ X : I ⟶ ℝ \to X : I ⟶ ℝ$
25	17	a1i	$⊢ X : I ⟶ ℝ \to 1 \in I$
26	24 25	ffvelrnd	$⊢ X : I ⟶ ℝ \to X (1) \in ℝ$
27	23 26	sylbi	$⊢ X \in (ℝ^{I}) \to X (1) \in ℝ$
28	27 3	eleq2s	$⊢ X \in P \to X (1) \in ℝ$
29	28	3ad2ant1	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to X (1) \in ℝ$
30	29	adantr	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land p \in P) \to X (1) \in ℝ$
31	10 12	elmap	$⊢ Y \in (ℝ^{I}) \leftrightarrow Y : I ⟶ ℝ$
32		id	$⊢ Y : I ⟶ ℝ \to Y : I ⟶ ℝ$
33	17	a1i	$⊢ Y : I ⟶ ℝ \to 1 \in I$
34	32 33	ffvelrnd	$⊢ Y : I ⟶ ℝ \to Y (1) \in ℝ$
35	31 34	sylbi	$⊢ Y \in (ℝ^{I}) \to Y (1) \in ℝ$
36	35 3	eleq2s	$⊢ Y \in P \to Y (1) \in ℝ$
37	36	3ad2ant2	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to Y (1) \in ℝ$
38	37	adantr	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land p \in P) \to Y (1) \in ℝ$
39		simpl3	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land p \in P) \to X (1) \neq Y (1)$
40		2ex	$⊢ 2 \in V$
41	40	prid2	$⊢ 2 \in \{1, 2\}$
42	41 1	eleqtrri	$⊢ 2 \in I$
43	42	a1i	$⊢ p : I ⟶ ℝ \to 2 \in I$
44	14 43	ffvelrnd	$⊢ p : I ⟶ ℝ \to p (2) \in ℝ$
45	13 44	sylbi	$⊢ p \in (ℝ^{I}) \to p (2) \in ℝ$
46	45 3	eleq2s	$⊢ p \in P \to p (2) \in ℝ$
47	46	adantl	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land p \in P) \to p (2) \in ℝ$
48	42	a1i	$⊢ X : I ⟶ ℝ \to 2 \in I$
49	24 48	ffvelrnd	$⊢ X : I ⟶ ℝ \to X (2) \in ℝ$
50	23 49	sylbi	$⊢ X \in (ℝ^{I}) \to X (2) \in ℝ$
51	50 3	eleq2s	$⊢ X \in P \to X (2) \in ℝ$
52	51	3ad2ant1	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to X (2) \in ℝ$
53	52	adantr	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land p \in P) \to X (2) \in ℝ$
54	3	eleq2i	$⊢ Y \in P \leftrightarrow Y \in (ℝ^{I})$
55	54 31	bitri	$⊢ Y \in P \leftrightarrow Y : I ⟶ ℝ$
56	42	a1i	$⊢ Y : I ⟶ ℝ \to 2 \in I$
57	32 56	ffvelrnd	$⊢ Y : I ⟶ ℝ \to Y (2) \in ℝ$
58	55 57	sylbi	$⊢ Y \in P \to Y (2) \in ℝ$
59	58	3ad2ant2	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to Y (2) \in ℝ$
60	59	adantr	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land p \in P) \to Y (2) \in ℝ$
61	22 30 38 39 47 53 60 5	affinecomb1	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land p \in P) \to (\exists t \in ℝ (p (1) = (1 - t) X (1) + t Y (1) \land p (2) = (1 - t) X (2) + t Y (2)) \leftrightarrow p (2) = S (p (1) - X (1)) + X (2))$
62	61	rabbidva	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to \{p \in P \| \exists t \in ℝ (p (1) = (1 - t) X (1) + t Y (1) \land p (2) = (1 - t) X (2) + t Y (2))\} = \{p \in P \| p (2) = S (p (1) - X (1)) + X (2)\}$
63	9 62	eqtrd	$⊢ (X \in P \land Y \in P \land X (1) \neq Y (1)) \to X L Y = \{p \in P \| p (2) = S (p (1) - X (1)) + X (2)\}$

Metamath Proof Explorer

Theorem rrx2linesl

Proof