Metamath Proof Explorer

Theorem axeuclidlem

Description: Lemma for axeuclid . Handle the algebraic aspects of the theorem. (Contributed by Scott Fenton, 9-Sep-2013)

Ref Expression
Assertion axeuclidlem 
|- ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) /\ A. i e. ( 1 ... N ) ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( T ` i ) ) ) = ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) -> E. x e. ( EE ` N ) E. y e. ( EE ` N ) E. r e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simp21 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) /\ A. i e. ( 1 ... N ) ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( T ` i ) ) ) = ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) -> P e. ( 0 [,] 1 ) )
2 simp22 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) /\ A. i e. ( 1 ... N ) ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( T ` i ) ) ) = ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) -> Q e. ( 0 [,] 1 ) )
3 fveere 
 |-  ( ( A e. ( EE ` N ) /\ k e. ( 1 ... N ) ) -> ( A ` k ) e. RR )
4 3 expcom 
 |-  ( k e. ( 1 ... N ) -> ( A e. ( EE ` N ) -> ( A ` k ) e. RR ) )
5 fveere 
 |-  ( ( B e. ( EE ` N ) /\ k e. ( 1 ... N ) ) -> ( B ` k ) e. RR )
6 5 expcom 
 |-  ( k e. ( 1 ... N ) -> ( B e. ( EE ` N ) -> ( B ` k ) e. RR ) )
7 4 6 anim12d 
 |-  ( k e. ( 1 ... N ) -> ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) ) )
8 fveere 
 |-  ( ( C e. ( EE ` N ) /\ k e. ( 1 ... N ) ) -> ( C ` k ) e. RR )
9 8 expcom 
 |-  ( k e. ( 1 ... N ) -> ( C e. ( EE ` N ) -> ( C ` k ) e. RR ) )
10 fveere 
 |-  ( ( T e. ( EE ` N ) /\ k e. ( 1 ... N ) ) -> ( T ` k ) e. RR )
11 10 expcom 
 |-  ( k e. ( 1 ... N ) -> ( T e. ( EE ` N ) -> ( T ` k ) e. RR ) )
12 9 11 anim12d 
 |-  ( k e. ( 1 ... N ) -> ( ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) -> ( ( C ` k ) e. RR /\ ( T ` k ) e. RR ) ) )
13 7 12 anim12d 
 |-  ( k e. ( 1 ... N ) -> ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) -> ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) /\ ( ( C ` k ) e. RR /\ ( T ` k ) e. RR ) ) ) )
14 13 impcom 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ k e. ( 1 ... N ) ) -> ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) /\ ( ( C ` k ) e. RR /\ ( T ` k ) e. RR ) ) )
15 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
16 15 sseli 
 |-  ( P e. ( 0 [,] 1 ) -> P e. RR )
17 16 3ad2ant1 
 |-  ( ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) -> P e. RR )
18 17 adantl 
 |-  ( ( ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) /\ ( ( C ` k ) e. RR /\ ( T ` k ) e. RR ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> P e. RR )
19 peano2rem 
 |-  ( P e. RR -> ( P - 1 ) e. RR )
20 18 19 syl 
 |-  ( ( ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) /\ ( ( C ` k ) e. RR /\ ( T ` k ) e. RR ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( P - 1 ) e. RR )
21 simplll 
 |-  ( ( ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) /\ ( ( C ` k ) e. RR /\ ( T ` k ) e. RR ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( A ` k ) e. RR )
