# Metamath Proof Explorer

## Theorem 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}\left({E}\right)$
Assertion rrxlinesc ${⊢}{I}\in \mathrm{Fin}\to {L}=\left({x}\in {P},{y}\in \left({P}\setminus \left\{{x}\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\}\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 rrxlines ${⊢}{I}\in \mathrm{Fin}\to {L}=\left({x}\in {P},{y}\in \left({P}\setminus \left\{{x}\right\}\right)⟼\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\}\right)$
7 eqid ${⊢}{\mathrm{Base}}_{{E}}={\mathrm{Base}}_{{E}}$
8 simpll1 ${⊢}\left(\left(\left({I}\in \mathrm{Fin}\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\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 {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\wedge {t}\in ℝ\right)\to 1\in ℝ$
10 simpr ${⊢}\left(\left(\left({I}\in \mathrm{Fin}\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\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 {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\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 biimpa ${⊢}\left({I}\in \mathrm{Fin}\wedge {x}\in {P}\right)\to {x}\in {\mathrm{Base}}_{{E}}$
17 16 3adant3 ${⊢}\left({I}\in \mathrm{Fin}\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\to {x}\in {\mathrm{Base}}_{{E}}$
18 17 ad2antrr ${⊢}\left(\left(\left({I}\in \mathrm{Fin}\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\wedge {t}\in ℝ\right)\to {x}\in {\mathrm{Base}}_{{E}}$
19 eldifi ${⊢}{y}\in \left({P}\setminus \left\{{x}\right\}\right)\to {y}\in {P}$
20 14 eleq2d ${⊢}{I}\in \mathrm{Fin}\to \left({y}\in {P}↔{y}\in {\mathrm{Base}}_{{E}}\right)$
21 19 20 syl5ib ${⊢}{I}\in \mathrm{Fin}\to \left({y}\in \left({P}\setminus \left\{{x}\right\}\right)\to {y}\in {\mathrm{Base}}_{{E}}\right)$
22 21 a1d ${⊢}{I}\in \mathrm{Fin}\to \left({x}\in {P}\to \left({y}\in \left({P}\setminus \left\{{x}\right\}\right)\to {y}\in {\mathrm{Base}}_{{E}}\right)\right)$
23 22 3imp ${⊢}\left({I}\in \mathrm{Fin}\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\to {y}\in {\mathrm{Base}}_{{E}}$
24 23 ad2antrr ${⊢}\left(\left(\left({I}\in \mathrm{Fin}\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\wedge {t}\in ℝ\right)\to {y}\in {\mathrm{Base}}_{{E}}$
25 14 3ad2ant1 ${⊢}\left({I}\in \mathrm{Fin}\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\to {P}={\mathrm{Base}}_{{E}}$
26 25 eleq2d ${⊢}\left({I}\in \mathrm{Fin}\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\to \left({p}\in {P}↔{p}\in {\mathrm{Base}}_{{E}}\right)$
27 26 biimpa ${⊢}\left(\left({I}\in \mathrm{Fin}\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\to {p}\in {\mathrm{Base}}_{{E}}$
28 27 adantr ${⊢}\left(\left(\left({I}\in \mathrm{Fin}\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\right)\right)\wedge {p}\in {P}\right)\wedge {t}\in ℝ\right)\to {p}\in {\mathrm{Base}}_{{E}}$
29 1 7 4 8 11 18 24 28 5 10 rrxplusgvscavalb ${⊢}\left(\left(\left({I}\in \mathrm{Fin}\wedge {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\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 {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\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 {x}\in {P}\wedge {y}\in \left({P}\setminus \left\{{x}\right\}\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 31 mpoeq3dva ${⊢}{I}\in \mathrm{Fin}\to \left({x}\in {P},{y}\in \left({P}\setminus \left\{{x}\right\}\right)⟼\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\}\right)=\left({x}\in {P},{y}\in \left({P}\setminus \left\{{x}\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\}\right)$
33 6 32 eqtrd ${⊢}{I}\in \mathrm{Fin}\to {L}=\left({x}\in {P},{y}\in \left({P}\setminus \left\{{x}\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\}\right)$