# Metamath Proof Explorer

## Theorem 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}={{I}}^{}$
rrxlinesc.p ${⊢}{P}={ℝ}^{{I}}$
rrxlinesc.l ${⊢}{L}={Line}_{M}\left({E}\right)$
Assertion rrxlinec ${⊢}\left({I}\in \mathrm{Fin}\wedge \left({X}\in {P}\wedge {Y}\in {P}\wedge {X}\ne {Y}\right)\right)\to {X}{L}{Y}=\left\{{p}\in {P}|\exists {t}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{t}\right){X}\left({i}\right)+{t}{Y}\left({i}\right)\right\}$

### Proof

Step Hyp Ref Expression
1 rrxlinesc.e ${⊢}{E}={{I}}^{}$
2 rrxlinesc.p ${⊢}{P}={ℝ}^{{I}}$
3 rrxlinesc.l ${⊢}{L}={Line}_{M}\left({E}\right)$
4 eqid ${⊢}{\cdot }_{{E}}={\cdot }_{{E}}$
5 eqid ${⊢}{+}_{{E}}={+}_{{E}}$
6 1 2 3 4 5 rrxline ${⊢}\left({I}\in \mathrm{Fin}\wedge \left({X}\in {P}\wedge {Y}\in {P}\wedge {X}\ne {Y}\right)\right)\to {X}{L}{Y}=\left\{{p}\in {P}|\exists {t}\in ℝ\phantom{\rule{.4em}{0ex}}{p}=\left(\left(1-{t}\right){\cdot }_{{E}}{X}\right){+}_{{E}}\left({t}{\cdot }_{{E}}{Y}\right)\right\}$
7 eqid ${⊢}{\mathrm{Base}}_{{E}}={\mathrm{Base}}_{{E}}$
8 simplll ${⊢}\left(\left(\left({I}\in \mathrm{Fin}\wedge \left({X}\in {P}\wedge {Y}\in {P}\wedge {X}\ne {Y}\right)\right)\wedge {p}\in {P}\right)\wedge {t}\in ℝ\right)\to {I}\in \mathrm{Fin}$
9 1red ${⊢}\left(\left(\left({I}\in \mathrm{Fin}\wedge \left({X}\in {P}\wedge {Y}\in {P}\wedge {X}\ne {Y}\right)\right)\wedge {p}\in {P}\right)\wedge {t}\in ℝ\right)\to 1\in ℝ$
10 simpr ${⊢}\left(\left(\left({I}\in \mathrm{Fin}\wedge \left({X}\in {P}\wedge {Y}\in {P}\wedge {X}\ne {Y}\right)\right)\wedge {p}\in {P}\right)\wedge {t}\in ℝ\right)\to {t}\in ℝ$
11 9 10 resubcld ${⊢}\left(\left(\left({I}\in \mathrm{Fin}\wedge \left({X}\in {P}\wedge {Y}\in {P}\wedge {X}\ne {Y}\right)\right)\wedge {p}\in {P}\right)\wedge {t}\in ℝ\right)\to 1-{t}\in ℝ$
12 id ${⊢}{I}\in \mathrm{Fin}\to {I}\in \mathrm{Fin}$
13 12 1 7 rrxbasefi ${⊢}{I}\in \mathrm{Fin}\to {\mathrm{Base}}_{{E}}={ℝ}^{{I}}$
14 13 2 syl6reqr ${⊢}{I}\in \mathrm{Fin}\to {P}={\mathrm{Base}}_{{E}}$
15 14 eleq2d ${⊢}{I}\in \mathrm{Fin}\to \left({X}\in {P}↔{X}\in {\mathrm{Base}}_{{E}}\right)$
16 15 biimpcd ${⊢}{X}\in {P}\to \left({I}\in \mathrm{Fin}\to {X}\in {\mathrm{Base}}_{{E}}\right)$
17 16 3ad2ant1 ${⊢}\left({X}\in {P}\wedge {Y}\in {P}\wedge {X}\ne {Y}\right)\to \left({I}\in \mathrm{Fin}\to {X}\in {\mathrm{Base}}_{{E}}\right)$
18 17 impcom ${⊢}\left({I}\in \mathrm{Fin}\wedge \left({X}\in {P}\wedge {Y}\in {P}\wedge {X}\ne {Y}\right)\right)\to {X}\in {\mathrm{Base}}_{{E}}$
19 18 ad2antrr ${⊢}\left(\left(\left({I}\in \mathrm{Fin}\wedge \left({X}\in {P}\wedge {Y}\in {P}\wedge {X}\ne {Y}\right)\right)\wedge {p}\in {P}\right)\wedge {t}\in ℝ\right)\to {X}\in {\mathrm{Base}}_{{E}}$
20 14 eleq2d ${⊢}{I}\in \mathrm{Fin}\to \left({Y}\in {P}↔{Y}\in {\mathrm{Base}}_{{E}}\right)$
21 20 biimpcd ${⊢}{Y}\in {P}\to \left({I}\in \mathrm{Fin}\to {Y}\in {\mathrm{Base}}_{{E}}\right)$
22 21 3ad2ant2 ${⊢}\left({X}\in {P}\wedge {Y}\in {P}\wedge {X}\ne {Y}\right)\to \left({I}\in \mathrm{Fin}\to {Y}\in {\mathrm{Base}}_{{E}}\right)$
23 22 impcom ${⊢}\left({I}\in \mathrm{Fin}\wedge \left({X}\in {P}\wedge {Y}\in {P}\wedge {X}\ne {Y}\right)\right)\to {Y}\in {\mathrm{Base}}_{{E}}$
24 23 ad2antrr ${⊢}\left(\left(\left({I}\in \mathrm{Fin}\wedge \left({X}\in {P}\wedge {Y}\in {P}\wedge {X}\ne {Y}\right)\right)\wedge {p}\in {P}\right)\wedge {t}\in ℝ\right)\to {Y}\in {\mathrm{Base}}_{{E}}$
25 14 adantr ${⊢}\left({I}\in \mathrm{Fin}\wedge \left({X}\in {P}\wedge {Y}\in {P}\wedge {X}\ne {Y}\right)\right)\to {P}={\mathrm{Base}}_{{E}}$
26 25 eleq2d ${⊢}\left({I}\in \mathrm{Fin}\wedge \left({X}\in {P}\wedge {Y}\in {P}\wedge {X}\ne {Y}\right)\right)\to \left({p}\in {P}↔{p}\in {\mathrm{Base}}_{{E}}\right)$
27 26 biimpa ${⊢}\left(\left({I}\in \mathrm{Fin}\wedge \left({X}\in {P}\wedge {Y}\in {P}\wedge {X}\ne {Y}\right)\right)\wedge {p}\in {P}\right)\to {p}\in {\mathrm{Base}}_{{E}}$
28 27 adantr ${⊢}\left(\left(\left({I}\in \mathrm{Fin}\wedge \left({X}\in {P}\wedge {Y}\in {P}\wedge {X}\ne {Y}\right)\right)\wedge {p}\in {P}\right)\wedge {t}\in ℝ\right)\to {p}\in {\mathrm{Base}}_{{E}}$
29 1 7 4 8 11 19 24 28 5 10 rrxplusgvscavalb ${⊢}\left(\left(\left({I}\in \mathrm{Fin}\wedge \left({X}\in {P}\wedge {Y}\in {P}\wedge {X}\ne {Y}\right)\right)\wedge {p}\in {P}\right)\wedge {t}\in ℝ\right)\to \left({p}=\left(\left(1-{t}\right){\cdot }_{{E}}{X}\right){+}_{{E}}\left({t}{\cdot }_{{E}}{Y}\right)↔\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{t}\right){X}\left({i}\right)+{t}{Y}\left({i}\right)\right)$
30 29 rexbidva ${⊢}\left(\left({I}\in \mathrm{Fin}\wedge \left({X}\in {P}\wedge {Y}\in {P}\wedge {X}\ne {Y}\right)\right)\wedge {p}\in {P}\right)\to \left(\exists {t}\in ℝ\phantom{\rule{.4em}{0ex}}{p}=\left(\left(1-{t}\right){\cdot }_{{E}}{X}\right){+}_{{E}}\left({t}{\cdot }_{{E}}{Y}\right)↔\exists {t}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{t}\right){X}\left({i}\right)+{t}{Y}\left({i}\right)\right)$
31 30 rabbidva ${⊢}\left({I}\in \mathrm{Fin}\wedge \left({X}\in {P}\wedge {Y}\in {P}\wedge {X}\ne {Y}\right)\right)\to \left\{{p}\in {P}|\exists {t}\in ℝ\phantom{\rule{.4em}{0ex}}{p}=\left(\left(1-{t}\right){\cdot }_{{E}}{X}\right){+}_{{E}}\left({t}{\cdot }_{{E}}{Y}\right)\right\}=\left\{{p}\in {P}|\exists {t}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{t}\right){X}\left({i}\right)+{t}{Y}\left({i}\right)\right\}$
32 6 31 eqtrd ${⊢}\left({I}\in \mathrm{Fin}\wedge \left({X}\in {P}\wedge {Y}\in {P}\wedge {X}\ne {Y}\right)\right)\to {X}{L}{Y}=\left\{{p}\in {P}|\exists {t}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{t}\right){X}\left({i}\right)+{t}{Y}\left({i}\right)\right\}$