22 20 21 remulcld 
 |-  ( ( ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) /\ ( ( C ` k ) e. RR /\ ( T ` k ) e. RR ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( P - 1 ) x. ( A ` k ) ) e. RR )
23 simpllr 
 |-  ( ( ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) /\ ( ( C ` k ) e. RR /\ ( T ` k ) e. RR ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( B ` k ) e. RR )
24 22 23 readdcld 
 |-  ( ( ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) /\ ( ( C ` k ) e. RR /\ ( T ` k ) e. RR ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( P - 1 ) x. ( A ` k ) ) + ( B ` k ) ) e. RR )
25 simpr3 
 |-  ( ( ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) /\ ( ( C ` k ) e. RR /\ ( T ` k ) e. RR ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> P =/= 0 )
26 24 18 25 redivcld 
 |-  ( ( ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) /\ ( ( C ` k ) e. RR /\ ( T ` k ) e. RR ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( B ` k ) ) / P ) e. RR )
27 14 26 sylan 
 |-  ( ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ k e. ( 1 ... N ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( B ` k ) ) / P ) e. RR )
28 27 an32s 
 |-  ( ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) /\ k e. ( 1 ... N ) ) -> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( B ` k ) ) / P ) e. RR )
29 28 ralrimiva 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> A. k e. ( 1 ... N ) ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( B ` k ) ) / P ) e. RR )
30 eleenn 
 |-  ( A e. ( EE ` N ) -> N e. NN )
31 30 ad3antrrr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> N e. NN )
32 mptelee 
 |-  ( N e. NN -> ( ( k e. ( 1 ... N ) |-> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( B ` k ) ) / P ) ) e. ( EE ` N ) <-> A. k e. ( 1 ... N ) ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( B ` k ) ) / P ) e. RR ) )
33 31 32 syl 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( k e. ( 1 ... N ) |-> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( B ` k ) ) / P ) ) e. ( EE ` N ) <-> A. k e. ( 1 ... N ) ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( B ` k ) ) / P ) e. RR ) )
34 29 33 mpbird 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( k e. ( 1 ... N ) |-> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( B ` k ) ) / P ) ) e. ( EE ` N ) )
35 34 3adant3 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) /\ A. i e. ( 1 ... N ) ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( T ` i ) ) ) = ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) -> ( k e. ( 1 ... N ) |-> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( B ` k ) ) / P ) ) e. ( EE ` N ) )
36 simplrl 
 |-  ( ( ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) /\ ( ( C ` k ) e. RR /\ ( T ` k ) e. RR ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( C ` k ) e. RR )
37 22 36 readdcld 
 |-  ( ( ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) /\ ( ( C ` k ) e. RR /\ ( T ` k ) e. RR ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( P - 1 ) x. ( A ` k ) ) + ( C ` k ) ) e. RR )
38 37 18 25 redivcld 
 |-  ( ( ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) /\ ( ( C ` k ) e. RR /\ ( T ` k ) e. RR ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( C ` k ) ) / P ) e. RR )
39 14 38 sylan 
 |-  ( ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ k e. ( 1 ... N ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( C ` k ) ) / P ) e. RR )
40 39 an32s 
 |-  ( ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) /\ k e. ( 1 ... N ) ) -> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( C ` k ) ) / P ) e. RR )
41 40 ralrimiva 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> A. k e. ( 1 ... N ) ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( C ` k ) ) / P ) e. RR )
42 mptelee 
 |-  ( N e. NN -> ( ( k e. ( 1 ... N ) |-> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( C ` k ) ) / P ) ) e. ( EE ` N ) <-> A. k e. ( 1 ... N ) ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( C ` k ) ) / P ) e. RR ) )
43 31 42 syl 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( k e. ( 1 ... N ) |-> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( C ` k ) ) / P ) ) e. ( EE ` N ) <-> A. k e. ( 1 ... N ) ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( C ` k ) ) / P ) e. RR ) )
44 41 43 mpbird 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( k e. ( 1 ... N ) |-> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( C ` k ) ) / P ) ) e. ( EE ` N ) )
45 44 3adant3 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) /\ A. i e. ( 1 ... N ) ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( T ` i ) ) ) = ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) -> ( k e. ( 1 ... N ) |-> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( C ` k ) ) / P ) ) e. ( EE ` N ) )
46 fveecn 
 |-  ( ( A e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. CC )
47 46 expcom 
 |-  ( i e. ( 1 ... N ) -> ( A e. ( EE ` N ) -> ( A ` i ) e. CC ) )
48 fveecn 
 |-  ( ( B e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. CC )
49 48 expcom 
 |-  ( i e. ( 1 ... N ) -> ( B e. ( EE ` N ) -> ( B ` i ) e. CC ) )
50 47 49 anim12d 
 |-  ( i e. ( 1 ... N ) -> ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) ) )
