Metamath Proof Explorer

Theorem aacllem

Description: Lemma for other theorems about AA . (Contributed by Brendan Leahy, 3-Jan-2020) (Revised by Alexander van der Vekens and David A. Wheeler, 25-Apr-2020)

Ref Expression
Hypotheses aacllem.0 
|- ( ph -> A e. CC )
aacllem.1 
|- ( ph -> N e. NN0 )
aacllem.2 
|- ( ( ph /\ n e. ( 1 ... N ) ) -> X e. CC )
aacllem.3 
|- ( ( ph /\ k e. ( 0 ... N ) /\ n e. ( 1 ... N ) ) -> C e. QQ )
aacllem.4 
|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( A ^ k ) = sum_ n e. ( 1 ... N ) ( C x. X ) )
Assertion aacllem 
|- ( ph -> A e. AA )

Proof

Step Hyp Ref Expression
1 aacllem.0 
 |-  ( ph -> A e. CC )
2 aacllem.1 
 |-  ( ph -> N e. NN0 )
3 aacllem.2 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> X e. CC )
4 aacllem.3 
 |-  ( ( ph /\ k e. ( 0 ... N ) /\ n e. ( 1 ... N ) ) -> C e. QQ )
5 aacllem.4 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( A ^ k ) = sum_ n e. ( 1 ... N ) ( C x. X ) )
6 2 nn0red 
 |-  ( ph -> N e. RR )
7 6 ltp1d 
 |-  ( ph -> N < ( N + 1 ) )
8 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
9 2 8 syl 
 |-  ( ph -> ( N + 1 ) e. NN0 )
10 9 nn0red 
 |-  ( ph -> ( N + 1 ) e. RR )
11 6 10 ltnled 
 |-  ( ph -> ( N < ( N + 1 ) <-> -. ( N + 1 ) <_ N ) )
12 7 11 mpbid 
 |-  ( ph -> -. ( N + 1 ) <_ N )
13 4 3expa 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> C e. QQ )
14 13 fmpttd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( n e. ( 1 ... N ) |-> C ) : ( 1 ... N ) --> QQ )
15 qex 
 |-  QQ e. _V
16 ovex 
 |-  ( 1 ... N ) e. _V
17 15 16 elmap 
 |-  ( ( n e. ( 1 ... N ) |-> C ) e. ( QQ ^m ( 1 ... N ) ) <-> ( n e. ( 1 ... N ) |-> C ) : ( 1 ... N ) --> QQ )
18 14 17 sylibr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( n e. ( 1 ... N ) |-> C ) e. ( QQ ^m ( 1 ... N ) ) )
19 18 fmpttd 
 |-  ( ph -> ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) --> ( QQ ^m ( 1 ... N ) ) )
20 eqid 
 |-  ( CCfld |`s QQ ) = ( CCfld |`s QQ )
21 20 qdrng 
 |-  ( CCfld |`s QQ ) e. DivRing
22 drngring 
 |-  ( ( CCfld |`s QQ ) e. DivRing -> ( CCfld |`s QQ ) e. Ring )
23 21 22 ax-mp 
 |-  ( CCfld |`s QQ ) e. Ring
24 fzfi 
 |-  ( 1 ... N ) e. Fin
25 eqid 
 |-  ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) = ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) )
