Metamath Proof Explorer

Theorem rrxlines

Description: Definition of lines passing through two different points in a generalized real Euclidean space of finite dimension. (Contributed by AV, 14-Jan-2023)

Ref Expression
Hypotheses rrxlines.e 
|- E = ( RR^ ` I )
rrxlines.p 
|- P = ( RR ^m I )
rrxlines.l 
|- L = ( LineM ` E )
rrxlines.m 
|- .x. = ( .s ` E )
rrxlines.a 
|- .+ = ( +g ` E )
Assertion rrxlines 
|- ( I e. Fin -> L = ( x e. P , y e. ( P \ { x } ) |-> { p e. P | E. t e. RR p = ( ( ( 1 - t ) .x. x ) .+ ( t .x. y ) ) } ) )

Proof

Step Hyp Ref Expression
1 rrxlines.e 
 |-  E = ( RR^ ` I )
2 rrxlines.p 
 |-  P = ( RR ^m I )
3 rrxlines.l 
 |-  L = ( LineM ` E )
4 rrxlines.m 
 |-  .x. = ( .s ` E )
5 rrxlines.a 
 |-  .+ = ( +g ` E )
6 1 fvexi 
 |-  E e. _V
7 eqid 
 |-  ( Base ` E ) = ( Base ` E )
8 eqid 
 |-  ( Scalar ` E ) = ( Scalar ` E )
9 eqid 
 |-  ( Base ` ( Scalar ` E ) ) = ( Base ` ( Scalar ` E ) )
10 eqid 
 |-  ( -g ` ( Scalar ` E ) ) = ( -g ` ( Scalar ` E ) )
11 eqid 
 |-  ( 1r ` ( Scalar ` E ) ) = ( 1r ` ( Scalar ` E ) )
12 7 3 8 9 4 5 10 11 lines 
 |-  ( E e. _V -> L = ( x e. ( Base ` E ) , y e. ( ( Base ` E ) \ { x } ) |-> { p e. ( Base ` E ) | E. t e. ( Base ` ( Scalar ` E ) ) p = ( ( ( ( 1r ` ( Scalar ` E ) ) ( -g ` ( Scalar ` E ) ) t ) .x. x ) .+ ( t .x. y ) ) } ) )
13 6 12 mp1i 
 |-  ( I e. Fin -> L = ( x e. ( Base ` E ) , y e. ( ( Base ` E ) \ { x } ) |-> { p e. ( Base ` E ) | E. t e. ( Base ` ( Scalar ` E ) ) p = ( ( ( ( 1r ` ( Scalar ` E ) ) ( -g ` ( Scalar ` E ) ) t ) .x. x ) .+ ( t .x. y ) ) } ) )
14 id 
 |-  ( I e. Fin -> I e. Fin )
15 14 1 7 rrxbasefi 
 |-  ( I e. Fin -> ( Base ` E ) = ( RR ^m I ) )
16 15 2 eqtr4di 
 |-  ( I e. Fin -> ( Base ` E ) = P )
17 16 difeq1d 
 |-  ( I e. Fin -> ( ( Base ` E ) \ { x } ) = ( P \ { x } ) )
18 1 rrxsca 
 |-  ( I e. Fin -> ( Scalar ` E ) = RRfld )
19 18 fveq2d 
 |-  ( I e. Fin -> ( Base ` ( Scalar ` E ) ) = ( Base ` RRfld ) )
20 rebase 
 |-  RR = ( Base ` RRfld )
21 19 20 eqtr4di 
 |-  ( I e. Fin -> ( Base ` ( Scalar ` E ) ) = RR )
22 18 fveq2d 
 |-  ( I e. Fin -> ( 1r ` ( Scalar ` E ) ) = ( 1r ` RRfld ) )
23 re1r 
 |-  1 = ( 1r ` RRfld )
24 22 23 eqtr4di 
 |-  ( I e. Fin -> ( 1r ` ( Scalar ` E ) ) = 1 )
25 24 oveq1d 
 |-  ( I e. Fin -> ( ( 1r ` ( Scalar ` E ) ) ( -g ` ( Scalar ` E ) ) t ) = ( 1 ( -g ` ( Scalar ` E ) ) t ) )
26 25 adantr 
 |-  ( ( I e. Fin /\ t e. ( Base ` ( Scalar ` E ) ) ) -> ( ( 1r ` ( Scalar ` E ) ) ( -g ` ( Scalar ` E ) ) t ) = ( 1 ( -g ` ( Scalar ` E ) ) t ) )
27 18 fveq2d 
 |-  ( I e. Fin -> ( -g ` ( Scalar ` E ) ) = ( -g ` RRfld ) )
28 27 oveqd 
 |-  ( I e. Fin -> ( 1 ( -g ` ( Scalar ` E ) ) t ) = ( 1 ( -g ` RRfld ) t ) )