51 fveecn 
 |-  ( ( C e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( C ` i ) e. CC )
52 51 expcom 
 |-  ( i e. ( 1 ... N ) -> ( C e. ( EE ` N ) -> ( C ` i ) e. CC ) )
53 fveecn 
 |-  ( ( T e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( T ` i ) e. CC )
54 53 expcom 
 |-  ( i e. ( 1 ... N ) -> ( T e. ( EE ` N ) -> ( T ` i ) e. CC ) )
55 52 54 anim12d 
 |-  ( i e. ( 1 ... N ) -> ( ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) -> ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) )
56 50 55 anim12d 
 |-  ( i e. ( 1 ... N ) -> ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) -> ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) ) )
57 56 impcom 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) )
58 eqcom 
 |-  ( ( T ` i ) = ( ( ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) ) + ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) / P ) <-> ( ( ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) ) + ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) / P ) = ( T ` i ) )
59 ax-1cn 
 |-  1 e. CC
60 simpr2 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> Q e. ( 0 [,] 1 ) )
61 15 sseli 
 |-  ( Q e. ( 0 [,] 1 ) -> Q e. RR )
62 61 recnd 
 |-  ( Q e. ( 0 [,] 1 ) -> Q e. CC )
63 60 62 syl 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> Q e. CC )
64 subcl 
 |-  ( ( 1 e. CC /\ Q e. CC ) -> ( 1 - Q ) e. CC )
65 59 63 64 sylancr 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( 1 - Q ) e. CC )
66 simpr1 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> P e. ( 0 [,] 1 ) )
67 16 recnd 
 |-  ( P e. ( 0 [,] 1 ) -> P e. CC )
68 66 67 syl 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> P e. CC )
69 subcl 
 |-  ( ( P e. CC /\ 1 e. CC ) -> ( P - 1 ) e. CC )
70 68 59 69 sylancl 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( P - 1 ) e. CC )
71 simplll 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( A ` i ) e. CC )
72 70 71 mulcld 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( P - 1 ) x. ( A ` i ) ) e. CC )
73 65 72 mulcld 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) e. CC )
74 63 72 mulcld 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) e. CC )
75 73 74 addcld 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) ) e. CC )
76 simpllr 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( B ` i ) e. CC )
77 65 76 mulcld 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( 1 - Q ) x. ( B ` i ) ) e. CC )
78 simplrl 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( C ` i ) e. CC )
79 63 78 mulcld 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( Q x. ( C ` i ) ) e. CC )
80 77 79 addcld 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) e. CC )
81 75 80 addcld 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) ) + ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) e. CC )
82 simplrr 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( T ` i ) e. CC )
83 simpr3 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> P =/= 0 )
84 81 68 82 83 divmuld 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) ) + ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) / P ) = ( T ` i ) <-> ( P x. ( T ` i ) ) = ( ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) ) + ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) ) )
85 58 84 syl5bb 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( T ` i ) = ( ( ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) ) + ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) / P ) <-> ( P x. ( T ` i ) ) = ( ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) ) + ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) ) )
86 negsubdi2 
 |-  ( ( 1 e. CC /\ P e. CC ) -> -u ( 1 - P ) = ( P - 1 ) )
87 59 68 86 sylancr 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> -u ( 1 - P ) = ( P - 1 ) )
88 87 oveq1d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( -u ( 1 - P ) x. ( A ` i ) ) = ( ( P - 1 ) x. ( A ` i ) ) )
89 subcl 
 |-  ( ( 1 e. CC /\ P e. CC ) -> ( 1 - P ) e. CC )
90 59 68 89 sylancr 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( 1 - P ) e. CC )
91 90 71 mulneg1d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( -u ( 1 - P ) x. ( A ` i ) ) = -u ( ( 1 - P ) x. ( A ` i ) ) )
92 npcan 
 |-  ( ( 1 e. CC /\ Q e. CC ) -> ( ( 1 - Q ) + Q ) = 1 )
93 59 63 92 sylancr 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( 1 - Q ) + Q ) = 1 )
94 93 oveq1d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( 1 - Q ) + Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) = ( 1 x. ( ( P - 1 ) x. ( A ` i ) ) ) )
95 65 63 72 adddird 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( 1 - Q ) + Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) = ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) ) )
96 72 mulid2d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( 1 x. ( ( P - 1 ) x. ( A ` i ) ) ) = ( ( P - 1 ) x. ( A ` i ) ) )
97 94 95 96 3eqtr3rd 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( P - 1 ) x. ( A ` i ) ) = ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) ) )
98 88 91 97 3eqtr3d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> -u ( ( 1 - P ) x. ( A ` i ) ) = ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) ) )
99 98 oveq2d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) + -u ( ( 1 - P ) x. ( A ` i ) ) ) = ( ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) + ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) ) ) )
100 90 71 mulcld 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( 1 - P ) x. ( A ` i ) ) e. CC )
101 80 100 negsubd 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) + -u ( ( 1 - P ) x. ( A ` i ) ) ) = ( ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) - ( ( 1 - P ) x. ( A ` i ) ) ) )
102 80 75 addcomd 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) + ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) ) ) = ( ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) ) + ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) )
103 99 101 102 3eqtr3d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) - ( ( 1 - P ) x. ( A ` i ) ) ) = ( ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) ) + ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) )
104 103 eqeq1d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) - ( ( 1 - P ) x. ( A ` i ) ) ) = ( P x. ( T ` i ) ) <-> ( ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) ) + ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) = ( P x. ( T ` i ) ) ) )
105 eqcom 
 |-  ( ( ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) ) + ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) = ( P x. ( T ` i ) ) <-> ( P x. ( T ` i ) ) = ( ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) ) + ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) )