26 25 frlmlmod 
 |-  ( ( ( CCfld |`s QQ ) e. Ring /\ ( 1 ... N ) e. Fin ) -> ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) e. LMod )
27 23 24 26 mp2an 
 |-  ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) e. LMod
28 fzfi 
 |-  ( 0 ... N ) e. Fin
29 20 qrngbas 
 |-  QQ = ( Base ` ( CCfld |`s QQ ) )
30 25 29 frlmfibas 
 |-  ( ( ( CCfld |`s QQ ) e. DivRing /\ ( 1 ... N ) e. Fin ) -> ( QQ ^m ( 1 ... N ) ) = ( Base ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) )
31 21 24 30 mp2an 
 |-  ( QQ ^m ( 1 ... N ) ) = ( Base ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
32 25 frlmsca 
 |-  ( ( ( CCfld |`s QQ ) e. DivRing /\ ( 1 ... N ) e. Fin ) -> ( CCfld |`s QQ ) = ( Scalar ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) )
33 21 24 32 mp2an 
 |-  ( CCfld |`s QQ ) = ( Scalar ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
34 eqid 
 |-  ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) = ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
35 20 qrng0 
 |-  0 = ( 0g ` ( CCfld |`s QQ ) )
36 25 35 frlm0 
 |-  ( ( ( CCfld |`s QQ ) e. Ring /\ ( 1 ... N ) e. Fin ) -> ( ( 1 ... N ) X. { 0 } ) = ( 0g ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) )
37 23 24 36 mp2an 
 |-  ( ( 1 ... N ) X. { 0 } ) = ( 0g ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
38 eqid 
 |-  ( ( CCfld |`s QQ ) freeLMod ( 0 ... N ) ) = ( ( CCfld |`s QQ ) freeLMod ( 0 ... N ) )
39 38 29 frlmfibas 
 |-  ( ( ( CCfld |`s QQ ) e. DivRing /\ ( 0 ... N ) e. Fin ) -> ( QQ ^m ( 0 ... N ) ) = ( Base ` ( ( CCfld |`s QQ ) freeLMod ( 0 ... N ) ) ) )
40 21 28 39 mp2an 
 |-  ( QQ ^m ( 0 ... N ) ) = ( Base ` ( ( CCfld |`s QQ ) freeLMod ( 0 ... N ) ) )
41 31 33 34 37 35 40 islindf4 
 |-  ( ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) e. LMod /\ ( 0 ... N ) e. Fin /\ ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) --> ( QQ ^m ( 1 ... N ) ) ) -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) LIndF ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) <-> A. w e. ( QQ ^m ( 0 ... N ) ) ( ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) = ( ( 1 ... N ) X. { 0 } ) -> w = ( ( 0 ... N ) X. { 0 } ) ) ) )
42 27 28 41 mp3an12 
 |-  ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) --> ( QQ ^m ( 1 ... N ) ) -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) LIndF ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) <-> A. w e. ( QQ ^m ( 0 ... N ) ) ( ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) = ( ( 1 ... N ) X. { 0 } ) -> w = ( ( 0 ... N ) X. { 0 } ) ) ) )
43 19 42 syl 
 |-  ( ph -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) LIndF ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) <-> A. w e. ( QQ ^m ( 0 ... N ) ) ( ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) = ( ( 1 ... N ) X. { 0 } ) -> w = ( ( 0 ... N ) X. { 0 } ) ) ) )
44 elmapi 
 |-  ( w e. ( QQ ^m ( 0 ... N ) ) -> w : ( 0 ... N ) --> QQ )
45 fzfid 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( 0 ... N ) e. Fin )
46 fvexd 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( w ` k ) e. _V )
47 16 mptex 
 |-  ( n e. ( 1 ... N ) |-> C ) e. _V
48 47 a1i 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( n e. ( 1 ... N ) |-> C ) e. _V )
49 simpr 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> w : ( 0 ... N ) --> QQ )
50 49 feqmptd 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> w = ( k e. ( 0 ... N ) |-> ( w ` k ) ) )
51 eqidd 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) = ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) )
52 45 46 48 50 51 offval2 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) = ( k e. ( 0 ... N ) |-> ( ( w ` k ) ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( n e. ( 1 ... N ) |-> C ) ) ) )
53 fzfid 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( 1 ... N ) e. Fin )
54 ffvelrn 
 |-  ( ( w : ( 0 ... N ) --> QQ /\ k e. ( 0 ... N ) ) -> ( w ` k ) e. QQ )
55 54 adantll 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( w ` k ) e. QQ )
56 18 adantlr 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( n e. ( 1 ... N ) |-> C ) e. ( QQ ^m ( 1 ... N ) ) )
57 cnfldmul 
 |-  x. = ( .r ` CCfld )
58 20 57 ressmulr 
 |-  ( QQ e. _V -> x. = ( .r ` ( CCfld |`s QQ ) ) )
59 15 58 ax-mp 
 |-  x. = ( .r ` ( CCfld |`s QQ ) )
60 25 31 29 53 55 56 34 59 frlmvscafval 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( ( w ` k ) ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( n e. ( 1 ... N ) |-> C ) ) = ( ( ( 1 ... N ) X. { ( w ` k ) } ) oF x. ( n e. ( 1 ... N ) |-> C ) ) )
61 fvexd 
 |-  ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> ( w ` k ) e. _V )
62 13 adantllr 
 |-  ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> C e. QQ )
63 fconstmpt 
 |-  ( ( 1 ... N ) X. { ( w ` k ) } ) = ( n e. ( 1 ... N ) |-> ( w ` k ) )
64 63 a1i 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( ( 1 ... N ) X. { ( w ` k ) } ) = ( n e. ( 1 ... N ) |-> ( w ` k ) ) )
65 eqidd 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( n e. ( 1 ... N ) |-> C ) = ( n e. ( 1 ... N ) |-> C ) )
66 53 61 62 64 65 offval2 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( ( ( 1 ... N ) X. { ( w ` k ) } ) oF x. ( n e. ( 1 ... N ) |-> C ) ) = ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) )
67 60 66 eqtrd 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( ( w ` k ) ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( n e. ( 1 ... N ) |-> C ) ) = ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) )
68 67 mpteq2dva 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( k e. ( 0 ... N ) |-> ( ( w ` k ) ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( n e. ( 1 ... N ) |-> C ) ) ) = ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) ) )
69 52 68 eqtrd 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) = ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) ) )
70 69 oveq2d 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) = ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) ) ) )
71 fzfid 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( 1 ... N ) e. Fin )
72 23 a1i 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( CCfld |`s QQ ) e. Ring )
73 55 adantlr 
 |-  ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) /\ k e. ( 0 ... N ) ) -> ( w ` k ) e. QQ )
74 13 an32s 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ k e. ( 0 ... N ) ) -> C e. QQ )
75 74 adantllr 
 |-  ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) /\ k e. ( 0 ... N ) ) -> C e. QQ )
76 qmulcl 
 |-  ( ( ( w ` k ) e. QQ /\ C e. QQ ) -> ( ( w ` k ) x. C ) e. QQ )
77 73 75 76 syl2anc 
 |-  ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) /\ k e. ( 0 ... N ) ) -> ( ( w ` k ) x. C ) e. QQ )
78 77 an32s 
 |-  ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> ( ( w ` k ) x. C ) e. QQ )
79 78 fmpttd 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) : ( 1 ... N ) --> QQ )
80 15 16 elmap 
 |-  ( ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) e. ( QQ ^m ( 1 ... N ) ) <-> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) : ( 1 ... N ) --> QQ )
81 79 80 sylibr 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) e. ( QQ ^m ( 1 ... N ) ) )
82 eqid 
 |-  ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) ) = ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) )
83 16 mptex 
 |-  ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) e. _V
84 83 a1i 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) e. _V )
85 snex 
 |-  { 0 } e. _V
86 16 85 xpex 
 |-  ( ( 1 ... N ) X. { 0 } ) e. _V
87 86 a1i 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( 1 ... N ) X. { 0 } ) e. _V )
88 82 45 84 87 fsuppmptdm 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) ) finSupp ( ( 1 ... N ) X. { 0 } ) )
89 25 31 37 71 45 72 81 88 frlmgsum 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) ) ) = ( n e. ( 1 ... N ) |-> ( ( CCfld |`s QQ ) gsum ( k e. ( 0 ... N ) |-> ( ( w ` k ) x. C ) ) ) ) )
90 cnfldbas 
 |-  CC = ( Base ` CCfld )
91 cnfldadd 
 |-  + = ( +g ` CCfld )
92 cnfldex 
 |-  CCfld e. _V
93 92 a1i 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> CCfld e. _V )
94 fzfid 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> ( 0 ... N ) e. Fin )
95 qsscn 
 |-  QQ C_ CC
96 95 a1i 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> QQ C_ CC )
97 77 fmpttd 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> ( k e. ( 0 ... N ) |-> ( ( w ` k ) x. C ) ) : ( 0 ... N ) --> QQ )
98 0z 
 |-  0 e. ZZ
99 zq 
 |-  ( 0 e. ZZ -> 0 e. QQ )
100 98 99 ax-mp 
 |-  0 e. QQ
101 100 a1i 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> 0 e. QQ )
102 addid2 
 |-  ( x e. CC -> ( 0 + x ) = x )
103 addid1 
 |-  ( x e. CC -> ( x + 0 ) = x )
104 102 103 jca 
 |-  ( x e. CC -> ( ( 0 + x ) = x /\ ( x + 0 ) = x ) )
105 104 adantl 
 |-  ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) /\ x e. CC ) -> ( ( 0 + x ) = x /\ ( x + 0 ) = x ) )
106 90 91 20 93 94 96 97 101 105 gsumress 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> ( CCfld gsum ( k e. ( 0 ... N ) |-> ( ( w ` k ) x. C ) ) ) = ( ( CCfld |`s QQ ) gsum ( k e. ( 0 ... N ) |-> ( ( w ` k ) x. C ) ) ) )
107 simplr 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> w : ( 0 ... N ) --> QQ )
108 qcn 
 |-  ( ( w ` k ) e. QQ -> ( w ` k ) e. CC )
109 54 108 syl 
 |-  ( ( w : ( 0 ... N ) --> QQ /\ k e. ( 0 ... N ) ) -> ( w ` k ) e. CC )
110 107 109 sylan 
 |-  ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) /\ k e. ( 0 ... N ) ) -> ( w ` k ) e. CC )
111 qcn 
 |-  ( C e. QQ -> C e. CC )
112 13 111 syl 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> C e. CC )
113 112 an32s 
 |-  ( ( ( ph /\ n e. ( 1 ... N ) ) /\ k e. ( 0 ... N ) ) -> C e. CC )
114 113 adantllr 
 |-  ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) /\ k e. ( 0 ... N ) ) -> C e. CC )
115 110 114 mulcld 
 |-  ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) /\ k e. ( 0 ... N ) ) -> ( ( w ` k ) x. C ) e. CC )
