Metamath Proof Explorer

Theorem eenglngeehlnmlem1

Description: Lemma 1 for eenglngeehlnm . (Contributed by AV, 15-Feb-2023)

Ref Expression
Assertion eenglngeehlnmlem1 
|- ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) -> ( ( E. k e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) \/ E. l e. ( 0 [,) 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) \/ E. m e. ( 0 (,] 1 ) A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) ) -> E. t e. RR A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( k = t -> ( 1 - k ) = ( 1 - t ) )
2 1 oveq1d 
 |-  ( k = t -> ( ( 1 - k ) x. ( x ` i ) ) = ( ( 1 - t ) x. ( x ` i ) ) )
3 oveq1 
 |-  ( k = t -> ( k x. ( y ` i ) ) = ( t x. ( y ` i ) ) )
4 2 3 oveq12d 
 |-  ( k = t -> ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) )
5 4 eqeq2d 
 |-  ( k = t -> ( ( p ` i ) = ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) <-> ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) )
6 5 ralbidv 
 |-  ( k = t -> ( A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) <-> A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) )
7 6 cbvrexvw 
 |-  ( E. k e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) )
8 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
9 ssrexv 
 |-  ( ( 0 [,] 1 ) C_ RR -> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) -> E. t e. RR A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) )
10 8 9 mp1i 
 |-  ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) -> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) -> E. t e. RR A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) )
11 7 10 syl5bi 
 |-  ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) -> ( E. k e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) -> E. t e. RR A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) )
12 0re 
 |-  0 e. RR
13 1xr 
 |-  1 e. RR*
14 elico2 
 |-  ( ( 0 e. RR /\ 1 e. RR* ) -> ( l e. ( 0 [,) 1 ) <-> ( l e. RR /\ 0 <_ l /\ l < 1 ) ) )
15 12 13 14 mp2an 
 |-  ( l e. ( 0 [,) 1 ) <-> ( l e. RR /\ 0 <_ l /\ l < 1 ) )
16 simp1 
 |-  ( ( l e. RR /\ 0 <_ l /\ l < 1 ) -> l e. RR )
17 1red 
 |-  ( ( l e. RR /\ 0 <_ l /\ l < 1 ) -> 1 e. RR )
18 17 16 resubcld 
 |-  ( ( l e. RR /\ 0 <_ l /\ l < 1 ) -> ( 1 - l ) e. RR )
19 1cnd 
 |-  ( ( l e. RR /\ 0 <_ l /\ l < 1 ) -> 1 e. CC )
20 16 recnd 
 |-  ( ( l e. RR /\ 0 <_ l /\ l < 1 ) -> l e. CC )
21 ltne 
 |-  ( ( l e. RR /\ l < 1 ) -> 1 =/= l )
22 21 3adant2 
 |-  ( ( l e. RR /\ 0 <_ l /\ l < 1 ) -> 1 =/= l )
23 19 20 22 subne0d 
 |-  ( ( l e. RR /\ 0 <_ l /\ l < 1 ) -> ( 1 - l ) =/= 0 )
24 16 18 23 redivcld 
 |-  ( ( l e. RR /\ 0 <_ l /\ l < 1 ) -> ( l / ( 1 - l ) ) e. RR )
25 15 24 sylbi 
 |-  ( l e. ( 0 [,) 1 ) -> ( l / ( 1 - l ) ) e. RR )
26 25 ad2antlr 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) ) -> ( l / ( 1 - l ) ) e. RR )
27 26 renegcld 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) ) -> -u ( l / ( 1 - l ) ) e. RR )
28 oveq2 
 |-  ( t = -u ( l / ( 1 - l ) ) -> ( 1 - t ) = ( 1 - -u ( l / ( 1 - l ) ) ) )
29 28 oveq1d 
 |-  ( t = -u ( l / ( 1 - l ) ) -> ( ( 1 - t ) x. ( x ` i ) ) = ( ( 1 - -u ( l / ( 1 - l ) ) ) x. ( x ` i ) ) )
30 oveq1 
 |-  ( t = -u ( l / ( 1 - l ) ) -> ( t x. ( y ` i ) ) = ( -u ( l / ( 1 - l ) ) x. ( y ` i ) ) )
31 29 30 oveq12d 
 |-  ( t = -u ( l / ( 1 - l ) ) -> ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) = ( ( ( 1 - -u ( l / ( 1 - l ) ) ) x. ( x ` i ) ) + ( -u ( l / ( 1 - l ) ) x. ( y ` i ) ) ) )
32 31 eqeq2d 
 |-  ( t = -u ( l / ( 1 - l ) ) -> ( ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) <-> ( p ` i ) = ( ( ( 1 - -u ( l / ( 1 - l ) ) ) x. ( x ` i ) ) + ( -u ( l / ( 1 - l ) ) x. ( y ` i ) ) ) ) )
