Metamath Proof Explorer

Theorem rrxline

Description: The line passing through the two different points X and Y 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 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 ) .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 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 ) .x. x ) .+ ( t .x. y ) ) } ) )
7 6 oveqd 
 |-  ( I e. Fin -> ( X L Y ) = ( X ( x e. P , y e. ( P \ { x } ) |-> { p e. P | E. t e. RR p = ( ( ( 1 - t ) .x. x ) .+ ( t .x. y ) ) } ) Y ) )
8 7 adantr 
 |-  ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) -> ( X L Y ) = ( X ( x e. P , y e. ( P \ { x } ) |-> { p e. P | E. t e. RR p = ( ( ( 1 - t ) .x. x ) .+ ( t .x. y ) ) } ) Y ) )
9 eqidd 
 |-  ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) -> ( x e. P , y e. ( P \ { x } ) |-> { p e. P | E. t e. RR p = ( ( ( 1 - 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 ) ) } ) )
10 simpl 
 |-  ( ( x = X /\ y = Y ) -> x = X )
11 10 oveq2d 
 |-  ( ( x = X /\ y = Y ) -> ( ( 1 - t ) .x. x ) = ( ( 1 - t ) .x. X ) )
12 simpr 
 |-  ( ( x = X /\ y = Y ) -> y = Y )
13 12 oveq2d 
 |-  ( ( x = X /\ y = Y ) -> ( t .x. y ) = ( t .x. Y ) )
14 11 13 oveq12d 
 |-  ( ( x = X /\ y = Y ) -> ( ( ( 1 - t ) .x. x ) .+ ( t .x. y ) ) = ( ( ( 1 - t ) .x. X ) .+ ( t .x. Y ) ) )
15 14 eqeq2d 
 |-  ( ( x = X /\ y = Y ) -> ( p = ( ( ( 1 - t ) .x. x ) .+ ( t .x. y ) ) <-> p = ( ( ( 1 - t ) .x. X ) .+ ( t .x. Y ) ) ) )
16 15 rexbidv 
 |-  ( ( x = X /\ y = Y ) -> ( E. t e. RR p = ( ( ( 1 - t ) .x. x ) .+ ( t .x. y ) ) <-> E. t e. RR p = ( ( ( 1 - t ) .x. X ) .+ ( t .x. Y ) ) ) )
17 16 rabbidv 
 |-  ( ( x = X /\ y = Y ) -> { p e. P | E. t e. RR p = ( ( ( 1 - t ) .x. x ) .+ ( t .x. y ) ) } = { p e. P | E. t e. RR p = ( ( ( 1 - t ) .x. X ) .+ ( t .x. Y ) ) } )
18 17 adantl 
 |-  ( ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ ( x = X /\ y = Y ) ) -> { p e. P | E. t e. RR p = ( ( ( 1 - t ) .x. x ) .+ ( t .x. y ) ) } = { p e. P | E. t e. RR p = ( ( ( 1 - t ) .x. X ) .+ ( t .x. Y ) ) } )
19 sneq 
 |-  ( x = X -> { x } = { X } )
20 19 difeq2d 
 |-  ( x = X -> ( P \ { x } ) = ( P \ { X } ) )
21 20 adantl 
 |-  ( ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ x = X ) -> ( P \ { x } ) = ( P \ { X } ) )
22 simpr1 
 |-  ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) -> X e. P )
23 id 
 |-  ( X =/= Y -> X =/= Y )
24 23 necomd 
 |-  ( X =/= Y -> Y =/= X )
25 24 anim2i 
 |-  ( ( Y e. P /\ X =/= Y ) -> ( Y e. P /\ Y =/= X ) )
26 25 3adant1 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( Y e. P /\ Y =/= X ) )
27 eldifsn 
 |-  ( Y e. ( P \ { X } ) <-> ( Y e. P /\ Y =/= X ) )
28 26 27 sylibr 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> Y e. ( P \ { X } ) )
29 28 adantl 
 |-  ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) -> Y e. ( P \ { X } ) )
30 2 ovexi 
 |-  P e. _V
31 30 rabex 
 |-  { p e. P | E. t e. RR p = ( ( ( 1 - t ) .x. X ) .+ ( t .x. Y ) ) } e. _V
32 31 a1i 
 |-  ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) -> { p e. P | E. t e. RR p = ( ( ( 1 - t ) .x. X ) .+ ( t .x. Y ) ) } e. _V )
33 9 18 21 22 29 32 ovmpodx 
 |-  ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) -> ( X ( x e. P , y e. ( P \ { x } ) |-> { p e. P | E. t e. RR p = ( ( ( 1 - t ) .x. x ) .+ ( t .x. y ) ) } ) Y ) = { p e. P | E. t e. RR p = ( ( ( 1 - t ) .x. X ) .+ ( t .x. Y ) ) } )
34 8 33 eqtrd 
 |-  ( ( I e. Fin /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) -> ( X L Y ) = { p e. P | E. t e. RR p = ( ( ( 1 - t ) .x. X ) .+ ( t .x. Y ) ) } )