116 94 115 gsumfsum 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> ( CCfld gsum ( k e. ( 0 ... N ) |-> ( ( w ` k ) x. C ) ) ) = sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) )
117 106 116 eqtr3d 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> ( ( CCfld |`s QQ ) gsum ( k e. ( 0 ... N ) |-> ( ( w ` k ) x. C ) ) ) = sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) )
118 117 mpteq2dva 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( n e. ( 1 ... N ) |-> ( ( CCfld |`s QQ ) gsum ( k e. ( 0 ... N ) |-> ( ( w ` k ) x. C ) ) ) ) = ( n e. ( 1 ... N ) |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) ) )
119 70 89 118 3eqtrd 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) = ( n e. ( 1 ... N ) |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) ) )
120 qaddcl 
 |-  ( ( x e. QQ /\ y e. QQ ) -> ( x + y ) e. QQ )
121 120 adantl 
 |-  ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( x + y ) e. QQ )
122 96 121 94 77 101 fsumcllem 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) e. QQ )
123 122 fmpttd 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( n e. ( 1 ... N ) |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) ) : ( 1 ... N ) --> QQ )
124 15 16 elmap 
 |-  ( ( n e. ( 1 ... N ) |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) ) e. ( QQ ^m ( 1 ... N ) ) <-> ( n e. ( 1 ... N ) |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) ) : ( 1 ... N ) --> QQ )
125 123 124 sylibr 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( n e. ( 1 ... N ) |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) ) e. ( QQ ^m ( 1 ... N ) ) )
126 119 125 eqeltrd 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) e. ( QQ ^m ( 1 ... N ) ) )
127 elmapi 
 |-  ( ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) e. ( QQ ^m ( 1 ... N ) ) -> ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) : ( 1 ... N ) --> QQ )
128 ffn 
 |-  ( ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) : ( 1 ... N ) --> QQ -> ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) Fn ( 1 ... N ) )
129 126 127 128 3syl 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) Fn ( 1 ... N ) )
130 c0ex 
 |-  0 e. _V
131 fnconstg 
 |-  ( 0 e. _V -> ( ( 1 ... N ) X. { 0 } ) Fn ( 1 ... N ) )
132 130 131 ax-mp 
 |-  ( ( 1 ... N ) X. { 0 } ) Fn ( 1 ... N )
133 nfcv 
 |-  F/_ n ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) )
134 nfcv 
 |-  F/_ n gsum
135 nfcv 
 |-  F/_ n w
136 nfcv 
 |-  F/_ n oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
137 nfcv 
 |-  F/_ n ( 0 ... N )
138 nfmpt1 
 |-  F/_ n ( n e. ( 1 ... N ) |-> C )
139 137 138 nfmpt 
 |-  F/_ n ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) )
140 135 136 139 nfov 
 |-  F/_ n ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) )
141 133 134 140 nfov 
 |-  F/_ n ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) )
142 nfcv 
 |-  F/_ n ( ( 1 ... N ) X. { 0 } )
143 141 142 eqfnfv2f 
 |-  ( ( ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) Fn ( 1 ... N ) /\ ( ( 1 ... N ) X. { 0 } ) Fn ( 1 ... N ) ) -> ( ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) = ( ( 1 ... N ) X. { 0 } ) <-> A. n e. ( 1 ... N ) ( ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) ` n ) = ( ( ( 1 ... N ) X. { 0 } ) ` n ) ) )
144 129 132 143 sylancl 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) = ( ( 1 ... N ) X. { 0 } ) <-> A. n e. ( 1 ... N ) ( ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) ` n ) = ( ( ( 1 ... N ) X. { 0 } ) ` n ) ) )
145 119 fveq1d 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) ` n ) = ( ( n e. ( 1 ... N ) |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) ) ` n ) )
146 sumex 
 |-  sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) e. _V
147 eqid 
 |-  ( n e. ( 1 ... N ) |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) ) = ( n e. ( 1 ... N ) |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) )
148 147 fvmpt2 
 |-  ( ( n e. ( 1 ... N ) /\ sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) e. _V ) -> ( ( n e. ( 1 ... N ) |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) ) ` n ) = sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) )
149 146 148 mpan2 
 |-  ( n e. ( 1 ... N ) -> ( ( n e. ( 1 ... N ) |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) ) ` n ) = sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) )
150 145 149 sylan9eq 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> ( ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) ` n ) = sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) )
151 130 fvconst2 
 |-  ( n e. ( 1 ... N ) -> ( ( ( 1 ... N ) X. { 0 } ) ` n ) = 0 )
152 151 adantl 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> ( ( ( 1 ... N ) X. { 0 } ) ` n ) = 0 )
153 150 152 eqeq12d 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> ( ( ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) ` n ) = ( ( ( 1 ... N ) X. { 0 } ) ` n ) <-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) )
154 153 ralbidva 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( A. n e. ( 1 ... N ) ( ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) ` n ) = ( ( ( 1 ... N ) X. { 0 } ) ` n ) <-> A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) )
155 144 154 bitrd 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) = ( ( 1 ... N ) X. { 0 } ) <-> A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) )
156 155 imbi1d 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) = ( ( 1 ... N ) X. { 0 } ) -> w = ( ( 0 ... N ) X. { 0 } ) ) <-> ( A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 -> w = ( ( 0 ... N ) X. { 0 } ) ) ) )
157 44 156 sylan2 
 |-  ( ( ph /\ w e. ( QQ ^m ( 0 ... N ) ) ) -> ( ( ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) = ( ( 1 ... N ) X. { 0 } ) -> w = ( ( 0 ... N ) X. { 0 } ) ) <-> ( A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 -> w = ( ( 0 ... N ) X. { 0 } ) ) ) )
158 157 ralbidva 
 |-  ( ph -> ( A. w e. ( QQ ^m ( 0 ... N ) ) ( ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) gsum ( w oF ( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) = ( ( 1 ... N ) X. { 0 } ) -> w = ( ( 0 ... N ) X. { 0 } ) ) <-> A. w e. ( QQ ^m ( 0 ... N ) ) ( A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 -> w = ( ( 0 ... N ) X. { 0 } ) ) ) )
159 43 158 bitrd 
 |-  ( ph -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) LIndF ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) <-> A. w e. ( QQ ^m ( 0 ... N ) ) ( A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 -> w = ( ( 0 ... N ) X. { 0 } ) ) ) )
160 drngnzr 
 |-  ( ( CCfld |`s QQ ) e. DivRing -> ( CCfld |`s QQ ) e. NzRing )
161 21 160 ax-mp 
 |-  ( CCfld |`s QQ ) e. NzRing
162 33 islindf3 
 |-  ( ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) e. LMod /\ ( CCfld |`s QQ ) e. NzRing ) -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) LIndF ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) <-> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : dom ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) -1-1-> _V /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. ( LIndS ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) ) )
163 27 161 162 mp2an 
 |-  ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) LIndF ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) <-> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : dom ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) -1-1-> _V /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. ( LIndS ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) )
164 eqid 
 |-  ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) = ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) )
165 47 164 dmmpti 
 |-  dom ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) = ( 0 ... N )
166 f1eq2 
 |-  ( dom ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) = ( 0 ... N ) -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : dom ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) -1-1-> _V <-> ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V ) )
167 165 166 ax-mp 
 |-  ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : dom ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) -1-1-> _V <-> ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V )
168 167 anbi1i 
 |-  ( ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : dom ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) -1-1-> _V /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. ( LIndS ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) <-> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. ( LIndS ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) )
169 163 168 bitri 
 |-  ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) LIndF ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) <-> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. ( LIndS ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) )
170 con34b 
 |-  ( ( A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 -> w = ( ( 0 ... N ) X. { 0 } ) ) <-> ( -. w = ( ( 0 ... N ) X. { 0 } ) -> -. A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) )
171 df-nel 
 |-  ( w e/ { ( ( 0 ... N ) X. { 0 } ) } <-> -. w e. { ( ( 0 ... N ) X. { 0 } ) } )
172 velsn 
 |-  ( w e. { ( ( 0 ... N ) X. { 0 } ) } <-> w = ( ( 0 ... N ) X. { 0 } ) )
173 171 172 xchbinx 
 |-  ( w e/ { ( ( 0 ... N ) X. { 0 } ) } <-> -. w = ( ( 0 ... N ) X. { 0 } ) )
174 173 imbi1i 
 |-  ( ( w e/ { ( ( 0 ... N ) X. { 0 } ) } -> -. A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) <-> ( -. w = ( ( 0 ... N ) X. { 0 } ) -> -. A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) )
175 170 174 bitr4i 
 |-  ( ( A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 -> w = ( ( 0 ... N ) X. { 0 } ) ) <-> ( w e/ { ( ( 0 ... N ) X. { 0 } ) } -> -. A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) )
176 175 ralbii 
 |-  ( A. w e. ( QQ ^m ( 0 ... N ) ) ( A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 -> w = ( ( 0 ... N ) X. { 0 } ) ) <-> A. w e. ( QQ ^m ( 0 ... N ) ) ( w e/ { ( ( 0 ... N ) X. { 0 } ) } -> -. A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) )