106 104 105 bitrdi 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) - ( ( 1 - P ) x. ( A ` i ) ) ) = ( P x. ( T ` i ) ) <-> ( P x. ( T ` i ) ) = ( ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) ) + ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) ) )
107 85 106 bitr4d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( T ` i ) = ( ( ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) ) + ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) / P ) <-> ( ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) - ( ( 1 - P ) x. ( A ` i ) ) ) = ( P x. ( T ` i ) ) ) )
108 73 74 77 79 add4d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) ) + ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) = ( ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( ( 1 - Q ) x. ( B ` i ) ) ) + ( ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( C ` i ) ) ) ) )
109 65 72 76 adddid 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( 1 - Q ) x. ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) ) = ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( ( 1 - Q ) x. ( B ` i ) ) ) )
110 63 72 78 adddid 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( Q x. ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) ) = ( ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( C ` i ) ) ) )
111 109 110 oveq12d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( 1 - Q ) x. ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) ) + ( Q x. ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) ) ) = ( ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( ( 1 - Q ) x. ( B ` i ) ) ) + ( ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( C ` i ) ) ) ) )
112 108 111 eqtr4d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) ) + ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) = ( ( ( 1 - Q ) x. ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) ) + ( Q x. ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) ) ) )
113 112 oveq1d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) ) + ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) / P ) = ( ( ( ( 1 - Q ) x. ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) ) + ( Q x. ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) ) ) / P ) )
114 72 76 addcld 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) e. CC )
115 65 114 mulcld 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( 1 - Q ) x. ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) ) e. CC )
116 72 78 addcld 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) e. CC )
117 63 116 mulcld 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( Q x. ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) ) e. CC )
118 115 117 68 83 divdird 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( 1 - Q ) x. ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) ) + ( Q x. ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) ) ) / P ) = ( ( ( ( 1 - Q ) x. ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) ) / P ) + ( ( Q x. ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) ) / P ) ) )
119 65 114 68 83 divassd 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( 1 - Q ) x. ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) ) / P ) = ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) )
120 63 116 68 83 divassd 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( Q x. ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) ) / P ) = ( Q x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) )
121 119 120 oveq12d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( 1 - Q ) x. ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) ) / P ) + ( ( Q x. ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) ) / P ) ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) )
122 113 118 121 3eqtrd 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) ) + ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) / P ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) )
123 122 eqeq2d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( T ` i ) = ( ( ( ( ( 1 - Q ) x. ( ( P - 1 ) x. ( A ` i ) ) ) + ( Q x. ( ( P - 1 ) x. ( A ` i ) ) ) ) + ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) / P ) <-> ( T ` i ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) ) )
124 68 82 mulcld 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( P x. ( T ` i ) ) e. CC )
125 80 100 124 subaddd 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) - ( ( 1 - P ) x. ( A ` i ) ) ) = ( P x. ( T ` i ) ) <-> ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( T ` i ) ) ) = ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) )
126 107 123 125 3bitr3rd 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( T ` i ) ) ) = ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) <-> ( T ` i ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) ) )
127 126 biimpd 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( T ` i ) ) ) = ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) -> ( T ` i ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) ) )
128 npncan2 
 |-  ( ( 1 e. CC /\ P e. CC ) -> ( ( 1 - P ) + ( P - 1 ) ) = 0 )
