rrxline

Description: The line passing through the two different points X and Y in a generalized real Euclidean space of finite dimension. (Contributed by AV, 14-Jan-2023)

	Ref	Expression
Hypotheses	rrxlines.e	$⊢ E = I$
	rrxlines.p	$⊢ P = ℝ^{I}$
	rrxlines.l	$⊢ L = {Line}_{M} (E)$
	rrxlines.m	$⊢ \underset{˙}{\cdot} = \cdot_{E}$
	rrxlines.a	$⊢ \underset{˙}{+} = +_{E}$
Assertion	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) \underset{˙}{\cdot} X) \underset{˙}{+} (t \underset{˙}{\cdot} Y)\}$

Proof

Step	Hyp	Ref	Expression
1		rrxlines.e	$⊢ E = I$
2		rrxlines.p	$⊢ P = ℝ^{I}$
3		rrxlines.l	$⊢ L = {Line}_{M} (E)$
4		rrxlines.m	$⊢ \underset{˙}{\cdot} = \cdot_{E}$
5		rrxlines.a	$⊢ \underset{˙}{+} = +_{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) \underset{˙}{\cdot} x) \underset{˙}{+} (t \underset{˙}{\cdot} y)\})$
7	6	oveqd	$⊢ I \in Fin \to X L Y = X (x \in P, y \in (P ∖ \{x\}) ⟼ \{p \in P \| \exists t \in ℝ p = ((1 - t) \underset{˙}{\cdot} x) \underset{˙}{+} (t \underset{˙}{\cdot} y)\}) Y$
8	7	adantr	$⊢ (I \in Fin \land (X \in P \land Y \in P \land X \neq Y)) \to X L Y = X (x \in P, y \in (P ∖ \{x\}) ⟼ \{p \in P \| \exists t \in ℝ p = ((1 - t) \underset{˙}{\cdot} x) \underset{˙}{+} (t \underset{˙}{\cdot} y)\}) Y$
9		eqidd	$⊢ (I \in Fin \land (X \in P \land Y \in P \land X \neq Y)) \to (x \in P, y \in (P ∖ \{x\}) ⟼ \{p \in P \| \exists t \in ℝ p = ((1 - t) \underset{˙}{\cdot} x) \underset{˙}{+} (t \underset{˙}{\cdot} y)\}) = (x \in P, y \in (P ∖ \{x\}) ⟼ \{p \in P \| \exists t \in ℝ p = ((1 - t) \underset{˙}{\cdot} x) \underset{˙}{+} (t \underset{˙}{\cdot} y)\})$
10		simpl	$⊢ (x = X \land y = Y) \to x = X$
11	10	oveq2d	$⊢ (x = X \land y = Y) \to (1 - t) \underset{˙}{\cdot} x = (1 - t) \underset{˙}{\cdot} X$
12		simpr	$⊢ (x = X \land y = Y) \to y = Y$
13	12	oveq2d	$⊢ (x = X \land y = Y) \to t \underset{˙}{\cdot} y = t \underset{˙}{\cdot} Y$
14	11 13	oveq12d	$⊢ (x = X \land y = Y) \to ((1 - t) \underset{˙}{\cdot} x) \underset{˙}{+} (t \underset{˙}{\cdot} y) = ((1 - t) \underset{˙}{\cdot} X) \underset{˙}{+} (t \underset{˙}{\cdot} Y)$
15	14	eqeq2d	$⊢ (x = X \land y = Y) \to (p = ((1 - t) \underset{˙}{\cdot} x) \underset{˙}{+} (t \underset{˙}{\cdot} y) \leftrightarrow p = ((1 - t) \underset{˙}{\cdot} X) \underset{˙}{+} (t \underset{˙}{\cdot} Y))$
16	15	rexbidv	$⊢ (x = X \land y = Y) \to (\exists t \in ℝ p = ((1 - t) \underset{˙}{\cdot} x) \underset{˙}{+} (t \underset{˙}{\cdot} y) \leftrightarrow \exists t \in ℝ p = ((1 - t) \underset{˙}{\cdot} X) \underset{˙}{+} (t \underset{˙}{\cdot} Y))$
17	16	rabbidv	$⊢ (x = X \land y = Y) \to \{p \in P \| \exists t \in ℝ p = ((1 - t) \underset{˙}{\cdot} x) \underset{˙}{+} (t \underset{˙}{\cdot} y)\} = \{p \in P \| \exists t \in ℝ p = ((1 - t) \underset{˙}{\cdot} X) \underset{˙}{+} (t \underset{˙}{\cdot} Y)\}$
18	17	adantl	$⊢ ((I \in Fin \land (X \in P \land Y \in P \land X \neq Y)) \land (x = X \land y = Y)) \to \{p \in P \| \exists t \in ℝ p = ((1 - t) \underset{˙}{\cdot} x) \underset{˙}{+} (t \underset{˙}{\cdot} y)\} = \{p \in P \| \exists t \in ℝ p = ((1 - t) \underset{˙}{\cdot} X) \underset{˙}{+} (t \underset{˙}{\cdot} Y)\}$
19		sneq	$⊢ x = X \to \{x\} = \{X\}$
20	19	difeq2d	$⊢ x = X \to P ∖ \{x\} = P ∖ \{X\}$
21	20	adantl	$⊢ ((I \in Fin \land (X \in P \land Y \in P \land X \neq Y)) \land x = X) \to P ∖ \{x\} = P ∖ \{X\}$
22		simpr1	$⊢ (I \in Fin \land (X \in P \land Y \in P \land X \neq Y)) \to X \in P$
23		id	$⊢ X \neq Y \to X \neq Y$
24	23	necomd	$⊢ X \neq Y \to Y \neq X$
25	24	anim2i	$⊢ (Y \in P \land X \neq Y) \to (Y \in P \land Y \neq X)$
26	25	3adant1	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (Y \in P \land Y \neq X)$
27		eldifsn	$⊢ Y \in (P ∖ \{X\}) \leftrightarrow (Y \in P \land Y \neq X)$
28	26 27	sylibr	$⊢ (X \in P \land Y \in P \land X \neq Y) \to Y \in (P ∖ \{X\})$
29	28	adantl	$⊢ (I \in Fin \land (X \in P \land Y \in P \land X \neq Y)) \to Y \in (P ∖ \{X\})$
30	2	ovexi	$⊢ P \in V$
31	30	rabex	$⊢ \{p \in P \| \exists t \in ℝ p = ((1 - t) \underset{˙}{\cdot} X) \underset{˙}{+} (t \underset{˙}{\cdot} Y)\} \in V$
32	31	a1i	$⊢ (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) \underset{˙}{\cdot} X) \underset{˙}{+} (t \underset{˙}{\cdot} Y)\} \in V$
33	9 18 21 22 29 32	ovmpodx	$⊢ (I \in Fin \land (X \in P \land Y \in P \land X \neq Y)) \to X (x \in P, y \in (P ∖ \{x\}) ⟼ \{p \in P \| \exists t \in ℝ p = ((1 - t) \underset{˙}{\cdot} x) \underset{˙}{+} (t \underset{˙}{\cdot} y)\}) Y = \{p \in P \| \exists t \in ℝ p = ((1 - t) \underset{˙}{\cdot} X) \underset{˙}{+} (t \underset{˙}{\cdot} Y)\}$
34	8 33	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 ℝ p = ((1 - t) \underset{˙}{\cdot} X) \underset{˙}{+} (t \underset{˙}{\cdot} Y)\}$

Metamath Proof Explorer

Theorem rrxline

Proof