177 raldifb 
 |-  ( A. w e. ( QQ ^m ( 0 ... N ) ) ( w e/ { ( ( 0 ... N ) X. { 0 } ) } -> -. A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) <-> A. w e. ( ( QQ ^m ( 0 ... N ) ) \ { ( ( 0 ... N ) X. { 0 } ) } ) -. A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 )
178 ralnex 
 |-  ( A. w e. ( ( QQ ^m ( 0 ... N ) ) \ { ( ( 0 ... N ) X. { 0 } ) } ) -. A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 <-> -. E. w e. ( ( QQ ^m ( 0 ... N ) ) \ { ( ( 0 ... N ) X. { 0 } ) } ) A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 )
179 176 177 178 3bitri 
 |-  ( A. w e. ( QQ ^m ( 0 ... N ) ) ( A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 -> w = ( ( 0 ... N ) X. { 0 } ) ) <-> -. E. w e. ( ( QQ ^m ( 0 ... N ) ) \ { ( ( 0 ... N ) X. { 0 } ) } ) A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 )
180 159 169 179 3bitr3g 
 |-  ( ph -> ( ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. ( LIndS ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) <-> -. E. w e. ( ( QQ ^m ( 0 ... N ) ) \ { ( ( 0 ... N ) X. { 0 } ) } ) A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) )
181 eqid 
 |-  ( LSubSp ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) = ( LSubSp ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
182 31 181 lssmre 
 |-  ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) e. LMod -> ( LSubSp ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) e. ( Moore ` ( QQ ^m ( 1 ... N ) ) ) )
183 27 182 ax-mp 
 |-  ( LSubSp ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) e. ( Moore ` ( QQ ^m ( 1 ... N ) ) )
184 183 a1i 
 |-  ( ( ph /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. ( LIndS ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) -> ( LSubSp ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) e. ( Moore ` ( QQ ^m ( 1 ... N ) ) ) )
185 eqid 
 |-  ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) = ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
186 eqid 
 |-  ( mrCls ` ( LSubSp ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) = ( mrCls ` ( LSubSp ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) )
187 181 185 186 mrclsp 
 |-  ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) e. LMod -> ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) = ( mrCls ` ( LSubSp ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) )
188 27 187 ax-mp 
 |-  ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) = ( mrCls ` ( LSubSp ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) )
189 eqid 
 |-  ( mrInd ` ( LSubSp ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) = ( mrInd ` ( LSubSp ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) )
190 33 islvec 
 |-  ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) e. LVec <-> ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) e. LMod /\ ( CCfld |`s QQ ) e. DivRing ) )
191 27 21 190 mpbir2an 
 |-  ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) e. LVec
192 181 188 31 lssacsex 
 |-  ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) e. LVec -> ( ( LSubSp ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) e. ( ACS ` ( QQ ^m ( 1 ... N ) ) ) /\ A. z e. ~P ( QQ ^m ( 1 ... N ) ) A. x e. ( QQ ^m ( 1 ... N ) ) A. y e. ( ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ` ( z u. { x } ) ) \ ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ` z ) ) x e. ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ` ( z u. { y } ) ) ) )
193 192 simprd 
 |-  ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) e. LVec -> A. z e. ~P ( QQ ^m ( 1 ... N ) ) A. x e. ( QQ ^m ( 1 ... N ) ) A. y e. ( ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ` ( z u. { x } ) ) \ ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ` z ) ) x e. ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ` ( z u. { y } ) ) )
194 191 193 ax-mp 
 |-  A. z e. ~P ( QQ ^m ( 1 ... N ) ) A. x e. ( QQ ^m ( 1 ... N ) ) A. y e. ( ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ` ( z u. { x } ) ) \ ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ` z ) ) x e. ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ` ( z u. { y } ) )
195 194 a1i 
 |-  ( ( ph /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. ( LIndS ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) -> A. z e. ~P ( QQ ^m ( 1 ... N ) ) A. x e. ( QQ ^m ( 1 ... N ) ) A. y e. ( ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ` ( z u. { x } ) ) \ ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ` z ) ) x e. ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ` ( z u. { y } ) ) )
196 19 frnd 
 |-  ( ph -> ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) C_ ( QQ ^m ( 1 ... N ) ) )
197 dif0 
 |-  ( ( QQ ^m ( 1 ... N ) ) \ (/) ) = ( QQ ^m ( 1 ... N ) )
198 196 197 sseqtrrdi 
 |-  ( ph -> ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) C_ ( ( QQ ^m ( 1 ... N ) ) \ (/) ) )
199 198 adantr 
 |-  ( ( ph /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. ( LIndS ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) -> ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) C_ ( ( QQ ^m ( 1 ... N ) ) \ (/) ) )
200 eqid 
 |-  ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) = ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
201 200 25 31 uvcff 
 |-  ( ( ( CCfld |`s QQ ) e. Ring /\ ( 1 ... N ) e. Fin ) -> ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) : ( 1 ... N ) --> ( QQ ^m ( 1 ... N ) ) )
202 23 24 201 mp2an 
 |-  ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) : ( 1 ... N ) --> ( QQ ^m ( 1 ... N ) )
203 frn 
 |-  ( ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) : ( 1 ... N ) --> ( QQ ^m ( 1 ... N ) ) -> ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) C_ ( QQ ^m ( 1 ... N ) ) )
204 202 203 ax-mp 
 |-  ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) C_ ( QQ ^m ( 1 ... N ) )
205 204 197 sseqtrri 
 |-  ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) C_ ( ( QQ ^m ( 1 ... N ) ) \ (/) )
206 205 a1i 
 |-  ( ( ph /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. ( LIndS ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) -> ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) C_ ( ( QQ ^m ( 1 ... N ) ) \ (/) ) )
207 un0 
 |-  ( ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) u. (/) ) = ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
208 207 fveq2i 
 |-  ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ` ( ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) u. (/) ) ) = ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ` ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) )
209 eqid 
 |-  ( LBasis ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) = ( LBasis ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
210 25 200 209 frlmlbs 
 |-  ( ( ( CCfld |`s QQ ) e. Ring /\ ( 1 ... N ) e. Fin ) -> ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) e. ( LBasis ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) )
211 23 24 210 mp2an 
 |-  ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) e. ( LBasis ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
212 31 209 185 lbssp 
 |-  ( ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) e. ( LBasis ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) -> ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ` ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) ) = ( QQ ^m ( 1 ... N ) ) )
213 211 212 ax-mp 
 |-  ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ` ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) ) = ( QQ ^m ( 1 ... N ) )
214 208 213 eqtri 
 |-  ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ` ( ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) u. (/) ) ) = ( QQ ^m ( 1 ... N ) )
215 196 214 sseqtrrdi 
 |-  ( ph -> ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) C_ ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ` ( ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) u. (/) ) ) )
216 215 adantr 
 |-  ( ( ph /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. ( LIndS ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) -> ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) C_ ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ` ( ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) u. (/) ) ) )
217 un0 
 |-  ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) u. (/) ) = ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) )
218 27 161 pm3.2i 
 |-  ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) e. LMod /\ ( CCfld |`s QQ ) e. NzRing )
219 185 33 lindsind2 
 |-  ( ( ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) e. LMod /\ ( CCfld |`s QQ ) e. NzRing ) /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. ( LIndS ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) /\ x e. ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) -> -. x e. ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ` ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) \ { x } ) ) )
220 218 219 mp3an1 
 |-  ( ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. ( LIndS ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) /\ x e. ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) -> -. x e. ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ` ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) \ { x } ) ) )
