rrxlinesc

Description: Definition of lines passing through two different points in a generalized real Euclidean space of finite dimension, expressed by their coordinates. (Contributed by AV, 13-Feb-2023)

	Ref	Expression
Hypotheses	rrxlinesc.e	$⊢ E = I$
	rrxlinesc.p	$⊢ P = ℝ^{I}$
	rrxlinesc.l	$⊢ L = {Line}_{M} (E)$
Assertion	rrxlinesc	$⊢ I \in Fin \to L = (x \in P, y \in (P ∖ \{x\}) ⟼ \{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 = I$
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	rrxlines	$⊢ I \in Fin \to L = (x \in P, y \in (P ∖ \{x\}) ⟼ \{p \in P \| \exists t \in ℝ p = ((1 - t) \cdot_{E} x) +_{E} (t \cdot_{E} y)\})$
7		eqid	$⊢ {Base}_{E} = {Base}_{E}$
8		simpll1	$⊢ (((I \in Fin \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \land t \in ℝ) \to I \in Fin$
9		1red	$⊢ (((I \in Fin \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \land t \in ℝ) \to 1 \in ℝ$
10		simpr	$⊢ (((I \in Fin \land x \in P \land y \in (P ∖ \{x\})) \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 ∖ \{x\})) \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	biimpa	$⊢ (I \in Fin \land x \in P) \to x \in {Base}_{E}$
17	16	3adant3	$⊢ (I \in Fin \land x \in P \land y \in (P ∖ \{x\})) \to x \in {Base}_{E}$
18	17	ad2antrr	$⊢ (((I \in Fin \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \land t \in ℝ) \to x \in {Base}_{E}$
19		eldifi	$⊢ y \in (P ∖ \{x\}) \to y \in P$
20	14	eleq2d	$⊢ I \in Fin \to (y \in P \leftrightarrow y \in {Base}_{E})$
21	19 20	imbitrid	$⊢ I \in Fin \to (y \in (P ∖ \{x\}) \to y \in {Base}_{E})$
22	21	a1d	$⊢ I \in Fin \to (x \in P \to (y \in (P ∖ \{x\}) \to y \in {Base}_{E}))$
23	22	3imp	$⊢ (I \in Fin \land x \in P \land y \in (P ∖ \{x\})) \to y \in {Base}_{E}$
24	23	ad2antrr	$⊢ (((I \in Fin \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \land t \in ℝ) \to y \in {Base}_{E}$
25	14	3ad2ant1	$⊢ (I \in Fin \land x \in P \land y \in (P ∖ \{x\})) \to P = {Base}_{E}$
26	25	eleq2d	$⊢ (I \in Fin \land x \in P \land y \in (P ∖ \{x\})) \to (p \in P \leftrightarrow p \in {Base}_{E})$
27	26	biimpa	$⊢ ((I \in Fin \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \to p \in {Base}_{E}$
28	27	adantr	$⊢ (((I \in Fin \land x \in P \land y \in (P ∖ \{x\})) \land p \in P) \land t \in ℝ) \to p \in {Base}_{E}$
29	1 7 4 8 11 18 24 28 5 10	rrxplusgvscavalb	$⊢ (((I \in Fin \land x \in P \land y \in (P ∖ \{x\})) \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 ∖ \{x\})) \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 ∖ \{x\})) \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	31	mpoeq3dva	$⊢ I \in Fin \to (x \in P, y \in (P ∖ \{x\}) ⟼ \{p \in P \| \exists t \in ℝ p = ((1 - t) \cdot_{E} x) +_{E} (t \cdot_{E} y)\}) = (x \in P, y \in (P ∖ \{x\}) ⟼ \{p \in P \| \exists t \in ℝ \forall i \in I p (i) = (1 - t) x (i) + t y (i)\})$
33	6 32	eqtrd	$⊢ I \in Fin \to L = (x \in P, y \in (P ∖ \{x\}) ⟼ \{p \in P \| \exists t \in ℝ \forall i \in I p (i) = (1 - t) x (i) + t y (i)\})$

Metamath Proof Explorer

Theorem rrxlinesc

Proof