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 2 13 eqtr4id 
 |-  ( 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 ) ) )
17 16 3ad2ant1 
 |-  ( ( 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 ) )
19 18 ad2antrr 
 |-  ( ( ( ( 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 ) ) )
22 21 3ad2ant2 
 |-  ( ( 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 ) )
24 23 ad2antrr 
 |-  ( ( ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) /\ t e. RR ) -> Y e. ( Base ` E ) )
25 14 adantr 
 |-  ( ( 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 ) )
28 27 adantr 
 |-  ( ( ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ p e. P ) /\ t e. RR ) -> p e. ( Base ` E ) )
29 1 7 4 8 11 19 24 28 5 10 rrxplusgvscavalb 
 |-  ( ( ( ( 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 ) ) ) ) )
30 29 rexbidva 
 |-  ( ( ( 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 ) ) ) ) )
31 30 rabbidva 
 |-  ( ( 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 ) ) ) } )
32 6 31 eqtrd 
 |-  ( ( 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 ) ) ) } )