29 28 adantr 
 |-  ( ( I e. Fin /\ t e. ( Base ` ( Scalar ` E ) ) ) -> ( 1 ( -g ` ( Scalar ` E ) ) t ) = ( 1 ( -g ` RRfld ) t ) )
30 21 eleq2d 
 |-  ( I e. Fin -> ( t e. ( Base ` ( Scalar ` E ) ) <-> t e. RR ) )
31 1re 
 |-  1 e. RR
32 eqid 
 |-  ( -g ` RRfld ) = ( -g ` RRfld )
33 32 resubgval 
 |-  ( ( 1 e. RR /\ t e. RR ) -> ( 1 - t ) = ( 1 ( -g ` RRfld ) t ) )
34 33 eqcomd 
 |-  ( ( 1 e. RR /\ t e. RR ) -> ( 1 ( -g ` RRfld ) t ) = ( 1 - t ) )
35 31 34 mpan 
 |-  ( t e. RR -> ( 1 ( -g ` RRfld ) t ) = ( 1 - t ) )
36 30 35 syl6bi 
 |-  ( I e. Fin -> ( t e. ( Base ` ( Scalar ` E ) ) -> ( 1 ( -g ` RRfld ) t ) = ( 1 - t ) ) )
37 36 imp 
 |-  ( ( I e. Fin /\ t e. ( Base ` ( Scalar ` E ) ) ) -> ( 1 ( -g ` RRfld ) t ) = ( 1 - t ) )
38 26 29 37 3eqtrd 
 |-  ( ( I e. Fin /\ t e. ( Base ` ( Scalar ` E ) ) ) -> ( ( 1r ` ( Scalar ` E ) ) ( -g ` ( Scalar ` E ) ) t ) = ( 1 - t ) )
39 38 oveq1d 
 |-  ( ( I e. Fin /\ t e. ( Base ` ( Scalar ` E ) ) ) -> ( ( ( 1r ` ( Scalar ` E ) ) ( -g ` ( Scalar ` E ) ) t ) .x. x ) = ( ( 1 - t ) .x. x ) )
40 39 oveq1d 
 |-  ( ( I e. Fin /\ t e. ( Base ` ( Scalar ` E ) ) ) -> ( ( ( ( 1r ` ( Scalar ` E ) ) ( -g ` ( Scalar ` E ) ) t ) .x. x ) .+ ( t .x. y ) ) = ( ( ( 1 - t ) .x. x ) .+ ( t .x. y ) ) )
41 40 eqeq2d 
 |-  ( ( I e. Fin /\ t e. ( Base ` ( Scalar ` E ) ) ) -> ( p = ( ( ( ( 1r ` ( Scalar ` E ) ) ( -g ` ( Scalar ` E ) ) t ) .x. x ) .+ ( t .x. y ) ) <-> p = ( ( ( 1 - t ) .x. x ) .+ ( t .x. y ) ) ) )
42 21 41 rexeqbidva 
 |-  ( I e. Fin -> ( E. t e. ( Base ` ( Scalar ` E ) ) p = ( ( ( ( 1r ` ( Scalar ` E ) ) ( -g ` ( Scalar ` E ) ) t ) .x. x ) .+ ( t .x. y ) ) <-> E. t e. RR p = ( ( ( 1 - t ) .x. x ) .+ ( t .x. y ) ) ) )
43 16 42 rabeqbidv 
 |-  ( I e. Fin -> { p e. ( Base ` E ) | E. t e. ( Base ` ( Scalar ` E ) ) p = ( ( ( ( 1r ` ( Scalar ` E ) ) ( -g ` ( Scalar ` E ) ) t ) .x. x ) .+ ( t .x. y ) ) } = { p e. P | E. t e. RR p = ( ( ( 1 - t ) .x. x ) .+ ( t .x. y ) ) } )
44 16 17 43 mpoeq123dv 
 |-  ( I e. Fin -> ( x e. ( Base ` E ) , y e. ( ( Base ` E ) \ { x } ) |-> { p e. ( Base ` E ) | E. t e. ( Base ` ( Scalar ` E ) ) p = ( ( ( ( 1r ` ( Scalar ` E ) ) ( -g ` ( Scalar ` E ) ) t ) .x. x ) .+ ( t .x. y ) ) } ) = ( x e. P , y e. ( P \ { x } ) |-> { p e. P | E. t e. RR p = ( ( ( 1 - t ) .x. x ) .+ ( t .x. y ) ) } ) )
45 13 44 eqtrd 
 |-  ( I e. Fin -> L = ( x e. P , y e. ( P \ { x } ) |-> { p e. P | E. t e. RR p = ( ( ( 1 - t ) .x. x ) .+ ( t .x. y ) ) } ) )