# 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 ) )`
` |-  ( ( I e. Fin /\ x e. P /\ y e. ( P \ { x } ) ) -> x e. ( Base ` E ) )`
` |-  ( ( ( ( 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 ) )`
` |-  ( ( ( ( I e. Fin /\ x e. P /\ y e. ( P \ { x } ) ) /\ p e. P ) /\ t e. RR ) -> y e. ( Base ` E ) )`
` |-  ( ( 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 ) )`
` |-  ( ( ( ( I e. Fin /\ x e. P /\ y e. ( P \ { x } ) ) /\ p e. P ) /\ t e. RR ) -> p e. ( Base ` E ) )`
` |-  ( ( ( ( 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 ) ) ) ) )`
` |-  ( ( ( 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 ) ) ) ) )`
` |-  ( ( 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 ) ) ) } )`
` |-  ( 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 ) ) ) } ) )`
` |-  ( 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 ) ) ) } ) )`