221 220 ralrimiva 
 |-  ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. ( LIndS ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) -> A. x e. ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) -. x e. ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ` ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) \ { x } ) ) )
222 188 189 ismri2 
 |-  ( ( ( LSubSp ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) e. ( Moore ` ( QQ ^m ( 1 ... N ) ) ) /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) C_ ( QQ ^m ( 1 ... N ) ) ) -> ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. ( mrInd ` ( LSubSp ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) <-> A. x e. ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) -. x e. ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ` ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) \ { x } ) ) ) )
223 183 196 222 sylancr 
 |-  ( ph -> ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. ( mrInd ` ( LSubSp ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) <-> A. x e. ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) -. x e. ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ` ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) \ { x } ) ) ) )
224 223 biimpar 
 |-  ( ( ph /\ A. x e. ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) -. x e. ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ` ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) \ { x } ) ) ) -> ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. ( mrInd ` ( LSubSp ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) )
225 221 224 sylan2 
 |-  ( ( ph /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. ( LIndS ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) -> ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. ( mrInd ` ( LSubSp ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) )
226 217 225 eqeltrid 
 |-  ( ( ph /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. ( LIndS ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) -> ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) u. (/) ) e. ( mrInd ` ( LSubSp ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) )
227 mptfi 
 |-  ( ( 0 ... N ) e. Fin -> ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. Fin )
228 rnfi 
 |-  ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. Fin -> ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. Fin )
229 28 227 228 mp2b 
 |-  ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. Fin
230 229 orci 
 |-  ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. Fin \/ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) e. Fin )
231 230 a1i 
 |-  ( ( ph /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. ( LIndS ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) -> ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. Fin \/ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) e. Fin ) )
232 184 188 189 195 199 206 216 226 231 mreexexd 
 |-  ( ( ph /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. ( LIndS ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) -> E. v e. ~P ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~~ v /\ ( v u. (/) ) e. ( mrInd ` ( LSubSp ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) ) )
233 232 ex 
 |-  ( ph -> ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. ( LIndS ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) -> E. v e. ~P ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~~ v /\ ( v u. (/) ) e. ( mrInd ` ( LSubSp ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) ) ) )
234 ovex 
 |-  ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) e. _V
235 234 rnex 
 |-  ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) e. _V
236 elpwi 
 |-  ( v e. ~P ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) -> v C_ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) )
237 ssdomg 
 |-  ( ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) e. _V -> ( v C_ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) -> v ~<_ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) ) )
238 235 236 237 mpsyl 
 |-  ( v e. ~P ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) -> v ~<_ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) )
239 endomtr 
 |-  ( ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~~ v /\ v ~<_ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) ) -> ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~<_ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) )
240 239 ancoms 
 |-  ( ( v ~<_ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~~ v ) -> ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~<_ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) )
241 f1f1orn 
 |-  ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V -> ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-onto-> ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) )
242 ovex 
 |-  ( 0 ... N ) e. _V
243 242 f1oen 
 |-  ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-onto-> ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) -> ( 0 ... N ) ~~ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) )
244 241 243 syl 
 |-  ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V -> ( 0 ... N ) ~~ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) )
245 endomtr 
 |-  ( ( ( 0 ... N ) ~~ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~<_ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) ) -> ( 0 ... N ) ~<_ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) )
246 200 uvcendim 
 |-  ( ( ( CCfld |`s QQ ) e. NzRing /\ ( 1 ... N ) e. Fin ) -> ( 1 ... N ) ~~ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) )
247 161 24 246 mp2an 
 |-  ( 1 ... N ) ~~ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
248 247 ensymi 
 |-  ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) ~~ ( 1 ... N )
249 domentr 
 |-  ( ( ( 0 ... N ) ~<_ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) /\ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) ~~ ( 1 ... N ) ) -> ( 0 ... N ) ~<_ ( 1 ... N ) )
250 hashdom 
 |-  ( ( ( 0 ... N ) e. Fin /\ ( 1 ... N ) e. Fin ) -> ( ( # ` ( 0 ... N ) ) <_ ( # ` ( 1 ... N ) ) <-> ( 0 ... N ) ~<_ ( 1 ... N ) ) )
251 28 24 250 mp2an 
 |-  ( ( # ` ( 0 ... N ) ) <_ ( # ` ( 1 ... N ) ) <-> ( 0 ... N ) ~<_ ( 1 ... N ) )
252 hashfz0 
 |-  ( N e. NN0 -> ( # ` ( 0 ... N ) ) = ( N + 1 ) )
253 2 252 syl 
 |-  ( ph -> ( # ` ( 0 ... N ) ) = ( N + 1 ) )
254 hashfz1 
 |-  ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )
255 2 254 syl 
 |-  ( ph -> ( # ` ( 1 ... N ) ) = N )
256 253 255 breq12d 
 |-  ( ph -> ( ( # ` ( 0 ... N ) ) <_ ( # ` ( 1 ... N ) ) <-> ( N + 1 ) <_ N ) )
257 251 256 bitr3id 
 |-  ( ph -> ( ( 0 ... N ) ~<_ ( 1 ... N ) <-> ( N + 1 ) <_ N ) )
258 249 257 syl5ib 
 |-  ( ph -> ( ( ( 0 ... N ) ~<_ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) /\ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) ~~ ( 1 ... N ) ) -> ( N + 1 ) <_ N ) )
259 248 258 mpan2i 
 |-  ( ph -> ( ( 0 ... N ) ~<_ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) -> ( N + 1 ) <_ N ) )
260 245 259 syl5 
 |-  ( ph -> ( ( ( 0 ... N ) ~~ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~<_ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) ) -> ( N + 1 ) <_ N ) )
261 260 expd 
 |-  ( ph -> ( ( 0 ... N ) ~~ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) -> ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~<_ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) -> ( N + 1 ) <_ N ) ) )
262 244 261 syl5 
 |-  ( ph -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V -> ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~<_ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) -> ( N + 1 ) <_ N ) ) )
263 262 com23 
 |-  ( ph -> ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~<_ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V -> ( N + 1 ) <_ N ) ) )
264 240 263 syl5 
 |-  ( ph -> ( ( v ~<_ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~~ v ) -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V -> ( N + 1 ) <_ N ) ) )
265 264 expdimp 
 |-  ( ( ph /\ v ~<_ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) ) -> ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~~ v -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V -> ( N + 1 ) <_ N ) ) )
266 238 265 sylan2 
 |-  ( ( ph /\ v e. ~P ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) ) -> ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~~ v -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V -> ( N + 1 ) <_ N ) ) )
267 266 adantrd 
 |-  ( ( ph /\ v e. ~P ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) ) -> ( ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~~ v /\ ( v u. (/) ) e. ( mrInd ` ( LSubSp ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) ) -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V -> ( N + 1 ) <_ N ) ) )
268 267 rexlimdva 
 |-  ( ph -> ( E. v e. ~P ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~~ v /\ ( v u. (/) ) e. ( mrInd ` ( LSubSp ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) ) -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V -> ( N + 1 ) <_ N ) ) )
269 233 268 syld 
 |-  ( ph -> ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. ( LIndS ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V -> ( N + 1 ) <_ N ) ) )
270 269 impd 
 |-  ( ph -> ( ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. ( LIndS ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) /\ ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V ) -> ( N + 1 ) <_ N ) )
271 270 ancomsd 
 |-  ( ph -> ( ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. ( LIndS ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) -> ( N + 1 ) <_ N ) )
272 180 271 sylbird 
 |-  ( ph -> ( -. E. w e. ( ( QQ ^m ( 0 ... N ) ) \ { ( ( 0 ... N ) X. { 0 } ) } ) A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 -> ( N + 1 ) <_ N ) )
273 12 272 mt3d 
 |-  ( ph -> E. w e. ( ( QQ ^m ( 0 ... N ) ) \ { ( ( 0 ... N ) X. { 0 } ) } ) A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 )
