On Fri, 10 Apr 2020 03:33:42 -0700 (PDT), Thomas Brendan Leahy
<[email protected]> wrote:
> I've deleted the proof itself, but to give you an idea, here's an HTML file
> I made.
...
I'm trying to recover your proof of aacllem. Even after a few renames
I can't *quite* make it work in mmj2.
Below is the proof in mmj2 format.
mmj2 is reporting the following:
E-PA-0410 Theorem aacllem: Step 85: Unification failure in derivation proof
step frlmgsum. The step's formula and/or its hypotheses could not be reconciled
with the referenced Assertion. Try the Unify/Step Selector Search to find
unifiable assertions for the step.
Suggestions? It's probably a tiny problem.
--- David A. Wheeler
========
$( <MM> <PROOF_ASST> THEOREM=aacllem LOC_AFTER=?
* Lemma for other theorems about ` AA ` .
Proof by Brendan Leahy, retyped by David A. Wheeler.
(Contributed by Brendan Leahy , 3-Jan-2020.)
hh1::aacllem.0 |- ( ph -> A e. CC )
hh2::aacllem.1 |- ( ph -> N e. NN0 )
hh3::aacllem.2 |- ( ( ph /\ n e. ( 1 ... N ) )
-> X e. CC )
hh4::aacllem.3 |- ( ( ph /\ k e. ( 0 ... N ) /\ n e. ( 1 ... N ) )
-> C e. QQ )
hh5::aacllem.4 |- ( ( ph /\ k e. ( 0 ... N ) )
-> ( A ^ k ) = sum_ n e. ( 1 ... N ) ( C x. X ) )
3:h2:nn0red |- ( ph -> N e. RR )
4:3:ltp1d |- ( ph -> N < ( N + 1 ) )
5::peano2nn0 |- ( N e. NN0 -> ( N + 1 ) e. NN0 )
6:h2,5:syl |- ( ph -> ( N + 1 ) e. NN0 )
7:6:nn0red |- ( ph -> ( N + 1 ) e. RR )
8:3,7:ltnled |- ( ph
-> ( N < ( N + 1 )
<-> -. ( N + 1 ) <_ N ) )
9:4,8:mpbid |- ( ph
-> -. ( N + 1 ) <_ N )
11:h4:3expa |- ( ( ( ph /\ k e. ( 0 ... N ) )
/\ n e. ( 1 ... N ) )
-> C e. QQ )
12::eqid |- ( n e. ( 1 ... N ) |-> C ) = ( n e. ( 1 ... N ) |-> C )
13:11,12:fmptd |- ( ( ph /\ k e. ( 0 ... N ) )
-> ( n e. ( 1 ... N ) |-> C ) : ( 1 ... N ) --> QQ )
14::qex |- QQ e. _V
15::ovex |- ( 1 ... N ) e. _V
16:14,15:elmap |- ( ( n e. ( 1 ... N ) |-> C ) e. ( QQ ^m ( 1 ... N ) )
<-> ( n e. ( 1 ... N ) |-> C ) : ( 1 ... N ) --> QQ )
17:13,16:sylibr |- ( ( ph /\ k e. ( 0 ... N ) )
-> ( n e. ( 1 ... N ) |-> C ) e. ( QQ ^m ( 1 ... N ) ) )
18::eqid |- ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) )
= ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) )
19:17,18:fmptd |- ( 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. &S1
e. ( QQ ^m ( 0 ... N ) )
( ( ( ( CCfld |`s QQ )
freeLMod
( 1 ... N ) )
gsum
( &S1
oF ( .s
` ( ( CCfld |`s QQ )
freeLMod
( 1 ... N ) ) )
( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) ) ) )
= ( ( 1 ... N ) X. { 0 } )
-> &S1 = ( ( 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. &S1
e. ( QQ ^m ( 0 ... N ) )
( ( ( ( CCfld |`s QQ )
freeLMod
( 1 ... N ) )
gsum
( &S1
oF ( .s
` ( ( CCfld |`s QQ )
freeLMod
( 1 ... N ) ) )
( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) ) ) )
= ( ( 1 ... N ) X. { 0 } )
-> &S1 = ( ( 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. &S1
e. ( QQ ^m ( 0 ... N ) )
( ( ( ( CCfld |`s QQ )
freeLMod
( 1 ... N ) )
gsum
( &S1
oF ( .s
` ( ( CCfld |`s QQ )
freeLMod
( 1 ... N ) ) )
( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) ) ) )
= ( ( 1 ... N ) X. { 0 } )
-> &S1 = ( ( 0 ... N ) X. { 0 } ) ) ) )
44::elmapi |- ( &C37 e. ( QQ ^m ( 0 ... N ) )
-> &C37 : ( 0 ... N ) --> QQ )
45::fzfid |- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( 0 ... N ) e. Fin )
46::fvex |- ( &C37 ` k ) e. _V
47:46:a1i |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
-> ( &C37 ` k ) e. _V )
48:15:mptex |- ( n e. ( 1 ... N ) |-> C ) e. _V
49:48:a1i |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
-> ( n e. ( 1 ... N ) |-> C ) e. _V )
50::simpr |- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> &C37 : ( 0 ... N ) --> QQ )
51:50:feqmptd |- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> &C37 = ( k e. ( 0 ... N ) |-> ( &C37 ` k ) ) )
52::eqidd |- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) )
= ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) )
)
53:45,47,49,51,52:offval2
|- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( &C37
oF ( .s
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) ) )
= ( k
e. ( 0 ... N )
|-> ( ( &C37 ` k )
( .s
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
( n e. ( 1 ... N ) |-> C ) ) ) )
54::fzfid |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
-> ( 1 ... N ) e. Fin )
55::ffvelrn |- ( ( &C37 : ( 0 ... N ) --> QQ /\ k e. ( 0 ... N ) )
-> ( &C37 ` k ) e. QQ )
56:55:adantll |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
-> ( &C37 ` k ) e. QQ )
57:17:adantlr |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
-> ( n e. ( 1 ... N ) |-> C ) e. ( QQ ^m ( 1 ... N ) ) )
58::cnfldmul |- x. = ( .r ` CCfld )
59:20,58:ressmulr |- ( QQ e. _V
-> x. = ( .r ` ( CCfld |`s QQ ) ) )
60:14,59:ax-mp |- x. = ( .r ` ( CCfld |`s QQ ) )
61:25,31,29,54,56,57,34,60:frlmvscafval
|- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
-> ( ( &C37 ` k )
( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
( n e. ( 1 ... N ) |-> C ) )
= ( ( ( 1 ... N ) X. { ( &C37 ` k ) } )
oF x.
( n e. ( 1 ... N ) |-> C ) ) )
62:46:a1i |- ( ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
/\ n e. ( 1 ... N ) )
-> ( &C37 ` k ) e. _V )
63:11:adantllr |- ( ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
/\ n e. ( 1 ... N ) )
-> C e. QQ )
64::fconstmpt |- ( ( 1 ... N ) X. { ( &C37 ` k ) } )
= ( n e. ( 1 ... N ) |-> ( &C37 ` k ) )
65:64:a1i |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
-> ( ( 1 ... N ) X. { ( &C37 ` k ) } )
= ( n e. ( 1 ... N ) |-> ( &C37 ` k ) ) )
66::eqidd |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
-> ( n e. ( 1 ... N ) |-> C )
= ( n e. ( 1 ... N ) |-> C ) )
67:54,62,63,65,66:offval2
|- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
-> ( ( ( 1 ... N ) X. { ( &C37 ` k ) } )
oF x.
( n e. ( 1 ... N ) |-> C ) )
= ( n e. ( 1 ... N ) |-> ( ( &C37 ` k ) x. C ) ) )
68:61,67:eqtrd |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
-> ( ( &C37 ` k )
( .s ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
( n e. ( 1 ... N ) |-> C ) )
= ( n e. ( 1 ... N ) |-> ( ( &C37 ` k ) x. C ) ) )
69:68:mpteq2dva |- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( k
e. ( 0 ... N )
|-> ( ( &C37 ` k )
( .s
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
( n e. ( 1 ... N ) |-> C ) ) )
= ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> ( ( &C37 ` k ) x. C ) ) )
)
70:53,69:eqtrd |- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( &C37
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 ) |-> ( ( &C37 ` k ) x. C ) ) )
)
71:70:oveq2d |- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( &C6
&C7
( &C37
oF ( .s
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) ) ) )
= ( &C6
&C7
( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> ( ( &C37 ` k ) x. C ) )
) ) )
72::fzfid |- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( 1 ... N ) e. Fin )
73:23:a1i |- ( &W3 -> ( CCfld |`s QQ ) e. Ring )
74:56:adantlr |- ( ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ n e. ( 1 ... N ) )
/\ k e. ( 0 ... N ) )
-> ( &C37 ` k ) e. QQ )
75:11:an32s |- ( ( ( ph /\ n e. ( 1 ... N ) )
/\ k e. ( 0 ... N ) )
-> C e. QQ )
76:75:adantllr |- ( ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ n e. ( 1 ... N ) )
/\ k e. ( 0 ... N ) )
-> C e. QQ )
77::qmulcl |- ( ( ( &C37 ` k ) e. QQ /\ C e. QQ )
-> ( ( &C37 ` k ) x. C ) e. QQ )
78:74,76,77:syl2anc
|- ( ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ n e. ( 1 ... N ) )
/\ k e. ( 0 ... N ) )
-> ( ( &C37 ` k ) x. C ) e. QQ )
79:78:an32s |- ( ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
/\ n e. ( 1 ... N ) )
-> ( ( &C37 ` k ) x. C ) e. QQ )
80::eqid |- ( n e. ( 1 ... N ) |-> ( ( &C37 ` k ) x. C ) )
= ( n e. ( 1 ... N ) |-> ( ( &C37 ` k ) x. C ) )
81:79,80:fmptd |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
-> ( n e. ( 1 ... N ) |-> ( ( &C37 ` k ) x. C ) )
: ( 1 ... N )
--> QQ )
82:14,15:elmap |- ( ( n e. ( 1 ... N ) |-> ( ( &C37 ` k ) x. C ) )
e. ( QQ ^m ( 1 ... N ) )
<-> ( n e. ( 1 ... N ) |-> ( ( &C37 ` k ) x. C ) )
: ( 1 ... N )
--> QQ )
83:81,82:sylibr |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
-> ( n e. ( 1 ... N ) |-> ( ( &C37 ` k ) x. C ) )
e. ( QQ ^m ( 1 ... N ) ) )
84:45:cnvimamptfin |- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( `' ( &S2 e. ( 0 ... N ) |-> &C12 )
" &C13 )
e. Fin )
85:25,31,37,72,45,73,83,84:frlmgsum
86::cnfldbas |- CC = ( Base ` CCfld )
87::cnfldadd |- + = ( +g ` CCfld )
88::cnfldex |- CCfld e. _V
89:88:a1i |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ n e. ( 1 ... N ) )
-> CCfld e. _V )
90::fzfid |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ n e. ( 1 ... N ) )
-> ( 0 ... N ) e. Fin )
91::qsscn |- QQ C_ CC
92:91:a1i |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ n e. ( 1 ... N ) )
-> QQ C_ CC )
93::eqid |- ( k e. ( 0 ... N ) |-> ( ( &C37 ` k ) x. C ) )
= ( k e. ( 0 ... N ) |-> ( ( &C37 ` k ) x. C ) )
94:78,93:fmptd |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ n e. ( 1 ... N ) )
-> ( k e. ( 0 ... N ) |-> ( ( &C37 ` k ) x. C ) )
: ( 0 ... N )
--> QQ )
95::0z |- 0 e. ZZ
96::zq |- ( 0 e. ZZ -> 0 e. QQ )
97:95,96:ax-mp |- 0 e. QQ
98:97:a1i |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ n e. ( 1 ... N ) )
-> 0 e. QQ )
99::addid2 |- ( &S3 e. CC -> ( 0 + &S3 ) = &S3 )
100::addid1 |- ( &S3 e. CC -> ( &S3 + 0 ) = &S3 )
101:99,100:jca |- ( &S3 e. CC
-> ( ( 0 + &S3 ) = &S3 /\ ( &S3 + 0 ) = &S3 ) )
102:101:adantl |- ( ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ n e. ( 1 ... N ) )
/\ &S3 e. CC )
-> ( ( 0 + &S3 ) = &S3 /\ ( &S3 + 0 ) = &S3 ) )
103:86,87,20,89,90,92,94,98,102:gsumress
|- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ n e. ( 1 ... N ) )
-> ( CCfld
gsum
( k e. ( 0 ... N ) |-> ( ( &C37 ` k ) x. C ) ) )
= ( ( CCfld |`s QQ )
gsum
( k e. ( 0 ... N ) |-> ( ( &C37 ` k ) x. C ) ) ) )
104::simplr |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ n e. ( 1 ... N ) )
-> &C37 : ( 0 ... N ) --> QQ )
105::qcn |- ( ( &C37 ` k ) e. QQ -> ( &C37 ` k ) e. CC )
106:55,105:syl |- ( ( &C37 : ( 0 ... N ) --> QQ /\ k e. ( 0 ... N ) )
-> ( &C37 ` k ) e. CC )
107:104,106:sylan |- ( ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ n e. ( 1 ... N ) )
/\ k e. ( 0 ... N ) )
-> ( &C37 ` k ) e. CC )
108::qcn |- ( C e. QQ -> C e. CC )
109:11,108:syl |- ( ( ( ph /\ k e. ( 0 ... N ) )
/\ n e. ( 1 ... N ) )
-> C e. CC )
110:109:an32s |- ( ( ( ph /\ n e. ( 1 ... N ) )
/\ k e. ( 0 ... N ) )
-> C e. CC )
111:110:adantllr |- ( ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ n e. ( 1 ... N ) )
/\ k e. ( 0 ... N ) )
-> C e. CC )
112:107,111:mulcld |- ( ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ n e. ( 1 ... N ) )
/\ k e. ( 0 ... N ) )
-> ( ( &C37 ` k ) x. C ) e. CC )
113:90,112:gsumfsum
|- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ n e. ( 1 ... N ) )
-> ( CCfld
gsum
( k e. ( 0 ... N ) |-> ( ( &C37 ` k ) x. C ) ) )
= sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C ) )
114:103,113:eqtr3d |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ n e. ( 1 ... N ) )
-> ( ( CCfld |`s QQ )
gsum
( k e. ( 0 ... N ) |-> ( ( &C37 ` k ) x. C ) ) )
= sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C ) )
115:114:mpteq2dva |- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( n
e. ( 1 ... N )
|-> ( ( CCfld |`s QQ )
gsum
( k e. ( 0 ... N ) |-> ( ( &C37 ` k ) x. C ) )
) )
= ( n
e. ( 1 ... N )
|-> sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C ) ) )
116:71,85,115:3eqtrd
117::qaddcl |- ( ( &S4 e. QQ /\ &S5 e. QQ ) -> ( &S4 + &S5 ) e. QQ )
118:117:adantl |- ( ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ n e. ( 1 ... N ) )
/\ ( &S4 e. QQ /\ &S5 e. QQ ) )
-> ( &S4 + &S5 ) e. QQ )
119:92,118,90,78,98:fsumcllem
|- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ n e. ( 1 ... N ) )
-> sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
e. QQ )
120::eqid |- ( n
e. ( 1 ... N )
|-> sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C ) )
= ( n
e. ( 1 ... N )
|-> sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C ) )
121:119,120:fmptd |- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( n
e. ( 1 ... N )
|-> sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C ) )
: ( 1 ... N )
--> QQ )
122:14,15:elmap |- ( ( n
e. ( 1 ... N )
|-> sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C ) )
e. ( QQ ^m ( 1 ... N ) )
<-> ( n
e. ( 1 ... N )
|-> sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C ) )
: ( 1 ... N )
--> QQ )
123:121,122:sylibr |- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( n
e. ( 1 ... N )
|-> sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C ) )
e. ( QQ ^m ( 1 ... N ) ) )
124:116,123:eqeltrd
125::elmapi |- ( &C15 e. ( &C16 ^m &C17 ) -> &C15 : &C17 --> &C16 )
126::ffn |- ( &C20 : &C18 --> &C19 -> &C20 Fn &C18 )
127:124,125,126:3syl
128::c0ex |- 0 e. _V
129::fnconstg |- ( 0 e. _V
-> ( &C21 X. { 0 } ) Fn &C21 )
130:128,129:ax-mp |- ( &C21 X. { 0 } ) Fn &C21
131::nfcv |- F/_ &S6 &C22
132::nfcv |- F/_ &S6 &C23
133::nfcv |- F/_ &S6 &C24
134::nfcv |- F/_ &S6 &C25
135::nfcv |- F/_ &S6 &C26
136::nfmpt1 |- F/_ &S6 ( &S6 e. &C27 |-> &C28 )
137:135,136:nfmpt |- F/_ &S6 ( &S13 e. &C26 |-> ( &S6 e. &C27 |-> &C28 ) )
138:133,134,137:nfov
|- F/_ &S6
( &C24
&C25
( &S13 e. &C26 |-> ( &S6 e. &C27 |-> &C28 ) ) )
139:131,132,138:nfov
|- F/_ &S6
( &C22
&C23
( &C24
&C25
( &S13 e. &C26 |-> ( &S6 e. &C27 |-> &C28 ) ) ) )
140::nfcv |- F/_ &S6 &C29
141:139,140:eqfnfv2f
|- ( ( ( &C22
&C23
( &C24
&C25
( &S13
e. &C26
|-> ( &S6 e. &C27 |-> &C28 ) ) ) )
Fn &C30
/\ &C29 Fn &C30 )
-> ( ( &C22
&C23
( &C24
&C25
( &S13
e. &C26
|-> ( &S6 e. &C27 |-> &C28 ) ) ) )
= &C29
<-> A. &S6
e. &C30
( ( &C22
&C23
( &C24
&C25
( &S13
e. &C26
|-> ( &S6 e. &C27 |-> &C28 ) ) ) )
` &S6 )
= ( &C29 ` &S6 ) ) )
142:127,130,141:sylancl
143:116:fveq1d
144::sumex |- sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
e. _V
145:120:fvmpt2 |- ( ( n e. ( 1 ... N )
/\ sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
e. _V )
-> ( ( n
e. ( 1 ... N )
|-> sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C ) )
` n )
= sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C ) )
146:144,145:mpan2 |- ( n e. ( 1 ... N )
-> ( ( n
e. ( 1 ... N )
|-> sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C ) )
` n )
= sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C ) )
147:143,146:sylan9eq
148:128:fvconst2 |- ( &C33 e. &C31
-> ( ( &C31 X. { 0 } ) ` &C33 )
= 0 )
149:148:adantl |- ( ( &W5 /\ &C33 e. &C31 )
-> ( ( &C31 X. { 0 } ) ` &C33 )
= 0 )
150:147,149:eqeq12d
151:150:ralbidva
152:142,151:bitrd
153:152:imbi1d
154:44,153:sylan2
155:154:ralbidva
156:43,155:bitrd
157::drngnzr |- ( ( CCfld |`s QQ ) e. DivRing
-> ( CCfld |`s QQ ) e. NzRing )
158:21,157:ax-mp |- ( CCfld |`s QQ ) e. NzRing
159: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 ) )
) ) ) )
160:27,158,159: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 ) ) ) )
)
161:48,18:dmmpti |- dom ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) )
= ( 0 ... N )
162::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 ) )
163:161,162: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 )
164:163: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 ) ) ) )
)
165:160,164: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 ) ) ) )
)
166::con34b |- ( ( &W6 -> &S10 = &C35 )
<-> ( -. &S10 = &C35 -> -. &W6 ) )
167::df-nel |- ( &S10 e/ { &C35 }
<-> -. &S10 e. { &C35 } )
168::elsn |- ( &S10 e. { &C35 } <-> &S10 = &C35 )
169:167,168:xchbinx
|- ( &S10 e/ { &C35 } <-> -. &S10 = &C35 )
170:169:imbi1i |- ( ( &S10 e/ { &C35 } -> -. &W6 )
<-> ( -. &S10 = &C35 -> -. &W6 ) )
171:166,170:bitr4i |- ( ( &W6 -> &S10 = &C35 )
<-> ( &S10 e/ { &C35 } -> -. &W6 ) )
172:171:ralbii |- ( A. &S10 e. &C34 ( &W6 -> &S10 = &C35 )
<-> A. &S10
e. &C34
( &S10 e/ { &C35 } -> -. &W6 ) )
173::raldifb |- ( A. &S10
e. &C34
( &S10 e/ { &C35 } -> -. &W6 )
<-> A. &S10 e. ( &C34 \ { &C35 } ) -. &W6 )
174::ralnex |- ( A. &S10 e. ( &C34 \ { &C35 } ) -. &W6
<-> -. E. &S10 e. ( &C34 \ { &C35 } ) &W6 )
175:172,173,174:3bitri
|- ( A. &S10 e. &C34 ( &W6 -> &S10 = &C35 )
<-> -. E. &S10 e. ( &C34 \ { &C35 } ) &W6 )
176:156,165,175:3bitr3g
177::eqid |- ( LSubSp ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
= ( LSubSp ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
178:31,177:lssmre |- ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) e. LMod
-> ( LSubSp
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
e. ( Moore ` ( QQ ^m ( 1 ... N ) ) ) )
179:27,178:ax-mp |- ( LSubSp ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
e. ( Moore ` ( QQ ^m ( 1 ... N ) ) )
180:179: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 ) ) ) )
181::eqid |- ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
= ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
182::eqid |- ( mrCls
` ( LSubSp
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) )
= ( mrCls
` ( LSubSp
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) )
183:177,181,182:mrclsp
|- ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) e. LMod
-> ( LSpan
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
= ( mrCls
` ( LSubSp
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) )
184:27,183:ax-mp |- ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
= ( mrCls
` ( LSubSp
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) )
185::eqid |- ( mrInd
` ( LSubSp
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) )
= ( mrInd
` ( LSubSp
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) )
186:33:islvec |- ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) e. LVec
<-> ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) e. LMod
/\ ( CCfld |`s QQ ) e. DivRing ) )
187:27,21,186:mpbir2an
|- ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) e. LVec
188:177,184,31:lssacsex
|- ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) e. LVec
-> ( ( LSubSp
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
e. ( ACS ` ( QQ ^m ( 1 ... N ) ) )
/\ A. &S9
e. ~P ( QQ ^m ( 1 ... N ) )
A. &S7
e. ( QQ ^m ( 1 ... N ) )
A. &S8
e. ( ( ( LSpan
` ( ( CCfld |`s QQ )
freeLMod
( 1 ... N ) ) )
` ( &S9 u. { &S7 } ) )
\ ( ( LSpan
` ( ( CCfld |`s QQ )
freeLMod
( 1 ... N ) ) )
` &S9 ) )
&S7
e. ( ( LSpan
` ( ( CCfld |`s QQ )
freeLMod
( 1 ... N ) ) )
` ( &S9 u. { &S8 } ) ) ) )
189:188:simprd |- ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) e. LVec
-> A. &S9
e. ~P ( QQ ^m ( 1 ... N ) )
A. &S7
e. ( QQ ^m ( 1 ... N ) )
A. &S8
e. ( ( ( LSpan
` ( ( CCfld |`s QQ )
freeLMod
( 1 ... N ) ) )
` ( &S9 u. { &S7 } ) )
\ ( ( LSpan
` ( ( CCfld |`s QQ )
freeLMod
( 1 ... N ) ) )
` &S9 ) )
&S7
e. ( ( LSpan
` ( ( CCfld |`s QQ )
freeLMod
( 1 ... N ) ) )
` ( &S9 u. { &S8 } ) ) )
190:187,189:ax-mp |- A. &S9
e. ~P ( QQ ^m ( 1 ... N ) )
A. &S7
e. ( QQ ^m ( 1 ... N ) )
A. &S8
e. ( ( ( LSpan
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) )
)
` ( &S9 u. { &S7 } ) )
\ ( ( LSpan
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) )
)
` &S9 ) )
&S7
e. ( ( LSpan
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) )
)
` ( &S9 u. { &S8 } ) )
191:190:a1i |- ( ( ph
/\ ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
e. ( LIndS
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) )
-> A. &S9
e. ~P ( QQ ^m ( 1 ... N ) )
A. &S7
e. ( QQ ^m ( 1 ... N ) )
A. &S8
e. ( ( ( LSpan
` ( ( CCfld |`s QQ )
freeLMod
( 1 ... N ) ) )
` ( &S9 u. { &S7 } ) )
\ ( ( LSpan
` ( ( CCfld |`s QQ )
freeLMod
( 1 ... N ) ) )
` &S9 ) )
&S7
e. ( ( LSpan
` ( ( CCfld |`s QQ )
freeLMod
( 1 ... N ) ) )
` ( &S9 u. { &S8 } ) ) )
192::frn |- ( ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
: ( 0 ... N )
--> ( QQ ^m ( 1 ... N ) )
-> ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
C_ ( QQ ^m ( 1 ... N ) ) )
193:19,192:syl |- ( ph
-> ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
C_ ( QQ ^m ( 1 ... N ) ) )
194::dif0 |- ( ( QQ ^m ( 1 ... N ) ) \ (/) )
= ( QQ ^m ( 1 ... N ) )
195:193,194:syl6sseqr
|- ( ph
-> ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
C_ ( ( QQ ^m ( 1 ... N ) ) \ (/) ) )
196:195: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 ) ) \ (/) ) )
197::eqid |- ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
= ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
198:197,25,31:uvcff
|- ( ( ( CCfld |`s QQ ) e. Ring /\ ( 1 ... N ) e. Fin )
-> ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
: ( 1 ... N )
--> ( QQ ^m ( 1 ... N ) ) )
199:23,24,198:mp2an
|- ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
: ( 1 ... N )
--> ( QQ ^m ( 1 ... N ) )
200::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 ) ) )
201:199,200:ax-mp |- ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
C_ ( QQ ^m ( 1 ... N ) )
202:201,194:sseqtr4i
|- ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
C_ ( ( QQ ^m ( 1 ... N ) ) \ (/) )
203:202: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 ) ) \ (/) ) )
204::un0 |- ( ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
u. (/) )
= ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
205:204: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 ) ) )
206::eqid |- ( LBasis ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
= ( LBasis ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
207:25,197,206: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 ) ) ) )
208:23,24,207:mp2an
|- ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
e. ( LBasis ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
209:31,206,181: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 ) ) )
210:208,209:ax-mp |- ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
` ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) )
= ( QQ ^m ( 1 ... N ) )
211:205,210:eqtri |- ( ( LSpan ` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
` ( ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
u. (/) ) )
= ( QQ ^m ( 1 ... N ) )
212:193,211:syl6sseqr
|- ( 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. (/) ) ) )
213:212: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. (/) ) ) )
214::un0 |- ( ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
u. (/) )
= ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) )
215:27,158:pm3.2i |- ( ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) e. LMod
/\ ( CCfld |`s QQ ) e. NzRing )
216:181,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 ) ) )
/\ &S12
e. ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) ) )
-> -. &S12
e. ( ( LSpan
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
` ( ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
\ { &S12 } ) ) )
217:215,216:mp3an1 |- ( ( ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
e. ( LIndS
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
/\ &S12
e. ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) ) )
-> -. &S12
e. ( ( LSpan
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
` ( ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
\ { &S12 } ) ) )
218:217:ralrimiva |- ( ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
e. ( LIndS
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
-> A. &S12
e. ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
-. &S12
e. ( ( LSpan
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) )
)
` ( ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
\ { &S12 } ) ) )
219:184,185: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. &S12
e. ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
-. &S12
e. ( ( LSpan
` ( ( CCfld |`s QQ )
freeLMod
( 1 ... N ) ) )
` ( ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
\ { &S12 } ) ) ) )
220:179,193,219:sylancr
|- ( ph
-> ( ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
e. ( mrInd
` ( LSubSp
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
)
<-> A. &S12
e. ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
-. &S12
e. ( ( LSpan
` ( ( CCfld |`s QQ )
freeLMod
( 1 ... N ) ) )
` ( ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
\ { &S12 } ) ) ) )
221:220:biimpar |- ( ( ph
/\ A. &S12
e. ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
-. &S12
e. ( ( LSpan
` ( ( CCfld |`s QQ )
freeLMod
( 1 ... N ) ) )
` ( ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
\ { &S12 } ) ) )
-> ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
e. ( mrInd
` ( LSubSp
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) ) )
222:218,221: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 ) ) ) ) )
223:214,222:syl5eqel
|- ( ( 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 ) ) ) ) )
224::mptfi |- ( ( 0 ... N ) e. Fin
-> ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) )
e. Fin )
225::rnfi |- ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) )
e. Fin
-> ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
e. Fin )
226:28,224,225:mp2b
|- ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
e. Fin
227:226:orci |- ( ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
e. Fin
\/ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
e. Fin )
228:227: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 ) )
229:180,184,185,191,196,203,213,223,228:mreexexd
|- ( ( ph
/\ ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
e. ( LIndS
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) ) )
-> E. &S11
e. ~P ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
( ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
~~
&S11
/\ ( &S11 u. (/) )
e. ( mrInd
` ( LSubSp
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) )
) ) ) )
230:229:ex |- ( ph
-> ( ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
e. ( LIndS
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
-> E. &S11
e. ~P ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
( ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
~~
&S11
/\ ( &S11 u. (/) )
e. ( mrInd
` ( LSubSp
` ( ( CCfld |`s QQ )
freeLMod
( 1 ... N ) ) ) ) ) ) )
231::ovex |- ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) e. _V
232:231:rnex |- ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
e. _V
233::elpwi |- ( &S11
e. ~P ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
-> &S11
C_ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) )
234::ssdomg |- ( ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
e. _V
-> ( &S11
C_ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
-> &S11
~<_
ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) ) )
235:232,233,234:mpsyl
|- ( &S11
e. ~P ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
-> &S11
~<_
ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) )
236::endomtr |- ( ( ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
~~
&S11
/\ &S11
~<_
ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) )
-> ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
~<_
ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) )
237:236:ancoms |- ( ( &S11
~<_
ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
/\ ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
~~
&S11 )
-> ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
~<_
ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) )
238::f1f1orn |- ( ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
: ( 0 ... N )
-1-1-> &C49
-> ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
: ( 0 ... N )
-1-1-onto-> ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) ) )
239::ovex |- ( 0 ... N ) e. _V
240:239: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 ) ) )
241:238,240:syl |- ( ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
: ( 0 ... N )
-1-1-> &C49
-> ( 0 ... N )
~~
ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) ) )
242::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 ) ) )
243:197:uvcendim |- ( ( ( CCfld |`s QQ ) e. NzRing /\ ( 1 ... N ) e. Fin )
-> ( 1 ... N )
~~
ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) )
244:158,24,243:mp2an
|- ( 1 ... N )
~~
ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
245:244:ensymi |- ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
~~
( 1 ... N )
246::domentr |- ( ( ( 0 ... N )
~<_
ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
/\ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
~~
( 1 ... N ) )
-> ( 0 ... N ) ~<_ ( 1 ... N ) )
247::hashdom |- ( ( ( 0 ... N ) e. Fin /\ ( 1 ... N ) e. Fin )
-> ( ( # ` ( 0 ... N ) ) <_ ( # ` ( 1 ... N ) )
<-> ( 0 ... N ) ~<_ ( 1 ... N ) ) )
248:28,24,247:mp2an
|- ( ( # ` ( 0 ... N ) ) <_ ( # ` ( 1 ... N ) )
<-> ( 0 ... N ) ~<_ ( 1 ... N ) )
249::hashfz0 |- ( N e. NN0
-> ( # ` ( 0 ... N ) ) = ( N + 1 ) )
250:h2,249:syl |- ( ph
-> ( # ` ( 0 ... N ) ) = ( N + 1 ) )
251::hashfz1 |- ( N e. NN0
-> ( # ` ( 1 ... N ) ) = N )
252:h2,251:syl |- ( ph
-> ( # ` ( 1 ... N ) ) = N )
253:250,252:breq12d
|- ( ph
-> ( ( # ` ( 0 ... N ) ) <_ ( # ` ( 1 ... N ) )
<-> ( N + 1 ) <_ N ) )
254:248,253:syl5bbr
|- ( ph
-> ( ( 0 ... N ) ~<_ ( 1 ... N ) <-> ( N + 1 ) <_ N ) )
255:246,254:syl5ib |- ( ph
-> ( ( ( 0 ... N )
~<_
ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
/\ ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
~~
( 1 ... N ) )
-> ( N + 1 ) <_ N ) )
256:245,255:mpan2i |- ( ph
-> ( ( 0 ... N )
~<_
ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
-> ( N + 1 ) <_ N ) )
257:242,256: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 ) )
258:257: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 ) ) )
259:241,258:syl5 |- ( ph
-> ( ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
: ( 0 ... N )
-1-1-> &C49
-> ( ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
~<_
ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
-> ( N + 1 ) <_ N ) ) )
260:259: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-> &C49
-> ( N + 1 ) <_ N ) ) )
261:237,260:syl5 |- ( ph
-> ( ( &S11
~<_
ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
/\ ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
~~
&S11 )
-> ( ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
: ( 0 ... N )
-1-1-> &C49
-> ( N + 1 ) <_ N ) ) )
262:261:expdimp |- ( ( ph
/\ &S11
~<_
ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) ) )
-> ( ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
~~
&S11
-> ( ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
: ( 0 ... N )
-1-1-> &C49
-> ( N + 1 ) <_ N ) ) )
263:235,262:sylan2 |- ( ( ph
/\ &S11
e. ~P ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
)
-> ( ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
~~
&S11
-> ( ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
: ( 0 ... N )
-1-1-> &C49
-> ( N + 1 ) <_ N ) ) )
264:263:adantrd |- ( ( ph
/\ &S11
e. ~P ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
)
-> ( ( ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
~~
&S11
/\ ( &S11 u. (/) )
e. ( mrInd
` ( LSubSp
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) )
) ) )
-> ( ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
: ( 0 ... N )
-1-1-> &C49
-> ( N + 1 ) <_ N ) ) )
265:264:rexlimdva |- ( ph
-> ( E. &S11
e. ~P ran ( ( CCfld |`s QQ ) unitVec ( 1 ... N ) )
( ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
~~
&S11
/\ ( &S11 u. (/) )
e. ( mrInd
` ( LSubSp
` ( ( CCfld |`s QQ )
freeLMod
( 1 ... N ) ) ) ) )
-> ( ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
: ( 0 ... N )
-1-1-> &C49
-> ( N + 1 ) <_ N ) ) )
266:230,265: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-> &C49
-> ( N + 1 ) <_ N ) ) )
267:266: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-> &C49 )
-> ( N + 1 ) <_ N ) )
268:267:ancomsd |- ( ph
-> ( ( ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
: ( 0 ... N )
-1-1-> &C49
/\ ran ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> C ) )
e. ( LIndS
` ( ( CCfld |`s QQ ) freeLMod ( 1 ... N ) ) )
)
-> ( N + 1 ) <_ N ) )
269:176,268:sylbird
270:9,269:mt3d
271::eldifsn |- ( &C37
e. ( ( QQ ^m ( 0 ... N ) )
\ { ( ( 0 ... N ) X. { 0 } ) } )
<-> ( &C37 e. ( QQ ^m ( 0 ... N ) )
/\ &C37 =/= ( ( 0 ... N ) X. { 0 } ) ) )
272:44:anim1i |- ( ( &C37 e. ( QQ ^m ( 0 ... N ) )
/\ &C37 =/= ( ( 0 ... N ) X. { 0 } ) )
-> ( &C37 : ( 0 ... N ) --> QQ
/\ &C37 =/= ( ( 0 ... N ) X. { 0 } ) ) )
273:271,272:sylbi |- ( &C37
e. ( ( QQ ^m ( 0 ... N ) )
\ { ( ( 0 ... N ) X. { 0 } ) } )
-> ( &C37 : ( 0 ... N ) --> QQ
/\ &C37 =/= ( ( 0 ... N ) X. { 0 } ) ) )
274:91:a1i |- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> QQ C_ CC )
275:h2:adantr |- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> N e. NN0 )
276:274,275,56:elplyd
|- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
e. ( Poly ` QQ ) )
277:276:adantrr |- ( ( ph
/\ ( &C37 : ( 0 ... N ) --> QQ
/\ &C37 =/= ( ( 0 ... N ) X. { 0 } ) ) )
-> ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
e. ( Poly ` QQ ) )
278::uzdisj |- ( ( 0 ... ( ( N + 1 ) - 1 ) )
i^i ( ZZ>= ` ( N + 1 ) ) )
= (/)
279:h2:nn0cnd |- ( ph -> N e. CC )
280::pncan1 |- ( N e. CC
-> ( ( N + 1 ) - 1 ) = N )
281:279,280:syl |- ( ph
-> ( ( N + 1 ) - 1 ) = N )
282:281:oveq2d |- ( ph
-> ( 0 ... ( ( N + 1 ) - 1 ) )
= ( 0 ... N ) )
283:282:ineq1d |- ( ph
-> ( ( 0 ... ( ( N + 1 ) - 1 ) )
i^i ( ZZ>= ` ( N + 1 ) ) )
= ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) )
284:278,283:syl5eqr
|- ( ph
-> (/)
= ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) )
285:284:eqcomd |- ( ph
-> ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) )
= (/) )
286:128:fconst |- ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } )
: ( ZZ>= ` ( N + 1 ) )
--> { 0 }
287::snssi |- ( 0 e. QQ -> { 0 } C_ QQ )
288:95,96,287:mp2b |- { 0 } C_ QQ
289:288,91:sstri |- { 0 } C_ CC
290::fss |- ( ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } )
: ( ZZ>= ` ( N + 1 ) )
--> { 0 }
/\ { 0 } C_ CC )
-> ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } )
: ( ZZ>= ` ( N + 1 ) )
--> CC )
291:286,289,290:mp2an
|- ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } )
: ( ZZ>= ` ( N + 1 ) )
--> CC
292::fun |- ( ( ( &C37 : ( 0 ... N ) --> QQ
/\ ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } )
: ( ZZ>= ` ( N + 1 ) )
--> CC )
/\ ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) )
= (/) )
-> ( &C37
u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) )
: ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) )
--> ( QQ u. CC ) )
293:291,292:mpanl2 |- ( ( &C37 : ( 0 ... N ) --> QQ
/\ ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) )
= (/) )
-> ( &C37
u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) )
: ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) )
--> ( QQ u. CC ) )
294:285,293:sylan2 |- ( ( &C37 : ( 0 ... N ) --> QQ /\ ph )
-> ( &C37
u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) )
: ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) )
--> ( QQ u. CC ) )
295:294:ancoms |- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( &C37
u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) )
: ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) )
--> ( QQ u. CC ) )
296::nn0uz |- NN0 = ( ZZ>= ` 0 )
297:6,296:syl6eleq |- ( ph -> ( N + 1 ) e. ( ZZ>= ` 0 ) )
298::uzsplit |- ( ( N + 1 ) e. ( ZZ>= ` 0 )
-> ( ZZ>= ` 0 )
= ( ( 0 ... ( ( N + 1 ) - 1 ) )
u. ( ZZ>= ` ( N + 1 ) ) ) )
299:297,298:syl |- ( ph
-> ( ZZ>= ` 0 )
= ( ( 0 ... ( ( N + 1 ) - 1 ) )
u. ( ZZ>= ` ( N + 1 ) ) ) )
300:296,299:syl5eq |- ( ph
-> NN0
= ( ( 0 ... ( ( N + 1 ) - 1 ) )
u. ( ZZ>= ` ( N + 1 ) ) ) )
301:282:uneq1d |- ( ph
-> ( ( 0 ... ( ( N + 1 ) - 1 ) )
u. ( ZZ>= ` ( N + 1 ) ) )
= ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
302:300,301:eqtr2d |- ( ph
-> ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) )
= NN0 )
303::ssequn1 |- ( QQ C_ CC <-> ( QQ u. CC ) = CC )
304:91,303:mpbi |- ( QQ u. CC ) = CC
305:304:a1i |- ( ph -> ( QQ u. CC ) = CC )
306:302,305:feq23d |- ( ph
-> ( ( &C37
u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) )
: ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) )
--> ( QQ u. CC )
<-> ( &C37
u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) )
: NN0
--> CC ) )
307:306:adantr |- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( ( &C37
u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) )
: ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) )
--> ( QQ u. CC )
<-> ( &C37
u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) )
: NN0
--> CC ) )
308:295,307:mpbid |- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( &C37
u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) )
: NN0
--> CC )
309::ffn |- ( &C37 : ( 0 ... N ) --> QQ -> &C37 Fn ( 0 ... N ) )
310::fnimadisj |- ( ( &C37 Fn ( 0 ... N )
/\ ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) )
= (/) )
-> ( &C37 " ( ZZ>= ` ( N + 1 ) ) )
= (/) )
311:309,285,310:syl2anr
|- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( &C37 " ( ZZ>= ` ( N + 1 ) ) )
= (/) )
312:h2:nn0zd |- ( ph -> N e. ZZ )
313:312:peano2zd |- ( ph -> ( N + 1 ) e. ZZ )
314::uzid |- ( ( N + 1 ) e. ZZ
-> ( N + 1 ) e. ( ZZ>= ` ( N + 1 ) ) )
315::ne0i |- ( ( N + 1 ) e. ( ZZ>= ` ( N + 1 ) )
-> ( ZZ>= ` ( N + 1 ) ) =/= (/) )
316:313,314,315:3syl
|- ( ph
-> ( ZZ>= ` ( N + 1 ) ) =/= (/) )
317::inidm |- ( ( ZZ>= ` ( N + 1 ) ) i^i ( ZZ>= ` ( N + 1 ) ) )
= ( ZZ>= ` ( N + 1 ) )
318:317:neeq1i |- ( ( ( ZZ>= ` ( N + 1 ) ) i^i ( ZZ>= ` ( N + 1 ) ) )
=/= (/)
<-> ( ZZ>= ` ( N + 1 ) ) =/= (/) )
319:316,318:sylibr |- ( ph
-> ( ( ZZ>= ` ( N + 1 ) ) i^i ( ZZ>= ` ( N + 1 ) ) )
=/= (/) )
320::xpima2 |- ( ( ( ZZ>= ` ( N + 1 ) ) i^i ( ZZ>= ` ( N + 1 ) ) )
=/= (/)
-> ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } )
" ( ZZ>= ` ( N + 1 ) ) )
= { 0 } )
321:319,320:syl |- ( ph
-> ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } )
" ( ZZ>= ` ( N + 1 ) ) )
= { 0 } )
322:321:adantr |- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } )
" ( ZZ>= ` ( N + 1 ) ) )
= { 0 } )
323:311,322:uneq12d
|- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( ( &C37 " ( ZZ>= ` ( N + 1 ) ) )
u. ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } )
" ( ZZ>= ` ( N + 1 ) ) ) )
= ( (/) u. { 0 } ) )
324::imaundir |- ( ( &C37
u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) )
" ( ZZ>= ` ( N + 1 ) ) )
= ( ( &C37 " ( ZZ>= ` ( N + 1 ) ) )
u. ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } )
" ( ZZ>= ` ( N + 1 ) ) ) )
325::uncom |- ( (/) u. { 0 } ) = ( { 0 } u. (/) )
326::un0 |- ( { 0 } u. (/) ) = { 0 }
327:325,326:eqtr2i |- { 0 } = ( (/) u. { 0 } )
328:323,324,327:3eqtr4g
|- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( ( &C37
u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) )
" ( ZZ>= ` ( N + 1 ) ) )
= { 0 } )
329:285,309:anim12ci
|- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( &C37 Fn ( 0 ... N )
/\ ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) )
= (/) ) )
330::fnconstg |- ( 0 e. _V
-> ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } )
Fn ( ZZ>= ` ( N + 1 ) ) )
331:128,330:ax-mp |- ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } )
Fn ( ZZ>= ` ( N + 1 ) )
332::fvun1 |- ( ( &C37 Fn ( 0 ... N )
/\ ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } )
Fn ( ZZ>= ` ( N + 1 ) )
/\ ( ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) )
= (/)
/\ k e. ( 0 ... N ) ) )
-> ( ( &C37
u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) )
` k )
= ( &C37 ` k ) )
333:331,332:mp3an2 |- ( ( &C37 Fn ( 0 ... N )
/\ ( ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) )
= (/)
/\ k e. ( 0 ... N ) ) )
-> ( ( &C37
u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) )
` k )
= ( &C37 ` k ) )
334:333:anassrs |- ( ( ( &C37 Fn ( 0 ... N )
/\ ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) )
= (/) )
/\ k e. ( 0 ... N ) )
-> ( ( &C37
u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) )
` k )
= ( &C37 ` k ) )
335:329,334:sylan |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
-> ( ( &C37
u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) )
` k )
= ( &C37 ` k ) )
336:335:eqcomd |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
-> ( &C37 ` k )
= ( ( &C37
u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) )
` k ) )
337:336:oveq1d |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
-> ( ( &C37 ` k ) x. ( &S21 ^ k ) )
= ( ( ( &C37
u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) )
` k )
x.
( &S21 ^ k ) ) )
338:337:sumeq2dv |- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) )
= sum_ k
e. ( 0 ... N )
( ( ( &C37
u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) )
` k )
x.
( &S21 ^ k ) ) )
339:338:mpteq2dv |- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
= ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( ( &C37
u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) )
` k )
x.
( &S21 ^ k ) ) ) )
340:276,275,308,328,339:coeeq
|- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( coeff
` ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) ) )
= ( &C37
u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) )
341:340:reseq1d |- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( ( coeff
` ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) ) )
|` ( 0 ... N ) )
= ( ( &C37
u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) )
|` ( 0 ... N ) ) )
342::res0 |- ( &C37 |` (/) ) = (/)
343:284:reseq2d |- ( ph
-> ( &C37 |` (/) )
= ( &C37
|` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) ) )
344::res0 |- ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } )
|` (/) )
= (/)
345:284:reseq2d |- ( ph
-> ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } )
|` (/) )
= ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } )
|` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) ) )
346:344,345:syl5eqr
|- ( ph
-> (/)
= ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } )
|` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) ) )
347:342,343,346:3eqtr3a
|- ( ph
-> ( &C37
|` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) )
= ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } )
|` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) ) )
348::fss |- ( ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } )
: ( ZZ>= ` ( N + 1 ) )
--> { 0 }
/\ { 0 } C_ QQ )
-> ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } )
: ( ZZ>= ` ( N + 1 ) )
--> QQ )
349:286,288,348:mp2an
|- ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } )
: ( ZZ>= ` ( N + 1 ) )
--> QQ
350::fresaunres1 |- ( ( &C37 : ( 0 ... N ) --> QQ
/\ ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } )
: ( ZZ>= ` ( N + 1 ) )
--> QQ
/\ ( &C37
|` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) )
= ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } )
|` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) ) )
-> ( ( &C37
u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) )
|` ( 0 ... N ) )
= &C37 )
351:349,350:mp3an2 |- ( ( &C37 : ( 0 ... N ) --> QQ
/\ ( &C37
|` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) )
= ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } )
|` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) ) )
-> ( ( &C37
u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) )
|` ( 0 ... N ) )
= &C37 )
352:347,351:sylan2 |- ( ( &C37 : ( 0 ... N ) --> QQ /\ ph )
-> ( ( &C37
u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) )
|` ( 0 ... N ) )
= &C37 )
353:352:ancoms |- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( ( &C37
u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) )
|` ( 0 ... N ) )
= &C37 )
354:341,353:eqtrd |- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( ( coeff
` ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) ) )
|` ( 0 ... N ) )
= &C37 )
355::fveq2 |- ( ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
= 0p
-> ( coeff
` ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) ) )
= ( coeff ` 0p ) )
356:355:reseq1d |- ( ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
= 0p
-> ( ( coeff
` ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) ) )
|` ( 0 ... N ) )
= ( ( coeff ` 0p ) |` ( 0 ... N ) ) )
357::eqtr2 |- ( ( ( ( coeff
` ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
)
|` ( 0 ... N ) )
= &C37
/\ ( ( coeff
` ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
)
|` ( 0 ... N ) )
= ( ( coeff ` 0p ) |` ( 0 ... N ) ) )
-> &C37 = ( ( coeff ` 0p ) |` ( 0 ... N ) ) )
358::coe0 |- ( coeff ` 0p ) = ( NN0 X. { 0 } )
359:358:reseq1i |- ( ( coeff ` 0p ) |` ( 0 ... N ) )
= ( ( NN0 X. { 0 } ) |` ( 0 ... N ) )
360::elfznn0 |- ( &S17 e. ( 0 ... N ) -> &S17 e. NN0 )
361:360:ssriv |- ( 0 ... N ) C_ NN0
362::xpssres |- ( ( 0 ... N ) C_ NN0
-> ( ( NN0 X. { 0 } ) |` ( 0 ... N ) )
= ( ( 0 ... N ) X. { 0 } ) )
363:361,362:ax-mp |- ( ( NN0 X. { 0 } ) |` ( 0 ... N ) )
= ( ( 0 ... N ) X. { 0 } )
364:359,363:eqtri |- ( ( coeff ` 0p ) |` ( 0 ... N ) )
= ( ( 0 ... N ) X. { 0 } )
365:357,364:syl6eq |- ( ( ( ( coeff
` ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
)
|` ( 0 ... N ) )
= &C37
/\ ( ( coeff
` ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
)
|` ( 0 ... N ) )
= ( ( coeff ` 0p ) |` ( 0 ... N ) ) )
-> &C37 = ( ( 0 ... N ) X. { 0 } ) )
366:365:ex |- ( ( ( coeff
` ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) ) )
|` ( 0 ... N ) )
= &C37
-> ( ( ( coeff
` ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
)
|` ( 0 ... N ) )
= ( ( coeff ` 0p ) |` ( 0 ... N ) )
-> &C37 = ( ( 0 ... N ) X. { 0 } ) ) )
367:354,356,366:syl2im
|- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
= 0p
-> &C37 = ( ( 0 ... N ) X. { 0 } ) ) )
368:367:necon3d |- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> ( &C37 =/= ( ( 0 ... N ) X. { 0 } )
-> ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
=/= 0p ) )
369:368:impr |- ( ( ph
/\ ( &C37 : ( 0 ... N ) --> QQ
/\ &C37 =/= ( ( 0 ... N ) X. { 0 } ) ) )
-> ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
=/= 0p )
370::eldifsn |- ( ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
e. ( ( Poly ` QQ ) \ { 0p } )
<-> ( ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
e. ( Poly ` QQ )
/\ ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
=/= 0p ) )
371:277,369,370:sylanbrc
|- ( ( ph
/\ ( &C37 : ( 0 ... N ) --> QQ
/\ &C37 =/= ( ( 0 ... N ) X. { 0 } ) ) )
-> ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
e. ( ( Poly ` QQ ) \ { 0p } ) )
372:371:adantrr |- ( ( ph
/\ ( ( &C37 : ( 0 ... N ) --> QQ
/\ &C37 =/= ( ( 0 ... N ) X. { 0 } ) )
/\ A. n
e. ( 1 ... N )
sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
= 0 ) )
-> ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
e. ( ( Poly ` QQ ) \ { 0p } ) )
373::oveq1 |- ( &S21 = A -> ( &S21 ^ k ) = ( A ^ k ) )
374:373:oveq2d |- ( &S21 = A
-> ( ( &C37 ` k ) x. ( &S21 ^ k ) )
= ( ( &C37 ` k ) x. ( A ^ k ) ) )
375:374:sumeq2sdv |- ( &S21 = A
-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) )
= sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. ( A ^ k ) )
)
376::eqid |- ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
= ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
377::sumex |- sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. ( A ^ k ) )
e. _V
378:375,376,377:fvmpt
|- ( A e. CC
-> ( ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
` A )
= sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. ( A ^ k ) )
)
379:h1,378:syl |- ( ph
-> ( ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
` A )
= sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. ( A ^ k ) )
)
380:379:adantr |- ( ( ph
/\ ( &C37 : ( 0 ... N ) --> QQ
/\ A. n
e. ( 1 ... N )
sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
= 0 ) )
-> ( ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
` A )
= sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. ( A ^ k ) )
)
381:106:adantll |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
-> ( &C37 ` k ) e. CC )
383:h3:adantlr |- ( ( ( ph /\ k e. ( 0 ... N ) )
/\ n e. ( 1 ... N ) )
-> X e. CC )
384:109,383:mulcld |- ( ( ( ph /\ k e. ( 0 ... N ) )
/\ n e. ( 1 ... N ) )
-> ( C x. X ) e. CC )
385:384:adantllr |- ( ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
/\ n e. ( 1 ... N ) )
-> ( C x. X ) e. CC )
386:54,381,385:fsummulc2
|- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
-> ( ( &C37 ` k ) x. sum_ n e. ( 1 ... N ) ( C x. X ) )
= sum_ n e. ( 1 ... N ) ( ( &C37 ` k ) x. ( C x. X ) )
)
388:h5:oveq2d |- ( ( ph /\ k e. ( 0 ... N ) )
-> ( ( &C37 ` k ) x. ( A ^ k ) )
= ( ( &C37 ` k ) x. sum_ n e. ( 1 ... N ) ( C x. X ) )
)
389:388:adantlr |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
-> ( ( &C37 ` k ) x. ( A ^ k ) )
= ( ( &C37 ` k ) x. sum_ n e. ( 1 ... N ) ( C x. X ) )
)
390:381:adantr |- ( ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
/\ n e. ( 1 ... N ) )
-> ( &C37 ` k ) e. CC )
391:109:adantllr |- ( ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
/\ n e. ( 1 ... N ) )
-> C e. CC )
392::simpll |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
-> ph )
393:392,h3:sylan |- ( ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
/\ n e. ( 1 ... N ) )
-> X e. CC )
394:390,391,393:mulassd
|- ( ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
/\ n e. ( 1 ... N ) )
-> ( ( ( &C37 ` k ) x. C ) x. X )
= ( ( &C37 ` k ) x. ( C x. X ) ) )
395:394:sumeq2dv |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
-> sum_ n
e. ( 1 ... N )
( ( ( &C37 ` k ) x. C ) x. X )
= sum_ n e. ( 1 ... N ) ( ( &C37 ` k ) x. ( C x. X ) )
)
396:386,389,395:3eqtr4d
|- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ k e. ( 0 ... N ) )
-> ( ( &C37 ` k ) x. ( A ^ k ) )
= sum_ n
e. ( 1 ... N )
( ( ( &C37 ` k ) x. C ) x. X ) )
397:396:sumeq2dv |- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. ( A ^ k ) )
= sum_ k
e. ( 0 ... N )
sum_ n
e. ( 1 ... N )
( ( ( &C37 ` k ) x. C ) x. X ) )
398:106:ad2ant2lr |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ ( k e. ( 0 ... N ) /\ n e. ( 1 ... N ) ) )
-> ( &C37 ` k ) e. CC )
399:109:anasss |- ( ( ph
/\ ( k e. ( 0 ... N ) /\ n e. ( 1 ... N ) ) )
-> C e. CC )
400:399:adantlr |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ ( k e. ( 0 ... N ) /\ n e. ( 1 ... N ) ) )
-> C e. CC )
401:398,400:mulcld |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ ( k e. ( 0 ... N ) /\ n e. ( 1 ... N ) ) )
-> ( ( &C37 ` k ) x. C ) e. CC )
402:h3:ad2ant2rl |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ ( k e. ( 0 ... N ) /\ n e. ( 1 ... N ) ) )
-> X e. CC )
403:401,402:mulcld |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ ( k e. ( 0 ... N ) /\ n e. ( 1 ... N ) ) )
-> ( ( ( &C37 ` k ) x. C ) x. X )
e. CC )
404:45,72,403:fsumcom
|- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> sum_ k
e. ( 0 ... N )
sum_ n
e. ( 1 ... N )
( ( ( &C37 ` k ) x. C ) x. X )
= sum_ n
e. ( 1 ... N )
sum_ k
e. ( 0 ... N )
( ( ( &C37 ` k ) x. C ) x. X ) )
405:397,404:eqtrd |- ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
-> sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. ( A ^ k ) )
= sum_ n
e. ( 1 ... N )
sum_ k
e. ( 0 ... N )
( ( ( &C37 ` k ) x. C ) x. X ) )
406:405:adantrr |- ( ( ph
/\ ( &C37 : ( 0 ... N ) --> QQ
/\ A. n
e. ( 1 ... N )
sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
= 0 ) )
-> sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. ( A ^ k ) )
= sum_ n
e. ( 1 ... N )
sum_ k
e. ( 0 ... N )
( ( ( &C37 ` k ) x. C ) x. X ) )
407::nfv |- F/ n ph
408::nfv |- F/ n &C37 : ( 0 ... N ) --> QQ
409::nfra1 |- F/ n
A. n
e. ( 1 ... N )
sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
= 0
410:408,409:nfan |- F/ n
( &C37 : ( 0 ... N ) --> QQ
/\ A. n
e. ( 1 ... N )
sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
= 0 )
411:407,410:nfan |- F/ n
( ph
/\ ( &C37 : ( 0 ... N ) --> QQ
/\ A. n
e. ( 1 ... N )
sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
= 0 ) )
412::rsp |- ( A. n
e. ( 1 ... N )
sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
= 0
-> ( n e. ( 1 ... N )
-> sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
= 0 ) )
413:412:imp |- ( ( A. n
e. ( 1 ... N )
sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
= 0
/\ n e. ( 1 ... N ) )
-> sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
= 0 )
414:413:oveq1d |- ( ( A. n
e. ( 1 ... N )
sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
= 0
/\ n e. ( 1 ... N ) )
-> ( sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
x.
X )
= ( 0 x. X ) )
415:414:adantll |- ( ( ( &C37 : ( 0 ... N ) --> QQ
/\ A. n
e. ( 1 ... N )
sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
= 0 )
/\ n e. ( 1 ... N ) )
-> ( sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
x.
X )
= ( 0 x. X ) )
416:415:adantll |- ( ( ( ph
/\ ( &C37 : ( 0 ... N ) --> QQ
/\ A. n
e. ( 1 ... N )
sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. C )
= 0 ) )
/\ n e. ( 1 ... N ) )
-> ( sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
x.
X )
= ( 0 x. X ) )
417:h3:adantlr |- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ n e. ( 1 ... N ) )
-> X e. CC )
418:90,417,112:fsummulc1
|- ( ( ( ph /\ &C37 : ( 0 ... N ) --> QQ )
/\ n e. ( 1 ... N ) )
-> ( sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
x.
X )
= sum_ k
e. ( 0 ... N )
( ( ( &C37 ` k ) x. C ) x. X ) )
419:418:adantlrr |- ( ( ( ph
/\ ( &C37 : ( 0 ... N ) --> QQ
/\ A. n
e. ( 1 ... N )
sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. C )
= 0 ) )
/\ n e. ( 1 ... N ) )
-> ( sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
x.
X )
= sum_ k
e. ( 0 ... N )
( ( ( &C37 ` k ) x. C ) x. X ) )
420:h3:mul02d |- ( ( ph /\ n e. ( 1 ... N ) )
-> ( 0 x. X ) = 0 )
421:420:adantlr |- ( ( ( ph
/\ ( &C37 : ( 0 ... N ) --> QQ
/\ A. n
e. ( 1 ... N )
sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. C )
= 0 ) )
/\ n e. ( 1 ... N ) )
-> ( 0 x. X ) = 0 )
422:416,419,421:3eqtr3d
|- ( ( ( ph
/\ ( &C37 : ( 0 ... N ) --> QQ
/\ A. n
e. ( 1 ... N )
sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. C )
= 0 ) )
/\ n e. ( 1 ... N ) )
-> sum_ k
e. ( 0 ... N )
( ( ( &C37 ` k ) x. C ) x. X )
= 0 )
423:422:ex |- ( ( ph
/\ ( &C37 : ( 0 ... N ) --> QQ
/\ A. n
e. ( 1 ... N )
sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
= 0 ) )
-> ( n e. ( 1 ... N )
-> sum_ k
e. ( 0 ... N )
( ( ( &C37 ` k ) x. C ) x. X )
= 0 ) )
424:411,423:ralrimi
|- ( ( ph
/\ ( &C37 : ( 0 ... N ) --> QQ
/\ A. n
e. ( 1 ... N )
sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
= 0 ) )
-> A. n
e. ( 1 ... N )
sum_ k
e. ( 0 ... N )
( ( ( &C37 ` k ) x. C ) x. X )
= 0 )
425:424:sumeq2d |- ( ( ph
/\ ( &C37 : ( 0 ... N ) --> QQ
/\ A. n
e. ( 1 ... N )
sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
= 0 ) )
-> sum_ n
e. ( 1 ... N )
sum_ k
e. ( 0 ... N )
( ( ( &C37 ` k ) x. C ) x. X )
= sum_ n e. ( 1 ... N ) 0 )
426:406,425:eqtrd |- ( ( ph
/\ ( &C37 : ( 0 ... N ) --> QQ
/\ A. n
e. ( 1 ... N )
sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
= 0 ) )
-> sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. ( A ^ k ) )
= sum_ n e. ( 1 ... N ) 0 )
427:24:olci |- ( ( 1 ... N ) C_ ( ZZ>= ` &C5 ) \/ ( 1 ... N ) e. Fin )
428::sumz |- ( ( ( 1 ... N ) C_ ( ZZ>= ` &C5 )
\/ ( 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:syl6eq |- ( ( ph
/\ ( &C37 : ( 0 ... N ) --> QQ
/\ A. n
e. ( 1 ... N )
sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
= 0 ) )
-> sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. ( A ^ k ) )
= 0 )
431:380,430:eqtrd |- ( ( ph
/\ ( &C37 : ( 0 ... N ) --> QQ
/\ A. n
e. ( 1 ... N )
sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
= 0 ) )
-> ( ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
` A )
= 0 )
432:431:adantrlr |- ( ( ph
/\ ( ( &C37 : ( 0 ... N ) --> QQ
/\ &C37 =/= ( ( 0 ... N ) X. { 0 } ) )
/\ A. n
e. ( 1 ... N )
sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
= 0 ) )
-> ( ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
` A )
= 0 )
433::fveq1 |- ( &S20
= ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
-> ( &S20 ` A )
= ( ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
` A ) )
434:433:eqeq1d |- ( &S20
= ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
-> ( ( &S20 ` A ) = 0
<-> ( ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
` A )
= 0 ) )
435:434:rspcev |- ( ( ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
e. ( ( Poly ` QQ ) \ { 0p } )
/\ ( ( &S21
e. CC
|-> sum_ k
e. ( 0 ... N )
( ( &C37 ` k ) x. ( &S21 ^ k ) ) )
` A )
= 0 )
-> E. &S20 e. ( ( Poly ` QQ ) \ { 0p } ) ( &S20 ` A ) = 0
)
436:372,432,435:syl2anc
|- ( ( ph
/\ ( ( &C37 : ( 0 ... N ) --> QQ
/\ &C37 =/= ( ( 0 ... N ) X. { 0 } ) )
/\ A. n
e. ( 1 ... N )
sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
= 0 ) )
-> E. &S20 e. ( ( Poly ` QQ ) \ { 0p } ) ( &S20 ` A ) = 0
)
437:273,436:sylanr1
|- ( ( ph
/\ ( &C37
e. ( ( QQ ^m ( 0 ... N ) )
\ { ( ( 0 ... N ) X. { 0 } ) } )
/\ A. n
e. ( 1 ... N )
sum_ k e. ( 0 ... N ) ( ( &C37 ` k ) x. C )
= 0 ) )
-> E. &S20 e. ( ( Poly ` QQ ) \ { 0p } ) ( &S20 ` A ) = 0
)
438:270,437:rexlimddv
439::elqaa |- ( &C1 e. AA
<-> ( &C1 e. CC
/\ E. &S19
e. ( ( Poly ` QQ ) \ { 0p } )
( &S19 ` &C1 ) = 0 ) )
qed:h1,438,439:sylanbrc |- ( ph -> A e. AA )
$)
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/E1jSDZa-0007sF-UH%40rmmprod06.runbox.