33 32 ralbidv 
 |-  ( t = -u ( l / ( 1 - l ) ) -> ( A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) <-> A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - -u ( l / ( 1 - l ) ) ) x. ( x ` i ) ) + ( -u ( l / ( 1 - l ) ) x. ( y ` i ) ) ) ) )
34 33 adantl 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) ) /\ t = -u ( l / ( 1 - l ) ) ) -> ( A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) <-> A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - -u ( l / ( 1 - l ) ) ) x. ( x ` i ) ) + ( -u ( l / ( 1 - l ) ) x. ( y ` i ) ) ) ) )
35 eqcom 
 |-  ( ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) <-> ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) = ( x ` i ) )
36 elmapi 
 |-  ( x e. ( RR ^m ( 1 ... N ) ) -> x : ( 1 ... N ) --> RR )
37 36 3ad2ant2 
 |-  ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) -> x : ( 1 ... N ) --> RR )
38 37 ad2antrr 
 |-  ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) -> x : ( 1 ... N ) --> RR )
39 38 ffvelrnda 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( x ` i ) e. RR )
40 39 recnd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( x ` i ) e. CC )
41 15 16 sylbi 
 |-  ( l e. ( 0 [,) 1 ) -> l e. RR )
42 41 ad2antlr 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> l e. RR )
43 42 recnd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> l e. CC )
44 eldifi 
 |-  ( y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) -> y e. ( RR ^m ( 1 ... N ) ) )
45 elmapi 
 |-  ( y e. ( RR ^m ( 1 ... N ) ) -> y : ( 1 ... N ) --> RR )
46 44 45 syl 
 |-  ( y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) -> y : ( 1 ... N ) --> RR )
47 46 3ad2ant3 
 |-  ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) -> y : ( 1 ... N ) --> RR )
48 47 ad2antrr 
 |-  ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) -> y : ( 1 ... N ) --> RR )
49 48 ffvelrnda 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( y ` i ) e. RR )
50 49 recnd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( y ` i ) e. CC )
51 43 50 mulcld 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( l x. ( y ` i ) ) e. CC )
52 1cnd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> 1 e. CC )
53 52 43 subcld 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( 1 - l ) e. CC )
54 elmapi 
 |-  ( p e. ( RR ^m ( 1 ... N ) ) -> p : ( 1 ... N ) --> RR )
55 54 ad2antlr 
 |-  ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) -> p : ( 1 ... N ) --> RR )
56 55 ffvelrnda 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( p ` i ) e. RR )
57 56 recnd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( p ` i ) e. CC )
58 53 57 mulcld 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( 1 - l ) x. ( p ` i ) ) e. CC )
59 40 51 58 subadd2d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( x ` i ) - ( l x. ( y ` i ) ) ) = ( ( 1 - l ) x. ( p ` i ) ) <-> ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) = ( x ` i ) ) )
60 35 59 bitr4id 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) <-> ( ( x ` i ) - ( l x. ( y ` i ) ) ) = ( ( 1 - l ) x. ( p ` i ) ) ) )
61 eqcom 
 |-  ( ( ( x ` i ) - ( l x. ( y ` i ) ) ) = ( ( 1 - l ) x. ( p ` i ) ) <-> ( ( 1 - l ) x. ( p ` i ) ) = ( ( x ` i ) - ( l x. ( y ` i ) ) ) )
