Theorem lines

Description: The lines passing through two different points in a left module (or any extended structure having a base set, an addition, and a scalar multiplication). (Contributed by AV, 14-Jan-2023)

	Ref	Expression
Hypotheses	lines.b	$$⊢B={\mathrm{Base}}_W$$
	lines.l	$$⊢L={Line}_M\left(W\right)$$
	lines.s	$$⊢S=\mathrm{Scalar}\left(W\right)$$
	lines.k	$$⊢K={\mathrm{Base}}_S$$
	lines.p	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	lines.a	$$⊢\underset{\dot{}}{+}={+}_W$$
	lines.m	$$⊢\underset{\dot{}}{-}={-}_S$$
	lines.1	$$⊢\underset{\dot{}}{1}=1_S$$
Assertion	lines	$$⊢W\in V\to L=\left(x\in B,y\in \left(B\setminus \left\{x\right\}\right)⟼\left\{p\in B|\exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		lines.b	$$⊢B={\mathrm{Base}}_W$$
2		lines.l	$$⊢L={Line}_M\left(W\right)$$
3		lines.s	$$⊢S=\mathrm{Scalar}\left(W\right)$$
4		lines.k	$$⊢K={\mathrm{Base}}_S$$
5		lines.p	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
6		lines.a	$$⊢\underset{\dot{}}{+}={+}_W$$
7		lines.m	$$⊢\underset{\dot{}}{-}={-}_S$$
8		lines.1	$$⊢\underset{\dot{}}{1}=1_S$$
9		df-line	$$⊢{Line}_M=\left(w\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_w,y\in \left({\mathrm{Base}}_w\setminus \left\{x\right\}\right)⟼\left\{p\in {\mathrm{Base}}_w|\exists t\in {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}p=\left(\left(1_{\mathrm{Scalar}\left(w\right)}{-}_{\mathrm{Scalar}\left(w\right)}t\right){\cdot }_{w}x\right){+}_w\left(t{\cdot }_{w}y\right)\right\}\right)\right)$$
10		fveq2	$$⊢W=w\to {\mathrm{Base}}_W={\mathrm{Base}}_w$$
11	1 10	syl5eq	$$⊢W=w\to B={\mathrm{Base}}_w$$
12	11	difeq1d	$$⊢W=w\to B\setminus \left\{x\right\}={\mathrm{Base}}_w\setminus \left\{x\right\}$$
13		fveq2	$$⊢W=w\to \mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(w\right)$$
14	3 13	syl5eq	$$⊢W=w\to S=\mathrm{Scalar}\left(w\right)$$
15	14	fveq2d	$$⊢W=w\to {\mathrm{Base}}_S={\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}$$
16	4 15	syl5eq	$$⊢W=w\to K={\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}$$
17		fveq2	$$⊢W=w\to {+}_W={+}_w$$
18	6 17	syl5eq	$$⊢W=w\to \underset{\dot{}}{+}={+}_w$$
19		fveq2	$$⊢W=w\to {\cdot }_W={\cdot }_w$$
20	5 19	syl5eq	$$⊢W=w\to \underset{\dot{}}{·}={\cdot }_w$$
21	3	fveq2i	$$⊢{-}_S={-}_{\mathrm{Scalar}\left(W\right)}$$
22	7 21	eqtri	$$⊢\underset{\dot{}}{-}={-}_{\mathrm{Scalar}\left(W\right)}$$
23		2fveq3	$$⊢W=w\to {-}_{\mathrm{Scalar}\left(W\right)}={-}_{\mathrm{Scalar}\left(w\right)}$$
24	22 23	syl5eq	$$⊢W=w\to \underset{\dot{}}{-}={-}_{\mathrm{Scalar}\left(w\right)}$$
25	3	fveq2i	$$⊢1_S=1_{\mathrm{Scalar}\left(W\right)}$$
26	8 25	eqtri	$$⊢\underset{\dot{}}{1}=1_{\mathrm{Scalar}\left(W\right)}$$
27		2fveq3	$$⊢W=w\to 1_{\mathrm{Scalar}\left(W\right)}=1_{\mathrm{Scalar}\left(w\right)}$$
28	26 27	syl5eq	$$⊢W=w\to \underset{\dot{}}{1}=1_{\mathrm{Scalar}\left(w\right)}$$
29		eqidd	$$⊢W=w\to t=t$$
30	24 28 29	oveq123d	$$⊢W=w\to \underset{\dot{}}{1}\underset{\dot{}}{-}t=1_{\mathrm{Scalar}\left(w\right)}{-}_{\mathrm{Scalar}\left(w\right)}t$$
31		eqidd	$$⊢W=w\to x=x$$
32	20 30 31	oveq123d	$$⊢W=w\to \left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}x=\left(1_{\mathrm{Scalar}\left(w\right)}{-}_{\mathrm{Scalar}\left(w\right)}t\right){\cdot }_{w}x$$
33	20	oveqd	$$⊢W=w\to t\underset{\dot{}}{·}y=t{\cdot }_{w}y$$
34	18 32 33	oveq123d	$$⊢W=w\to \left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)=\left(\left(1_{\mathrm{Scalar}\left(w\right)}{-}_{\mathrm{Scalar}\left(w\right)}t\right){\cdot }_{w}x\right){+}_w\left(t{\cdot }_{w}y\right)$$
35	34	eqeq2d	$$⊢W=w\to \left(p=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\leftrightarrow p=\left(\left(1_{\mathrm{Scalar}\left(w\right)}{-}_{\mathrm{Scalar}\left(w\right)}t\right){\cdot }_{w}x\right){+}_w\left(t{\cdot }_{w}y\right)\right)$$
36	16 35	rexeqbidv	$$⊢W=w\to \left(\exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\leftrightarrow \exists t\in {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}p=\left(\left(1_{\mathrm{Scalar}\left(w\right)}{-}_{\mathrm{Scalar}\left(w\right)}t\right){\cdot }_{w}x\right){+}_w\left(t{\cdot }_{w}y\right)\right)$$
37	11 36	rabeqbidv	$$⊢W=w\to \left\{p\in B|\exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right\}=\left\{p\in {\mathrm{Base}}_w|\exists t\in {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}p=\left(\left(1_{\mathrm{Scalar}\left(w\right)}{-}_{\mathrm{Scalar}\left(w\right)}t\right){\cdot }_{w}x\right){+}_w\left(t{\cdot }_{w}y\right)\right\}$$
38	11 12 37	mpoeq123dv	$$⊢W=w\to \left(x\in B,y\in \left(B\setminus \left\{x\right\}\right)⟼\left\{p\in B|\exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right\}\right)=\left(x\in {\mathrm{Base}}_w,y\in \left({\mathrm{Base}}_w\setminus \left\{x\right\}\right)⟼\left\{p\in {\mathrm{Base}}_w|\exists t\in {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}p=\left(\left(1_{\mathrm{Scalar}\left(w\right)}{-}_{\mathrm{Scalar}\left(w\right)}t\right){\cdot }_{w}x\right){+}_w\left(t{\cdot }_{w}y\right)\right\}\right)$$
39	38	eqcomd	$$⊢W=w\to \left(x\in {\mathrm{Base}}_w,y\in \left({\mathrm{Base}}_w\setminus \left\{x\right\}\right)⟼\left\{p\in {\mathrm{Base}}_w|\exists t\in {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}p=\left(\left(1_{\mathrm{Scalar}\left(w\right)}{-}_{\mathrm{Scalar}\left(w\right)}t\right){\cdot }_{w}x\right){+}_w\left(t{\cdot }_{w}y\right)\right\}\right)=\left(x\in B,y\in \left(B\setminus \left\{x\right\}\right)⟼\left\{p\in B|\exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right\}\right)$$
40	39	eqcoms	$$⊢w=W\to \left(x\in {\mathrm{Base}}_w,y\in \left({\mathrm{Base}}_w\setminus \left\{x\right\}\right)⟼\left\{p\in {\mathrm{Base}}_w|\exists t\in {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}p=\left(\left(1_{\mathrm{Scalar}\left(w\right)}{-}_{\mathrm{Scalar}\left(w\right)}t\right){\cdot }_{w}x\right){+}_w\left(t{\cdot }_{w}y\right)\right\}\right)=\left(x\in B,y\in \left(B\setminus \left\{x\right\}\right)⟼\left\{p\in B|\exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right\}\right)$$
41		elex	$$⊢W\in V\to W\in \mathrm{V}$$
42	1	fvexi	$$⊢B\in \mathrm{V}$$
43	42	difexi	$$⊢B\setminus \left\{x\right\}\in \mathrm{V}$$
44	42 43	mpoex	$$⊢\left(x\in B,y\in \left(B\setminus \left\{x\right\}\right)⟼\left\{p\in B|\exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right\}\right)\in \mathrm{V}$$
45	44	a1i	$$⊢W\in V\to \left(x\in B,y\in \left(B\setminus \left\{x\right\}\right)⟼\left\{p\in B|\exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right\}\right)\in \mathrm{V}$$
46	9 40 41 45	fvmptd3	$$⊢W\in V\to {Line}_M\left(W\right)=\left(x\in B,y\in \left(B\setminus \left\{x\right\}\right)⟼\left\{p\in B|\exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right\}\right)$$
47	2 46	syl5eq	$$⊢W\in V\to L=\left(x\in B,y\in \left(B\setminus \left\{x\right\}\right)⟼\left\{p\in B|\exists t\in Kp=\left(\left(\underset{\dot{}}{1}\underset{\dot{}}{-}t\right)\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}\left(t\underset{\dot{}}{·}y\right)\right\}\right)$$