Metamath Proof Explorer

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 = ( Base ` W )
lines.l 
|- L = ( LineM ` W )
lines.s 
|- S = ( Scalar ` W )
lines.k 
|- K = ( Base ` S )
lines.p 
|- .x. = ( .s ` W )
lines.a 
|- .+ = ( +g ` W )
lines.m 
|- .- = ( -g ` S )
lines.1 
|- .1. = ( 1r ` S )
Assertion lines 
|- ( W e. V -> L = ( x e. B , y e. ( B \ { x } ) |-> { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) } ) )

Proof

Step Hyp Ref Expression
1 lines.b 
 |-  B = ( Base ` W )
2 lines.l 
 |-  L = ( LineM ` W )
3 lines.s 
 |-  S = ( Scalar ` W )
4 lines.k 
 |-  K = ( Base ` S )
5 lines.p 
 |-  .x. = ( .s ` W )
6 lines.a 
 |-  .+ = ( +g ` W )
7 lines.m 
 |-  .- = ( -g ` S )
8 lines.1 
 |-  .1. = ( 1r ` S )
9 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 ) ) } ) )
10 fveq2 
 |-  ( W = w -> ( Base ` W ) = ( Base ` w ) )
11 1 10 eqtrid 
 |-  ( W = w -> B = ( Base ` w ) )
12 11 difeq1d 
 |-  ( W = w -> ( B \ { x } ) = ( ( Base ` w ) \ { x } ) )
13 fveq2 
 |-  ( W = w -> ( Scalar ` W ) = ( Scalar ` w ) )
14 3 13 eqtrid 
 |-  ( W = w -> S = ( Scalar ` w ) )
15 14 fveq2d 
 |-  ( W = w -> ( Base ` S ) = ( Base ` ( Scalar ` w ) ) )
16 4 15 eqtrid 
 |-  ( W = w -> K = ( Base ` ( Scalar ` w ) ) )
17 fveq2 
 |-  ( W = w -> ( +g ` W ) = ( +g ` w ) )
18 6 17 eqtrid 
 |-  ( W = w -> .+ = ( +g ` w ) )
19 fveq2 
 |-  ( W = w -> ( .s ` W ) = ( .s ` w ) )
20 5 19 eqtrid 
 |-  ( W = w -> .x. = ( .s ` w ) )
21 3 fveq2i 
 |-  ( -g ` S ) = ( -g ` ( Scalar ` W ) )
22 7 21 eqtri 
 |-  .- = ( -g ` ( Scalar ` W ) )
23 2fveq3 
 |-  ( W = w -> ( -g ` ( Scalar ` W ) ) = ( -g ` ( Scalar ` w ) ) )
24 22 23 eqtrid 
 |-  ( W = w -> .- = ( -g ` ( Scalar ` w ) ) )
25 3 fveq2i 
 |-  ( 1r ` S ) = ( 1r ` ( Scalar ` W ) )
26 8 25 eqtri 
 |-  .1. = ( 1r ` ( Scalar ` W ) )
27 2fveq3 
 |-  ( W = w -> ( 1r ` ( Scalar ` W ) ) = ( 1r ` ( Scalar ` w ) ) )
28 26 27 eqtrid 
 |-  ( W = w -> .1. = ( 1r ` ( Scalar ` w ) ) )
29 eqidd 
 |-  ( W = w -> t = t )
30 24 28 29 oveq123d 
 |-  ( W = w -> ( .1. .- t ) = ( ( 1r ` ( Scalar ` w ) ) ( -g ` ( Scalar ` w ) ) t ) )
31 eqidd 
 |-  ( W = w -> x = x )
32 20 30 31 oveq123d 
 |-  ( W = w -> ( ( .1. .- t ) .x. x ) = ( ( ( 1r ` ( Scalar ` w ) ) ( -g ` ( Scalar ` w ) ) t ) ( .s ` w ) x ) )
33 20 oveqd 
 |-  ( W = w -> ( t .x. y ) = ( t ( .s ` w ) y ) )
34 18 32 33 oveq123d 
 |-  ( W = w -> ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) = ( ( ( ( 1r ` ( Scalar ` w ) ) ( -g ` ( Scalar ` w ) ) t ) ( .s ` w ) x ) ( +g ` w ) ( t ( .s ` w ) y ) ) )
35 34 eqeq2d 
 |-  ( W = w -> ( p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) <-> p = ( ( ( ( 1r ` ( Scalar ` w ) ) ( -g ` ( Scalar ` w ) ) t ) ( .s ` w ) x ) ( +g ` w ) ( t ( .s ` w ) y ) ) ) )
36 16 35 rexeqbidv 
 |-  ( W = w -> ( E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) <-> E. t e. ( Base ` ( Scalar ` w ) ) p = ( ( ( ( 1r ` ( Scalar ` w ) ) ( -g ` ( Scalar ` w ) ) t ) ( .s ` w ) x ) ( +g ` w ) ( t ( .s ` w ) y ) ) ) )
37 11 36 rabeqbidv 
 |-  ( W = w -> { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) } = { 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 ) ) } )
38 11 12 37 mpoeq123dv 
 |-  ( W = w -> ( x e. B , y e. ( B \ { x } ) |-> { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) } ) = ( 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 ) ) } ) )
39 38 eqcomd 
 |-  ( W = w -> ( 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 ) ) } ) = ( x e. B , y e. ( B \ { x } ) |-> { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) } ) )
40 39 eqcoms 
 |-  ( w = W -> ( 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 ) ) } ) = ( x e. B , y e. ( B \ { x } ) |-> { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) } ) )
41 elex 
 |-  ( W e. V -> W e. _V )
42 1 fvexi 
 |-  B e. _V
43 42 difexi 
 |-  ( B \ { x } ) e. _V
44 42 43 mpoex 
 |-  ( x e. B , y e. ( B \ { x } ) |-> { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) } ) e. _V
45 44 a1i 
 |-  ( W e. V -> ( x e. B , y e. ( B \ { x } ) |-> { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) } ) e. _V )
46 9 40 41 45 fvmptd3 
 |-  ( W e. V -> ( LineM ` W ) = ( x e. B , y e. ( B \ { x } ) |-> { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) } ) )
47 2 46 eqtrid 
 |-  ( W e. V -> L = ( x e. B , y e. ( B \ { x } ) |-> { p e. B | E. t e. K p = ( ( ( .1. .- t ) .x. x ) .+ ( t .x. y ) ) } ) )