129 59 68 128 sylancr 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( 1 - P ) + ( P - 1 ) ) = 0 )
130 129 oveq1d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( 1 - P ) + ( P - 1 ) ) x. ( A ` i ) ) = ( 0 x. ( A ` i ) ) )
131 90 70 71 adddird 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( 1 - P ) + ( P - 1 ) ) x. ( A ` i ) ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( ( P - 1 ) x. ( A ` i ) ) ) )
132 mul02 
 |-  ( ( A ` i ) e. CC -> ( 0 x. ( A ` i ) ) = 0 )
133 132 ad3antrrr 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( 0 x. ( A ` i ) ) = 0 )
134 130 131 133 3eqtr3d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( 1 - P ) x. ( A ` i ) ) + ( ( P - 1 ) x. ( A ` i ) ) ) = 0 )
135 134 oveq1d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( 1 - P ) x. ( A ` i ) ) + ( ( P - 1 ) x. ( A ` i ) ) ) + ( B ` i ) ) = ( 0 + ( B ` i ) ) )
136 100 72 76 addassd 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( 1 - P ) x. ( A ` i ) ) + ( ( P - 1 ) x. ( A ` i ) ) ) + ( B ` i ) ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) ) )
137 76 addid2d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( 0 + ( B ` i ) ) = ( B ` i ) )
138 135 136 137 3eqtr3rd 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) ) )
139 114 68 83 divcan2d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) = ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) )
140 139 oveq2d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) ) )
141 138 140 eqtr4d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) ) )
142 134 oveq1d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( 1 - P ) x. ( A ` i ) ) + ( ( P - 1 ) x. ( A ` i ) ) ) + ( C ` i ) ) = ( 0 + ( C ` i ) ) )
143 100 72 78 addassd 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( 1 - P ) x. ( A ` i ) ) + ( ( P - 1 ) x. ( A ` i ) ) ) + ( C ` i ) ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) ) )
144 78 addid2d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( 0 + ( C ` i ) ) = ( C ` i ) )
145 142 143 144 3eqtr3rd 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) ) )
146 116 68 83 divcan2d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) = ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) )
147 146 oveq2d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) ) )
148 145 147 eqtr4d 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) )
149 141 148 jca 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) ) )
150 127 149 jctild 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( T ` i ) ) ) = ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) -> ( ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) ) ) )
151 df-3an 
 |-  ( ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) ) <-> ( ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) ) )
152 150 151 syl6ibr 
 |-  ( ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) /\ ( ( C ` i ) e. CC /\ ( T ` i ) e. CC ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( T ` i ) ) ) = ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) -> ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) ) ) )
153 57 152 sylan 
 |-  ( ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( T ` i ) ) ) = ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) -> ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) ) ) )
154 153 an32s 
 |-  ( ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( T ` i ) ) ) = ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) -> ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) ) ) )
155 154 ralimdva 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) ) -> ( A. i e. ( 1 ... N ) ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( T ` i ) ) ) = ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) -> A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) ) ) )
156 155 3impia 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) /\ A. i e. ( 1 ... N ) ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( T ` i ) ) ) = ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) -> A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) ) )
157 fveq1 
 |-  ( x = ( k e. ( 1 ... N ) |-> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( B ` k ) ) / P ) ) -> ( x ` i ) = ( ( k e. ( 1 ... N ) |-> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( B ` k ) ) / P ) ) ` i ) )
158 fveq2 
 |-  ( k = i -> ( A ` k ) = ( A ` i ) )
159 158 oveq2d 
 |-  ( k = i -> ( ( P - 1 ) x. ( A ` k ) ) = ( ( P - 1 ) x. ( A ` i ) ) )
160 fveq2 
 |-  ( k = i -> ( B ` k ) = ( B ` i ) )
161 159 160 oveq12d 
 |-  ( k = i -> ( ( ( P - 1 ) x. ( A ` k ) ) + ( B ` k ) ) = ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) )
162 161 oveq1d 
 |-  ( k = i -> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( B ` k ) ) / P ) = ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) )
