Metamath Proof Explorer

Theorem axcontlem2

Description: Lemma for axcont . The idea here is to set up a mapping F that will allow us to transfer dedekind to two sets of points. Here, we set up F and show its domain and range. (Contributed by Scott Fenton, 17-Jun-2013)

Ref Expression
Hypotheses axcontlem2.1 
|- D = { p e. ( EE ` N ) | ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) }
axcontlem2.2 
|- F = { <. x , t >. | ( x e. D /\ ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) }
Assertion axcontlem2 
|- ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> F : D -1-1-onto-> ( 0 [,) +oo ) )

Proof

Step Hyp Ref Expression
1 axcontlem2.1 
 |-  D = { p e. ( EE ` N ) | ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) }
2 axcontlem2.2 
 |-  F = { <. x , t >. | ( x e. D /\ ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) }
3 opeq2 
 |-  ( p = x -> <. Z , p >. = <. Z , x >. )
4 3 breq2d 
 |-  ( p = x -> ( U Btwn <. Z , p >. <-> U Btwn <. Z , x >. ) )
5 breq1 
 |-  ( p = x -> ( p Btwn <. Z , U >. <-> x Btwn <. Z , U >. ) )
6 4 5 orbi12d 
 |-  ( p = x -> ( ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) <-> ( U Btwn <. Z , x >. \/ x Btwn <. Z , U >. ) ) )
7 6 1 elrab2 
 |-  ( x e. D <-> ( x e. ( EE ` N ) /\ ( U Btwn <. Z , x >. \/ x Btwn <. Z , U >. ) ) )
8 simpll3 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) -> U e. ( EE ` N ) )
9 simpll2 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) -> Z e. ( EE ` N ) )
10 simpr 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) -> x e. ( EE ` N ) )
11 brbtwn 
 |-  ( ( U e. ( EE ` N ) /\ Z e. ( EE ` N ) /\ x e. ( EE ` N ) ) -> ( U Btwn <. Z , x >. <-> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) )
12 8 9 10 11 syl3anc 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) -> ( U Btwn <. Z , x >. <-> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) )
13 12 biimpa 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ U Btwn <. Z , x >. ) -> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) )
14 simp-4r 
 |-  ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) -> Z =/= U )
15 oveq2 
 |-  ( s = 0 -> ( 1 - s ) = ( 1 - 0 ) )
16 1m0e1 
 |-  ( 1 - 0 ) = 1
17 15 16 eqtrdi 
 |-  ( s = 0 -> ( 1 - s ) = 1 )
18 17 oveq1d 
 |-  ( s = 0 -> ( ( 1 - s ) x. ( Z ` i ) ) = ( 1 x. ( Z ` i ) ) )
19 oveq1 
 |-  ( s = 0 -> ( s x. ( x ` i ) ) = ( 0 x. ( x ` i ) ) )
20 18 19 oveq12d 
 |-  ( s = 0 -> ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) = ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( x ` i ) ) ) )
21 20 eqeq2d 
 |-  ( s = 0 -> ( ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) <-> ( U ` i ) = ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( x ` i ) ) ) ) )
22 21 ralbidv 
 |-  ( s = 0 -> ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) <-> A. i e. ( 1 ... N ) ( U ` i ) = ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( x ` i ) ) ) ) )
23 22 biimpac 
 |-  ( ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) /\ s = 0 ) -> A. i e. ( 1 ... N ) ( U ` i ) = ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( x ` i ) ) ) )
24 eqcom 
 |-  ( Z = U <-> U = Z )
25 8 adantr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) -> U e. ( EE ` N ) )
26 9 adantr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) -> Z e. ( EE ` N ) )
27 eqeefv 
 |-  ( ( U e. ( EE ` N ) /\ Z e. ( EE ` N ) ) -> ( U = Z <-> A. i e. ( 1 ... N ) ( U ` i ) = ( Z ` i ) ) )
28 25 26 27 syl2anc 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) -> ( U = Z <-> A. i e. ( 1 ... N ) ( U ` i ) = ( Z ` i ) ) )
29 9 ad2antrr 
 |-  ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ i e. ( 1 ... N ) ) -> Z e. ( EE ` N ) )
30 fveecn 
 |-  ( ( Z e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( Z ` i ) e. CC )
31 29 30 sylancom 
 |-  ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( Z ` i ) e. CC )
32 fveecn 
 |-  ( ( x e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( x ` i ) e. CC )
33 32 ad4ant24 
 |-  ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( x ` i ) e. CC )
34 mulid2 
 |-  ( ( Z ` i ) e. CC -> ( 1 x. ( Z ` i ) ) = ( Z ` i ) )
35 mul02 
 |-  ( ( x ` i ) e. CC -> ( 0 x. ( x ` i ) ) = 0 )
36 34 35 oveqan12d 
 |-  ( ( ( Z ` i ) e. CC /\ ( x ` i ) e. CC ) -> ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( x ` i ) ) ) = ( ( Z ` i ) + 0 ) )
37 addid1 
 |-  ( ( Z ` i ) e. CC -> ( ( Z ` i ) + 0 ) = ( Z ` i ) )
38 37 adantr 
 |-  ( ( ( Z ` i ) e. CC /\ ( x ` i ) e. CC ) -> ( ( Z ` i ) + 0 ) = ( Z ` i ) )
39 36 38 eqtrd 
 |-  ( ( ( Z ` i ) e. CC /\ ( x ` i ) e. CC ) -> ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( x ` i ) ) ) = ( Z ` i ) )
40 39 eqeq2d 
 |-  ( ( ( Z ` i ) e. CC /\ ( x ` i ) e. CC ) -> ( ( U ` i ) = ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( x ` i ) ) ) <-> ( U ` i ) = ( Z ` i ) ) )
41 31 33 40 syl2anc 
 |-  ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( U ` i ) = ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( x ` i ) ) ) <-> ( U ` i ) = ( Z ` i ) ) )
42 41 ralbidva 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) -> ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( x ` i ) ) ) <-> A. i e. ( 1 ... N ) ( U ` i ) = ( Z ` i ) ) )
43 28 42 bitr4d 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) -> ( U = Z <-> A. i e. ( 1 ... N ) ( U ` i ) = ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( x ` i ) ) ) ) )
44 24 43 syl5bb 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) -> ( Z = U <-> A. i e. ( 1 ... N ) ( U ` i ) = ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( x ` i ) ) ) ) )
45 23 44 syl5ibr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) -> ( ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) /\ s = 0 ) -> Z = U ) )
46 45 expdimp 
 |-  ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) -> ( s = 0 -> Z = U ) )
47 46 necon3d 
 |-  ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) -> ( Z =/= U -> s =/= 0 ) )
48 14 47 mpd 
 |-  ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) -> s =/= 0 )
49 elicc01 
 |-  ( s e. ( 0 [,] 1 ) <-> ( s e. RR /\ 0 <_ s /\ s <_ 1 ) )
50 49 simp1bi 
 |-  ( s e. ( 0 [,] 1 ) -> s e. RR )
51 rereccl 
 |-  ( ( s e. RR /\ s =/= 0 ) -> ( 1 / s ) e. RR )
52 50 51 sylan 
 |-  ( ( s e. ( 0 [,] 1 ) /\ s =/= 0 ) -> ( 1 / s ) e. RR )
53 50 adantr 
 |-  ( ( s e. ( 0 [,] 1 ) /\ s =/= 0 ) -> s e. RR )
54 49 simp2bi 
 |-  ( s e. ( 0 [,] 1 ) -> 0 <_ s )
55 54 adantr 
 |-  ( ( s e. ( 0 [,] 1 ) /\ s =/= 0 ) -> 0 <_ s )