62 40 51 subcld 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( x ` i ) - ( l x. ( y ` i ) ) ) e. CC )
63 15 22 sylbi 
 |-  ( l e. ( 0 [,) 1 ) -> 1 =/= l )
64 63 ad2antlr 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> 1 =/= l )
65 52 43 64 subne0d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( 1 - l ) =/= 0 )
66 62 53 57 65 divmuld 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( x ` i ) - ( l x. ( y ` i ) ) ) / ( 1 - l ) ) = ( p ` i ) <-> ( ( 1 - l ) x. ( p ` i ) ) = ( ( x ` i ) - ( l x. ( y ` i ) ) ) ) )
67 61 66 bitr4id 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( x ` i ) - ( l x. ( y ` i ) ) ) = ( ( 1 - l ) x. ( p ` i ) ) <-> ( ( ( x ` i ) - ( l x. ( y ` i ) ) ) / ( 1 - l ) ) = ( p ` i ) ) )
68 eqcom 
 |-  ( ( ( ( x ` i ) - ( l x. ( y ` i ) ) ) / ( 1 - l ) ) = ( p ` i ) <-> ( p ` i ) = ( ( ( x ` i ) - ( l x. ( y ` i ) ) ) / ( 1 - l ) ) )
69 40 51 53 65 divsubdird 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( x ` i ) - ( l x. ( y ` i ) ) ) / ( 1 - l ) ) = ( ( ( x ` i ) / ( 1 - l ) ) - ( ( l x. ( y ` i ) ) / ( 1 - l ) ) ) )
70 40 53 65 divrec2d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( x ` i ) / ( 1 - l ) ) = ( ( 1 / ( 1 - l ) ) x. ( x ` i ) ) )
71 43 50 53 65 div23d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( l x. ( y ` i ) ) / ( 1 - l ) ) = ( ( l / ( 1 - l ) ) x. ( y ` i ) ) )
72 70 71 oveq12d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( x ` i ) / ( 1 - l ) ) - ( ( l x. ( y ` i ) ) / ( 1 - l ) ) ) = ( ( ( 1 / ( 1 - l ) ) x. ( x ` i ) ) - ( ( l / ( 1 - l ) ) x. ( y ` i ) ) ) )
73 69 72 eqtrd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( x ` i ) - ( l x. ( y ` i ) ) ) / ( 1 - l ) ) = ( ( ( 1 / ( 1 - l ) ) x. ( x ` i ) ) - ( ( l / ( 1 - l ) ) x. ( y ` i ) ) ) )
74 73 eqeq2d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( p ` i ) = ( ( ( x ` i ) - ( l x. ( y ` i ) ) ) / ( 1 - l ) ) <-> ( p ` i ) = ( ( ( 1 / ( 1 - l ) ) x. ( x ` i ) ) - ( ( l / ( 1 - l ) ) x. ( y ` i ) ) ) ) )
75 68 74 syl5bb 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( x ` i ) - ( l x. ( y ` i ) ) ) / ( 1 - l ) ) = ( p ` i ) <-> ( p ` i ) = ( ( ( 1 / ( 1 - l ) ) x. ( x ` i ) ) - ( ( l / ( 1 - l ) ) x. ( y ` i ) ) ) ) )
76 43 53 65 divcld 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( l / ( 1 - l ) ) e. CC )
77 76 50 mulneg1d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( -u ( l / ( 1 - l ) ) x. ( y ` i ) ) = -u ( ( l / ( 1 - l ) ) x. ( y ` i ) ) )
78 77 eqcomd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> -u ( ( l / ( 1 - l ) ) x. ( y ` i ) ) = ( -u ( l / ( 1 - l ) ) x. ( y ` i ) ) )
79 78 oveq2d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 / ( 1 - l ) ) x. ( x ` i ) ) + -u ( ( l / ( 1 - l ) ) x. ( y ` i ) ) ) = ( ( ( 1 / ( 1 - l ) ) x. ( x ` i ) ) + ( -u ( l / ( 1 - l ) ) x. ( y ` i ) ) ) )
80 53 65 reccld 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( 1 / ( 1 - l ) ) e. CC )
81 80 40 mulcld 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( 1 / ( 1 - l ) ) x. ( x ` i ) ) e. CC )
82 76 50 mulcld 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( l / ( 1 - l ) ) x. ( y ` i ) ) e. CC )
83 81 82 negsubd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 / ( 1 - l ) ) x. ( x ` i ) ) + -u ( ( l / ( 1 - l ) ) x. ( y ` i ) ) ) = ( ( ( 1 / ( 1 - l ) ) x. ( x ` i ) ) - ( ( l / ( 1 - l ) ) x. ( y ` i ) ) ) )
84 52 76 subnegd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( 1 - -u ( l / ( 1 - l ) ) ) = ( 1 + ( l / ( 1 - l ) ) ) )
85 muldivdir 
 |-  ( ( 1 e. CC /\ l e. CC /\ ( ( 1 - l ) e. CC /\ ( 1 - l ) =/= 0 ) ) -> ( ( ( ( 1 - l ) x. 1 ) + l ) / ( 1 - l ) ) = ( 1 + ( l / ( 1 - l ) ) ) )