163 eqid 
 |-  ( k e. ( 1 ... N ) |-> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( B ` k ) ) / P ) ) = ( k e. ( 1 ... N ) |-> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( B ` k ) ) / P ) )
164 ovex 
 |-  ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) e. _V
165 162 163 164 fvmpt 
 |-  ( i e. ( 1 ... N ) -> ( ( k e. ( 1 ... N ) |-> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( B ` k ) ) / P ) ) ` i ) = ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) )
166 157 165 sylan9eq 
 |-  ( ( x = ( k e. ( 1 ... N ) |-> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( B ` k ) ) / P ) ) /\ i e. ( 1 ... N ) ) -> ( x ` i ) = ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) )
167 oveq2 
 |-  ( ( x ` i ) = ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) -> ( P x. ( x ` i ) ) = ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) )
168 167 oveq2d 
 |-  ( ( x ` i ) = ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) -> ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( x ` i ) ) ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) ) )
169 168 eqeq2d 
 |-  ( ( x ` i ) = ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) -> ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( x ` i ) ) ) <-> ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) ) ) )
170 oveq2 
 |-  ( ( x ` i ) = ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) -> ( ( 1 - Q ) x. ( x ` i ) ) = ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) )
171 170 oveq1d 
 |-  ( ( x ` i ) = ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) -> ( ( ( 1 - Q ) x. ( x ` i ) ) + ( Q x. ( y ` i ) ) ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( y ` i ) ) ) )
172 171 eqeq2d 
 |-  ( ( x ` i ) = ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) -> ( ( T ` i ) = ( ( ( 1 - Q ) x. ( x ` i ) ) + ( Q x. ( y ` i ) ) ) <-> ( T ` i ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( y ` i ) ) ) ) )
173 169 172 3anbi13d 
 |-  ( ( x ` i ) = ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) -> ( ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( x ` i ) ) + ( Q x. ( y ` i ) ) ) ) <-> ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( y ` i ) ) ) ) ) )
174 166 173 syl 
 |-  ( ( x = ( k e. ( 1 ... N ) |-> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( B ` k ) ) / P ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( x ` i ) ) + ( Q x. ( y ` i ) ) ) ) <-> ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( y ` i ) ) ) ) ) )
175 174 ralbidva 
 |-  ( x = ( k e. ( 1 ... N ) |-> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( B ` k ) ) / P ) ) -> ( A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( x ` i ) ) + ( Q x. ( y ` i ) ) ) ) <-> A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( y ` i ) ) ) ) ) )
176 fveq1 
 |-  ( y = ( k e. ( 1 ... N ) |-> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( C ` k ) ) / P ) ) -> ( y ` i ) = ( ( k e. ( 1 ... N ) |-> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( C ` k ) ) / P ) ) ` i ) )
177 fveq2 
 |-  ( k = i -> ( C ` k ) = ( C ` i ) )
178 159 177 oveq12d 
 |-  ( k = i -> ( ( ( P - 1 ) x. ( A ` k ) ) + ( C ` k ) ) = ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) )
179 178 oveq1d 
 |-  ( k = i -> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( C ` k ) ) / P ) = ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) )
180 eqid 
 |-  ( k e. ( 1 ... N ) |-> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( C ` k ) ) / P ) ) = ( k e. ( 1 ... N ) |-> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( C ` k ) ) / P ) )
181 ovex 
 |-  ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) e. _V
182 179 180 181 fvmpt 
 |-  ( i e. ( 1 ... N ) -> ( ( k e. ( 1 ... N ) |-> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( C ` k ) ) / P ) ) ` i ) = ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) )
183 176 182 sylan9eq 
 |-  ( ( y = ( k e. ( 1 ... N ) |-> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( C ` k ) ) / P ) ) /\ i e. ( 1 ... N ) ) -> ( y ` i ) = ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) )
184 oveq2 
 |-  ( ( y ` i ) = ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) -> ( P x. ( y ` i ) ) = ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) )
185 184 oveq2d 
 |-  ( ( y ` i ) = ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) -> ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( y ` i ) ) ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) )
186 185 eqeq2d 
 |-  ( ( y ` i ) = ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) -> ( ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( y ` i ) ) ) <-> ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) ) )
187 oveq2 
 |-  ( ( y ` i ) = ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) -> ( Q x. ( y ` i ) ) = ( Q x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) )
188 187 oveq2d 
 |-  ( ( y ` i ) = ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) -> ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( y ` i ) ) ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) )
189 188 eqeq2d 
 |-  ( ( y ` i ) = ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) -> ( ( T ` i ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( y ` i ) ) ) <-> ( T ` i ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) ) )
190 186 189 3anbi23d 
 |-  ( ( y ` i ) = ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) -> ( ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( y ` i ) ) ) ) <-> ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) ) ) )
191 183 190 syl 
 |-  ( ( y = ( k e. ( 1 ... N ) |-> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( C ` k ) ) / P ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( y ` i ) ) ) ) <-> ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) ) ) )
192 191 ralbidva 
 |-  ( y = ( k e. ( 1 ... N ) |-> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( C ` k ) ) / P ) ) -> ( A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( y ` i ) ) ) ) <-> A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) ) ) )
193 175 192 rspc2ev 
 |-  ( ( ( k e. ( 1 ... N ) |-> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( B ` k ) ) / P ) ) e. ( EE ` N ) /\ ( k e. ( 1 ... N ) |-> ( ( ( ( P - 1 ) x. ( A ` k ) ) + ( C ` k ) ) / P ) ) e. ( EE ` N ) /\ A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( B ` i ) ) / P ) ) + ( Q x. ( ( ( ( P - 1 ) x. ( A ` i ) ) + ( C ` i ) ) / P ) ) ) ) ) -> E. x e. ( EE ` N ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( x ` i ) ) + ( Q x. ( y ` i ) ) ) ) )
