Metamath Proof Explorer


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 = w V x Base w , y Base w x p Base w | t Base Scalar w p = 1 Scalar w - Scalar w t w x + w t w y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cline class Line M
1 vw setvar w
2 cvv class V
3 vx setvar x
4 cbs class Base
5 1 cv setvar w
6 5 4 cfv class Base w
7 vy setvar y
8 3 cv setvar x
9 8 csn class x
10 6 9 cdif class Base w x
11 vp setvar p
12 vt setvar t
13 csca class Scalar
14 5 13 cfv class Scalar w
15 14 4 cfv class Base Scalar w
16 11 cv setvar p
17 cur class 1 r
18 14 17 cfv class 1 Scalar w
19 csg class - 𝑔
20 14 19 cfv class - Scalar w
21 12 cv setvar t
22 18 21 20 co class 1 Scalar w - Scalar w t
23 cvsca class 𝑠
24 5 23 cfv class w
25 22 8 24 co class 1 Scalar w - Scalar w t w x
26 cplusg class + 𝑔
27 5 26 cfv class + w
28 7 cv setvar y
29 21 28 24 co class t w y
30 25 29 27 co class 1 Scalar w - Scalar w t w x + w t w y
31 16 30 wceq wff p = 1 Scalar w - Scalar w t w x + w t w y
32 31 12 15 wrex wff t Base Scalar w p = 1 Scalar w - Scalar w t w x + w t w y
33 32 11 6 crab class p Base w | t Base Scalar w p = 1 Scalar w - Scalar w t w x + w t w y
34 3 7 6 10 33 cmpo class x Base w , y Base w x p Base w | t Base Scalar w p = 1 Scalar w - Scalar w t w x + w t w y
35 1 2 34 cmpt class w V x Base w , y Base w x p Base w | t Base Scalar w p = 1 Scalar w - Scalar w t w x + w t w y
36 0 35 wceq wff Line M = w V x Base w , y Base w x p Base w | t Base Scalar w p = 1 Scalar w - Scalar w t w x + w t w y