86 52 43 53 65 85 syl112anc 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( 1 - l ) x. 1 ) + l ) / ( 1 - l ) ) = ( 1 + ( l / ( 1 - l ) ) ) )
87 53 mulid1d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( 1 - l ) x. 1 ) = ( 1 - l ) )
88 87 oveq1d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - l ) x. 1 ) + l ) = ( ( 1 - l ) + l ) )
89 52 43 npcand 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( 1 - l ) + l ) = 1 )
90 88 89 eqtrd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - l ) x. 1 ) + l ) = 1 )
91 90 oveq1d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( 1 - l ) x. 1 ) + l ) / ( 1 - l ) ) = ( 1 / ( 1 - l ) ) )
92 84 86 91 3eqtr2d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( 1 - -u ( l / ( 1 - l ) ) ) = ( 1 / ( 1 - l ) ) )
93 92 eqcomd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( 1 / ( 1 - l ) ) = ( 1 - -u ( l / ( 1 - l ) ) ) )
94 93 oveq1d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( 1 / ( 1 - l ) ) x. ( x ` i ) ) = ( ( 1 - -u ( l / ( 1 - l ) ) ) x. ( x ` i ) ) )
95 94 oveq1d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 / ( 1 - l ) ) x. ( x ` i ) ) + ( -u ( l / ( 1 - l ) ) x. ( y ` i ) ) ) = ( ( ( 1 - -u ( l / ( 1 - l ) ) ) x. ( x ` i ) ) + ( -u ( l / ( 1 - l ) ) x. ( y ` i ) ) ) )
96 79 83 95 3eqtr3d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 / ( 1 - l ) ) x. ( x ` i ) ) - ( ( l / ( 1 - l ) ) x. ( y ` i ) ) ) = ( ( ( 1 - -u ( l / ( 1 - l ) ) ) x. ( x ` i ) ) + ( -u ( l / ( 1 - l ) ) x. ( y ` i ) ) ) )
97 96 eqeq2d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( p ` i ) = ( ( ( 1 / ( 1 - l ) ) x. ( x ` i ) ) - ( ( l / ( 1 - l ) ) x. ( y ` i ) ) ) <-> ( p ` i ) = ( ( ( 1 - -u ( l / ( 1 - l ) ) ) x. ( x ` i ) ) + ( -u ( l / ( 1 - l ) ) x. ( y ` i ) ) ) ) )
98 97 biimpd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( p ` i ) = ( ( ( 1 / ( 1 - l ) ) x. ( x ` i ) ) - ( ( l / ( 1 - l ) ) x. ( y ` i ) ) ) -> ( p ` i ) = ( ( ( 1 - -u ( l / ( 1 - l ) ) ) x. ( x ` i ) ) + ( -u ( l / ( 1 - l ) ) x. ( y ` i ) ) ) ) )
99 75 98 sylbid 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( x ` i ) - ( l x. ( y ` i ) ) ) / ( 1 - l ) ) = ( p ` i ) -> ( p ` i ) = ( ( ( 1 - -u ( l / ( 1 - l ) ) ) x. ( x ` i ) ) + ( -u ( l / ( 1 - l ) ) x. ( y ` i ) ) ) ) )
100 67 99 sylbid 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( x ` i ) - ( l x. ( y ` i ) ) ) = ( ( 1 - l ) x. ( p ` i ) ) -> ( p ` i ) = ( ( ( 1 - -u ( l / ( 1 - l ) ) ) x. ( x ` i ) ) + ( -u ( l / ( 1 - l ) ) x. ( y ` i ) ) ) ) )
101 60 100 sylbid 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) -> ( p ` i ) = ( ( ( 1 - -u ( l / ( 1 - l ) ) ) x. ( x ` i ) ) + ( -u ( l / ( 1 - l ) ) x. ( y ` i ) ) ) ) )
102 101 ralimdva 
 |-  ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) -> ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) -> A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - -u ( l / ( 1 - l ) ) ) x. ( x ` i ) ) + ( -u ( l / ( 1 - l ) ) x. ( y ` i ) ) ) ) )
103 102 imp 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) ) -> A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - -u ( l / ( 1 - l ) ) ) x. ( x ` i ) ) + ( -u ( l / ( 1 - l ) ) x. ( y ` i ) ) ) )
104 27 34 103 rspcedvd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ l e. ( 0 [,) 1 ) ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) ) -> E. t e. RR A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) )
105 104 rexlimdva2 
 |-  ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) -> ( E. l e. ( 0 [,) 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) -> E. t e. RR A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) )
106 0xr 
 |-  0 e. RR*
107 1re 
 |-  1 e. RR
108 elioc2 
 |-  ( ( 0 e. RR* /\ 1 e. RR ) -> ( m e. ( 0 (,] 1 ) <-> ( m e. RR /\ 0 < m /\ m <_ 1 ) ) )
109 106 107 108 mp2an 
 |-  ( m e. ( 0 (,] 1 ) <-> ( m e. RR /\ 0 < m /\ m <_ 1 ) )
110 simp1 
 |-  ( ( m e. RR /\ 0 < m /\ m <_ 1 ) -> m e. RR )
111 gt0ne0 
 |-  ( ( m e. RR /\ 0 < m ) -> m =/= 0 )
112 111 3adant3 
 |-  ( ( m e. RR /\ 0 < m /\ m <_ 1 ) -> m =/= 0 )
113 110 112 rereccld 
 |-  ( ( m e. RR /\ 0 < m /\ m <_ 1 ) -> ( 1 / m ) e. RR )
114 109 113 sylbi 
 |-  ( m e. ( 0 (,] 1 ) -> ( 1 / m ) e. RR )
115 114 ad2antlr 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) ) -> ( 1 / m ) e. RR )
116 oveq2 
 |-  ( t = ( 1 / m ) -> ( 1 - t ) = ( 1 - ( 1 / m ) ) )
117 116 oveq1d 
 |-  ( t = ( 1 / m ) -> ( ( 1 - t ) x. ( x ` i ) ) = ( ( 1 - ( 1 / m ) ) x. ( x ` i ) ) )
118 oveq1 
 |-  ( t = ( 1 / m ) -> ( t x. ( y ` i ) ) = ( ( 1 / m ) x. ( y ` i ) ) )
119 117 118 oveq12d 
 |-  ( t = ( 1 / m ) -> ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) = ( ( ( 1 - ( 1 / m ) ) x. ( x ` i ) ) + ( ( 1 / m ) x. ( y ` i ) ) ) )
120 119 eqeq2d 
 |-  ( t = ( 1 / m ) -> ( ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) <-> ( p ` i ) = ( ( ( 1 - ( 1 / m ) ) x. ( x ` i ) ) + ( ( 1 / m ) x. ( y ` i ) ) ) ) )
