Metamath Proof Explorer

Theorem rrxlinesc

Description: Definition of lines passing through two different points in a generalized real Euclidean space of finite dimension, expressed by their coordinates. (Contributed by AV, 13-Feb-2023)

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

Proof

Step Hyp Ref Expression
1 rrxlinesc.e 
 |-  E = ( RR^ ` I )
2 rrxlinesc.p 
 |-  P = ( RR ^m I )
3 rrxlinesc.l 
 |-  L = ( LineM ` E )
4 eqid 
 |-  ( .s ` E ) = ( .s ` E )
5 eqid 
 |-  ( +g ` E ) = ( +g ` E )
6 1 2 3 4 5 rrxlines 
 |-  ( I e. Fin -> L = ( x e. P , y e. ( P \ { x } ) |-> { p e. P | E. t e. RR p = ( ( ( 1 - t ) ( .s ` E ) x ) ( +g ` E ) ( t ( .s ` E ) y ) ) } ) )
7 eqid 
 |-  ( Base ` E ) = ( Base ` E )
8 simpll1 
 |-  ( ( ( ( I e. Fin /\ x e. P /\ y e. ( P \ { x } ) ) /\ p e. P ) /\ t e. RR ) -> I e. Fin )
9 1red 
 |-  ( ( ( ( I e. Fin /\ x e. P /\ y e. ( P \ { x } ) ) /\ p e. P ) /\ t e. RR ) -> 1 e. RR )
10 simpr 
 |-  ( ( ( ( I e. Fin /\ x e. P /\ y e. ( P \ { x } ) ) /\ p e. P ) /\ t e. RR ) -> t e. RR )
11 9 10 resubcld 
 |-  ( ( ( ( I e. Fin /\ x e. P /\ y e. ( P \ { x } ) ) /\ p e. P ) /\ t e. RR ) -> ( 1 - t ) e. RR )
12 id 
 |-  ( I e. Fin -> I e. Fin )
13 12 1 7 rrxbasefi 
 |-  ( I e. Fin -> ( Base ` E ) = ( RR ^m I ) )
14 2 13 eqtr4id 
 |-  ( I e. Fin -> P = ( Base ` E ) )
15 14 eleq2d 
 |-  ( I e. Fin -> ( x e. P <-> x e. ( Base ` E ) ) )
16 15 biimpa 
 |-  ( ( I e. Fin /\ x e. P ) -> x e. ( Base ` E ) )
17 16 3adant3 
 |-  ( ( I e. Fin /\ x e. P /\ y e. ( P \ { x } ) ) -> x e. ( Base ` E ) )
18 17 ad2antrr 
 |-  ( ( ( ( I e. Fin /\ x e. P /\ y e. ( P \ { x } ) ) /\ p e. P ) /\ t e. RR ) -> x e. ( Base ` E ) )
19 eldifi 
 |-  ( y e. ( P \ { x } ) -> y e. P )
20 14 eleq2d 
 |-  ( I e. Fin -> ( y e. P <-> y e. ( Base ` E ) ) )
21 19 20 syl5ib 
 |-  ( I e. Fin -> ( y e. ( P \ { x } ) -> y e. ( Base ` E ) ) )
22 21 a1d 
 |-  ( I e. Fin -> ( x e. P -> ( y e. ( P \ { x } ) -> y e. ( Base ` E ) ) ) )
23 22 3imp 
 |-  ( ( I e. Fin /\ x e. P /\ y e. ( P \ { x } ) ) -> y e. ( Base ` E ) )
24 23 ad2antrr 
 |-  ( ( ( ( I e. Fin /\ x e. P /\ y e. ( P \ { x } ) ) /\ p e. P ) /\ t e. RR ) -> y e. ( Base ` E ) )
25 14 3ad2ant1 
 |-  ( ( I e. Fin /\ x e. P /\ y e. ( P \ { x } ) ) -> P = ( Base ` E ) )
26 25 eleq2d 
 |-  ( ( I e. Fin /\ x e. P /\ y e. ( P \ { x } ) ) -> ( p e. P <-> p e. ( Base ` E ) ) )
27 26 biimpa 
 |-  ( ( ( I e. Fin /\ x e. P /\ y e. ( P \ { x } ) ) /\ p e. P ) -> p e. ( Base ` E ) )
28 27 adantr 
 |-  ( ( ( ( I e. Fin /\ x e. P /\ y e. ( P \ { x } ) ) /\ p e. P ) /\ t e. RR ) -> p e. ( Base ` E ) )
29 1 7 4 8 11 18 24 28 5 10 rrxplusgvscavalb 
 |-  ( ( ( ( I e. Fin /\ x e. P /\ y e. ( P \ { x } ) ) /\ p e. P ) /\ t e. RR ) -> ( p = ( ( ( 1 - t ) ( .s ` E ) x ) ( +g ` E ) ( t ( .s ` E ) y ) ) <-> A. i e. I ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) )
30 29 rexbidva 
 |-  ( ( ( I e. Fin /\ x e. P /\ y e. ( P \ { x } ) ) /\ p e. P ) -> ( E. t e. RR p = ( ( ( 1 - t ) ( .s ` E ) x ) ( +g ` E ) ( t ( .s ` E ) y ) ) <-> E. t e. RR A. i e. I ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) )
31 30 rabbidva 
 |-  ( ( I e. Fin /\ x e. P /\ y e. ( P \ { x } ) ) -> { p e. P | E. t e. RR p = ( ( ( 1 - t ) ( .s ` E ) x ) ( +g ` E ) ( t ( .s ` E ) y ) ) } = { p e. P | E. t e. RR A. i e. I ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) } )
32 31 mpoeq3dva 
 |-  ( I e. Fin -> ( x e. P , y e. ( P \ { x } ) |-> { p e. P | E. t e. RR p = ( ( ( 1 - t ) ( .s ` E ) x ) ( +g ` E ) ( t ( .s ` E ) y ) ) } ) = ( x e. P , y e. ( P \ { x } ) |-> { p e. P | E. t e. RR A. i e. I ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) } ) )
33 6 32 eqtrd 
 |-  ( I e. Fin -> L = ( x e. P , y e. ( P \ { x } ) |-> { p e. P | E. t e. RR A. i e. I ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) } ) )