56 simpr 
 |-  ( ( s e. ( 0 [,] 1 ) /\ s =/= 0 ) -> s =/= 0 )
57 53 55 56 ne0gt0d 
 |-  ( ( s e. ( 0 [,] 1 ) /\ s =/= 0 ) -> 0 < s )
58 1re 
 |-  1 e. RR
59 0le1 
 |-  0 <_ 1
60 divge0 
 |-  ( ( ( 1 e. RR /\ 0 <_ 1 ) /\ ( s e. RR /\ 0 < s ) ) -> 0 <_ ( 1 / s ) )
61 58 59 60 mpanl12 
 |-  ( ( s e. RR /\ 0 < s ) -> 0 <_ ( 1 / s ) )
62 53 57 61 syl2anc 
 |-  ( ( s e. ( 0 [,] 1 ) /\ s =/= 0 ) -> 0 <_ ( 1 / s ) )
63 elrege0 
 |-  ( ( 1 / s ) e. ( 0 [,) +oo ) <-> ( ( 1 / s ) e. RR /\ 0 <_ ( 1 / s ) ) )
64 52 62 63 sylanbrc 
 |-  ( ( s e. ( 0 [,] 1 ) /\ s =/= 0 ) -> ( 1 / s ) e. ( 0 [,) +oo ) )
65 64 adantll 
 |-  ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ s =/= 0 ) -> ( 1 / s ) e. ( 0 [,) +oo ) )
66 50 ad3antlr 
 |-  ( ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ s =/= 0 ) /\ i e. ( 1 ... N ) ) -> s e. RR )
67 66 recnd 
 |-  ( ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ s =/= 0 ) /\ i e. ( 1 ... N ) ) -> s e. CC )
68 simplr 
 |-  ( ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ s =/= 0 ) /\ i e. ( 1 ... N ) ) -> s =/= 0 )
69 32 ad5ant25 
 |-  ( ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ s =/= 0 ) /\ i e. ( 1 ... N ) ) -> ( x ` i ) e. CC )
70 9 ad3antrrr 
 |-  ( ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ s =/= 0 ) /\ i e. ( 1 ... N ) ) -> Z e. ( EE ` N ) )
71 70 30 sylancom 
 |-  ( ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ s =/= 0 ) /\ i e. ( 1 ... N ) ) -> ( Z ` i ) e. CC )
72 ax-1cn 
 |-  1 e. CC
73 reccl 
 |-  ( ( s e. CC /\ s =/= 0 ) -> ( 1 / s ) e. CC )
74 subcl 
 |-  ( ( 1 e. CC /\ ( 1 / s ) e. CC ) -> ( 1 - ( 1 / s ) ) e. CC )
75 72 73 74 sylancr 
 |-  ( ( s e. CC /\ s =/= 0 ) -> ( 1 - ( 1 / s ) ) e. CC )
76 75 adantr 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( 1 - ( 1 / s ) ) e. CC )
77 subcl 
 |-  ( ( 1 e. CC /\ s e. CC ) -> ( 1 - s ) e. CC )
78 72 77 mpan 
 |-  ( s e. CC -> ( 1 - s ) e. CC )
79 78 adantr 
 |-  ( ( s e. CC /\ s =/= 0 ) -> ( 1 - s ) e. CC )
80 73 79 mulcld 
 |-  ( ( s e. CC /\ s =/= 0 ) -> ( ( 1 / s ) x. ( 1 - s ) ) e. CC )
81 80 adantr 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( 1 / s ) x. ( 1 - s ) ) e. CC )
82 simprr 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( Z ` i ) e. CC )
83 76 81 82 adddird 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( ( 1 - ( 1 / s ) ) + ( ( 1 / s ) x. ( 1 - s ) ) ) x. ( Z ` i ) ) = ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( ( 1 / s ) x. ( 1 - s ) ) x. ( Z ` i ) ) ) )
84 simpl 
 |-  ( ( s e. CC /\ s =/= 0 ) -> s e. CC )
85 subdi 
 |-  ( ( ( 1 / s ) e. CC /\ 1 e. CC /\ s e. CC ) -> ( ( 1 / s ) x. ( 1 - s ) ) = ( ( ( 1 / s ) x. 1 ) - ( ( 1 / s ) x. s ) ) )
86 72 85 mp3an2 
 |-  ( ( ( 1 / s ) e. CC /\ s e. CC ) -> ( ( 1 / s ) x. ( 1 - s ) ) = ( ( ( 1 / s ) x. 1 ) - ( ( 1 / s ) x. s ) ) )
87 73 84 86 syl2anc 
 |-  ( ( s e. CC /\ s =/= 0 ) -> ( ( 1 / s ) x. ( 1 - s ) ) = ( ( ( 1 / s ) x. 1 ) - ( ( 1 / s ) x. s ) ) )
88 87 oveq2d 
 |-  ( ( s e. CC /\ s =/= 0 ) -> ( ( 1 - ( 1 / s ) ) + ( ( 1 / s ) x. ( 1 - s ) ) ) = ( ( 1 - ( 1 / s ) ) + ( ( ( 1 / s ) x. 1 ) - ( ( 1 / s ) x. s ) ) ) )
89 73 mulid1d 
 |-  ( ( s e. CC /\ s =/= 0 ) -> ( ( 1 / s ) x. 1 ) = ( 1 / s ) )
90 recid2 
 |-  ( ( s e. CC /\ s =/= 0 ) -> ( ( 1 / s ) x. s ) = 1 )
91 89 90 oveq12d 
 |-  ( ( s e. CC /\ s =/= 0 ) -> ( ( ( 1 / s ) x. 1 ) - ( ( 1 / s ) x. s ) ) = ( ( 1 / s ) - 1 ) )
92 91 oveq2d 
 |-  ( ( s e. CC /\ s =/= 0 ) -> ( ( 1 - ( 1 / s ) ) + ( ( ( 1 / s ) x. 1 ) - ( ( 1 / s ) x. s ) ) ) = ( ( 1 - ( 1 / s ) ) + ( ( 1 / s ) - 1 ) ) )
93 addsubass 
 |-  ( ( ( 1 - ( 1 / s ) ) e. CC /\ ( 1 / s ) e. CC /\ 1 e. CC ) -> ( ( ( 1 - ( 1 / s ) ) + ( 1 / s ) ) - 1 ) = ( ( 1 - ( 1 / s ) ) + ( ( 1 / s ) - 1 ) ) )
94 72 93 mp3an3 
 |-  ( ( ( 1 - ( 1 / s ) ) e. CC /\ ( 1 / s ) e. CC ) -> ( ( ( 1 - ( 1 / s ) ) + ( 1 / s ) ) - 1 ) = ( ( 1 - ( 1 / s ) ) + ( ( 1 / s ) - 1 ) ) )
95 75 73 94 syl2anc 
 |-  ( ( s e. CC /\ s =/= 0 ) -> ( ( ( 1 - ( 1 / s ) ) + ( 1 / s ) ) - 1 ) = ( ( 1 - ( 1 / s ) ) + ( ( 1 / s ) - 1 ) ) )
96 75 73 addcld 
 |-  ( ( s e. CC /\ s =/= 0 ) -> ( ( 1 - ( 1 / s ) ) + ( 1 / s ) ) e. CC )
97 npcan 
 |-  ( ( 1 e. CC /\ ( 1 / s ) e. CC ) -> ( ( 1 - ( 1 / s ) ) + ( 1 / s ) ) = 1 )