274 eldifsn 
 |-  ( w e. ( ( QQ ^m ( 0 ... N ) ) \ { ( ( 0 ... N ) X. { 0 } ) } ) <-> ( w e. ( QQ ^m ( 0 ... N ) ) /\ w =/= ( ( 0 ... N ) X. { 0 } ) ) )
275 44 anim1i 
 |-  ( ( w e. ( QQ ^m ( 0 ... N ) ) /\ w =/= ( ( 0 ... N ) X. { 0 } ) ) -> ( w : ( 0 ... N ) --> QQ /\ w =/= ( ( 0 ... N ) X. { 0 } ) ) )
276 274 275 sylbi 
 |-  ( w e. ( ( QQ ^m ( 0 ... N ) ) \ { ( ( 0 ... N ) X. { 0 } ) } ) -> ( w : ( 0 ... N ) --> QQ /\ w =/= ( ( 0 ... N ) X. { 0 } ) ) )
277 95 a1i 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> QQ C_ CC )
278 2 adantr 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> N e. NN0 )
279 277 278 55 elplyd 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) e. ( Poly ` QQ ) )
280 279 adantrr 
 |-  ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ w =/= ( ( 0 ... N ) X. { 0 } ) ) ) -> ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) e. ( Poly ` QQ ) )
281 uzdisj 
 |-  ( ( 0 ... ( ( N + 1 ) - 1 ) ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/)
282 2 nn0cnd 
 |-  ( ph -> N e. CC )
283 pncan1 
 |-  ( N e. CC -> ( ( N + 1 ) - 1 ) = N )
284 282 283 syl 
 |-  ( ph -> ( ( N + 1 ) - 1 ) = N )
285 284 oveq2d 
 |-  ( ph -> ( 0 ... ( ( N + 1 ) - 1 ) ) = ( 0 ... N ) )
286 285 ineq1d 
 |-  ( ph -> ( ( 0 ... ( ( N + 1 ) - 1 ) ) i^i ( ZZ>= ` ( N + 1 ) ) ) = ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) )
287 281 286 eqtr3id 
 |-  ( ph -> (/) = ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) )
288 287 eqcomd 
 |-  ( ph -> ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/) )
289 130 fconst 
 |-  ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) : ( ZZ>= ` ( N + 1 ) ) --> { 0 }
290 snssi 
 |-  ( 0 e. QQ -> { 0 } C_ QQ )
291 98 99 290 mp2b 
 |-  { 0 } C_ QQ
292 291 95 sstri 
 |-  { 0 } C_ CC
293 fss 
 |-  ( ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) : ( ZZ>= ` ( N + 1 ) ) --> { 0 } /\ { 0 } C_ CC ) -> ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) : ( ZZ>= ` ( N + 1 ) ) --> CC )
294 289 292 293 mp2an 
 |-  ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) : ( ZZ>= ` ( N + 1 ) ) --> CC
295 fun 
 |-  ( ( ( w : ( 0 ... N ) --> QQ /\ ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) : ( ZZ>= ` ( N + 1 ) ) --> CC ) /\ ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/) ) -> ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) : ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) --> ( QQ u. CC ) )
296 294 295 mpanl2 
 |-  ( ( w : ( 0 ... N ) --> QQ /\ ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/) ) -> ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) : ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) --> ( QQ u. CC ) )
297 288 296 sylan2 
 |-  ( ( w : ( 0 ... N ) --> QQ /\ ph ) -> ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) : ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) --> ( QQ u. CC ) )
298 297 ancoms 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) : ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) --> ( QQ u. CC ) )
299 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
300 9 299 eleqtrdi 
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` 0 ) )
301 uzsplit 
 |-  ( ( N + 1 ) e. ( ZZ>= ` 0 ) -> ( ZZ>= ` 0 ) = ( ( 0 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) )
302 300 301 syl 
 |-  ( ph -> ( ZZ>= ` 0 ) = ( ( 0 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) )
303 299 302 syl5eq 
 |-  ( ph -> NN0 = ( ( 0 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) )
304 285 uneq1d 
 |-  ( ph -> ( ( 0 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) = ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
305 303 304 eqtr2d 
 |-  ( ph -> ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) = NN0 )
306 ssequn1 
 |-  ( QQ C_ CC <-> ( QQ u. CC ) = CC )
307 95 306 mpbi 
 |-  ( QQ u. CC ) = CC
308 307 a1i 
 |-  ( ph -> ( QQ u. CC ) = CC )
309 305 308 feq23d 
 |-  ( ph -> ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) : ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) --> ( QQ u. CC ) <-> ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) : NN0 --> CC ) )
310 309 adantr 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) : ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) --> ( QQ u. CC ) <-> ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) : NN0 --> CC ) )
311 298 310 mpbid 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) : NN0 --> CC )
312 ffn 
 |-  ( w : ( 0 ... N ) --> QQ -> w Fn ( 0 ... N ) )
313 fnimadisj 
 |-  ( ( w Fn ( 0 ... N ) /\ ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/) ) -> ( w " ( ZZ>= ` ( N + 1 ) ) ) = (/) )
314 312 288 313 syl2anr 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( w " ( ZZ>= ` ( N + 1 ) ) ) = (/) )
315 2 nn0zd 
 |-  ( ph -> N e. ZZ )
316 315 peano2zd 
 |-  ( ph -> ( N + 1 ) e. ZZ )
317 uzid 
 |-  ( ( N + 1 ) e. ZZ -> ( N + 1 ) e. ( ZZ>= ` ( N + 1 ) ) )
318 ne0i 
 |-  ( ( N + 1 ) e. ( ZZ>= ` ( N + 1 ) ) -> ( ZZ>= ` ( N + 1 ) ) =/= (/) )
319 316 317 318 3syl 
 |-  ( ph -> ( ZZ>= ` ( N + 1 ) ) =/= (/) )
320 inidm 
 |-  ( ( ZZ>= ` ( N + 1 ) ) i^i ( ZZ>= ` ( N + 1 ) ) ) = ( ZZ>= ` ( N + 1 ) )
321 320 neeq1i 
 |-  ( ( ( ZZ>= ` ( N + 1 ) ) i^i ( ZZ>= ` ( N + 1 ) ) ) =/= (/) <-> ( ZZ>= ` ( N + 1 ) ) =/= (/) )
322 319 321 sylibr 
 |-  ( ph -> ( ( ZZ>= ` ( N + 1 ) ) i^i ( ZZ>= ` ( N + 1 ) ) ) =/= (/) )
323 xpima2 
 |-  ( ( ( ZZ>= ` ( N + 1 ) ) i^i ( ZZ>= ` ( N + 1 ) ) ) =/= (/) -> ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
324 322 323 syl 
 |-  ( ph -> ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
325 324 adantr 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
326 314 325 uneq12d 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( w " ( ZZ>= ` ( N + 1 ) ) ) u. ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) " ( ZZ>= ` ( N + 1 ) ) ) ) = ( (/) u. { 0 } ) )
327 imaundir 
 |-  ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) " ( ZZ>= ` ( N + 1 ) ) ) = ( ( w " ( ZZ>= ` ( N + 1 ) ) ) u. ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) " ( ZZ>= ` ( N + 1 ) ) ) )
328 uncom 
 |-  ( (/) u. { 0 } ) = ( { 0 } u. (/) )
329 un0 
 |-  ( { 0 } u. (/) ) = { 0 }
330 328 329 eqtr2i 
 |-  { 0 } = ( (/) u. { 0 } )
331 326 327 330 3eqtr4g 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
332 288 312 anim12ci 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( w Fn ( 0 ... N ) /\ ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/) ) )
333 fnconstg 
 |-  ( 0 e. _V -> ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) Fn ( ZZ>= ` ( N + 1 ) ) )
334 130 333 ax-mp 
 |-  ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) Fn ( ZZ>= ` ( N + 1 ) )
335 fvun1 
 |-  ( ( w Fn ( 0 ... N ) /\ ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) Fn ( ZZ>= ` ( N + 1 ) ) /\ ( ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/) /\ k e. ( 0 ... N ) ) ) -> ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) ` k ) = ( w ` k ) )
