# Metamath Proof Explorer

## Theorem rrxlines

Description: Definition of lines passing through two different points 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}\left({E}\right)$
rrxlines.m
rrxlines.a
Assertion rrxlines

### Proof

Step Hyp Ref Expression
1 rrxlines.e ${⊢}{E}={{I}}^{}$
2 rrxlines.p ${⊢}{P}={ℝ}^{{I}}$
3 rrxlines.l ${⊢}{L}={Line}_{M}\left({E}\right)$
4 rrxlines.m
5 rrxlines.a
6 1 fvexi ${⊢}{E}\in \mathrm{V}$
7 eqid ${⊢}{\mathrm{Base}}_{{E}}={\mathrm{Base}}_{{E}}$
8 eqid ${⊢}\mathrm{Scalar}\left({E}\right)=\mathrm{Scalar}\left({E}\right)$
9 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({E}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({E}\right)}$
10 eqid ${⊢}{-}_{\mathrm{Scalar}\left({E}\right)}={-}_{\mathrm{Scalar}\left({E}\right)}$
11 eqid ${⊢}{1}_{\mathrm{Scalar}\left({E}\right)}={1}_{\mathrm{Scalar}\left({E}\right)}$
12 7 3 8 9 4 5 10 11 lines
13 6 12 mp1i
14 id ${⊢}{I}\in \mathrm{Fin}\to {I}\in \mathrm{Fin}$
15 14 1 7 rrxbasefi ${⊢}{I}\in \mathrm{Fin}\to {\mathrm{Base}}_{{E}}={ℝ}^{{I}}$
16 15 2 eqtr4di ${⊢}{I}\in \mathrm{Fin}\to {\mathrm{Base}}_{{E}}={P}$
17 16 difeq1d ${⊢}{I}\in \mathrm{Fin}\to {\mathrm{Base}}_{{E}}\setminus \left\{{x}\right\}={P}\setminus \left\{{x}\right\}$
18 1 rrxsca ${⊢}{I}\in \mathrm{Fin}\to \mathrm{Scalar}\left({E}\right)={ℝ}_{\mathrm{fld}}$
19 18 fveq2d ${⊢}{I}\in \mathrm{Fin}\to {\mathrm{Base}}_{\mathrm{Scalar}\left({E}\right)}={\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$
20 rebase ${⊢}ℝ={\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$
21 19 20 eqtr4di ${⊢}{I}\in \mathrm{Fin}\to {\mathrm{Base}}_{\mathrm{Scalar}\left({E}\right)}=ℝ$
22 18 fveq2d ${⊢}{I}\in \mathrm{Fin}\to {1}_{\mathrm{Scalar}\left({E}\right)}={1}_{{ℝ}_{\mathrm{fld}}}$
23 re1r ${⊢}1={1}_{{ℝ}_{\mathrm{fld}}}$
24 22 23 eqtr4di ${⊢}{I}\in \mathrm{Fin}\to {1}_{\mathrm{Scalar}\left({E}\right)}=1$
25 24 oveq1d ${⊢}{I}\in \mathrm{Fin}\to {1}_{\mathrm{Scalar}\left({E}\right)}{-}_{\mathrm{Scalar}\left({E}\right)}{t}=1{-}_{\mathrm{Scalar}\left({E}\right)}{t}$
26 25 adantr ${⊢}\left({I}\in \mathrm{Fin}\wedge {t}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({E}\right)}\right)\to {1}_{\mathrm{Scalar}\left({E}\right)}{-}_{\mathrm{Scalar}\left({E}\right)}{t}=1{-}_{\mathrm{Scalar}\left({E}\right)}{t}$
27 18 fveq2d ${⊢}{I}\in \mathrm{Fin}\to {-}_{\mathrm{Scalar}\left({E}\right)}={-}_{{ℝ}_{\mathrm{fld}}}$
28 27 oveqd ${⊢}{I}\in \mathrm{Fin}\to 1{-}_{\mathrm{Scalar}\left({E}\right)}{t}=1{-}_{{ℝ}_{\mathrm{fld}}}{t}$
29 28 adantr ${⊢}\left({I}\in \mathrm{Fin}\wedge {t}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({E}\right)}\right)\to 1{-}_{\mathrm{Scalar}\left({E}\right)}{t}=1{-}_{{ℝ}_{\mathrm{fld}}}{t}$
30 21 eleq2d ${⊢}{I}\in \mathrm{Fin}\to \left({t}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({E}\right)}↔{t}\in ℝ\right)$
31 1re ${⊢}1\in ℝ$
32 eqid ${⊢}{-}_{{ℝ}_{\mathrm{fld}}}={-}_{{ℝ}_{\mathrm{fld}}}$
33 32 resubgval ${⊢}\left(1\in ℝ\wedge {t}\in ℝ\right)\to 1-{t}=1{-}_{{ℝ}_{\mathrm{fld}}}{t}$
34 33 eqcomd ${⊢}\left(1\in ℝ\wedge {t}\in ℝ\right)\to 1{-}_{{ℝ}_{\mathrm{fld}}}{t}=1-{t}$
35 31 34 mpan ${⊢}{t}\in ℝ\to 1{-}_{{ℝ}_{\mathrm{fld}}}{t}=1-{t}$
36 30 35 syl6bi ${⊢}{I}\in \mathrm{Fin}\to \left({t}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({E}\right)}\to 1{-}_{{ℝ}_{\mathrm{fld}}}{t}=1-{t}\right)$
37 36 imp ${⊢}\left({I}\in \mathrm{Fin}\wedge {t}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({E}\right)}\right)\to 1{-}_{{ℝ}_{\mathrm{fld}}}{t}=1-{t}$
38 26 29 37 3eqtrd ${⊢}\left({I}\in \mathrm{Fin}\wedge {t}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({E}\right)}\right)\to {1}_{\mathrm{Scalar}\left({E}\right)}{-}_{\mathrm{Scalar}\left({E}\right)}{t}=1-{t}$
39 38 oveq1d
40 39 oveq1d
41 40 eqeq2d
42 21 41 rexeqbidva
43 16 42 rabeqbidv
44 16 17 43 mpoeq123dv
45 13 44 eqtrd