98 72 73 97 sylancr 
 |-  ( ( s e. CC /\ s =/= 0 ) -> ( ( 1 - ( 1 / s ) ) + ( 1 / s ) ) = 1 )
99 96 98 subeq0bd 
 |-  ( ( s e. CC /\ s =/= 0 ) -> ( ( ( 1 - ( 1 / s ) ) + ( 1 / s ) ) - 1 ) = 0 )
100 92 95 99 3eqtr2d 
 |-  ( ( s e. CC /\ s =/= 0 ) -> ( ( 1 - ( 1 / s ) ) + ( ( ( 1 / s ) x. 1 ) - ( ( 1 / s ) x. s ) ) ) = 0 )
101 88 100 eqtrd 
 |-  ( ( s e. CC /\ s =/= 0 ) -> ( ( 1 - ( 1 / s ) ) + ( ( 1 / s ) x. ( 1 - s ) ) ) = 0 )
102 101 adantr 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( 1 - ( 1 / s ) ) + ( ( 1 / s ) x. ( 1 - s ) ) ) = 0 )
103 102 oveq1d 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( ( 1 - ( 1 / s ) ) + ( ( 1 / s ) x. ( 1 - s ) ) ) x. ( Z ` i ) ) = ( 0 x. ( Z ` i ) ) )
104 73 adantr 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( 1 / s ) e. CC )
105 78 ad2antrr 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( 1 - s ) e. CC )
106 104 105 82 mulassd 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( ( 1 / s ) x. ( 1 - s ) ) x. ( Z ` i ) ) = ( ( 1 / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) )
107 106 oveq2d 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( ( 1 / s ) x. ( 1 - s ) ) x. ( Z ` i ) ) ) = ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) ) )
108 83 103 107 3eqtr3rd 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) ) = ( 0 x. ( Z ` i ) ) )
109 mul02 
 |-  ( ( Z ` i ) e. CC -> ( 0 x. ( Z ` i ) ) = 0 )
110 109 ad2antll 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( 0 x. ( Z ` i ) ) = 0 )
111 108 110 eqtrd 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) ) = 0 )
112 simpll 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> s e. CC )
113 simprl 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( x ` i ) e. CC )
114 104 112 113 mulassd 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( ( 1 / s ) x. s ) x. ( x ` i ) ) = ( ( 1 / s ) x. ( s x. ( x ` i ) ) ) )
115 90 oveq1d 
 |-  ( ( s e. CC /\ s =/= 0 ) -> ( ( ( 1 / s ) x. s ) x. ( x ` i ) ) = ( 1 x. ( x ` i ) ) )
116 mulid2 
 |-  ( ( x ` i ) e. CC -> ( 1 x. ( x ` i ) ) = ( x ` i ) )
117 116 adantr 
 |-  ( ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) -> ( 1 x. ( x ` i ) ) = ( x ` i ) )
118 115 117 sylan9eq 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( ( 1 / s ) x. s ) x. ( x ` i ) ) = ( x ` i ) )
119 114 118 eqtr3d 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( 1 / s ) x. ( s x. ( x ` i ) ) ) = ( x ` i ) )
120 111 119 oveq12d 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) ) + ( ( 1 / s ) x. ( s x. ( x ` i ) ) ) ) = ( 0 + ( x ` i ) ) )
121 76 82 mulcld 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) e. CC )
122 simpr 
 |-  ( ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) -> ( Z ` i ) e. CC )
123 mulcl 
 |-  ( ( ( 1 - s ) e. CC /\ ( Z ` i ) e. CC ) -> ( ( 1 - s ) x. ( Z ` i ) ) e. CC )
124 79 122 123 syl2an 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( 1 - s ) x. ( Z ` i ) ) e. CC )
125 104 124 mulcld 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( 1 / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) e. CC )
126 mulcl 
 |-  ( ( s e. CC /\ ( x ` i ) e. CC ) -> ( s x. ( x ` i ) ) e. CC )
127 126 ad2ant2r 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( s x. ( x ` i ) ) e. CC )
128 104 127 mulcld 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( 1 / s ) x. ( s x. ( x ` i ) ) ) e. CC )
129 121 125 128 addassd 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) ) + ( ( 1 / s ) x. ( s x. ( x ` i ) ) ) ) = ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( ( 1 / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) + ( ( 1 / s ) x. ( s x. ( x ` i ) ) ) ) ) )
130 104 124 127 adddid 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( 1 / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) = ( ( ( 1 / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) + ( ( 1 / s ) x. ( s x. ( x ` i ) ) ) ) )
131 130 oveq2d 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) = ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( ( 1 / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) + ( ( 1 / s ) x. ( s x. ( x ` i ) ) ) ) ) )
132 129 131 eqtr4d 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) ) + ( ( 1 / s ) x. ( s x. ( x ` i ) ) ) ) = ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) )
133 addid2 
 |-  ( ( x ` i ) e. CC -> ( 0 + ( x ` i ) ) = ( x ` i ) )
134 133 ad2antrl 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( 0 + ( x ` i ) ) = ( x ` i ) )
135 120 132 134 3eqtr3rd 
 |-  ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( x ` i ) = ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) )
136 67 68 69 71 135 syl22anc 
 |-  ( ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ s =/= 0 ) /\ i e. ( 1 ... N ) ) -> ( x ` i ) = ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) )
137 136 ralrimiva 
 |-  ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ s =/= 0 ) -> A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) )
138 oveq2 
 |-  ( t = ( 1 / s ) -> ( 1 - t ) = ( 1 - ( 1 / s ) ) )
139 138 oveq1d 
 |-  ( t = ( 1 / s ) -> ( ( 1 - t ) x. ( Z ` i ) ) = ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) )
140 oveq1 
 |-  ( t = ( 1 / s ) -> ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) = ( ( 1 / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) )
141 139 140 oveq12d 
 |-  ( t = ( 1 / s ) -> ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) = ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) )
142 141 eqeq2d 
 |-  ( t = ( 1 / s ) -> ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) <-> ( x ` i ) = ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) ) )
143 142 ralbidv 
 |-  ( t = ( 1 / s ) -> ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) <-> A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) ) )
144 143 rspcev 
 |-  ( ( ( 1 / s ) e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) ) -> E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) )
145 65 137 144 syl2anc 
 |-  ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ s =/= 0 ) -> E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) )
146 oveq2 
 |-  ( ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) -> ( t x. ( U ` i ) ) = ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) )
147 146 oveq2d 
 |-  ( ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) -> ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) )
148 147 eqeq2d 
 |-  ( ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) -> ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) ) )
149 148 ralimi 
 |-  ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) -> A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) ) )
150 ralbi 
 |-  ( A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) ) -> ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) ) )
151 149 150 syl 
 |-  ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) -> ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) ) )
152 151 rexbidv 
 |-  ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) -> ( E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) ) )
153 145 152 syl5ibrcom 
 |-  ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ s =/= 0 ) -> ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) -> E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
154 153 impancom 
 |-  ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) -> ( s =/= 0 -> E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
155 48 154 mpd 
 |-  ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) -> E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
156 155 r19.29an 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) -> E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
157 13 156 syldan 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ U Btwn <. Z , x >. ) -> E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
158 3simpa 
 |-  ( ( x e. RR /\ 0 <_ x /\ x <_ 1 ) -> ( x e. RR /\ 0 <_ x ) )
159 elicc01 
 |-  ( x e. ( 0 [,] 1 ) <-> ( x e. RR /\ 0 <_ x /\ x <_ 1 ) )
160 elrege0 
 |-  ( x e. ( 0 [,) +oo ) <-> ( x e. RR /\ 0 <_ x ) )
161 158 159 160 3imtr4i 
 |-  ( x e. ( 0 [,] 1 ) -> x e. ( 0 [,) +oo ) )
162 161 ssriv 
 |-  ( 0 [,] 1 ) C_ ( 0 [,) +oo )
163 brbtwn 
 |-  ( ( x e. ( EE ` N ) /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) -> ( x Btwn <. Z , U >. <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
164 10 9 8 163 syl3anc 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) -> ( x Btwn <. Z , U >. <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
165 164 biimpa 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ x Btwn <. Z , U >. ) -> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
166 ssrexv 
 |-  ( ( 0 [,] 1 ) C_ ( 0 [,) +oo ) -> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) -> E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