336 334 335 mp3an2 
 |-  ( ( w Fn ( 0 ... N ) /\ ( ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/) /\ k e. ( 0 ... N ) ) ) -> ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) ` k ) = ( w ` k ) )
337 336 anassrs 
 |-  ( ( ( w Fn ( 0 ... N ) /\ ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/) ) /\ k e. ( 0 ... N ) ) -> ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) ` k ) = ( w ` k ) )
338 332 337 sylan 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) ` k ) = ( w ` k ) )
339 338 eqcomd 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( w ` k ) = ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) ` k ) )
340 339 oveq1d 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( ( w ` k ) x. ( y ^ k ) ) = ( ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) ` k ) x. ( y ^ k ) ) )
341 340 sumeq2dv 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) = sum_ k e. ( 0 ... N ) ( ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) ` k ) x. ( y ^ k ) ) )
342 341 mpteq2dv 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) = ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) ` k ) x. ( y ^ k ) ) ) )
343 279 278 311 331 342 coeeq 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( coeff ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ) = ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) )
344 343 reseq1d 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( coeff ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ) |` ( 0 ... N ) ) = ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) |` ( 0 ... N ) ) )
345 res0 
 |-  ( w |` (/) ) = (/)
346 287 reseq2d 
 |-  ( ph -> ( w |` (/) ) = ( w |` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) ) )
347 res0 
 |-  ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) |` (/) ) = (/)
348 287 reseq2d 
 |-  ( ph -> ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) |` (/) ) = ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) |` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) ) )
349 347 348 eqtr3id 
 |-  ( ph -> (/) = ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) |` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) ) )
350 345 346 349 3eqtr3a 
 |-  ( ph -> ( w |` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) ) = ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) |` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) ) )
351 fss 
 |-  ( ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) : ( ZZ>= ` ( N + 1 ) ) --> { 0 } /\ { 0 } C_ QQ ) -> ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) : ( ZZ>= ` ( N + 1 ) ) --> QQ )
352 289 291 351 mp2an 
 |-  ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) : ( ZZ>= ` ( N + 1 ) ) --> QQ
353 fresaunres1 
 |-  ( ( w : ( 0 ... N ) --> QQ /\ ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) : ( ZZ>= ` ( N + 1 ) ) --> QQ /\ ( w |` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) ) = ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) |` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) ) ) -> ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) |` ( 0 ... N ) ) = w )
354 352 353 mp3an2 
 |-  ( ( w : ( 0 ... N ) --> QQ /\ ( w |` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) ) = ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) |` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) ) ) -> ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) |` ( 0 ... N ) ) = w )
355 350 354 sylan2 
 |-  ( ( w : ( 0 ... N ) --> QQ /\ ph ) -> ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) |` ( 0 ... N ) ) = w )
356 355 ancoms 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) |` ( 0 ... N ) ) = w )
357 344 356 eqtrd 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( coeff ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ) |` ( 0 ... N ) ) = w )
358 fveq2 
 |-  ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) = 0p -> ( coeff ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ) = ( coeff ` 0p ) )
359 358 reseq1d 
 |-  ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) = 0p -> ( ( coeff ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ) |` ( 0 ... N ) ) = ( ( coeff ` 0p ) |` ( 0 ... N ) ) )
360 eqtr2 
 |-  ( ( ( ( coeff ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ) |` ( 0 ... N ) ) = w /\ ( ( coeff ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ) |` ( 0 ... N ) ) = ( ( coeff ` 0p ) |` ( 0 ... N ) ) ) -> w = ( ( coeff ` 0p ) |` ( 0 ... N ) ) )
361 coe0 
 |-  ( coeff ` 0p ) = ( NN0 X. { 0 } )
362 361 reseq1i 
 |-  ( ( coeff ` 0p ) |` ( 0 ... N ) ) = ( ( NN0 X. { 0 } ) |` ( 0 ... N ) )
363 elfznn0 
 |-  ( x e. ( 0 ... N ) -> x e. NN0 )
364 363 ssriv 
 |-  ( 0 ... N ) C_ NN0
365 xpssres 
 |-  ( ( 0 ... N ) C_ NN0 -> ( ( NN0 X. { 0 } ) |` ( 0 ... N ) ) = ( ( 0 ... N ) X. { 0 } ) )
366 364 365 ax-mp 
 |-  ( ( NN0 X. { 0 } ) |` ( 0 ... N ) ) = ( ( 0 ... N ) X. { 0 } )
367 362 366 eqtri 
 |-  ( ( coeff ` 0p ) |` ( 0 ... N ) ) = ( ( 0 ... N ) X. { 0 } )
368 360 367 eqtrdi 
 |-  ( ( ( ( coeff ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ) |` ( 0 ... N ) ) = w /\ ( ( coeff ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ) |` ( 0 ... N ) ) = ( ( coeff ` 0p ) |` ( 0 ... N ) ) ) -> w = ( ( 0 ... N ) X. { 0 } ) )
369 368 ex 
 |-  ( ( ( coeff ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ) |` ( 0 ... N ) ) = w -> ( ( ( coeff ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ) |` ( 0 ... N ) ) = ( ( coeff ` 0p ) |` ( 0 ... N ) ) -> w = ( ( 0 ... N ) X. { 0 } ) ) )
370 357 359 369 syl2im 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) = 0p -> w = ( ( 0 ... N ) X. { 0 } ) ) )
371 370 necon3d 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( w =/= ( ( 0 ... N ) X. { 0 } ) -> ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) =/= 0p ) )
372 371 impr 
 |-  ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ w =/= ( ( 0 ... N ) X. { 0 } ) ) ) -> ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) =/= 0p )
373 eldifsn 
 |-  ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) e. ( ( Poly ` QQ ) \ { 0p } ) <-> ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) e. ( Poly ` QQ ) /\ ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) =/= 0p ) )
374 280 372 373 sylanbrc 
 |-  ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ w =/= ( ( 0 ... N ) X. { 0 } ) ) ) -> ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) e. ( ( Poly ` QQ ) \ { 0p } ) )
375 374 adantrr 
 |-  ( ( ph /\ ( ( w : ( 0 ... N ) --> QQ /\ w =/= ( ( 0 ... N ) X. { 0 } ) ) /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) -> ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) e. ( ( Poly ` QQ ) \ { 0p } ) )
376 oveq1 
 |-  ( y = A -> ( y ^ k ) = ( A ^ k ) )
377 376 oveq2d 
 |-  ( y = A -> ( ( w ` k ) x. ( y ^ k ) ) = ( ( w ` k ) x. ( A ^ k ) ) )
378 377 sumeq2sdv 
 |-  ( y = A -> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) = sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( A ^ k ) ) )
379 eqid 
 |-  ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) = ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) )
380 sumex 
 |-  sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( A ^ k ) ) e. _V
381 378 379 380 fvmpt 
 |-  ( A e. CC -> ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ` A ) = sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( A ^ k ) ) )
382 1 381 syl 
 |-  ( ph -> ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ` A ) = sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( A ^ k ) ) )
383 382 adantr 
 |-  ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) -> ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ` A ) = sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( A ^ k ) ) )
384 109 adantll 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( w ` k ) e. CC )
385 3 adantlr 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> X e. CC )
386 112 385 mulcld 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> ( C x. X ) e. CC )
387 386 adantllr 
 |-  ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> ( C x. X ) e. CC )
