rrxlinec

Description: The line passing through the two different points X and Y in a generalized real Euclidean space of finite dimension, expressed by its coordinates. Remark: This proof is shorter and requires less distinct variables than the proof using rrxlinesc . (Contributed by AV, 13-Feb-2023)

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

Proof

Step	Hyp	Ref	Expression
1		rrxlinesc.e	$⊢ E = msup$
2		rrxlinesc.p	$⊢ P = ℝ^{I}$
3		rrxlinesc.l	$⊢ L = {Line}_{M} (E)$
4		eqid	$⊢ \cdot_{E} = \cdot_{E}$
5		eqid	$⊢ +_{E} = +_{E}$
6	1 2 3 4 5	rrxline	$⊢ (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 ℝ p = ((1 - t) \cdot_{E} X) +_{E} (t \cdot_{E} Y)\}$
7		eqid	$⊢ {Base}_{E} = {Base}_{E}$
8		simplll	$⊢ (((I \in Fin \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \land t \in ℝ) \to I \in Fin$
9		1red	$⊢ (((I \in Fin \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \land t \in ℝ) \to 1 \in ℝ$
10		simpr	$⊢ (((I \in Fin \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \land t \in ℝ) \to t \in ℝ$
11	9 10	resubcld	$⊢ (((I \in Fin \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \land t \in ℝ) \to 1 - t \in ℝ$
12		id	$⊢ I \in Fin \to I \in Fin$
13	12 1 7	rrxbasefi	$⊢ I \in Fin \to {Base}_{E} = ℝ^{I}$
14	2 13	eqtr4id	$⊢ I \in Fin \to P = {Base}_{E}$
15	14	eleq2d	$⊢ I \in Fin \to (X \in P \leftrightarrow X \in {Base}_{E})$
16	15	biimpcd	$⊢ X \in P \to (I \in Fin \to X \in {Base}_{E})$
17	16	3ad2ant1	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (I \in Fin \to X \in {Base}_{E})$
18	17	impcom	$⊢ (I \in Fin \land (X \in P \land Y \in P \land X \neq Y)) \to X \in {Base}_{E}$
19	18	ad2antrr	$⊢ (((I \in Fin \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \land t \in ℝ) \to X \in {Base}_{E}$
20	14	eleq2d	$⊢ I \in Fin \to (Y \in P \leftrightarrow Y \in {Base}_{E})$
21	20	biimpcd	$⊢ Y \in P \to (I \in Fin \to Y \in {Base}_{E})$
22	21	3ad2ant2	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (I \in Fin \to Y \in {Base}_{E})$
23	22	impcom	$⊢ (I \in Fin \land (X \in P \land Y \in P \land X \neq Y)) \to Y \in {Base}_{E}$
24	23	ad2antrr	$⊢ (((I \in Fin \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \land t \in ℝ) \to Y \in {Base}_{E}$
25	14	adantr	$⊢ (I \in Fin \land (X \in P \land Y \in P \land X \neq Y)) \to P = {Base}_{E}$
26	25	eleq2d	$⊢ (I \in Fin \land (X \in P \land Y \in P \land X \neq Y)) \to (p \in P \leftrightarrow p \in {Base}_{E})$
27	26	biimpa	$⊢ ((I \in Fin \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to p \in {Base}_{E}$
28	27	adantr	$⊢ (((I \in Fin \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \land t \in ℝ) \to p \in {Base}_{E}$
29	1 7 4 8 11 19 24 28 5 10	rrxplusgvscavalb	$⊢ (((I \in Fin \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \land t \in ℝ) \to (p = ((1 - t) \cdot_{E} X) +_{E} (t \cdot_{E} Y) \leftrightarrow \forall i \in I p (i) = (1 - t) X (i) + t Y (i))$
30	29	rexbidva	$⊢ ((I \in Fin \land (X \in P \land Y \in P \land X \neq Y)) \land p \in P) \to (\exists t \in ℝ p = ((1 - t) \cdot_{E} X) +_{E} (t \cdot_{E} Y) \leftrightarrow \exists t \in ℝ \forall i \in I p (i) = (1 - t) X (i) + t Y (i))$
31	30	rabbidva	$⊢ (I \in Fin \land (X \in P \land Y \in P \land X \neq Y)) \to \{p \in P \| \exists t \in ℝ p = ((1 - t) \cdot_{E} X) +_{E} (t \cdot_{E} Y)\} = \{p \in P \| \exists t \in ℝ \forall i \in I p (i) = (1 - t) X (i) + t Y (i)\}$
32	6 31	eqtrd	$⊢ (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)\}$

Metamath Proof Explorer

Theorem rrxlinec

Proof