167 162 165 166 mpsyl 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ x Btwn <. Z , U >. ) -> E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
168 157 167 jaodan 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ ( U Btwn <. Z , x >. \/ x Btwn <. Z , U >. ) ) -> E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
169 168 anasss 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( x e. ( EE ` N ) /\ ( U Btwn <. Z , x >. \/ x Btwn <. Z , U >. ) ) ) -> E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
170 7 169 sylan2b 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. D ) -> E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
171 r19.26 
 |-  ( A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) <-> ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) )
172 eqtr2 
 |-  ( ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) -> ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) )
173 172 ralimi 
 |-  ( A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) -> A. i e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) )
174 171 173 sylbir 
 |-  ( ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) -> A. i e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) )
175 elrege0 
 |-  ( t e. ( 0 [,) +oo ) <-> ( t e. RR /\ 0 <_ t ) )
176 175 simplbi 
 |-  ( t e. ( 0 [,) +oo ) -> t e. RR )
177 176 recnd 
 |-  ( t e. ( 0 [,) +oo ) -> t e. CC )
178 elrege0 
 |-  ( s e. ( 0 [,) +oo ) <-> ( s e. RR /\ 0 <_ s ) )
179 178 simplbi 
 |-  ( s e. ( 0 [,) +oo ) -> s e. RR )
180 179 recnd 
 |-  ( s e. ( 0 [,) +oo ) -> s e. CC )
181 177 180 anim12i 
 |-  ( ( t e. ( 0 [,) +oo ) /\ s e. ( 0 [,) +oo ) ) -> ( t e. CC /\ s e. CC ) )
182 simplr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) /\ i e. ( 1 ... N ) ) -> ( t e. CC /\ s e. CC ) )
183 simpl2 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> Z e. ( EE ` N ) )
184 183 ad2antrr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) /\ i e. ( 1 ... N ) ) -> Z e. ( EE ` N ) )
185 184 30 sylancom 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) /\ i e. ( 1 ... N ) ) -> ( Z ` i ) e. CC )
186 simpl3 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> U e. ( EE ` N ) )
187 186 ad2antrr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) /\ i e. ( 1 ... N ) ) -> U e. ( EE ` N ) )
188 fveecn 
 |-  ( ( U e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( U ` i ) e. CC )
189 187 188 sylancom 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) /\ i e. ( 1 ... N ) ) -> ( U ` i ) e. CC )
190 subcl 
 |-  ( ( 1 e. CC /\ t e. CC ) -> ( 1 - t ) e. CC )
191 72 190 mpan 
 |-  ( t e. CC -> ( 1 - t ) e. CC )
192 191 adantr 
 |-  ( ( t e. CC /\ s e. CC ) -> ( 1 - t ) e. CC )
193 simpl 
 |-  ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) -> ( Z ` i ) e. CC )
194 mulcl 
 |-  ( ( ( 1 - t ) e. CC /\ ( Z ` i ) e. CC ) -> ( ( 1 - t ) x. ( Z ` i ) ) e. CC )
195 192 193 194 syl2an 
 |-  ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( 1 - t ) x. ( Z ` i ) ) e. CC )
196 mulcl 
 |-  ( ( t e. CC /\ ( U ` i ) e. CC ) -> ( t x. ( U ` i ) ) e. CC )
197 196 ad2ant2rl 
 |-  ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( t x. ( U ` i ) ) e. CC )
198 78 adantl 
 |-  ( ( t e. CC /\ s e. CC ) -> ( 1 - s ) e. CC )
199 198 193 123 syl2an 
 |-  ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( 1 - s ) x. ( Z ` i ) ) e. CC )
200 mulcl 
 |-  ( ( s e. CC /\ ( U ` i ) e. CC ) -> ( s x. ( U ` i ) ) e. CC )
201 200 ad2ant2l 
 |-  ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( s x. ( U ` i ) ) e. CC )
202 195 197 199 201 addsubeq4d 
 |-  ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) <-> ( ( ( 1 - s ) x. ( Z ` i ) ) - ( ( 1 - t ) x. ( Z ` i ) ) ) = ( ( t x. ( U ` i ) ) - ( s x. ( U ` i ) ) ) ) )
203 nnncan1 
 |-  ( ( 1 e. CC /\ s e. CC /\ t e. CC ) -> ( ( 1 - s ) - ( 1 - t ) ) = ( t - s ) )
204 72 203 mp3an1 
 |-  ( ( s e. CC /\ t e. CC ) -> ( ( 1 - s ) - ( 1 - t ) ) = ( t - s ) )
205 204 ancoms 
 |-  ( ( t e. CC /\ s e. CC ) -> ( ( 1 - s ) - ( 1 - t ) ) = ( t - s ) )
206 205 oveq1d 
 |-  ( ( t e. CC /\ s e. CC ) -> ( ( ( 1 - s ) - ( 1 - t ) ) x. ( Z ` i ) ) = ( ( t - s ) x. ( Z ` i ) ) )
207 206 adantr 
 |-  ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( 1 - s ) - ( 1 - t ) ) x. ( Z ` i ) ) = ( ( t - s ) x. ( Z ` i ) ) )
208 78 ad2antlr 
 |-  ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( 1 - s ) e. CC )
209 191 ad2antrr 
 |-  ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( 1 - t ) e. CC )
210 simprl 
 |-  ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( Z ` i ) e. CC )
211 208 209 210 subdird 
 |-  ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( 1 - s ) - ( 1 - t ) ) x. ( Z ` i ) ) = ( ( ( 1 - s ) x. ( Z ` i ) ) - ( ( 1 - t ) x. ( Z ` i ) ) ) )
212 207 211 eqtr3d 
 |-  ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( t - s ) x. ( Z ` i ) ) = ( ( ( 1 - s ) x. ( Z ` i ) ) - ( ( 1 - t ) x. ( Z ` i ) ) ) )
213 simpll 
 |-  ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> t e. CC )
214 simplr 
 |-  ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> s e. CC )
215 simprr 
 |-  ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( U ` i ) e. CC )
216 213 214 215 subdird 
 |-  ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( t - s ) x. ( U ` i ) ) = ( ( t x. ( U ` i ) ) - ( s x. ( U ` i ) ) ) )
217 212 216 eqeq12d 
 |-  ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( t - s ) x. ( Z ` i ) ) = ( ( t - s ) x. ( U ` i ) ) <-> ( ( ( 1 - s ) x. ( Z ` i ) ) - ( ( 1 - t ) x. ( Z ` i ) ) ) = ( ( t x. ( U ` i ) ) - ( s x. ( U ` i ) ) ) ) )
218 subcl 
 |-  ( ( t e. CC /\ s e. CC ) -> ( t - s ) e. CC )
219 218 adantr 
 |-  ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( t - s ) e. CC )
220 mulcan1g 
 |-  ( ( ( t - s ) e. CC /\ ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) -> ( ( ( t - s ) x. ( Z ` i ) ) = ( ( t - s ) x. ( U ` i ) ) <-> ( ( t - s ) = 0 \/ ( Z ` i ) = ( U ` i ) ) ) )