121 120 ralbidv 
 |-  ( t = ( 1 / m ) -> ( A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) <-> A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - ( 1 / m ) ) x. ( x ` i ) ) + ( ( 1 / m ) x. ( y ` i ) ) ) ) )
122 121 adantl 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) ) /\ t = ( 1 / m ) ) -> ( A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) <-> A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - ( 1 / m ) ) x. ( x ` i ) ) + ( ( 1 / m ) x. ( y ` i ) ) ) ) )
123 eqcom 
 |-  ( ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) <-> ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) = ( y ` i ) )
124 47 ad2antrr 
 |-  ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) -> y : ( 1 ... N ) --> RR )
125 124 ffvelrnda 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( y ` i ) e. RR )
126 125 recnd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( y ` i ) e. CC )
127 1cnd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> 1 e. CC )
128 109 110 sylbi 
 |-  ( m e. ( 0 (,] 1 ) -> m e. RR )
129 128 recnd 
 |-  ( m e. ( 0 (,] 1 ) -> m e. CC )
130 129 ad2antlr 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> m e. CC )
131 127 130 subcld 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( 1 - m ) e. CC )
132 37 ad2antrr 
 |-  ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) -> x : ( 1 ... N ) --> RR )
133 132 ffvelrnda 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( x ` i ) e. RR )
134 133 recnd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( x ` i ) e. CC )
135 131 134 mulcld 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( 1 - m ) x. ( x ` i ) ) e. CC )
136 126 135 negsubd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( y ` i ) + -u ( ( 1 - m ) x. ( x ` i ) ) ) = ( ( y ` i ) - ( ( 1 - m ) x. ( x ` i ) ) ) )
137 131 134 mulneg1d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( -u ( 1 - m ) x. ( x ` i ) ) = -u ( ( 1 - m ) x. ( x ` i ) ) )
138 127 130 negsubdi2d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> -u ( 1 - m ) = ( m - 1 ) )
139 138 oveq1d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( -u ( 1 - m ) x. ( x ` i ) ) = ( ( m - 1 ) x. ( x ` i ) ) )
140 137 139 eqtr3d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> -u ( ( 1 - m ) x. ( x ` i ) ) = ( ( m - 1 ) x. ( x ` i ) ) )
141 140 oveq2d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( y ` i ) + -u ( ( 1 - m ) x. ( x ` i ) ) ) = ( ( y ` i ) + ( ( m - 1 ) x. ( x ` i ) ) ) )
142 136 141 eqtr3d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( y ` i ) - ( ( 1 - m ) x. ( x ` i ) ) ) = ( ( y ` i ) + ( ( m - 1 ) x. ( x ` i ) ) ) )
143 142 eqeq1d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( y ` i ) - ( ( 1 - m ) x. ( x ` i ) ) ) = ( m x. ( p ` i ) ) <-> ( ( y ` i ) + ( ( m - 1 ) x. ( x ` i ) ) ) = ( m x. ( p ` i ) ) ) )
144 54 ad2antlr 
 |-  ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) -> p : ( 1 ... N ) --> RR )
