Metamath Proof Explorer

Theorem rrxlinec

Description: The line passing through the two different points X and Y in a generalized real Euclidean space of finite dimension, expressed by its coordinates. Remark: This proof is shorter and requires less distinct variables than the proof using rrxlinesc . (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 rrxlinec
`|- ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) -> ( X L Y ) = { 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 rrxline
` |-  ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) -> ( X L Y ) = { 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 simplll
` |-  ( ( ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) /\ t e. RR ) -> I e. Fin )`
9 1red
` |-  ( ( ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) /\ t e. RR ) -> 1 e. RR )`
10 simpr
` |-  ( ( ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) /\ t e. RR ) -> t e. RR )`
11 9 10 resubcld
` |-  ( ( ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ 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 13 2 syl6reqr
` |-  ( I e. Fin -> P = ( Base ` E ) )`
15 14 eleq2d
` |-  ( I e. Fin -> ( X e. P <-> X e. ( Base ` E ) ) )`
16 15 biimpcd
` |-  ( X e. P -> ( I e. Fin -> X e. ( Base ` E ) ) )`
` |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( I e. Fin -> X e. ( Base ` E ) ) )`
18 17 impcom
` |-  ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) -> X e. ( Base ` E ) )`
` |-  ( ( ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) /\ t e. RR ) -> X e. ( Base ` E ) )`
20 14 eleq2d
` |-  ( I e. Fin -> ( Y e. P <-> Y e. ( Base ` E ) ) )`
21 20 biimpcd
` |-  ( Y e. P -> ( I e. Fin -> Y e. ( Base ` E ) ) )`
` |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( I e. Fin -> Y e. ( Base ` E ) ) )`
23 22 impcom
` |-  ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) -> Y e. ( Base ` E ) )`
` |-  ( ( ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) /\ t e. RR ) -> Y e. ( Base ` E ) )`
` |-  ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) -> P = ( Base ` E ) )`
26 25 eleq2d
` |-  ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) -> ( p e. P <-> p e. ( Base ` E ) ) )`
27 26 biimpa
` |-  ( ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) -> p e. ( Base ` E ) )`
` |-  ( ( ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) /\ t e. RR ) -> p e. ( Base ` E ) )`
` |-  ( ( ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ 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 =/= Y ) ) /\ 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 =/= Y ) ) -> { 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 =/= Y ) ) -> ( X L Y ) = { p e. P | E. t e. RR A. i e. I ( p ` i ) = ( ( ( 1 - t ) x. ( X ` i ) ) + ( t x. ( Y ` i ) ) ) } )`