221 219 210 215 220 syl3anc 
 |-  ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( t - s ) x. ( Z ` i ) ) = ( ( t - s ) x. ( U ` i ) ) <-> ( ( t - s ) = 0 \/ ( Z ` i ) = ( U ` i ) ) ) )
222 202 217 221 3bitr2d 
 |-  ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) <-> ( ( t - s ) = 0 \/ ( Z ` i ) = ( U ` i ) ) ) )
223 182 185 189 222 syl12anc 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) <-> ( ( t - s ) = 0 \/ ( Z ` i ) = ( U ` i ) ) ) )
224 223 ralbidva 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) -> ( A. i e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) <-> A. i e. ( 1 ... N ) ( ( t - s ) = 0 \/ ( Z ` i ) = ( U ` i ) ) ) )
225 r19.32v 
 |-  ( A. i e. ( 1 ... N ) ( ( t - s ) = 0 \/ ( Z ` i ) = ( U ` i ) ) <-> ( ( t - s ) = 0 \/ A. i e. ( 1 ... N ) ( Z ` i ) = ( U ` i ) ) )
226 simplr 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) -> Z =/= U )
227 226 neneqd 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) -> -. Z = U )
228 simpll2 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) -> Z e. ( EE ` N ) )
229 simpll3 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) -> U e. ( EE ` N ) )
230 eqeefv 
 |-  ( ( Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) -> ( Z = U <-> A. i e. ( 1 ... N ) ( Z ` i ) = ( U ` i ) ) )
231 228 229 230 syl2anc 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) -> ( Z = U <-> A. i e. ( 1 ... N ) ( Z ` i ) = ( U ` i ) ) )
232 227 231 mtbid 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) -> -. A. i e. ( 1 ... N ) ( Z ` i ) = ( U ` i ) )
233 orel2 
 |-  ( -. A. i e. ( 1 ... N ) ( Z ` i ) = ( U ` i ) -> ( ( ( t - s ) = 0 \/ A. i e. ( 1 ... N ) ( Z ` i ) = ( U ` i ) ) -> ( t - s ) = 0 ) )
234 232 233 syl 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) -> ( ( ( t - s ) = 0 \/ A. i e. ( 1 ... N ) ( Z ` i ) = ( U ` i ) ) -> ( t - s ) = 0 ) )
235 subeq0 
 |-  ( ( t e. CC /\ s e. CC ) -> ( ( t - s ) = 0 <-> t = s ) )
236 235 adantl 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) -> ( ( t - s ) = 0 <-> t = s ) )
237 234 236 sylibd 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) -> ( ( ( t - s ) = 0 \/ A. i e. ( 1 ... N ) ( Z ` i ) = ( U ` i ) ) -> t = s ) )
238 225 237 syl5bi 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) -> ( A. i e. ( 1 ... N ) ( ( t - s ) = 0 \/ ( Z ` i ) = ( U ` i ) ) -> t = s ) )
239 224 238 sylbid 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) -> ( A. i e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) -> t = s ) )
240 181 239 sylan2 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. ( 0 [,) +oo ) /\ s e. ( 0 [,) +oo ) ) ) -> ( A. i e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) -> t = s ) )
241 174 240 syl5 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. ( 0 [,) +oo ) /\ s e. ( 0 [,) +oo ) ) ) -> ( ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) -> t = s ) )
242 241 ralrimivva 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> A. t e. ( 0 [,) +oo ) A. s e. ( 0 [,) +oo ) ( ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) -> t = s ) )
243 242 adantr 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. D ) -> A. t e. ( 0 [,) +oo ) A. s e. ( 0 [,) +oo ) ( ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) -> t = s ) )
244 oveq2 
 |-  ( t = s -> ( 1 - t ) = ( 1 - s ) )
245 244 oveq1d 
 |-  ( t = s -> ( ( 1 - t ) x. ( Z ` i ) ) = ( ( 1 - s ) x. ( Z ` i ) ) )
246 oveq1 
 |-  ( t = s -> ( t x. ( U ` i ) ) = ( s x. ( U ` i ) ) )
247 245 246 oveq12d 
 |-  ( t = s -> ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) )
248 247 eqeq2d 
 |-  ( t = s -> ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> ( x ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) )
249 248 ralbidv 
 |-  ( t = s -> ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) )
250 249 reu4 
 |-  ( E! t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> ( E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. t e. ( 0 [,) +oo ) A. s e. ( 0 [,) +oo ) ( ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) -> t = s ) ) )
251 170 243 250 sylanbrc 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. D ) -> E! t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
252 df-reu 
 |-  ( E! t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> E! t ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
253 251 252 sylib 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. D ) -> E! t ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
254 253 ralrimiva 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> A. x e. D E! t ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
255 2 fnopabg 
 |-  ( A. x e. D E! t ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) <-> F Fn D )
256 254 255 sylib 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> F Fn D )
257 176 ad2antlr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ k e. ( 1 ... N ) ) -> t e. RR )
258 183 ad2antrr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ k e. ( 1 ... N ) ) -> Z e. ( EE ` N ) )
259 fveere 
 |-  ( ( Z e. ( EE ` N ) /\ k e. ( 1 ... N ) ) -> ( Z ` k ) e. RR )
260 258 259 sylancom 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ k e. ( 1 ... N ) ) -> ( Z ` k ) e. RR )
261 186 ad2antrr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ k e. ( 1 ... N ) ) -> U e. ( EE ` N ) )
262 fveere 
 |-  ( ( U e. ( EE ` N ) /\ k e. ( 1 ... N ) ) -> ( U ` k ) e. RR )
263 261 262 sylancom 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ k e. ( 1 ... N ) ) -> ( U ` k ) e. RR )
264 resubcl 
 |-  ( ( 1 e. RR /\ t e. RR ) -> ( 1 - t ) e. RR )
265 58 264 mpan 
 |-  ( t e. RR -> ( 1 - t ) e. RR )
266 remulcl 
 |-  ( ( ( 1 - t ) e. RR /\ ( Z ` k ) e. RR ) -> ( ( 1 - t ) x. ( Z ` k ) ) e. RR )
267 265 266 sylan 
 |-  ( ( t e. RR /\ ( Z ` k ) e. RR ) -> ( ( 1 - t ) x. ( Z ` k ) ) e. RR )
268 267 3adant3 
 |-  ( ( t e. RR /\ ( Z ` k ) e. RR /\ ( U ` k ) e. RR ) -> ( ( 1 - t ) x. ( Z ` k ) ) e. RR )
269 remulcl 
 |-  ( ( t e. RR /\ ( U ` k ) e. RR ) -> ( t x. ( U ` k ) ) e. RR )
270 269 3adant2 
 |-  ( ( t e. RR /\ ( Z ` k ) e. RR /\ ( U ` k ) e. RR ) -> ( t x. ( U ` k ) ) e. RR )
271 268 270 readdcld 
 |-  ( ( t e. RR /\ ( Z ` k ) e. RR /\ ( U ` k ) e. RR ) -> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) e. RR )