145 144 ffvelrnda 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( p ` i ) e. RR )
146 145 recnd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( p ` i ) e. CC )
147 130 146 mulcld 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( m x. ( p ` i ) ) e. CC )
148 126 135 147 subaddd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( y ` i ) - ( ( 1 - m ) x. ( x ` i ) ) ) = ( m x. ( p ` i ) ) <-> ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) = ( y ` i ) ) )
149 eqcom 
 |-  ( ( ( ( y ` i ) + ( ( m - 1 ) x. ( x ` i ) ) ) / m ) = ( p ` i ) <-> ( p ` i ) = ( ( ( y ` i ) + ( ( m - 1 ) x. ( x ` i ) ) ) / m ) )
150 149 a1i 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( y ` i ) + ( ( m - 1 ) x. ( x ` i ) ) ) / m ) = ( p ` i ) <-> ( p ` i ) = ( ( ( y ` i ) + ( ( m - 1 ) x. ( x ` i ) ) ) / m ) ) )
151 130 127 subcld 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( m - 1 ) e. CC )
152 151 134 mulcld 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( m - 1 ) x. ( x ` i ) ) e. CC )
153 126 152 addcld 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( y ` i ) + ( ( m - 1 ) x. ( x ` i ) ) ) e. CC )
154 elioc1 
 |-  ( ( 0 e. RR* /\ 1 e. RR* ) -> ( m e. ( 0 (,] 1 ) <-> ( m e. RR* /\ 0 < m /\ m <_ 1 ) ) )