388 53 384 387 fsummulc2 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( ( w ` k ) x. sum_ n e. ( 1 ... N ) ( C x. X ) ) = sum_ n e. ( 1 ... N ) ( ( w ` k ) x. ( C x. X ) ) )
389 5 oveq2d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( w ` k ) x. ( A ^ k ) ) = ( ( w ` k ) x. sum_ n e. ( 1 ... N ) ( C x. X ) ) )
390 389 adantlr 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( ( w ` k ) x. ( A ^ k ) ) = ( ( w ` k ) x. sum_ n e. ( 1 ... N ) ( C x. X ) ) )
391 384 adantr 
 |-  ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> ( w ` k ) e. CC )
392 112 adantllr 
 |-  ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> C e. CC )
393 simpll 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ph )
394 393 3 sylan 
 |-  ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> X e. CC )
395 391 392 394 mulassd 
 |-  ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( w ` k ) x. C ) x. X ) = ( ( w ` k ) x. ( C x. X ) ) )
396 395 sumeq2dv 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> sum_ n e. ( 1 ... N ) ( ( ( w ` k ) x. C ) x. X ) = sum_ n e. ( 1 ... N ) ( ( w ` k ) x. ( C x. X ) ) )
397 388 390 396 3eqtr4d 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( ( w ` k ) x. ( A ^ k ) ) = sum_ n e. ( 1 ... N ) ( ( ( w ` k ) x. C ) x. X ) )
398 397 sumeq2dv 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( A ^ k ) ) = sum_ k e. ( 0 ... N ) sum_ n e. ( 1 ... N ) ( ( ( w ` k ) x. C ) x. X ) )
399 109 ad2ant2lr 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ ( k e. ( 0 ... N ) /\ n e. ( 1 ... N ) ) ) -> ( w ` k ) e. CC )
400 112 anasss 
 |-  ( ( ph /\ ( k e. ( 0 ... N ) /\ n e. ( 1 ... N ) ) ) -> C e. CC )
401 400 adantlr 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ ( k e. ( 0 ... N ) /\ n e. ( 1 ... N ) ) ) -> C e. CC )
402 399 401 mulcld 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ ( k e. ( 0 ... N ) /\ n e. ( 1 ... N ) ) ) -> ( ( w ` k ) x. C ) e. CC )
403 3 ad2ant2rl 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ ( k e. ( 0 ... N ) /\ n e. ( 1 ... N ) ) ) -> X e. CC )
404 402 403 mulcld 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ ( k e. ( 0 ... N ) /\ n e. ( 1 ... N ) ) ) -> ( ( ( w ` k ) x. C ) x. X ) e. CC )
405 45 71 404 fsumcom 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> sum_ k e. ( 0 ... N ) sum_ n e. ( 1 ... N ) ( ( ( w ` k ) x. C ) x. X ) = sum_ n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( ( w ` k ) x. C ) x. X ) )
406 398 405 eqtrd 
 |-  ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( A ^ k ) ) = sum_ n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( ( w ` k ) x. C ) x. X ) )
407 406 adantrr 
 |-  ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) -> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( A ^ k ) ) = sum_ n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( ( w ` k ) x. C ) x. X ) )
408 nfv 
 |-  F/ n ph
409 nfv 
 |-  F/ n w : ( 0 ... N ) --> QQ
410 nfra1 
 |-  F/ n A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0
411 409 410 nfan 
 |-  F/ n ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 )
412 408 411 nfan 
 |-  F/ n ( ph /\ ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) )
413 rspa 
 |-  ( ( A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 /\ n e. ( 1 ... N ) ) -> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 )
414 413 oveq1d 
 |-  ( ( A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 /\ n e. ( 1 ... N ) ) -> ( sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) x. X ) = ( 0 x. X ) )
415 414 adantll 
 |-  ( ( ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) /\ n e. ( 1 ... N ) ) -> ( sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) x. X ) = ( 0 x. X ) )
416 415 adantll 
 |-  ( ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) /\ n e. ( 1 ... N ) ) -> ( sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) x. X ) = ( 0 x. X ) )
417 3 adantlr 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> X e. CC )
418 94 417 115 fsummulc1 
 |-  ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> ( sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) x. X ) = sum_ k e. ( 0 ... N ) ( ( ( w ` k ) x. C ) x. X ) )
419 418 adantlrr 
 |-  ( ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) /\ n e. ( 1 ... N ) ) -> ( sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) x. X ) = sum_ k e. ( 0 ... N ) ( ( ( w ` k ) x. C ) x. X ) )
420 3 mul02d 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( 0 x. X ) = 0 )
421 420 adantlr 
 |-  ( ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) /\ n e. ( 1 ... N ) ) -> ( 0 x. X ) = 0 )
422 416 419 421 3eqtr3d 
 |-  ( ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) /\ n e. ( 1 ... N ) ) -> sum_ k e. ( 0 ... N ) ( ( ( w ` k ) x. C ) x. X ) = 0 )
423 422 ex 
 |-  ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) -> ( n e. ( 1 ... N ) -> sum_ k e. ( 0 ... N ) ( ( ( w ` k ) x. C ) x. X ) = 0 ) )
424 412 423 ralrimi 
 |-  ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) -> A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( ( w ` k ) x. C ) x. X ) = 0 )
425 424 sumeq2d 
 |-  ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) -> sum_ n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( ( w ` k ) x. C ) x. X ) = sum_ n e. ( 1 ... N ) 0 )
426 407 425 eqtrd 
 |-  ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) -> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( A ^ k ) ) = sum_ n e. ( 1 ... N ) 0 )
427 24 olci 
 |-  ( ( 1 ... N ) C_ ( ZZ>= ` B ) \/ ( 1 ... N ) e. Fin )
428 sumz 
 |-  ( ( ( 1 ... N ) C_ ( ZZ>= ` B ) \/ ( 1 ... N ) e. Fin ) -> sum_ n e. ( 1 ... N ) 0 = 0 )
429 427 428 ax-mp 
 |-  sum_ n e. ( 1 ... N ) 0 = 0
430 426 429 eqtrdi 
 |-  ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) -> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( A ^ k ) ) = 0 )
431 383 430 eqtrd 
 |-  ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) -> ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ` A ) = 0 )
432 431 adantrlr 
 |-  ( ( ph /\ ( ( w : ( 0 ... N ) --> QQ /\ w =/= ( ( 0 ... N ) X. { 0 } ) ) /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) -> ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ` A ) = 0 )
433 fveq1 
 |-  ( x = ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) -> ( x ` A ) = ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ` A ) )
434 433 eqeq1d 
 |-  ( x = ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) -> ( ( x ` A ) = 0 <-> ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ` A ) = 0 ) )
435 434 rspcev 
 |-  ( ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) e. ( ( Poly ` QQ ) \ { 0p } ) /\ ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ` A ) = 0 ) -> E. x e. ( ( Poly ` QQ ) \ { 0p } ) ( x ` A ) = 0 )
436 375 432 435 syl2anc 
 |-  ( ( ph /\ ( ( w : ( 0 ... N ) --> QQ /\ w =/= ( ( 0 ... N ) X. { 0 } ) ) /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) -> E. x e. ( ( Poly ` QQ ) \ { 0p } ) ( x ` A ) = 0 )
437 276 436 sylanr1 
 |-  ( ( ph /\ ( w e. ( ( QQ ^m ( 0 ... N ) ) \ { ( ( 0 ... N ) X. { 0 } ) } ) /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) -> E. x e. ( ( Poly ` QQ ) \ { 0p } ) ( x ` A ) = 0 )
438 273 437 rexlimddv 
 |-  ( ph -> E. x e. ( ( Poly ` QQ ) \ { 0p } ) ( x ` A ) = 0 )
439 elqaa 
 |-  ( A e. AA <-> ( A e. CC /\ E. x e. ( ( Poly ` QQ ) \ { 0p } ) ( x ` A ) = 0 ) )
440 1 438 439 sylanbrc 
 |-  ( ph -> A e. AA )