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
	rrxlines.p	$$⊢P={ℝ}^I$$
	rrxlines.l	$$⊢L={Line}_M\left(E\right)$$
	rrxlines.m	$$⊢\underset{\dot{}}{·}={\cdot }_E$$
	rrxlines.a	$$⊢\underset{\dot{}}{+}={+}_E$$
Assertion	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 ℝp=\left(\left(1-t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		rrxlines.e
2		rrxlines.p	$$⊢P={ℝ}^I$$
3		rrxlines.l	$$⊢L={Line}_M\left(E\right)$$
4		rrxlines.m	$$⊢\underset{\dot{}}{·}={\cdot }_E$$
5		rrxlines.a	$$⊢\underset{\dot{}}{+}={+}_E$$
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	$$⊢E\in \mathrm{V}\to L=\left(x\in {\mathrm{Base}}_E,y\in \left({\mathrm{Base}}_E\setminus \left\{x\right\}\right)⟼\left\{p\in {\mathrm{Base}}_E|\exists t\in {\mathrm{Base}}_{\mathrm{Scalar}\left(E\right)}p=\left(\left(1_{\mathrm{Scalar}\left(E\right)}{-}_{\mathrm{Scalar}\left(E\right)}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right\}\right)$$
13	6 12	mp1i	$$⊢I\in \mathrm{Fin}\to L=\left(x\in {\mathrm{Base}}_E,y\in \left({\mathrm{Base}}_E\setminus \left\{x\right\}\right)⟼\left\{p\in {\mathrm{Base}}_E|\exists t\in {\mathrm{Base}}_{\mathrm{Scalar}\left(E\right)}p=\left(\left(1_{\mathrm{Scalar}\left(E\right)}{-}_{\mathrm{Scalar}\left(E\right)}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right\}\right)$$
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)}\leftrightarrow 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	$$⊢\left(I\in \mathrm{Fin}\wedge t\in {\mathrm{Base}}_{\mathrm{Scalar}\left(E\right)}\right)\to \left(1_{\mathrm{Scalar}\left(E\right)}{-}_{\mathrm{Scalar}\left(E\right)}t\right)\underset{\dot{}}{·}x=\left(1-t\right)\underset{\dot{}}{·}x$$
40	39	oveq1d	$$⊢\left(I\in \mathrm{Fin}\wedge t\in {\mathrm{Base}}_{\mathrm{Scalar}\left(E\right)}\right)\to \left(\left(1_{\mathrm{Scalar}\left(E\right)}{-}_{\mathrm{Scalar}\left(E\right)}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)=\left(\left(1-t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)$$
41	40	eqeq2d	$$⊢\left(I\in \mathrm{Fin}\wedge t\in {\mathrm{Base}}_{\mathrm{Scalar}\left(E\right)}\right)\to \left(p=\left(\left(1_{\mathrm{Scalar}\left(E\right)}{-}_{\mathrm{Scalar}\left(E\right)}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\leftrightarrow p=\left(\left(1-t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right)$$
42	21 41	rexeqbidva	$$⊢I\in \mathrm{Fin}\to \left(\exists t\in {\mathrm{Base}}_{\mathrm{Scalar}\left(E\right)}p=\left(\left(1_{\mathrm{Scalar}\left(E\right)}{-}_{\mathrm{Scalar}\left(E\right)}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\leftrightarrow \exists t\in ℝp=\left(\left(1-t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right)$$
43	16 42	rabeqbidv	$$⊢I\in \mathrm{Fin}\to \left\{p\in {\mathrm{Base}}_E|\exists t\in {\mathrm{Base}}_{\mathrm{Scalar}\left(E\right)}p=\left(\left(1_{\mathrm{Scalar}\left(E\right)}{-}_{\mathrm{Scalar}\left(E\right)}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right\}=\left\{p\in P|\exists t\in ℝp=\left(\left(1-t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right\}$$
44	16 17 43	mpoeq123dv	$$⊢I\in \mathrm{Fin}\to \left(x\in {\mathrm{Base}}_E,y\in \left({\mathrm{Base}}_E\setminus \left\{x\right\}\right)⟼\left\{p\in {\mathrm{Base}}_E|\exists t\in {\mathrm{Base}}_{\mathrm{Scalar}\left(E\right)}p=\left(\left(1_{\mathrm{Scalar}\left(E\right)}{-}_{\mathrm{Scalar}\left(E\right)}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right\}\right)=\left(x\in P,y\in \left(P\setminus \left\{x\right\}\right)⟼\left\{p\in P|\exists t\in ℝp=\left(\left(1-t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right\}\right)$$
45	13 44	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 ℝp=\left(\left(1-t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right\}\right)$$