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 = \{1, 2\}$
	rrx2line.e	$⊢ E = msup$
	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 (1) = (1 - t) X (1) + t Y (1) \land p (2) = (1 - t) X (2) + t Y (2))\}$

Proof

Step	Hyp	Ref	Expression
1		rrx2line.i	$⊢ I = \{1, 2\}$
2		rrx2line.e	$⊢ E = msup$
3		rrx2line.b	$⊢ P = ℝ^{I}$
4		rrx2line.l	$⊢ L = {Line}_{M} (E)$
5		prfi	$⊢ \{1, 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	1	a1i	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land p \in P) \land t \in ℝ) \to I = \{1, 2\}$
10	9	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 \{1, 2\} p (i) = (1 - t) X (i) + t Y (i))$
11		1ex	$⊢ 1 \in V$
12		2ex	$⊢ 2 \in V$
13		fveq2	$⊢ i = 1 \to p (i) = p (1)$
14		fveq2	$⊢ i = 1 \to X (i) = X (1)$
15	14	oveq2d	$⊢ i = 1 \to (1 - t) X (i) = (1 - t) X (1)$
16		fveq2	$⊢ i = 1 \to Y (i) = Y (1)$
17	16	oveq2d	$⊢ i = 1 \to t Y (i) = t Y (1)$
18	15 17	oveq12d	$⊢ i = 1 \to (1 - t) X (i) + t Y (i) = (1 - t) X (1) + t Y (1)$
19	13 18	eqeq12d	$⊢ i = 1 \to (p (i) = (1 - t) X (i) + t Y (i) \leftrightarrow p (1) = (1 - t) X (1) + t Y (1))$
20		fveq2	$⊢ i = 2 \to p (i) = p (2)$
21		fveq2	$⊢ i = 2 \to X (i) = X (2)$
22	21	oveq2d	$⊢ i = 2 \to (1 - t) X (i) = (1 - t) X (2)$
23		fveq2	$⊢ i = 2 \to Y (i) = Y (2)$
24	23	oveq2d	$⊢ i = 2 \to t Y (i) = t Y (2)$
25	22 24	oveq12d	$⊢ i = 2 \to (1 - t) X (i) + t Y (i) = (1 - t) X (2) + t Y (2)$
26	20 25	eqeq12d	$⊢ i = 2 \to (p (i) = (1 - t) X (i) + t Y (i) \leftrightarrow p (2) = (1 - t) X (2) + t Y (2))$
27	11 12 19 26	ralpr	$⊢ \forall i \in \{1, 2\} p (i) = (1 - t) X (i) + t Y (i) \leftrightarrow (p (1) = (1 - t) X (1) + t Y (1) \land p (2) = (1 - t) X (2) + t Y (2))$
28	10 27	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 (1) = (1 - t) X (1) + t Y (1) \land p (2) = (1 - t) X (2) + t Y (2)))$
29	28	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 (1) = (1 - t) X (1) + t Y (1) \land p (2) = (1 - t) X (2) + t Y (2)))$
30	29	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 (1) = (1 - t) X (1) + t Y (1) \land p (2) = (1 - t) X (2) + t Y (2))\}$
31	8 30	eqtrd	$⊢ (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))\}$

Metamath Proof Explorer

Theorem rrx2line

Proof