Definition df-line

Description: Definition of 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
Assertion	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)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cline	$$class{Line}_M$$
1		vw	$$setvarw$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarw$$
6	5 4	cfv	$$class{\mathrm{Base}}_w$$
7		vy	$$setvary$$
8	3	cv	$$setvarx$$
9	8	csn	$$class\left\{x\right\}$$
10	6 9	cdif	$$class\left({\mathrm{Base}}_w\setminus \left\{x\right\}\right)$$
11		vp	$$setvarp$$
12		vt	$$setvart$$
13		csca	$$class\mathrm{Scalar}$$
14	5 13	cfv	$$class\mathrm{Scalar}\left(w\right)$$
15	14 4	cfv	$$class{\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}$$
16	11	cv	$$setvarp$$
17		cur	$$class{1}_r$$
18	14 17	cfv	$$class{1}_{\mathrm{Scalar}\left(w\right)}$$
19		csg	$$class{-}_{𝑔}$$
20	14 19	cfv	$$class{-}_{\mathrm{Scalar}\left(w\right)}$$
21	12	cv	$$setvart$$
22	18 21 20	co	$$class\left(1_{\mathrm{Scalar}\left(w\right)}{-}_{\mathrm{Scalar}\left(w\right)}t\right)$$
23		cvsca	$$class{\cdot }_{𝑠}$$
24	5 23	cfv	$$class{\cdot }_w$$
25	22 8 24	co	$$class\left(\left(1_{\mathrm{Scalar}\left(w\right)}{-}_{\mathrm{Scalar}\left(w\right)}t\right){\cdot }_{w}x\right)$$
26		cplusg	$$class{+}_{𝑔}$$
27	5 26	cfv	$$class{+}_w$$
28	7	cv	$$setvary$$
29	21 28 24	co	$$class\left(t{\cdot }_{w}y\right)$$
30	25 29 27	co	$$class\left(\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)$$
31	16 30	wceq	$$wffp=\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)$$
32	31 12 15	wrex	$$wff\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)$$
33	32 11 6	crab	$$class\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\}$$
34	3 7 6 10 33	cmpo	$$class\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)$$
35	1 2 34	cmpt	$$class\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)$$
36	0 35	wceq	$$wff{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)$$