155 106 13 154 mp2an 
 |-  ( m e. ( 0 (,] 1 ) <-> ( m e. RR* /\ 0 < m /\ m <_ 1 ) )
156 12 a1i 
 |-  ( m e. RR* -> 0 e. RR )
157 156 anim1i 
 |-  ( ( m e. RR* /\ 0 < m ) -> ( 0 e. RR /\ 0 < m ) )
158 157 3adant3 
 |-  ( ( m e. RR* /\ 0 < m /\ m <_ 1 ) -> ( 0 e. RR /\ 0 < m ) )
159 ltne 
 |-  ( ( 0 e. RR /\ 0 < m ) -> m =/= 0 )
160 158 159 syl 
 |-  ( ( m e. RR* /\ 0 < m /\ m <_ 1 ) -> m =/= 0 )
161 155 160 sylbi 
 |-  ( m e. ( 0 (,] 1 ) -> m =/= 0 )
162 161 ad2antlr 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> m =/= 0 )
163 153 146 130 162 divmul2d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( y ` i ) + ( ( m - 1 ) x. ( x ` i ) ) ) / m ) = ( p ` i ) <-> ( ( y ` i ) + ( ( m - 1 ) x. ( x ` i ) ) ) = ( m x. ( p ` i ) ) ) )
164 126 152 130 162 divdird 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( y ` i ) + ( ( m - 1 ) x. ( x ` i ) ) ) / m ) = ( ( ( y ` i ) / m ) + ( ( ( m - 1 ) x. ( x ` i ) ) / m ) ) )
165 126 130 162 divrec2d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( y ` i ) / m ) = ( ( 1 / m ) x. ( y ` i ) ) )
166 151 134 130 162 div23d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( m - 1 ) x. ( x ` i ) ) / m ) = ( ( ( m - 1 ) / m ) x. ( x ` i ) ) )
167 130 127 130 162 divsubdird 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( m - 1 ) / m ) = ( ( m / m ) - ( 1 / m ) ) )
168 167 oveq1d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( m - 1 ) / m ) x. ( x ` i ) ) = ( ( ( m / m ) - ( 1 / m ) ) x. ( x ` i ) ) )
169 166 168 eqtrd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( m - 1 ) x. ( x ` i ) ) / m ) = ( ( ( m / m ) - ( 1 / m ) ) x. ( x ` i ) ) )
170 165 169 oveq12d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( y ` i ) / m ) + ( ( ( m - 1 ) x. ( x ` i ) ) / m ) ) = ( ( ( 1 / m ) x. ( y ` i ) ) + ( ( ( m / m ) - ( 1 / m ) ) x. ( x ` i ) ) ) )
171 164 170 eqtrd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( y ` i ) + ( ( m - 1 ) x. ( x ` i ) ) ) / m ) = ( ( ( 1 / m ) x. ( y ` i ) ) + ( ( ( m / m ) - ( 1 / m ) ) x. ( x ` i ) ) ) )
172 171 eqeq2d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( p ` i ) = ( ( ( y ` i ) + ( ( m - 1 ) x. ( x ` i ) ) ) / m ) <-> ( p ` i ) = ( ( ( 1 / m ) x. ( y ` i ) ) + ( ( ( m / m ) - ( 1 / m ) ) x. ( x ` i ) ) ) ) )
173 150 163 172 3bitr3d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( y ` i ) + ( ( m - 1 ) x. ( x ` i ) ) ) = ( m x. ( p ` i ) ) <-> ( p ` i ) = ( ( ( 1 / m ) x. ( y ` i ) ) + ( ( ( m / m ) - ( 1 / m ) ) x. ( x ` i ) ) ) ) )
174 143 148 173 3bitr3d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) = ( y ` i ) <-> ( p ` i ) = ( ( ( 1 / m ) x. ( y ` i ) ) + ( ( ( m / m ) - ( 1 / m ) ) x. ( x ` i ) ) ) ) )
175 123 174 syl5bb 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) <-> ( p ` i ) = ( ( ( 1 / m ) x. ( y ` i ) ) + ( ( ( m / m ) - ( 1 / m ) ) x. ( x ` i ) ) ) ) )
176 130 162 reccld 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( 1 / m ) e. CC )
177 176 126 mulcld 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( 1 / m ) x. ( y ` i ) ) e. CC )
178 127 176 subcld 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( 1 - ( 1 / m ) ) e. CC )
179 178 134 mulcld 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( 1 - ( 1 / m ) ) x. ( x ` i ) ) e. CC )
180 130 162 dividd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( m / m ) = 1 )
181 180 oveq1d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( m / m ) - ( 1 / m ) ) = ( 1 - ( 1 / m ) ) )
182 181 oveq1d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( m / m ) - ( 1 / m ) ) x. ( x ` i ) ) = ( ( 1 - ( 1 / m ) ) x. ( x ` i ) ) )
183 182 oveq2d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 / m ) x. ( y ` i ) ) + ( ( ( m / m ) - ( 1 / m ) ) x. ( x ` i ) ) ) = ( ( ( 1 / m ) x. ( y ` i ) ) + ( ( 1 - ( 1 / m ) ) x. ( x ` i ) ) ) )
184 177 179 183 comraddd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 / m ) x. ( y ` i ) ) + ( ( ( m / m ) - ( 1 / m ) ) x. ( x ` i ) ) ) = ( ( ( 1 - ( 1 / m ) ) x. ( x ` i ) ) + ( ( 1 / m ) x. ( y ` i ) ) ) )
185 184 eqeq2d 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( p ` i ) = ( ( ( 1 / m ) x. ( y ` i ) ) + ( ( ( m / m ) - ( 1 / m ) ) x. ( x ` i ) ) ) <-> ( p ` i ) = ( ( ( 1 - ( 1 / m ) ) x. ( x ` i ) ) + ( ( 1 / m ) x. ( y ` i ) ) ) ) )
186 185 biimpd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( p ` i ) = ( ( ( 1 / m ) x. ( y ` i ) ) + ( ( ( m / m ) - ( 1 / m ) ) x. ( x ` i ) ) ) -> ( p ` i ) = ( ( ( 1 - ( 1 / m ) ) x. ( x ` i ) ) + ( ( 1 / m ) x. ( y ` i ) ) ) ) )
187 175 186 sylbid 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) -> ( p ` i ) = ( ( ( 1 - ( 1 / m ) ) x. ( x ` i ) ) + ( ( 1 / m ) x. ( y ` i ) ) ) ) )
188 187 ralimdva 
 |-  ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) -> ( A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) -> A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - ( 1 / m ) ) x. ( x ` i ) ) + ( ( 1 / m ) x. ( y ` i ) ) ) ) )
189 188 imp 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) ) -> A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - ( 1 / m ) ) x. ( x ` i ) ) + ( ( 1 / m ) x. ( y ` i ) ) ) )
190 115 122 189 rspcedvd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ m e. ( 0 (,] 1 ) ) /\ A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) ) -> E. t e. RR A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) )
191 190 rexlimdva2 
 |-  ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) -> ( E. m e. ( 0 (,] 1 ) A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) -> E. t e. RR A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) )
192 11 105 191 3jaod 
 |-  ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) -> ( ( E. k e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) \/ E. l e. ( 0 [,) 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) \/ E. m e. ( 0 (,] 1 ) A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) ) -> E. t e. RR A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) )