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 
|- LineM = ( w e. _V |-> ( x e. ( Base ` w ) , y e. ( ( Base ` w ) \ { x } ) |-> { p e. ( Base ` w ) | E. t e. ( Base ` ( Scalar ` w ) ) p = ( ( ( ( 1r ` ( Scalar ` w ) ) ( -g ` ( Scalar ` w ) ) t ) ( .s ` w ) x ) ( +g ` w ) ( t ( .s ` w ) y ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cline 
 |-  LineM
1 vw 
 |-  w
2 cvv 
 |-  _V
3 vx 
 |-  x
4 cbs 
 |-  Base
5 1 cv 
 |-  w
6 5 4 cfv 
 |-  ( Base ` w )
7 vy 
 |-  y
8 3 cv 
 |-  x
9 8 csn 
 |-  { x }
10 6 9 cdif 
 |-  ( ( Base ` w ) \ { x } )
11 vp 
 |-  p
12 vt 
 |-  t
13 csca 
 |-  Scalar
14 5 13 cfv 
 |-  ( Scalar ` w )
15 14 4 cfv 
 |-  ( Base ` ( Scalar ` w ) )
16 11 cv 
 |-  p
17 cur 
 |-  1r
18 14 17 cfv 
 |-  ( 1r ` ( Scalar ` w ) )
19 csg 
 |-  -g
20 14 19 cfv 
 |-  ( -g ` ( Scalar ` w ) )
21 12 cv 
 |-  t
22 18 21 20 co 
 |-  ( ( 1r ` ( Scalar ` w ) ) ( -g ` ( Scalar ` w ) ) t )
23 cvsca 
 |-  .s
24 5 23 cfv 
 |-  ( .s ` w )
25 22 8 24 co 
 |-  ( ( ( 1r ` ( Scalar ` w ) ) ( -g ` ( Scalar ` w ) ) t ) ( .s ` w ) x )
26 cplusg 
 |-  +g
27 5 26 cfv 
 |-  ( +g ` w )
28 7 cv 
 |-  y
29 21 28 24 co 
 |-  ( t ( .s ` w ) y )
30 25 29 27 co 
 |-  ( ( ( ( 1r ` ( Scalar ` w ) ) ( -g ` ( Scalar ` w ) ) t ) ( .s ` w ) x ) ( +g ` w ) ( t ( .s ` w ) y ) )
31 16 30 wceq 
 |-  p = ( ( ( ( 1r ` ( Scalar ` w ) ) ( -g ` ( Scalar ` w ) ) t ) ( .s ` w ) x ) ( +g ` w ) ( t ( .s ` w ) y ) )
32 31 12 15 wrex 
 |-  E. t e. ( Base ` ( Scalar ` w ) ) p = ( ( ( ( 1r ` ( Scalar ` w ) ) ( -g ` ( Scalar ` w ) ) t ) ( .s ` w ) x ) ( +g ` w ) ( t ( .s ` w ) y ) )
33 32 11 6 crab 
 |-  { p e. ( Base ` w ) | E. t e. ( Base ` ( Scalar ` w ) ) p = ( ( ( ( 1r ` ( Scalar ` w ) ) ( -g ` ( Scalar ` w ) ) t ) ( .s ` w ) x ) ( +g ` w ) ( t ( .s ` w ) y ) ) }
34 3 7 6 10 33 cmpo 
 |-  ( x e. ( Base ` w ) , y e. ( ( Base ` w ) \ { x } ) |-> { p e. ( Base ` w ) | E. t e. ( Base ` ( Scalar ` w ) ) p = ( ( ( ( 1r ` ( Scalar ` w ) ) ( -g ` ( Scalar ` w ) ) t ) ( .s ` w ) x ) ( +g ` w ) ( t ( .s ` w ) y ) ) } )
35 1 2 34 cmpt 
 |-  ( w e. _V |-> ( x e. ( Base ` w ) , y e. ( ( Base ` w ) \ { x } ) |-> { p e. ( Base ` w ) | E. t e. ( Base ` ( Scalar ` w ) ) p = ( ( ( ( 1r ` ( Scalar ` w ) ) ( -g ` ( Scalar ` w ) ) t ) ( .s ` w ) x ) ( +g ` w ) ( t ( .s ` w ) y ) ) } ) )
36 0 35 wceq 
 |-  LineM = ( w e. _V |-> ( x e. ( Base ` w ) , y e. ( ( Base ` w ) \ { x } ) |-> { p e. ( Base ` w ) | E. t e. ( Base ` ( Scalar ` w ) ) p = ( ( ( ( 1r ` ( Scalar ` w ) ) ( -g ` ( Scalar ` w ) ) t ) ( .s ` w ) x ) ( +g ` w ) ( t ( .s ` w ) y ) ) } ) )