272 257 260 263 271 syl3anc 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ k e. ( 1 ... N ) ) -> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) e. RR )
273 272 ralrimiva 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) -> A. k e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) e. RR )
274 simpll1 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) -> N e. NN )
275 mptelee 
 |-  ( N e. NN -> ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) e. ( EE ` N ) <-> A. k e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) e. RR ) )
276 274 275 syl 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) -> ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) e. ( EE ` N ) <-> A. k e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) e. RR ) )
277 273 276 mpbird 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) -> ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) e. ( EE ` N ) )
278 letric 
 |-  ( ( 1 e. RR /\ t e. RR ) -> ( 1 <_ t \/ t <_ 1 ) )
279 58 176 278 sylancr 
 |-  ( t e. ( 0 [,) +oo ) -> ( 1 <_ t \/ t <_ 1 ) )
280 279 adantl 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) -> ( 1 <_ t \/ t <_ 1 ) )
281 simpr 
 |-  ( ( t e. ( 0 [,) +oo ) /\ 1 <_ t ) -> 1 <_ t )
282 176 adantr 
 |-  ( ( t e. ( 0 [,) +oo ) /\ 1 <_ t ) -> t e. RR )
283 0red 
 |-  ( ( t e. ( 0 [,) +oo ) /\ 1 <_ t ) -> 0 e. RR )
284 1red 
 |-  ( ( t e. ( 0 [,) +oo ) /\ 1 <_ t ) -> 1 e. RR )
285 0lt1 
 |-  0 < 1
286 285 a1i 
 |-  ( ( t e. ( 0 [,) +oo ) /\ 1 <_ t ) -> 0 < 1 )
287 283 284 282 286 281 ltletrd 
 |-  ( ( t e. ( 0 [,) +oo ) /\ 1 <_ t ) -> 0 < t )
288 divelunit 
 |-  ( ( ( 1 e. RR /\ 0 <_ 1 ) /\ ( t e. RR /\ 0 < t ) ) -> ( ( 1 / t ) e. ( 0 [,] 1 ) <-> 1 <_ t ) )
289 58 59 288 mpanl12 
 |-  ( ( t e. RR /\ 0 < t ) -> ( ( 1 / t ) e. ( 0 [,] 1 ) <-> 1 <_ t ) )
290 282 287 289 syl2anc 
 |-  ( ( t e. ( 0 [,) +oo ) /\ 1 <_ t ) -> ( ( 1 / t ) e. ( 0 [,] 1 ) <-> 1 <_ t ) )
291 281 290 mpbird 
 |-  ( ( t e. ( 0 [,) +oo ) /\ 1 <_ t ) -> ( 1 / t ) e. ( 0 [,] 1 ) )
292 291 adantll 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) -> ( 1 / t ) e. ( 0 [,] 1 ) )
293 176 ad3antlr 
 |-  ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) /\ i e. ( 1 ... N ) ) -> t e. RR )
294 293 recnd 
 |-  ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) /\ i e. ( 1 ... N ) ) -> t e. CC )
295 287 gt0ne0d 
 |-  ( ( t e. ( 0 [,) +oo ) /\ 1 <_ t ) -> t =/= 0 )
296 295 adantll 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) -> t =/= 0 )
297 296 adantr 
 |-  ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) /\ i e. ( 1 ... N ) ) -> t =/= 0 )
298 183 ad3antrrr 
 |-  ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) /\ i e. ( 1 ... N ) ) -> Z e. ( EE ` N ) )
299 298 30 sylancom 
 |-  ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) /\ i e. ( 1 ... N ) ) -> ( Z ` i ) e. CC )
300 186 ad3antrrr 
 |-  ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) /\ i e. ( 1 ... N ) ) -> U e. ( EE ` N ) )
301 300 188 sylancom 
 |-  ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) /\ i e. ( 1 ... N ) ) -> ( U ` i ) e. CC )
302 reccl 
 |-  ( ( t e. CC /\ t =/= 0 ) -> ( 1 / t ) e. CC )
303 302 adantr 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( 1 / t ) e. CC )
304 191 adantr 
 |-  ( ( t e. CC /\ t =/= 0 ) -> ( 1 - t ) e. CC )
305 304 193 194 syl2an 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( 1 - t ) x. ( Z ` i ) ) e. CC )
306 196 ad2ant2rl 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( t x. ( U ` i ) ) e. CC )
307 303 305 306 adddid 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( 1 / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) = ( ( ( 1 / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) + ( ( 1 / t ) x. ( t x. ( U ` i ) ) ) ) )
308 307 oveq2d 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( ( 1 / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) + ( ( 1 / t ) x. ( t x. ( U ` i ) ) ) ) ) )
309 subcl 
 |-  ( ( 1 e. CC /\ ( 1 / t ) e. CC ) -> ( 1 - ( 1 / t ) ) e. CC )
310 72 302 309 sylancr 
 |-  ( ( t e. CC /\ t =/= 0 ) -> ( 1 - ( 1 / t ) ) e. CC )
311 mulcl 
 |-  ( ( ( 1 - ( 1 / t ) ) e. CC /\ ( Z ` i ) e. CC ) -> ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) e. CC )
312 310 193 311 syl2an 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) e. CC )
313 303 305 mulcld 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( 1 / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) e. CC )
314 recid2 
 |-  ( ( t e. CC /\ t =/= 0 ) -> ( ( 1 / t ) x. t ) = 1 )
315 314 oveq1d 
 |-  ( ( t e. CC /\ t =/= 0 ) -> ( ( ( 1 / t ) x. t ) x. ( U ` i ) ) = ( 1 x. ( U ` i ) ) )
316 315 adantr 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( 1 / t ) x. t ) x. ( U ` i ) ) = ( 1 x. ( U ` i ) ) )
317 simpll 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> t e. CC )
318 simprr 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( U ` i ) e. CC )
319 303 317 318 mulassd 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( 1 / t ) x. t ) x. ( U ` i ) ) = ( ( 1 / t ) x. ( t x. ( U ` i ) ) ) )
320 mulid2 
 |-  ( ( U ` i ) e. CC -> ( 1 x. ( U ` i ) ) = ( U ` i ) )
321 320 ad2antll 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( 1 x. ( U ` i ) ) = ( U ` i ) )
322 316 319 321 3eqtr3d 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( 1 / t ) x. ( t x. ( U ` i ) ) ) = ( U ` i ) )
323 322 318 eqeltrd 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( 1 / t ) x. ( t x. ( U ` i ) ) ) e. CC )
324 312 313 323 addassd 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) ) + ( ( 1 / t ) x. ( t x. ( U ` i ) ) ) ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( ( 1 / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) + ( ( 1 / t ) x. ( t x. ( U ` i ) ) ) ) ) )
325 310 adantr 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( 1 - ( 1 / t ) ) e. CC )
326 302 304 mulcld 
 |-  ( ( t e. CC /\ t =/= 0 ) -> ( ( 1 / t ) x. ( 1 - t ) ) e. CC )
327 326 adantr 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( 1 / t ) x. ( 1 - t ) ) e. CC )
328 simprl 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( Z ` i ) e. CC )
329 325 327 328 adddird 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( 1 - ( 1 / t ) ) + ( ( 1 / t ) x. ( 1 - t ) ) ) x. ( Z ` i ) ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( ( 1 / t ) x. ( 1 - t ) ) x. ( Z ` i ) ) ) )
330 simpl 
 |-  ( ( t e. CC /\ t =/= 0 ) -> t e. CC )
331 subdi 
 |-  ( ( ( 1 / t ) e. CC /\ 1 e. CC /\ t e. CC ) -> ( ( 1 / t ) x. ( 1 - t ) ) = ( ( ( 1 / t ) x. 1 ) - ( ( 1 / t ) x. t ) ) )
332 72 331 mp3an2 
 |-  ( ( ( 1 / t ) e. CC /\ t e. CC ) -> ( ( 1 / t ) x. ( 1 - t ) ) = ( ( ( 1 / t ) x. 1 ) - ( ( 1 / t ) x. t ) ) )
333 302 330 332 syl2anc 
 |-  ( ( t e. CC /\ t =/= 0 ) -> ( ( 1 / t ) x. ( 1 - t ) ) = ( ( ( 1 / t ) x. 1 ) - ( ( 1 / t ) x. t ) ) )
334 302 mulid1d 
 |-  ( ( t e. CC /\ t =/= 0 ) -> ( ( 1 / t ) x. 1 ) = ( 1 / t ) )
335 334 314 oveq12d 
 |-  ( ( t e. CC /\ t =/= 0 ) -> ( ( ( 1 / t ) x. 1 ) - ( ( 1 / t ) x. t ) ) = ( ( 1 / t ) - 1 ) )
336 333 335 eqtrd 
 |-  ( ( t e. CC /\ t =/= 0 ) -> ( ( 1 / t ) x. ( 1 - t ) ) = ( ( 1 / t ) - 1 ) )
337 336 oveq2d 
 |-  ( ( t e. CC /\ t =/= 0 ) -> ( ( 1 - ( 1 / t ) ) + ( ( 1 / t ) x. ( 1 - t ) ) ) = ( ( 1 - ( 1 / t ) ) + ( ( 1 / t ) - 1 ) ) )
338 npncan2 
 |-  ( ( 1 e. CC /\ ( 1 / t ) e. CC ) -> ( ( 1 - ( 1 / t ) ) + ( ( 1 / t ) - 1 ) ) = 0 )
339 72 302 338 sylancr 
 |-  ( ( t e. CC /\ t =/= 0 ) -> ( ( 1 - ( 1 / t ) ) + ( ( 1 / t ) - 1 ) ) = 0 )
340 337 339 eqtrd 
 |-  ( ( t e. CC /\ t =/= 0 ) -> ( ( 1 - ( 1 / t ) ) + ( ( 1 / t ) x. ( 1 - t ) ) ) = 0 )
341 340 adantr 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( 1 - ( 1 / t ) ) + ( ( 1 / t ) x. ( 1 - t ) ) ) = 0 )
342 341 oveq1d 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( 1 - ( 1 / t ) ) + ( ( 1 / t ) x. ( 1 - t ) ) ) x. ( Z ` i ) ) = ( 0 x. ( Z ` i ) ) )
343 109 ad2antrl 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( 0 x. ( Z ` i ) ) = 0 )
344 342 343 eqtrd 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( 1 - ( 1 / t ) ) + ( ( 1 / t ) x. ( 1 - t ) ) ) x. ( Z ` i ) ) = 0 )
345 191 ad2antrr 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( 1 - t ) e. CC )
346 303 345 328 mulassd 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( 1 / t ) x. ( 1 - t ) ) x. ( Z ` i ) ) = ( ( 1 / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) )
347 346 oveq2d 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( ( 1 / t ) x. ( 1 - t ) ) x. ( Z ` i ) ) ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) ) )
348 329 344 347 3eqtr3rd 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) ) = 0 )
349 348 322 oveq12d 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) ) + ( ( 1 / t ) x. ( t x. ( U ` i ) ) ) ) = ( 0 + ( U ` i ) ) )
350 addid2 
 |-  ( ( U ` i ) e. CC -> ( 0 + ( U ` i ) ) = ( U ` i ) )
351 350 ad2antll 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( 0 + ( U ` i ) ) = ( U ` i ) )
352 349 351 eqtrd 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) ) + ( ( 1 / t ) x. ( t x. ( U ` i ) ) ) ) = ( U ` i ) )
353 308 324 352 3eqtr2rd 
 |-  ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( U ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) )
354 294 297 299 301 353 syl22anc 
 |-  ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) /\ i e. ( 1 ... N ) ) -> ( U ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) )
355 354 ralrimiva 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) -> A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) )
356 oveq2 
 |-  ( s = ( 1 / t ) -> ( 1 - s ) = ( 1 - ( 1 / t ) ) )
357 356 oveq1d 
 |-  ( s = ( 1 / t ) -> ( ( 1 - s ) x. ( Z ` i ) ) = ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) )
358 oveq1 
 |-  ( s = ( 1 / t ) -> ( s x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) = ( ( 1 / t ) x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) )
359 357 358 oveq12d 
 |-  ( s = ( 1 / t ) -> ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) )
360 359 eqeq2d 
 |-  ( s = ( 1 / t ) -> ( ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) <-> ( U ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) ) )
361 360 ralbidv 
 |-  ( s = ( 1 / t ) -> ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) <-> A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) ) )
362 fveq2 
 |-  ( k = i -> ( Z ` k ) = ( Z ` i ) )
363 362 oveq2d 
 |-  ( k = i -> ( ( 1 - t ) x. ( Z ` k ) ) = ( ( 1 - t ) x. ( Z ` i ) ) )
364 fveq2 
 |-  ( k = i -> ( U ` k ) = ( U ` i ) )
365 364 oveq2d 
 |-  ( k = i -> ( t x. ( U ` k ) ) = ( t x. ( U ` i ) ) )
366 363 365 oveq12d 
 |-  ( k = i -> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
367 eqid 
 |-  ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) = ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) )
368 ovex 
 |-  ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) e. _V
369 366 367 368 fvmpt 
 |-  ( i e. ( 1 ... N ) -> ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
370 369 oveq2d 
 |-  ( i e. ( 1 ... N ) -> ( ( 1 / t ) x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) = ( ( 1 / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
371 370 oveq2d 
 |-  ( i e. ( 1 ... N ) -> ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) )
372 371 eqeq2d 
 |-  ( i e. ( 1 ... N ) -> ( ( U ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) <-> ( U ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) ) )
373 372 ralbiia 
 |-  ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) <-> A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) )
374 361 373 bitrdi 
 |-  ( s = ( 1 / t ) -> ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) <-> A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) ) )
375 374 rspcev 
 |-  ( ( ( 1 / t ) e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) ) -> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) )
376 292 355 375 syl2anc 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) -> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) )
377 186 ad2antrr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) -> U e. ( EE ` N ) )
378 183 ad2antrr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) -> Z e. ( EE ` N ) )
379 277 adantr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) -> ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) e. ( EE ` N ) )
380 brbtwn 
 |-  ( ( U e. ( EE ` N ) /\ Z e. ( EE ` N ) /\ ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) e. ( EE ` N ) ) -> ( U Btwn <. Z , ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) >. <-> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) ) )
381 377 378 379 380 syl3anc 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) -> ( U Btwn <. Z , ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) >. <-> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) ) )
382 376 381 mpbird 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) -> U Btwn <. Z , ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) >. )
383 382 ex 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) -> ( 1 <_ t -> U Btwn <. Z , ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) >. ) )
384 simpll 
 |-  ( ( ( t e. RR /\ 0 <_ t ) /\ t <_ 1 ) -> t e. RR )
385 simplr 
 |-  ( ( ( t e. RR /\ 0 <_ t ) /\ t <_ 1 ) -> 0 <_ t )
386 simpr 
 |-  ( ( ( t e. RR /\ 0 <_ t ) /\ t <_ 1 ) -> t <_ 1 )
387 384 385 386 3jca 
 |-  ( ( ( t e. RR /\ 0 <_ t ) /\ t <_ 1 ) -> ( t e. RR /\ 0 <_ t /\ t <_ 1 ) )
388 175 anbi1i 
 |-  ( ( t e. ( 0 [,) +oo ) /\ t <_ 1 ) <-> ( ( t e. RR /\ 0 <_ t ) /\ t <_ 1 ) )
389 elicc01 
 |-  ( t e. ( 0 [,] 1 ) <-> ( t e. RR /\ 0 <_ t /\ t <_ 1 ) )
390 387 388 389 3imtr4i 
 |-  ( ( t e. ( 0 [,) +oo ) /\ t <_ 1 ) -> t e. ( 0 [,] 1 ) )
391 390 adantll 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ t <_ 1 ) -> t e. ( 0 [,] 1 ) )
392 369 rgen 
 |-  A. i e. ( 1 ... N ) ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) )
393 oveq2 
 |-  ( s = t -> ( 1 - s ) = ( 1 - t ) )
394 393 oveq1d 
 |-  ( s = t -> ( ( 1 - s ) x. ( Z ` i ) ) = ( ( 1 - t ) x. ( Z ` i ) ) )
395 oveq1 
 |-  ( s = t -> ( s x. ( U ` i ) ) = ( t x. ( U ` i ) ) )
396 394 395 oveq12d 
 |-  ( s = t -> ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
397 396 eqeq2d 
 |-  ( s = t -> ( ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) <-> ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
398 397 ralbidv 
 |-  ( s = t -> ( A. i e. ( 1 ... N ) ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) <-> A. i e. ( 1 ... N ) ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
399 398 rspcev 
 |-  ( ( t e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) -> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) )
400 391 392 399 sylancl 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ t <_ 1 ) -> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) )
401 277 adantr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ t <_ 1 ) -> ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) e. ( EE ` N ) )
402 183 ad2antrr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ t <_ 1 ) -> Z e. ( EE ` N ) )
403 186 ad2antrr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ t <_ 1 ) -> U e. ( EE ` N ) )
404 brbtwn 
 |-  ( ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) e. ( EE ` N ) /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) -> ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) Btwn <. Z , U >. <-> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) )
405 401 402 403 404 syl3anc 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ t <_ 1 ) -> ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) Btwn <. Z , U >. <-> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) )
406 400 405 mpbird 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ t <_ 1 ) -> ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) Btwn <. Z , U >. )
407 406 ex 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) -> ( t <_ 1 -> ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) Btwn <. Z , U >. ) )
408 383 407 orim12d 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) -> ( ( 1 <_ t \/ t <_ 1 ) -> ( U Btwn <. Z , ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) >. \/ ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) Btwn <. Z , U >. ) ) )
409 280 408 mpd 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) -> ( U Btwn <. Z , ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) >. \/ ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) Btwn <. Z , U >. ) )
410 opeq2 
 |-  ( p = ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) -> <. Z , p >. = <. Z , ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) >. )
411 410 breq2d 
 |-  ( p = ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) -> ( U Btwn <. Z , p >. <-> U Btwn <. Z , ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) >. ) )
412 breq1 
 |-  ( p = ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) -> ( p Btwn <. Z , U >. <-> ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) Btwn <. Z , U >. ) )
413 411 412 orbi12d 
 |-  ( p = ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) -> ( ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) <-> ( U Btwn <. Z , ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) >. \/ ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) Btwn <. Z , U >. ) ) )
414 413 1 elrab2 
 |-  ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) e. D <-> ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) e. ( EE ` N ) /\ ( U Btwn <. Z , ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) >. \/ ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) Btwn <. Z , U >. ) ) )
415 277 409 414 sylanbrc 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) -> ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) e. D )
416 fveq1 
 |-  ( x = ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) -> ( x ` i ) = ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) )
417 416 eqeq1d 
 |-  ( x = ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) -> ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
418 417 ralbidv 
 |-  ( x = ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) -> ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> A. i e. ( 1 ... N ) ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
419 418 rspcev 
 |-  ( ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) e. D /\ A. i e. ( 1 ... N ) ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) -> E. x e. D A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
420 415 392 419 sylancl 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) -> E. x e. D A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
421 7 simplbi 
 |-  ( x e. D -> x e. ( EE ` N ) )
422 1 ssrab3 
 |-  D C_ ( EE ` N )
423 422 sseli 
 |-  ( y e. D -> y e. ( EE ` N ) )
424 421 423 anim12i 
 |-  ( ( x e. D /\ y e. D ) -> ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) )
425 r19.26 
 |-  ( A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ ( y ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) <-> ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
426 eqtr3 
 |-  ( ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ ( y ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) -> ( x ` i ) = ( y ` i ) )
427 426 ralimi 
 |-  ( A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ ( y ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) -> A. i e. ( 1 ... N ) ( x ` i ) = ( y ` i ) )
428 425 427 sylbir 
 |-  ( ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) -> A. i e. ( 1 ... N ) ( x ` i ) = ( y ` i ) )
429 eqeefv 
 |-  ( ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) -> ( x = y <-> A. i e. ( 1 ... N ) ( x ` i ) = ( y ` i ) ) )
430 429 adantl 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> ( x = y <-> A. i e. ( 1 ... N ) ( x ` i ) = ( y ` i ) ) )
431 428 430 syl5ibr 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> ( ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) -> x = y ) )
432 424 431 sylan2 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( x e. D /\ y e. D ) ) -> ( ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) -> x = y ) )
433 432 ralrimivva 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> A. x e. D A. y e. D ( ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) -> x = y ) )
434 433 adantr 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) -> A. x e. D A. y e. D ( ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) -> x = y ) )
435 df-reu 
 |-  ( E! x e. D A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> E! x ( x e. D /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
436 fveq1 
 |-  ( x = y -> ( x ` i ) = ( y ` i ) )
437 436 eqeq1d 
 |-  ( x = y -> ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> ( y ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
438 437 ralbidv 
 |-  ( x = y -> ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
439 438 reu4 
 |-  ( E! x e. D A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> ( E. x e. D A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. x e. D A. y e. D ( ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) -> x = y ) ) )
440 435 439 bitr3i 
 |-  ( E! x ( x e. D /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) <-> ( E. x e. D A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. x e. D A. y e. D ( ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) -> x = y ) ) )
441 420 434 440 sylanbrc 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) -> E! x ( x e. D /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
442 441 ralrimiva 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> A. t e. ( 0 [,) +oo ) E! x ( x e. D /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
443 an12 
 |-  ( ( x e. D /\ ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) <-> ( t e. ( 0 [,) +oo ) /\ ( x e. D /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) )
444 443 opabbii 
 |-  { <. x , t >. | ( x e. D /\ ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) } = { <. x , t >. | ( t e. ( 0 [,) +oo ) /\ ( x e. D /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) }
445 2 444 eqtri 
 |-  F = { <. x , t >. | ( t e. ( 0 [,) +oo ) /\ ( x e. D /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) }
446 445 cnveqi 
 |-  `' F = `' { <. x , t >. | ( t e. ( 0 [,) +oo ) /\ ( x e. D /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) }
447 cnvopab 
 |-  `' { <. x , t >. | ( t e. ( 0 [,) +oo ) /\ ( x e. D /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) } = { <. t , x >. | ( t e. ( 0 [,) +oo ) /\ ( x e. D /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) }
448 446 447 eqtri 
 |-  `' F = { <. t , x >. | ( t e. ( 0 [,) +oo ) /\ ( x e. D /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) }
449 448 fnopabg 
 |-  ( A. t e. ( 0 [,) +oo ) E! x ( x e. D /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) <-> `' F Fn ( 0 [,) +oo ) )
450 442 449 sylib 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> `' F Fn ( 0 [,) +oo ) )
451 dff1o4 
 |-  ( F : D -1-1-onto-> ( 0 [,) +oo ) <-> ( F Fn D /\ `' F Fn ( 0 [,) +oo ) ) )
452 256 450 451 sylanbrc 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> F : D -1-1-onto-> ( 0 [,) +oo ) )