Definition df-line 45963

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.)

Assertion

Ref	Expression
df-line	⊢ LineM = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ ((Base‘𝑤) ∖ {𝑥}) ↦ {𝑝 ∈ (Base‘𝑤) ∣ ∃𝑡 ∈ (Base‘(Scalar‘𝑤))𝑝 = ((((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠 ‘𝑤)𝑥)(+g‘𝑤)(𝑡( ·𝑠 ‘𝑤)𝑦))}))

Distinct variable group:   𝑡,𝑝,𝑤,𝑥,𝑦

Detailed syntax breakdown of Definition df-line

Step	Hyp	Ref	Expression
1		cline 45961	. 2 class LineM
2		vw	. . 3 setvar 𝑤
3		cvv 3422	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5		vy	. . . 4 setvar 𝑦
6	2	cv 1538	. . . . 5 class 𝑤
7		cbs 16840	. . . . 5 class Base
8	6, 7	cfv 6418	. . . 4 class (Base‘𝑤)
9	4	cv 1538	. . . . . 6 class 𝑥
10	9	csn 4558	. . . . 5 class {𝑥}
11	8, 10	cdif 3880	. . . 4 class ((Base‘𝑤) ∖ {𝑥})
12		vp	. . . . . . . 8 setvar 𝑝
13	12	cv 1538	. . . . . . 7 class 𝑝
14		csca 16891	. . . . . . . . . . . 12 class Scalar
15	6, 14	cfv 6418	. . . . . . . . . . 11 class (Scalar‘𝑤)
16		cur 19652	. . . . . . . . . . 11 class 1r
17	15, 16	cfv 6418	. . . . . . . . . 10 class (1r‘(Scalar‘𝑤))
18		vt	. . . . . . . . . . 11 setvar 𝑡
19	18	cv 1538	. . . . . . . . . 10 class 𝑡
20		csg 18494	. . . . . . . . . . 11 class -g
21	15, 20	cfv 6418	. . . . . . . . . 10 class (-g‘(Scalar‘𝑤))
22	17, 19, 21	co 7255	. . . . . . . . 9 class ((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)
23		cvsca 16892	. . . . . . . . . 10 class ·𝑠
24	6, 23	cfv 6418	. . . . . . . . 9 class ( ·𝑠 ‘𝑤)
25	22, 9, 24	co 7255	. . . . . . . 8 class (((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠 ‘𝑤)𝑥)
26	5	cv 1538	. . . . . . . . 9 class 𝑦
27	19, 26, 24	co 7255	. . . . . . . 8 class (𝑡( ·𝑠 ‘𝑤)𝑦)
28		cplusg 16888	. . . . . . . . 9 class +g
29	6, 28	cfv 6418	. . . . . . . 8 class (+g‘𝑤)
30	25, 27, 29	co 7255	. . . . . . 7 class ((((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠 ‘𝑤)𝑥)(+g‘𝑤)(𝑡( ·𝑠 ‘𝑤)𝑦))
31	13, 30	wceq 1539	. . . . . 6 wff 𝑝 = ((((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠 ‘𝑤)𝑥)(+g‘𝑤)(𝑡( ·𝑠 ‘𝑤)𝑦))
32	15, 7	cfv 6418	. . . . . 6 class (Base‘(Scalar‘𝑤))
33	31, 18, 32	wrex 3064	. . . . 5 wff ∃𝑡 ∈ (Base‘(Scalar‘𝑤))𝑝 = ((((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠 ‘𝑤)𝑥)(+g‘𝑤)(𝑡( ·𝑠 ‘𝑤)𝑦))
34	33, 12, 8	crab 3067	. . . 4 class {𝑝 ∈ (Base‘𝑤) ∣ ∃𝑡 ∈ (Base‘(Scalar‘𝑤))𝑝 = ((((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠 ‘𝑤)𝑥)(+g‘𝑤)(𝑡( ·𝑠 ‘𝑤)𝑦))}
35	4, 5, 8, 11, 34	cmpo 7257	. . 3 class (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ ((Base‘𝑤) ∖ {𝑥}) ↦ {𝑝 ∈ (Base‘𝑤) ∣ ∃𝑡 ∈ (Base‘(Scalar‘𝑤))𝑝 = ((((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠 ‘𝑤)𝑥)(+g‘𝑤)(𝑡( ·𝑠 ‘𝑤)𝑦))})
36	2, 3, 35	cmpt 5153	. 2 class (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ ((Base‘𝑤) ∖ {𝑥}) ↦ {𝑝 ∈ (Base‘𝑤) ∣ ∃𝑡 ∈ (Base‘(Scalar‘𝑤))𝑝 = ((((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠 ‘𝑤)𝑥)(+g‘𝑤)(𝑡( ·𝑠 ‘𝑤)𝑦))}))
37	1, 36	wceq 1539	1 wff LineM = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ ((Base‘𝑤) ∖ {𝑥}) ↦ {𝑝 ∈ (Base‘𝑤) ∣ ∃𝑡 ∈ (Base‘(Scalar‘𝑤))𝑝 = ((((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠 ‘𝑤)𝑥)(+g‘𝑤)(𝑡( ·𝑠 ‘𝑤)𝑦))}))

This definition is referenced by:  lines  45965