194 35 45 156 193 syl3anc 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) /\ A. i e. ( 1 ... N ) ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( T ` i ) ) ) = ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) -> E. x e. ( EE ` N ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( x ` i ) ) + ( Q x. ( y ` i ) ) ) ) )
195 oveq2 
 |-  ( r = P -> ( 1 - r ) = ( 1 - P ) )
196 195 oveq1d 
 |-  ( r = P -> ( ( 1 - r ) x. ( A ` i ) ) = ( ( 1 - P ) x. ( A ` i ) ) )
197 oveq1 
 |-  ( r = P -> ( r x. ( x ` i ) ) = ( P x. ( x ` i ) ) )
198 196 197 oveq12d 
 |-  ( r = P -> ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( x ` i ) ) ) )
199 198 eqeq2d 
 |-  ( r = P -> ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) <-> ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( x ` i ) ) ) ) )
200 199 3anbi1d 
 |-  ( r = P -> ( ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) ) )
201 200 ralbidv 
 |-  ( r = P -> ( A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) ) )
202 201 2rexbidv 
 |-  ( r = P -> ( E. x e. ( EE ` N ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> E. x e. ( EE ` N ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) ) )
203 oveq2 
 |-  ( s = P -> ( 1 - s ) = ( 1 - P ) )
204 203 oveq1d 
 |-  ( s = P -> ( ( 1 - s ) x. ( A ` i ) ) = ( ( 1 - P ) x. ( A ` i ) ) )
205 oveq1 
 |-  ( s = P -> ( s x. ( y ` i ) ) = ( P x. ( y ` i ) ) )
206 204 205 oveq12d 
 |-  ( s = P -> ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( y ` i ) ) ) )
207 206 eqeq2d 
 |-  ( s = P -> ( ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) <-> ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( y ` i ) ) ) ) )
208 207 3anbi2d 
 |-  ( s = P -> ( ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) ) )
209 208 ralbidv 
 |-  ( s = P -> ( A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) ) )
210 209 2rexbidv 
 |-  ( s = P -> ( E. x e. ( EE ` N ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> E. x e. ( EE ` N ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) ) )
211 oveq2 
 |-  ( u = Q -> ( 1 - u ) = ( 1 - Q ) )
212 211 oveq1d 
 |-  ( u = Q -> ( ( 1 - u ) x. ( x ` i ) ) = ( ( 1 - Q ) x. ( x ` i ) ) )
213 oveq1 
 |-  ( u = Q -> ( u x. ( y ` i ) ) = ( Q x. ( y ` i ) ) )
214 212 213 oveq12d 
 |-  ( u = Q -> ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) = ( ( ( 1 - Q ) x. ( x ` i ) ) + ( Q x. ( y ` i ) ) ) )
