rrx2line

Description: The line passing through the two different points X and Y in a real Euclidean space of dimension 2. (Contributed by AV, 22-Jan-2023) (Proof shortened by AV, 13-Feb-2023)

	Ref	Expression
Hypotheses	rrx2line.i	$⊢ I = (0 ..^2)$
	rrx2line.e	$⊢ E = I$
	rrx2line.b	$⊢ P = ℝ^{I}$
	rrx2line.l	$⊢ L = {Line}_{M} (E)$
Assertion	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))\}$

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		fzofi	$⊢ (0 ..^2) \in Fin$
6	1 5	eqeltri	$⊢ I \in Fin$
7	2 3 4	rrxlinec	$⊢ (I \in Fin \land (X \in P \land Y \in P \land X \neq Y)) \to X L Y = \{p \in P \| \exists t \in ℝ \forall i \in I p (i) = (1 - t) X (i) + t Y (i)\}$
8	6 7	mpan	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X L Y = \{p \in P \| \exists t \in ℝ \forall i \in I p (i) = (1 - t) X (i) + t Y (i)\}$
9		fzo0to2pr	$⊢ (0 ..^2) = \{0, 1\}$
10	1 9	eqtri	$⊢ I = \{0, 1\}$
11	10	a1i	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \land t \in ℝ) \to I = \{0, 1\}$
12	11	raleqdv	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \land t \in ℝ) \to (\forall i \in I p (i) = (1 - t) X (i) + t Y (i) \leftrightarrow \forall i \in \{0, 1\} p (i) = (1 - t) X (i) + t Y (i))$
13		c0ex	$⊢ 0 \in V$
14		1ex	$⊢ 1 \in V$
15		fveq2	$⊢ i = 0 \to p (i) = p (0)$
16		fveq2	$⊢ i = 0 \to X (i) = X (0)$
17	16	oveq2d	$⊢ i = 0 \to (1 - t) X (i) = (1 - t) X (0)$
18		fveq2	$⊢ i = 0 \to Y (i) = Y (0)$
19	18	oveq2d	$⊢ i = 0 \to t Y (i) = t Y (0)$
20	17 19	oveq12d	$⊢ i = 0 \to (1 - t) X (i) + t Y (i) = (1 - t) X (0) + t Y (0)$
21	15 20	eqeq12d	$⊢ i = 0 \to (p (i) = (1 - t) X (i) + t Y (i) \leftrightarrow p (0) = (1 - t) X (0) + t Y (0))$
22		fveq2	$⊢ i = 1 \to p (i) = p (1)$
23		fveq2	$⊢ i = 1 \to X (i) = X (1)$
24	23	oveq2d	$⊢ i = 1 \to (1 - t) X (i) = (1 - t) X (1)$
25		fveq2	$⊢ i = 1 \to Y (i) = Y (1)$
26	25	oveq2d	$⊢ i = 1 \to t Y (i) = t Y (1)$
27	24 26	oveq12d	$⊢ i = 1 \to (1 - t) X (i) + t Y (i) = (1 - t) X (1) + t Y (1)$
28	22 27	eqeq12d	$⊢ i = 1 \to (p (i) = (1 - t) X (i) + t Y (i) \leftrightarrow p (1) = (1 - t) X (1) + t Y (1))$
29	13 14 21 28	ralpr	$⊢ \forall i \in \{0, 1\} p (i) = (1 - t) X (i) + t Y (i) \leftrightarrow (p (0) = (1 - t) X (0) + t Y (0) \land p (1) = (1 - t) X (1) + t Y (1))$
30	12 29	bitrdi	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \land t \in ℝ) \to (\forall i \in I p (i) = (1 - t) X (i) + t Y (i) \leftrightarrow (p (0) = (1 - t) X (0) + t Y (0) \land p (1) = (1 - t) X (1) + t Y (1)))$
31	30	rexbidva	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land p \in P) \to (\exists t \in ℝ \forall i \in I p (i) = (1 - t) X (i) + t Y (i) \leftrightarrow \exists t \in ℝ (p (0) = (1 - t) X (0) + t Y (0) \land p (1) = (1 - t) X (1) + t Y (1)))$
32	31	rabbidva	$⊢ (X \in P \land Y \in P \land X \neq Y) \to \{p \in P \| \exists t \in ℝ \forall i \in I p (i) = (1 - t) X (i) + t Y (i)\} = \{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))\}$
33	8 32	eqtrd	$⊢ (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))\}$

Metamath Proof Explorer

Theorem rrx2line

Proof