215 214 eqeq2d 
 |-  ( u = Q -> ( ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) <-> ( T ` i ) = ( ( ( 1 - Q ) x. ( x ` i ) ) + ( Q x. ( y ` i ) ) ) ) )
216 215 3anbi3d 
 |-  ( u = Q -> ( ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( x ` i ) ) + ( Q x. ( y ` i ) ) ) ) ) )
217 216 ralbidv 
 |-  ( u = Q -> ( A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( x ` i ) ) + ( Q x. ( y ` i ) ) ) ) ) )
218 217 2rexbidv 
 |-  ( u = Q -> ( E. x e. ( EE ` N ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> E. x e. ( EE ` N ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( x ` i ) ) + ( Q x. ( y ` i ) ) ) ) ) )
219 202 210 218 rspc3ev 
 |-  ( ( ( P e. ( 0 [,] 1 ) /\ P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) ) /\ E. x e. ( EE ` N ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - Q ) x. ( x ` i ) ) + ( Q x. ( y ` i ) ) ) ) ) -> E. r e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) E. x e. ( EE ` N ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )
220 1 1 2 194 219 syl31anc 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) /\ A. i e. ( 1 ... N ) ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( T ` i ) ) ) = ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) -> E. r e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) E. x e. ( EE ` N ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )
221 rexcom 
 |-  ( E. u e. ( 0 [,] 1 ) E. x e. ( EE ` N ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> E. x e. ( EE ` N ) E. u e. ( 0 [,] 1 ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )
222 221 rexbii 
 |-  ( E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) E. x e. ( EE ` N ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> E. s e. ( 0 [,] 1 ) E. x e. ( EE ` N ) E. u e. ( 0 [,] 1 ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )
223 rexcom 
 |-  ( E. s e. ( 0 [,] 1 ) E. x e. ( EE ` N ) E. u e. ( 0 [,] 1 ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> E. x e. ( EE ` N ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )
224 222 223 bitri 
 |-  ( E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) E. x e. ( EE ` N ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> E. x e. ( EE ` N ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )
225 224 rexbii 
 |-  ( E. r e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) E. x e. ( EE ` N ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> E. r e. ( 0 [,] 1 ) E. x e. ( EE ` N ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )
226 rexcom 
 |-  ( E. r e. ( 0 [,] 1 ) E. x e. ( EE ` N ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> E. x e. ( EE ` N ) E. r e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )
227 rexcom 
 |-  ( E. u e. ( 0 [,] 1 ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> E. y e. ( EE ` N ) E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )
228 227 rexbii 
 |-  ( E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> E. s e. ( 0 [,] 1 ) E. y e. ( EE ` N ) E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )
229 rexcom 
 |-  ( E. s e. ( 0 [,] 1 ) E. y e. ( EE ` N ) E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> E. y e. ( EE ` N ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )
230 228 229 bitri 
 |-  ( E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> E. y e. ( EE ` N ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )
231 230 rexbii 
 |-  ( E. r e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> E. r e. ( 0 [,] 1 ) E. y e. ( EE ` N ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )
232 rexcom 
 |-  ( E. r e. ( 0 [,] 1 ) E. y e. ( EE ` N ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> E. y e. ( EE ` N ) E. r e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )
233 231 232 bitri 
 |-  ( E. r e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> E. y e. ( EE ` N ) E. r e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )
234 233 rexbii 
 |-  ( E. x e. ( EE ` N ) E. r e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> E. x e. ( EE ` N ) E. y e. ( EE ` N ) E. r e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )
235 225 226 234 3bitri 
 |-  ( E. r e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) E. x e. ( EE ` N ) E. y e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> E. x e. ( EE ` N ) E. y e. ( EE ` N ) E. r e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )
236 220 235 sylib 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( P e. ( 0 [,] 1 ) /\ Q e. ( 0 [,] 1 ) /\ P =/= 0 ) /\ A. i e. ( 1 ... N ) ( ( ( 1 - P ) x. ( A ` i ) ) + ( P x. ( T ` i ) ) ) = ( ( ( 1 - Q ) x. ( B ` i ) ) + ( Q x. ( C ` i ) ) ) ) -> E. x e. ( EE ` N ) E. y e. ( EE ` N ) E. r e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )