Users' Mathboxes Mathbox for David A. Wheeler < Previous   Wrap >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  aacllem Structured version   Unicode version

Theorem aacllem 40191
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.)
Hypotheses
Ref Expression
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
Ref Expression
aacllem  |-  ( ph  ->  A  e.  AA )
Distinct variable groups:    A, k, n    k, N, n    k, X    ph, k, n
Allowed substitution hints:    C( k, n)    X( n)

Proof of Theorem aacllem
Dummy variables  w  x  y  B  v 
z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 aacllem.0 . 2  |-  ( ph  ->  A  e.  CC )
2 aacllem.1 . . . . . . 7  |-  ( ph  ->  N  e.  NN0 )
32nn0red 10934 . . . . . 6  |-  ( ph  ->  N  e.  RR )
43ltp1d 10545 . . . . 5  |-  ( ph  ->  N  <  ( N  +  1 ) )
5 peano2nn0 10918 . . . . . . . 8  |-  ( N  e.  NN0  ->  ( N  +  1 )  e. 
NN0 )
62, 5syl 17 . . . . . . 7  |-  ( ph  ->  ( N  +  1 )  e.  NN0 )
76nn0red 10934 . . . . . 6  |-  ( ph  ->  ( N  +  1 )  e.  RR )
83, 7ltnled 9790 . . . . 5  |-  ( ph  ->  ( N  <  ( N  +  1 )  <->  -.  ( N  +  1 )  <_  N )
)
94, 8mpbid 213 . . . 4  |-  ( ph  ->  -.  ( N  + 
1 )  <_  N
)
10 aacllem.3 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( 0 ... N
)  /\  n  e.  ( 1 ... N
) )  ->  C  e.  QQ )
11103expa 1205 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ( 0 ... N
) )  /\  n  e.  ( 1 ... N
) )  ->  C  e.  QQ )
12 eqid 2422 . . . . . . . . . . 11  |-  ( n  e.  ( 1 ... N )  |->  C )  =  ( n  e.  ( 1 ... N
)  |->  C )
1311, 12fmptd 6062 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  (
n  e.  ( 1 ... N )  |->  C ) : ( 1 ... N ) --> QQ )
14 qex 11284 . . . . . . . . . . 11  |-  QQ  e.  _V
15 ovex 6334 . . . . . . . . . . 11  |-  ( 1 ... N )  e. 
_V
1614, 15elmap 7512 . . . . . . . . . 10  |-  ( ( n  e.  ( 1 ... N )  |->  C )  e.  ( QQ 
^m  ( 1 ... N ) )  <->  ( n  e.  ( 1 ... N
)  |->  C ) : ( 1 ... N
) --> QQ )
1713, 16sylibr 215 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  (
n  e.  ( 1 ... N )  |->  C )  e.  ( QQ 
^m  ( 1 ... N ) ) )
18 eqid 2422 . . . . . . . . 9  |-  ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )  =  ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )
1917, 18fmptd 6062 . . . . . . . 8  |-  ( ph  ->  ( k  e.  ( 0 ... N ) 
|->  ( n  e.  ( 1 ... N ) 
|->  C ) ) : ( 0 ... N
) --> ( QQ  ^m  ( 1 ... N
) ) )
20 eqid 2422 . . . . . . . . . . . 12  |-  (flds  QQ )  =  (flds  QQ )
2120qdrng 24457 . . . . . . . . . . 11  |-  (flds  QQ )  e.  DivRing
22 drngring 17982 . . . . . . . . . . 11  |-  ( (flds  QQ )  e.  DivRing  ->  (flds  QQ )  e.  Ring )
2321, 22ax-mp 5 . . . . . . . . . 10  |-  (flds  QQ )  e.  Ring
24 fzfi 12192 . . . . . . . . . 10  |-  ( 1 ... N )  e. 
Fin
25 eqid 2422 . . . . . . . . . . 11  |-  ( (flds  QQ ) freeLMod  ( 1 ... N
) )  =  ( (flds  QQ ) freeLMod  ( 1 ... N ) )
2625frlmlmod 19311 . . . . . . . . . 10  |-  ( ( (flds  QQ )  e.  Ring  /\  (
1 ... N )  e. 
Fin )  ->  (
(flds  QQ ) freeLMod  ( 1 ... N
) )  e.  LMod )
2723, 24, 26mp2an 676 . . . . . . . . 9  |-  ( (flds  QQ ) freeLMod  ( 1 ... N
) )  e.  LMod
28 fzfi 12192 . . . . . . . . 9  |-  ( 0 ... N )  e. 
Fin
2920qrngbas 24456 . . . . . . . . . . . 12  |-  QQ  =  ( Base `  (flds  QQ ) )
3025, 29frlmfibas 19323 . . . . . . . . . . 11  |-  ( ( (flds  QQ )  e.  DivRing  /\  (
1 ... N )  e. 
Fin )  ->  ( QQ  ^m  ( 1 ... N ) )  =  ( Base `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) ) )
3121, 24, 30mp2an 676 . . . . . . . . . 10  |-  ( QQ 
^m  ( 1 ... N ) )  =  ( Base `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) )
3225frlmsca 19315 . . . . . . . . . . 11  |-  ( ( (flds  QQ )  e.  DivRing  /\  (
1 ... N )  e. 
Fin )  ->  (flds  QQ )  =  (Scalar `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) )
3321, 24, 32mp2an 676 . . . . . . . . . 10  |-  (flds  QQ )  =  (Scalar `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) )
34 eqid 2422 . . . . . . . . . 10  |-  ( .s
`  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) )  =  ( .s
`  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) )
3520qrng0 24458 . . . . . . . . . . . 12  |-  0  =  ( 0g `  (flds  QQ ) )
3625, 35frlm0 19316 . . . . . . . . . . 11  |-  ( ( (flds  QQ )  e.  Ring  /\  (
1 ... N )  e. 
Fin )  ->  (
( 1 ... N
)  X.  { 0 } )  =  ( 0g `  ( (flds  QQ ) freeLMod  ( 1 ... N
) ) ) )
3723, 24, 36mp2an 676 . . . . . . . . . 10  |-  ( ( 1 ... N )  X.  { 0 } )  =  ( 0g
`  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) )
38 eqid 2422 . . . . . . . . . . . 12  |-  ( (flds  QQ ) freeLMod  ( 0 ... N
) )  =  ( (flds  QQ ) freeLMod  ( 0 ... N ) )
3938, 29frlmfibas 19323 . . . . . . . . . . 11  |-  ( ( (flds  QQ )  e.  DivRing  /\  (
0 ... N )  e. 
Fin )  ->  ( QQ  ^m  ( 0 ... N ) )  =  ( Base `  (
(flds  QQ ) freeLMod  ( 0 ... N
) ) ) )
4021, 28, 39mp2an 676 . . . . . . . . . 10  |-  ( QQ 
^m  ( 0 ... N ) )  =  ( Base `  (
(flds  QQ ) freeLMod  ( 0 ... N
) ) )
4131, 33, 34, 37, 35, 40islindf4 19395 . . . . . . . . 9  |-  ( ( ( (flds  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 
( (flds  QQ ) freeLMod  ( 1 ... N ) )  <->  A. w  e.  ( QQ  ^m  (
0 ... N ) ) ( ( ( (flds  QQ ) freeLMod  ( 1 ... N
) )  gsumg  ( w  oF ( .s `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) ) ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) ) ) )  =  ( ( 1 ... N )  X. 
{ 0 } )  ->  w  =  ( ( 0 ... N
)  X.  { 0 } ) ) ) )
4227, 28, 41mp3an12 1350 . . . . . . . 8  |-  ( ( 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  ( (flds  QQ ) freeLMod  ( 1 ... N ) )  <->  A. w  e.  ( QQ  ^m  ( 0 ... N ) ) ( ( ( (flds  QQ ) freeLMod  ( 1 ... N ) ) 
gsumg  ( w  oF
( .s `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) ) ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) ) ) )  =  ( ( 1 ... N )  X. 
{ 0 } )  ->  w  =  ( ( 0 ... N
)  X.  { 0 } ) ) ) )
4319, 42syl 17 . . . . . . 7  |-  ( ph  ->  ( ( k  e.  ( 0 ... N
)  |->  ( n  e.  ( 1 ... N
)  |->  C ) ) LIndF 
( (flds  QQ ) freeLMod  ( 1 ... N ) )  <->  A. w  e.  ( QQ  ^m  (
0 ... N ) ) ( ( ( (flds  QQ ) freeLMod  ( 1 ... N
) )  gsumg  ( w  oF ( .s `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) ) ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) ) ) )  =  ( ( 1 ... N )  X. 
{ 0 } )  ->  w  =  ( ( 0 ... N
)  X.  { 0 } ) ) ) )
44 elmapi 7505 . . . . . . . . 9  |-  ( w  e.  ( QQ  ^m  ( 0 ... N
) )  ->  w : ( 0 ... N ) --> QQ )
45 fzfid 12193 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  -> 
( 0 ... N
)  e.  Fin )
46 fvex 5892 . . . . . . . . . . . . . . . . . . 19  |-  ( w `
 k )  e. 
_V
4746a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  k  e.  ( 0 ... N ) )  ->  ( w `  k )  e.  _V )
4815mptex 6152 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  ( 1 ... N )  |->  C )  e.  _V
4948a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  k  e.  ( 0 ... N ) )  ->  ( n  e.  ( 1 ... N
)  |->  C )  e. 
_V )
50 simpr 462 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  ->  w : ( 0 ... N ) --> QQ )
5150feqmptd 5935 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  ->  w  =  ( k  e.  ( 0 ... N
)  |->  ( w `  k ) ) )
52 eqidd 2423 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  -> 
( k  e.  ( 0 ... N ) 
|->  ( n  e.  ( 1 ... N ) 
|->  C ) )  =  ( k  e.  ( 0 ... N ) 
|->  ( n  e.  ( 1 ... N ) 
|->  C ) ) )
5345, 47, 49, 51, 52offval2 6563 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  -> 
( w  oF ( .s `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) ) ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) ) )  =  ( k  e.  ( 0 ... N ) 
|->  ( ( w `  k ) ( .s
`  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) ( n  e.  ( 1 ... N
)  |->  C ) ) ) )
54 fzfid 12193 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  k  e.  ( 0 ... N ) )  ->  ( 1 ... N )  e. 
Fin )
55 ffvelrn 6036 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( w : ( 0 ... N ) --> QQ 
/\  k  e.  ( 0 ... N ) )  ->  ( w `  k )  e.  QQ )
5655adantll 718 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  k  e.  ( 0 ... N ) )  ->  ( w `  k )  e.  QQ )
5717adantlr 719 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  k  e.  ( 0 ... N ) )  ->  ( n  e.  ( 1 ... N
)  |->  C )  e.  ( QQ  ^m  (
1 ... N ) ) )
58 cnfldmul 18976 . . . . . . . . . . . . . . . . . . . . . 22  |-  x.  =  ( .r ` fld )
5920, 58ressmulr 15250 . . . . . . . . . . . . . . . . . . . . 21  |-  ( QQ  e.  _V  ->  x.  =  ( .r `  (flds  QQ ) ) )
6014, 59ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  x.  =  ( .r `  (flds  QQ ) )
6125, 31, 29, 54, 56, 57, 34, 60frlmvscafval 19327 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  k  e.  ( 0 ... N ) )  ->  ( (
w `  k )
( .s `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) ) ( n  e.  ( 1 ... N )  |->  C ) )  =  ( ( ( 1 ... N )  X.  {
( w `  k
) } )  oF  x.  ( n  e.  ( 1 ... N )  |->  C ) ) )
6246a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  k  e.  ( 0 ... N ) )  /\  n  e.  ( 1 ... N
) )  ->  (
w `  k )  e.  _V )
6311adantllr 723 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  k  e.  ( 0 ... N ) )  /\  n  e.  ( 1 ... N
) )  ->  C  e.  QQ )
64 fconstmpt 4897 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1 ... N )  X.  { ( w `
 k ) } )  =  ( n  e.  ( 1 ... N )  |->  ( w `
 k ) )
6564a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  k  e.  ( 0 ... N ) )  ->  ( (
1 ... N )  X. 
{ ( w `  k ) } )  =  ( n  e.  ( 1 ... N
)  |->  ( w `  k ) ) )
66 eqidd 2423 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  k  e.  ( 0 ... N ) )  ->  ( n  e.  ( 1 ... N
)  |->  C )  =  ( n  e.  ( 1 ... N ) 
|->  C ) )
6754, 62, 63, 65, 66offval2 6563 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 ) ) )
6861, 67eqtrd 2463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  k  e.  ( 0 ... N ) )  ->  ( (
w `  k )
( .s `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) ) ( n  e.  ( 1 ... N )  |->  C ) )  =  ( n  e.  ( 1 ... N )  |->  ( ( w `  k
)  x.  C ) ) )
6968mpteq2dva 4510 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  -> 
( k  e.  ( 0 ... N ) 
|->  ( ( w `  k ) ( .s
`  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) ( n  e.  ( 1 ... N
)  |->  C ) ) )  =  ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  ( ( w `  k )  x.  C ) ) ) )
7053, 69eqtrd 2463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  -> 
( w  oF ( .s `  (
(flds  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
) ) ) )
7170oveq2d 6322 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  -> 
( ( (flds  QQ ) freeLMod  ( 1 ... N ) ) 
gsumg  ( w  oF
( .s `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) ) ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) ) ) )  =  ( ( (flds  QQ ) freeLMod  ( 1 ... N
) )  gsumg  ( k  e.  ( 0 ... N ) 
|->  ( n  e.  ( 1 ... N ) 
|->  ( ( w `  k )  x.  C
) ) ) ) )
72 fzfid 12193 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  -> 
( 1 ... N
)  e.  Fin )
7323a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  -> 
(flds  QQ )  e.  Ring )
7456adantlr 719 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  n  e.  ( 1 ... N ) )  /\  k  e.  ( 0 ... N
) )  ->  (
w `  k )  e.  QQ )
7511an32s 811 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  k  e.  ( 0 ... N
) )  ->  C  e.  QQ )
7675adantllr 723 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  n  e.  ( 1 ... N ) )  /\  k  e.  ( 0 ... N
) )  ->  C  e.  QQ )
77 qmulcl 11290 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( w `  k
)  e.  QQ  /\  C  e.  QQ )  ->  ( ( w `  k )  x.  C
)  e.  QQ )
7874, 76, 77syl2anc 665 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  n  e.  ( 1 ... N ) )  /\  k  e.  ( 0 ... N
) )  ->  (
( w `  k
)  x.  C )  e.  QQ )
7978an32s 811 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  k  e.  ( 0 ... N ) )  /\  n  e.  ( 1 ... N
) )  ->  (
( w `  k
)  x.  C )  e.  QQ )
80 eqid 2422 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  ( 1 ... N )  |->  ( ( w `  k )  x.  C ) )  =  ( n  e.  ( 1 ... N
)  |->  ( ( w `
 k )  x.  C ) )
8179, 80fmptd 6062 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  k  e.  ( 0 ... N ) )  ->  ( n  e.  ( 1 ... N
)  |->  ( ( w `
 k )  x.  C ) ) : ( 1 ... N
) --> QQ )
8214, 15elmap 7512 . . . . . . . . . . . . . . . . 17  |-  ( ( n  e.  ( 1 ... N )  |->  ( ( w `  k
)  x.  C ) )  e.  ( QQ 
^m  ( 1 ... N ) )  <->  ( n  e.  ( 1 ... N
)  |->  ( ( w `
 k )  x.  C ) ) : ( 1 ... N
) --> QQ )
8381, 82sylibr 215 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  k  e.  ( 0 ... N ) )  ->  ( n  e.  ( 1 ... N
)  |->  ( ( w `
 k )  x.  C ) )  e.  ( QQ  ^m  (
1 ... N ) ) )
84 eqid 2422 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  ( ( w `  k )  x.  C ) ) )  =  ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  ( ( w `  k )  x.  C ) ) )
8515mptex 6152 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  ( 1 ... N )  |->  ( ( w `  k )  x.  C ) )  e.  _V
8685a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  k  e.  ( 0 ... N ) )  ->  ( n  e.  ( 1 ... N
)  |->  ( ( w `
 k )  x.  C ) )  e. 
_V )
87 snex 4662 . . . . . . . . . . . . . . . . . . 19  |-  { 0 }  e.  _V
8815, 87xpex 6610 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1 ... N )  X.  { 0 } )  e.  _V
8988a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  -> 
( ( 1 ... N )  X.  {
0 } )  e. 
_V )
9084, 45, 86, 89fsuppmptdm 7904 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  -> 
( k  e.  ( 0 ... N ) 
|->  ( n  e.  ( 1 ... N ) 
|->  ( ( w `  k )  x.  C
) ) ) finSupp  (
( 1 ... N
)  X.  { 0 } ) )
9125, 31, 37, 72, 45, 73, 83, 90frlmgsum 19329 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  -> 
( ( (flds  QQ ) freeLMod  ( 1 ... N ) ) 
gsumg  ( k  e.  ( 0 ... N ) 
|->  ( n  e.  ( 1 ... N ) 
|->  ( ( w `  k )  x.  C
) ) ) )  =  ( n  e.  ( 1 ... N
)  |->  ( (flds  QQ )  gsumg  ( k  e.  ( 0 ... N ) 
|->  ( ( w `  k )  x.  C
) ) ) ) )
92 cnfldbas 18974 . . . . . . . . . . . . . . . . . 18  |-  CC  =  ( Base ` fld )
93 cnfldadd 18975 . . . . . . . . . . . . . . . . . 18  |-  +  =  ( +g  ` fld )
94 cnfldex 18973 . . . . . . . . . . . . . . . . . . 19  |-fld  e.  _V
9594a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  n  e.  ( 1 ... N ) )  ->fld  e.  _V )
96 fzfid 12193 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  n  e.  ( 1 ... N ) )  ->  ( 0 ... N )  e. 
Fin )
97 qsscn 11283 . . . . . . . . . . . . . . . . . . 19  |-  QQ  C_  CC
9897a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  n  e.  ( 1 ... N ) )  ->  QQ  C_  CC )
99 eqid 2422 . . . . . . . . . . . . . . . . . . 19  |-  ( k  e.  ( 0 ... N )  |->  ( ( w `  k )  x.  C ) )  =  ( k  e.  ( 0 ... N
)  |->  ( ( w `
 k )  x.  C ) )
10078, 99fmptd 6062 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  n  e.  ( 1 ... N ) )  ->  ( k  e.  ( 0 ... N
)  |->  ( ( w `
 k )  x.  C ) ) : ( 0 ... N
) --> QQ )
101 0z 10956 . . . . . . . . . . . . . . . . . . . 20  |-  0  e.  ZZ
102 zq 11278 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  e.  ZZ  ->  0  e.  QQ )
103101, 102ax-mp 5 . . . . . . . . . . . . . . . . . . 19  |-  0  e.  QQ
104103a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  n  e.  ( 1 ... N ) )  ->  0  e.  QQ )
105 addid2 9824 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  CC  ->  (
0  +  x )  =  x )
106 addid1 9821 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  CC  ->  (
x  +  0 )  =  x )
107105, 106jca 534 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  CC  ->  (
( 0  +  x
)  =  x  /\  ( x  +  0
)  =  x ) )
108107adantl 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  n  e.  ( 1 ... N ) )  /\  x  e.  CC )  ->  (
( 0  +  x
)  =  x  /\  ( x  +  0
)  =  x ) )
10992, 93, 20, 95, 96, 98, 100, 104, 108gsumress 16519 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  n  e.  ( 1 ... N ) )  ->  (fld  gsumg  ( k  e.  ( 0 ... N ) 
|->  ( ( w `  k )  x.  C
) ) )  =  ( (flds  QQ )  gsumg  ( k  e.  ( 0 ... N ) 
|->  ( ( w `  k )  x.  C
) ) ) )
110 simplr 760 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  n  e.  ( 1 ... N ) )  ->  w :
( 0 ... N
) --> QQ )
111 qcn 11286 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( w `  k )  e.  QQ  ->  (
w `  k )  e.  CC )
11255, 111syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( w : ( 0 ... N ) --> QQ 
/\  k  e.  ( 0 ... N ) )  ->  ( w `  k )  e.  CC )
113110, 112sylan 473 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  n  e.  ( 1 ... N ) )  /\  k  e.  ( 0 ... N
) )  ->  (
w `  k )  e.  CC )
114 qcn 11286 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( C  e.  QQ  ->  C  e.  CC )
11511, 114syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  k  e.  ( 0 ... N
) )  /\  n  e.  ( 1 ... N
) )  ->  C  e.  CC )
116115an32s 811 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  k  e.  ( 0 ... N
) )  ->  C  e.  CC )
117116adantllr 723 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  n  e.  ( 1 ... N ) )  /\  k  e.  ( 0 ... N
) )  ->  C  e.  CC )
118113, 117mulcld 9671 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  n  e.  ( 1 ... N ) )  /\  k  e.  ( 0 ... N
) )  ->  (
( w `  k
)  x.  C )  e.  CC )
11996, 118gsumfsum 19034 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  n  e.  ( 1 ... N ) )  ->  (fld  gsumg  ( k  e.  ( 0 ... N ) 
|->  ( ( w `  k )  x.  C
) ) )  = 
sum_ k  e.  ( 0 ... N ) ( ( w `  k )  x.  C
) )
120109, 119eqtr3d 2465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  n  e.  ( 1 ... N ) )  ->  ( (flds  QQ )  gsumg  ( k  e.  ( 0 ... N )  |->  ( ( w `  k
)  x.  C ) ) )  =  sum_ k  e.  ( 0 ... N ) ( ( w `  k
)  x.  C ) )
121120mpteq2dva 4510 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  -> 
( n  e.  ( 1 ... N ) 
|->  ( (flds  QQ )  gsumg  ( k  e.  ( 0 ... N ) 
|->  ( ( w `  k )  x.  C
) ) ) )  =  ( n  e.  ( 1 ... N
)  |->  sum_ k  e.  ( 0 ... N ) ( ( w `  k )  x.  C
) ) )
12271, 91, 1213eqtrd 2467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  -> 
( ( (flds  QQ ) freeLMod  ( 1 ... N ) ) 
gsumg  ( w  oF
( .s `  (
(flds  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
) ) )
123 qaddcl 11288 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  QQ  /\  y  e.  QQ )  ->  ( x  +  y )  e.  QQ )
124123adantl 467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  n  e.  ( 1 ... N ) )  /\  ( x  e.  QQ  /\  y  e.  QQ ) )  -> 
( x  +  y )  e.  QQ )
12598, 124, 96, 78, 104fsumcllem 13798 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  n  e.  ( 1 ... N ) )  ->  sum_ k  e.  ( 0 ... N
) ( ( w `
 k )  x.  C )  e.  QQ )
126 eqid 2422 . . . . . . . . . . . . . . . 16  |-  ( 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
) )
127125, 126fmptd 6062 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  -> 
( n  e.  ( 1 ... N ) 
|->  sum_ k  e.  ( 0 ... N ) ( ( w `  k )  x.  C
) ) : ( 1 ... N ) --> QQ )
12814, 15elmap 7512 . . . . . . . . . . . . . . 15  |-  ( ( 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 )
129127, 128sylibr 215 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  -> 
( n  e.  ( 1 ... N ) 
|->  sum_ k  e.  ( 0 ... N ) ( ( w `  k )  x.  C
) )  e.  ( QQ  ^m  ( 1 ... N ) ) )
130122, 129eqeltrd 2507 . . . . . . . . . . . . 13  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  -> 
( ( (flds  QQ ) freeLMod  ( 1 ... N ) ) 
gsumg  ( w  oF
( .s `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) ) ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) ) ) )  e.  ( QQ  ^m  ( 1 ... N
) ) )
131 elmapi 7505 . . . . . . . . . . . . 13  |-  ( ( ( (flds  QQ ) freeLMod  ( 1 ... N ) )  gsumg  ( w  oF ( .s
`  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) ( k  e.  ( 0 ... N
)  |->  ( n  e.  ( 1 ... N
)  |->  C ) ) ) )  e.  ( QQ  ^m  ( 1 ... N ) )  ->  ( ( (flds  QQ ) freeLMod  ( 1 ... N
) )  gsumg  ( w  oF ( .s `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) ) ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) ) ) ) : ( 1 ... N ) --> QQ )
132 ffn 5746 . . . . . . . . . . . . 13  |-  ( ( ( (flds  QQ ) freeLMod  ( 1 ... N ) )  gsumg  ( w  oF ( .s
`  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) ( k  e.  ( 0 ... N
)  |->  ( n  e.  ( 1 ... N
)  |->  C ) ) ) ) : ( 1 ... N ) --> QQ  ->  ( (
(flds  QQ ) freeLMod  ( 1 ... N
) )  gsumg  ( w  oF ( .s `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) ) ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) ) ) )  Fn  ( 1 ... N ) )
133130, 131, 1323syl 18 . . . . . . . . . . . 12  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  -> 
( ( (flds  QQ ) freeLMod  ( 1 ... N ) ) 
gsumg  ( w  oF
( .s `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) ) ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) ) ) )  Fn  ( 1 ... N ) )
134 c0ex 9645 . . . . . . . . . . . . 13  |-  0  e.  _V
135 fnconstg 5788 . . . . . . . . . . . . 13  |-  ( 0  e.  _V  ->  (
( 1 ... N
)  X.  { 0 } )  Fn  (
1 ... N ) )
136134, 135ax-mp 5 . . . . . . . . . . . 12  |-  ( ( 1 ... N )  X.  { 0 } )  Fn  ( 1 ... N )
137 nfcv 2580 . . . . . . . . . . . . . 14  |-  F/_ n
( (flds  QQ ) freeLMod  ( 1 ... N ) )
138 nfcv 2580 . . . . . . . . . . . . . 14  |-  F/_ n  gsumg
139 nfcv 2580 . . . . . . . . . . . . . . 15  |-  F/_ n w
140 nfcv 2580 . . . . . . . . . . . . . . 15  |-  F/_ n  oF ( .s
`  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) )
141 nfcv 2580 . . . . . . . . . . . . . . . 16  |-  F/_ n
( 0 ... N
)
142 nfmpt1 4513 . . . . . . . . . . . . . . . 16  |-  F/_ n
( n  e.  ( 1 ... N ) 
|->  C )
143141, 142nfmpt 4512 . . . . . . . . . . . . . . 15  |-  F/_ n
( k  e.  ( 0 ... N ) 
|->  ( n  e.  ( 1 ... N ) 
|->  C ) )
144139, 140, 143nfov 6332 . . . . . . . . . . . . . 14  |-  F/_ n
( w  oF ( .s `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) ) ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) ) )
145137, 138, 144nfov 6332 . . . . . . . . . . . . 13  |-  F/_ n
( ( (flds  QQ ) freeLMod  ( 1 ... N ) ) 
gsumg  ( w  oF
( .s `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) ) ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) ) ) )
146 nfcv 2580 . . . . . . . . . . . . 13  |-  F/_ n
( ( 1 ... N )  X.  {
0 } )
147145, 146eqfnfv2f 5996 . . . . . . . . . . . 12  |-  ( ( ( ( (flds  QQ ) freeLMod  ( 1 ... N ) ) 
gsumg  ( w  oF
( .s `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) ) ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) ) ) )  Fn  ( 1 ... N )  /\  (
( 1 ... N
)  X.  { 0 } )  Fn  (
1 ... N ) )  ->  ( ( ( (flds  QQ ) freeLMod  ( 1 ... N ) )  gsumg  ( w  oF ( .s
`  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) ( k  e.  ( 0 ... N
)  |->  ( n  e.  ( 1 ... N
)  |->  C ) ) ) )  =  ( ( 1 ... N
)  X.  { 0 } )  <->  A. n  e.  ( 1 ... N
) ( ( ( (flds  QQ ) freeLMod  ( 1 ... N ) )  gsumg  ( w  oF ( .s
`  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) ( k  e.  ( 0 ... N
)  |->  ( n  e.  ( 1 ... N
)  |->  C ) ) ) ) `  n
)  =  ( ( ( 1 ... N
)  X.  { 0 } ) `  n
) ) )
148133, 136, 147sylancl 666 . . . . . . . . . . 11  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  -> 
( ( ( (flds  QQ ) freeLMod  ( 1 ... N
) )  gsumg  ( w  oF ( .s `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) ) ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) ) ) )  =  ( ( 1 ... N )  X. 
{ 0 } )  <->  A. n  e.  (
1 ... N ) ( ( ( (flds  QQ ) freeLMod  ( 1 ... N ) ) 
gsumg  ( w  oF
( .s `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) ) ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) ) ) ) `
 n )  =  ( ( ( 1 ... N )  X. 
{ 0 } ) `
 n ) ) )
149122fveq1d 5884 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  -> 
( ( ( (flds  QQ ) freeLMod  ( 1 ... N
) )  gsumg  ( w  oF ( .s `  (
(flds  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
) )
150 sumex 13754 . . . . . . . . . . . . . . 15  |-  sum_ k  e.  ( 0 ... N
) ( ( w `
 k )  x.  C )  e.  _V
151126fvmpt2 5974 . . . . . . . . . . . . . . 15  |-  ( ( 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 ) )
152150, 151mpan2 675 . . . . . . . . . . . . . 14  |-  ( 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 ) )
153149, 152sylan9eq 2483 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  n  e.  ( 1 ... N ) )  ->  ( (
( (flds  QQ ) freeLMod  ( 1 ... N ) )  gsumg  ( w  oF ( .s
`  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) ( k  e.  ( 0 ... N
)  |->  ( n  e.  ( 1 ... N
)  |->  C ) ) ) ) `  n
)  =  sum_ k  e.  ( 0 ... N
) ( ( w `
 k )  x.  C ) )
154134fvconst2 6136 . . . . . . . . . . . . . 14  |-  ( n  e.  ( 1 ... N )  ->  (
( ( 1 ... N )  X.  {
0 } ) `  n )  =  0 )
155154adantl 467 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  n  e.  ( 1 ... N ) )  ->  ( (
( 1 ... N
)  X.  { 0 } ) `  n
)  =  0 )
156153, 155eqeq12d 2444 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  w : ( 0 ... N ) --> QQ )  /\  n  e.  ( 1 ... N ) )  ->  ( (
( ( (flds  QQ ) freeLMod  ( 1 ... N ) ) 
gsumg  ( w  oF
( .s `  (
(flds  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 ) )
157156ralbidva 2858 . . . . . . . . . . 11  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  -> 
( A. n  e.  ( 1 ... N
) ( ( ( (flds  QQ ) freeLMod  ( 1 ... N ) )  gsumg  ( w  oF ( .s
`  ( (flds  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 ) )
158148, 157bitrd 256 . . . . . . . . . 10  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  -> 
( ( ( (flds  QQ ) freeLMod  ( 1 ... N
) )  gsumg  ( w  oF ( .s `  (
(flds  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 ) )
159158imbi1d 318 . . . . . . . . 9  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  -> 
( ( ( ( (flds  QQ ) freeLMod  ( 1 ... N ) )  gsumg  ( w  oF ( .s
`  ( (flds  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 } ) ) ) )
16044, 159sylan2 476 . . . . . . . 8  |-  ( (
ph  /\  w  e.  ( QQ  ^m  (
0 ... N ) ) )  ->  ( (
( ( (flds  QQ ) freeLMod  ( 1 ... N ) ) 
gsumg  ( w  oF
( .s `  (
(flds  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 } ) ) ) )
161160ralbidva 2858 . . . . . . 7  |-  ( ph  ->  ( A. w  e.  ( QQ  ^m  (
0 ... N ) ) ( ( ( (flds  QQ ) freeLMod  ( 1 ... N
) )  gsumg  ( w  oF ( .s `  (
(flds  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 } ) ) ) )
16243, 161bitrd 256 . . . . . 6  |-  ( ph  ->  ( ( k  e.  ( 0 ... N
)  |->  ( n  e.  ( 1 ... N
)  |->  C ) ) LIndF 
( (flds  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 } ) ) ) )
163 drngnzr 18486 . . . . . . . . 9  |-  ( (flds  QQ )  e.  DivRing  ->  (flds  QQ )  e. NzRing )
16421, 163ax-mp 5 . . . . . . . 8  |-  (flds  QQ )  e. NzRing
16533islindf3 19383 . . . . . . . 8  |-  ( ( ( (flds  QQ ) freeLMod  ( 1 ... N ) )  e. 
LMod  /\  (flds  QQ )  e. NzRing )  ->  ( ( k  e.  ( 0 ... N ) 
|->  ( n  e.  ( 1 ... N ) 
|->  C ) ) LIndF  (
(flds  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 `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) ) ) ) )
16627, 164, 165mp2an 676 . . . . . . 7  |-  ( ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) ) LIndF  ( (flds  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 `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) ) ) )
16748, 18dmmpti 5725 . . . . . . . . 9  |-  dom  (
k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )  =  ( 0 ... N )
168 f1eq2 5792 . . . . . . . . 9  |-  ( 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 ) )
169167, 168ax-mp 5 . . . . . . . 8  |-  ( ( 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 )
170169anbi1i 699 . . . . . . 7  |-  ( ( ( 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 `  ( (flds  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 `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) ) ) )
171166, 170bitri 252 . . . . . 6  |-  ( ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) ) LIndF  ( (flds  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 `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) ) )
172 con34b 293 . . . . . . . . 9  |-  ( ( 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 ) )
173 df-nel 2617 . . . . . . . . . . 11  |-  ( w  e/  { ( ( 0 ... N )  X.  { 0 } ) }  <->  -.  w  e.  { ( ( 0 ... N )  X. 
{ 0 } ) } )
174 elsn 4012 . . . . . . . . . . 11  |-  ( w  e.  { ( ( 0 ... N )  X.  { 0 } ) }  <->  w  =  ( ( 0 ... N )  X.  {
0 } ) )
175173, 174xchbinx 311 . . . . . . . . . 10  |-  ( w  e/  { ( ( 0 ... N )  X.  { 0 } ) }  <->  -.  w  =  ( ( 0 ... N )  X. 
{ 0 } ) )
176175imbi1i 326 . . . . . . . . 9  |-  ( ( 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 ) )
177172, 176bitr4i 255 . . . . . . . 8  |-  ( ( 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 ) )
178177ralbii 2853 . . . . . . 7  |-  ( 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 ) )
179 raldifb 3605 . . . . . . 7  |-  ( 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 )
180 ralnex 2868 . . . . . . 7  |-  ( 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 )
181178, 179, 1803bitri 274 . . . . . 6  |-  ( 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 )
182162, 171, 1813bitr3g 290 . . . . 5  |-  ( 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 `  (
(flds  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 ) )
183 eqid 2422 . . . . . . . . . . . . 13  |-  ( LSubSp `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) )  =  ( LSubSp `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) )
18431, 183lssmre 18189 . . . . . . . . . . . 12  |-  ( ( (flds  QQ ) freeLMod  ( 1 ... N ) )  e. 
LMod  ->  ( LSubSp `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) )  e.  (Moore `  ( QQ  ^m  ( 1 ... N
) ) ) )
18527, 184ax-mp 5 . . . . . . . . . . 11  |-  ( LSubSp `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) )  e.  (Moore `  ( QQ  ^m  ( 1 ... N ) ) )
186185a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  ran  ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )  e.  (LIndS `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) )  ->  ( LSubSp `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) )  e.  (Moore `  ( QQ  ^m  ( 1 ... N ) ) ) )
187 eqid 2422 . . . . . . . . . . . 12  |-  ( LSpan `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) )  =  ( LSpan `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) )
188 eqid 2422 . . . . . . . . . . . 12  |-  (mrCls `  ( LSubSp `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) )  =  (mrCls `  ( LSubSp `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) )
189183, 187, 188mrclsp 18212 . . . . . . . . . . 11  |-  ( ( (flds  QQ ) freeLMod  ( 1 ... N ) )  e. 
LMod  ->  ( LSpan `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) )  =  (mrCls `  ( LSubSp `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) ) )
19027, 189ax-mp 5 . . . . . . . . . 10  |-  ( LSpan `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) )  =  (mrCls `  ( LSubSp `
 ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) )
191 eqid 2422 . . . . . . . . . 10  |-  (mrInd `  ( LSubSp `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) )  =  (mrInd `  ( LSubSp `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) )
19233islvec 18327 . . . . . . . . . . . . 13  |-  ( ( (flds  QQ ) freeLMod  ( 1 ... N ) )  e. 
LVec 
<->  ( ( (flds  QQ ) freeLMod  ( 1 ... N ) )  e.  LMod  /\  (flds  QQ )  e.  DivRing ) )
19327, 21, 192mpbir2an 928 . . . . . . . . . . . 12  |-  ( (flds  QQ ) freeLMod  ( 1 ... N
) )  e.  LVec
194183, 190, 31lssacsex 18367 . . . . . . . . . . . . 13  |-  ( ( (flds  QQ ) freeLMod  ( 1 ... N ) )  e. 
LVec  ->  ( ( LSubSp `  ( (flds  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 `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) ) `  ( z  u.  {
x } ) ) 
\  ( ( LSpan `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) `
 z ) ) x  e.  ( (
LSpan `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) `  ( z  u.  { y } ) ) ) )
195194simprd 464 . . . . . . . . . . . 12  |-  ( ( (flds  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 `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) ) `  ( z  u.  {
x } ) ) 
\  ( ( LSpan `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) `
 z ) ) x  e.  ( (
LSpan `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) `  ( z  u.  { y } ) ) )
196193, 195ax-mp 5 . . . . . . . . . . 11  |-  A. z  e.  ~P  ( QQ  ^m  ( 1 ... N
) ) A. x  e.  ( QQ  ^m  (
1 ... N ) ) A. y  e.  ( ( ( LSpan `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) ) `  ( z  u.  {
x } ) ) 
\  ( ( LSpan `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) `
 z ) ) x  e.  ( (
LSpan `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) `  ( z  u.  { y } ) )
197196a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  ran  ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )  e.  (LIndS `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) )  ->  A. z  e.  ~P  ( QQ  ^m  ( 1 ... N
) ) A. x  e.  ( QQ  ^m  (
1 ... N ) ) A. y  e.  ( ( ( LSpan `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) ) `  ( z  u.  {
x } ) ) 
\  ( ( LSpan `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) `
 z ) ) x  e.  ( (
LSpan `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) `  ( z  u.  { y } ) ) )
198 frn 5752 . . . . . . . . . . . . 13  |-  ( ( 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
) ) )
19919, 198syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ran  ( k  e.  ( 0 ... N
)  |->  ( n  e.  ( 1 ... N
)  |->  C ) ) 
C_  ( QQ  ^m  ( 1 ... N
) ) )
200 dif0 3867 . . . . . . . . . . . 12  |-  ( ( QQ  ^m  ( 1 ... N ) ) 
\  (/) )  =  ( QQ  ^m  ( 1 ... N ) )
201199, 200syl6sseqr 3511 . . . . . . . . . . 11  |-  ( ph  ->  ran  ( k  e.  ( 0 ... N
)  |->  ( n  e.  ( 1 ... N
)  |->  C ) ) 
C_  ( ( QQ 
^m  ( 1 ... N ) )  \  (/) ) )
202201adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  ran  ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )  e.  (LIndS `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) )  ->  ran  ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )  C_  ( ( QQ  ^m  ( 1 ... N ) )  \  (/) ) )
203 eqid 2422 . . . . . . . . . . . . . . 15  |-  ( (flds  QQ ) unitVec 
( 1 ... N
) )  =  ( (flds  QQ ) unitVec  ( 1 ... N ) )
204203, 25, 31uvcff 19348 . . . . . . . . . . . . . 14  |-  ( ( (flds  QQ )  e.  Ring  /\  (
1 ... N )  e. 
Fin )  ->  (
(flds  QQ ) unitVec  ( 1 ... N
) ) : ( 1 ... N ) --> ( QQ  ^m  (
1 ... N ) ) )
20523, 24, 204mp2an 676 . . . . . . . . . . . . 13  |-  ( (flds  QQ ) unitVec 
( 1 ... N
) ) : ( 1 ... N ) --> ( QQ  ^m  (
1 ... N ) )
206 frn 5752 . . . . . . . . . . . . 13  |-  ( ( (flds  QQ ) unitVec  ( 1 ... N ) ) : ( 1 ... N
) --> ( QQ  ^m  ( 1 ... N
) )  ->  ran  ( (flds  QQ ) unitVec  ( 1 ... N ) )  C_  ( QQ  ^m  (
1 ... N ) ) )
207205, 206ax-mp 5 . . . . . . . . . . . 12  |-  ran  (
(flds  QQ ) unitVec  ( 1 ... N
) )  C_  ( QQ  ^m  ( 1 ... N ) )
208207, 200sseqtr4i 3497 . . . . . . . . . . 11  |-  ran  (
(flds  QQ ) unitVec  ( 1 ... N
) )  C_  (
( QQ  ^m  (
1 ... N ) ) 
\  (/) )
209208a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  ran  ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )  e.  (LIndS `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) )  ->  ran  ( (flds  QQ ) unitVec 
( 1 ... N
) )  C_  (
( QQ  ^m  (
1 ... N ) ) 
\  (/) ) )
210 un0 3789 . . . . . . . . . . . . . 14  |-  ( ran  ( (flds  QQ ) unitVec  ( 1 ... N ) )  u.  (/) )  =  ran  ( (flds  QQ ) unitVec  ( 1 ... N ) )
211210fveq2i 5885 . . . . . . . . . . . . 13  |-  ( (
LSpan `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) `  ( ran  ( (flds  QQ ) unitVec  ( 1 ... N ) )  u.  (/) ) )  =  ( ( LSpan `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) `  ran  ( (flds  QQ ) unitVec  ( 1 ... N ) ) )
212 eqid 2422 . . . . . . . . . . . . . . . 16  |-  (LBasis `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) )  =  (LBasis `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) )
21325, 203, 212frlmlbs 19354 . . . . . . . . . . . . . . 15  |-  ( ( (flds  QQ )  e.  Ring  /\  (
1 ... N )  e. 
Fin )  ->  ran  ( (flds  QQ ) unitVec  ( 1 ... N ) )  e.  (LBasis `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) )
21423, 24, 213mp2an 676 . . . . . . . . . . . . . 14  |-  ran  (
(flds  QQ ) unitVec  ( 1 ... N
) )  e.  (LBasis `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) )
21531, 212, 187lbssp 18302 . . . . . . . . . . . . . 14  |-  ( ran  ( (flds  QQ ) unitVec  ( 1 ... N ) )  e.  (LBasis `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) )  ->  (
( LSpan `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) `  ran  ( (flds  QQ ) unitVec  ( 1 ... N ) ) )  =  ( QQ  ^m  ( 1 ... N
) ) )
216214, 215ax-mp 5 . . . . . . . . . . . . 13  |-  ( (
LSpan `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) `  ran  (
(flds  QQ ) unitVec  ( 1 ... N
) ) )  =  ( QQ  ^m  (
1 ... N ) )
217211, 216eqtri 2451 . . . . . . . . . . . 12  |-  ( (
LSpan `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) `  ( ran  ( (flds  QQ ) unitVec  ( 1 ... N ) )  u.  (/) ) )  =  ( QQ  ^m  ( 1 ... N ) )
218199, 217syl6sseqr 3511 . . . . . . . . . . 11  |-  ( ph  ->  ran  ( k  e.  ( 0 ... N
)  |->  ( n  e.  ( 1 ... N
)  |->  C ) ) 
C_  ( ( LSpan `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) `
 ( ran  (
(flds  QQ ) unitVec  ( 1 ... N
) )  u.  (/) ) ) )
219218adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  ran  ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )  e.  (LIndS `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) )  ->  ran  ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )  C_  ( ( LSpan `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) `  ( ran  ( (flds  QQ ) unitVec  ( 1 ... N ) )  u.  (/) ) ) )
220 un0 3789 . . . . . . . . . . 11  |-  ( ran  ( k  e.  ( 0 ... N ) 
|->  ( n  e.  ( 1 ... N ) 
|->  C ) )  u.  (/) )  =  ran  ( k  e.  ( 0 ... N ) 
|->  ( n  e.  ( 1 ... N ) 
|->  C ) )
22127, 164pm3.2i 456 . . . . . . . . . . . . . 14  |-  ( ( (flds  QQ ) freeLMod  ( 1 ... N ) )  e. 
LMod  /\  (flds  QQ )  e. NzRing )
222187, 33lindsind2 19376 . . . . . . . . . . . . . 14  |-  ( ( ( ( (flds  QQ ) freeLMod  ( 1 ... N ) )  e.  LMod  /\  (flds  QQ )  e. NzRing )  /\  ran  (
k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )  e.  (LIndS `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) )  /\  x  e.  ran  ( k  e.  ( 0 ... N ) 
|->  ( n  e.  ( 1 ... N ) 
|->  C ) ) )  ->  -.  x  e.  ( ( LSpan `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) ) `  ( ran  ( k  e.  ( 0 ... N
)  |->  ( n  e.  ( 1 ... N
)  |->  C ) ) 
\  { x }
) ) )
223221, 222mp3an1 1347 . . . . . . . . . . . . 13  |-  ( ( ran  ( k  e.  ( 0 ... N
)  |->  ( n  e.  ( 1 ... N
)  |->  C ) )  e.  (LIndS `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) )  /\  x  e.  ran  ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) ) )  ->  -.  x  e.  ( ( LSpan `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) `  ( ran  ( k  e.  ( 0 ... N ) 
|->  ( n  e.  ( 1 ... N ) 
|->  C ) )  \  { x } ) ) )
224223ralrimiva 2836 . . . . . . . . . . . 12  |-  ( ran  ( k  e.  ( 0 ... N ) 
|->  ( n  e.  ( 1 ... N ) 
|->  C ) )  e.  (LIndS `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) )  ->  A. x  e.  ran  ( k  e.  ( 0 ... N
)  |->  ( n  e.  ( 1 ... N
)  |->  C ) )  -.  x  e.  ( ( LSpan `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) `  ( ran  ( k  e.  ( 0 ... N ) 
|->  ( n  e.  ( 1 ... N ) 
|->  C ) )  \  { x } ) ) )
225190, 191ismri2 15538 . . . . . . . . . . . . . 14  |-  ( ( ( LSubSp `  ( (flds  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 `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) )  <->  A. x  e.  ran  ( k  e.  ( 0 ... N
)  |->  ( n  e.  ( 1 ... N
)  |->  C ) )  -.  x  e.  ( ( LSpan `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) `  ( ran  ( k  e.  ( 0 ... N ) 
|->  ( n  e.  ( 1 ... N ) 
|->  C ) )  \  { x } ) ) ) )
226185, 199, 225sylancr 667 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ran  ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )  e.  (mrInd `  ( LSubSp `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) )  <->  A. x  e.  ran  ( k  e.  ( 0 ... N
)  |->  ( n  e.  ( 1 ... N
)  |->  C ) )  -.  x  e.  ( ( LSpan `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) `  ( ran  ( k  e.  ( 0 ... N ) 
|->  ( n  e.  ( 1 ... N ) 
|->  C ) )  \  { x } ) ) ) )
227226biimpar 487 . . . . . . . . . . . 12  |-  ( (
ph  /\  A. x  e.  ran  ( k  e.  ( 0 ... N
)  |->  ( n  e.  ( 1 ... N
)  |->  C ) )  -.  x  e.  ( ( LSpan `  ( (flds  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 `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) ) )
228224, 227sylan2 476 . . . . . . . . . . 11  |-  ( (
ph  /\  ran  ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )  e.  (LIndS `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) )  ->  ran  ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )  e.  (mrInd `  ( LSubSp `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) ) )
229220, 228syl5eqel 2511 . . . . . . . . . 10  |-  ( (
ph  /\  ran  ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )  e.  (LIndS `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) )  ->  ( ran  ( k  e.  ( 0 ... N ) 
|->  ( n  e.  ( 1 ... N ) 
|->  C ) )  u.  (/) )  e.  (mrInd `  ( LSubSp `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) ) )
230 mptfi 7883 . . . . . . . . . . . . 13  |-  ( ( 0 ... N )  e.  Fin  ->  (
k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )  e.  Fin )
231 rnfi 7867 . . . . . . . . . . . . 13  |-  ( ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )  e.  Fin  ->  ran  ( k  e.  ( 0 ... N
)  |->  ( n  e.  ( 1 ... N
)  |->  C ) )  e.  Fin )
23228, 230, 231mp2b 10 . . . . . . . . . . . 12  |-  ran  (
k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )  e.  Fin
233232orci 391 . . . . . . . . . . 11  |-  ( ran  ( k  e.  ( 0 ... N ) 
|->  ( n  e.  ( 1 ... N ) 
|->  C ) )  e. 
Fin  \/  ran  ( (flds  QQ ) unitVec 
( 1 ... N
) )  e.  Fin )
234233a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  ran  ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )  e.  (LIndS `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) )  ->  ( ran  ( k  e.  ( 0 ... N ) 
|->  ( n  e.  ( 1 ... N ) 
|->  C ) )  e. 
Fin  \/  ran  ( (flds  QQ ) unitVec 
( 1 ... N
) )  e.  Fin ) )
235186, 190, 191, 197, 202, 209, 219, 229, 234mreexexd 15554 . . . . . . . . 9  |-  ( (
ph  /\  ran  ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )  e.  (LIndS `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) )  ->  E. v  e.  ~P  ran  ( (flds  QQ ) unitVec 
( 1 ... N
) ) ( ran  ( k  e.  ( 0 ... N ) 
|->  ( n  e.  ( 1 ... N ) 
|->  C ) )  ~~  v  /\  ( v  u.  (/) )  e.  (mrInd `  ( LSubSp `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) ) ) )
236235ex 435 . . . . . . . 8  |-  ( ph  ->  ( ran  ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )  e.  (LIndS `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) )  ->  E. v  e.  ~P  ran  ( (flds  QQ ) unitVec  ( 1 ... N ) ) ( ran  ( k  e.  ( 0 ... N
)  |->  ( n  e.  ( 1 ... N
)  |->  C ) ) 
~~  v  /\  (
v  u.  (/) )  e.  (mrInd `  ( LSubSp `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) ) ) ) )
237 ovex 6334 . . . . . . . . . . . . 13  |-  ( (flds  QQ ) unitVec 
( 1 ... N
) )  e.  _V
238237rnex 6742 . . . . . . . . . . . 12  |-  ran  (
(flds  QQ ) unitVec  ( 1 ... N
) )  e.  _V
239 elpwi 3990 . . . . . . . . . . . 12  |-  ( v  e.  ~P ran  (
(flds  QQ ) unitVec  ( 1 ... N
) )  ->  v  C_ 
ran  ( (flds  QQ ) unitVec  ( 1 ... N ) ) )
240 ssdomg 7626 . . . . . . . . . . . 12  |-  ( ran  ( (flds  QQ ) unitVec  ( 1 ... N ) )  e. 
_V  ->  ( v  C_  ran  ( (flds  QQ ) unitVec  ( 1 ... N ) )  -> 
v  ~<_  ran  ( (flds  QQ ) unitVec  ( 1 ... N ) ) ) )
241238, 239, 240mpsyl 65 . . . . . . . . . . 11  |-  ( v  e.  ~P ran  (
(flds  QQ ) unitVec  ( 1 ... N
) )  ->  v  ~<_  ran  ( (flds  QQ ) unitVec  ( 1 ... N ) ) )
242 endomtr 7638 . . . . . . . . . . . . . 14  |-  ( ( ran  ( k  e.  ( 0 ... N
)  |->  ( n  e.  ( 1 ... N
)  |->  C ) ) 
~~  v  /\  v  ~<_  ran  ( (flds  QQ ) unitVec  ( 1 ... N ) ) )  ->  ran  ( k  e.  ( 0 ... N
)  |->  ( n  e.  ( 1 ... N
)  |->  C ) )  ~<_  ran  ( (flds  QQ ) unitVec  ( 1 ... N ) ) )
243242ancoms 454 . . . . . . . . . . . . 13  |-  ( ( v  ~<_  ran  ( (flds  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  ( (flds  QQ ) unitVec  ( 1 ... N ) ) )
244 f1f1orn 5842 . . . . . . . . . . . . . . . 16  |-  ( ( 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 ) ) )
245 ovex 6334 . . . . . . . . . . . . . . . . 17  |-  ( 0 ... N )  e. 
_V
246245f1oen 7601 . . . . . . . . . . . . . . . 16  |-  ( ( 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 ) ) )
247244, 246syl 17 . . . . . . . . . . . . . . 15  |-  ( ( 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 ) ) )
248 endomtr 7638 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 0 ... N
)  ~~  ran  ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )  /\  ran  (
k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )  ~<_  ran  (
(flds  QQ ) unitVec  ( 1 ... N
) ) )  -> 
( 0 ... N
)  ~<_  ran  ( (flds  QQ ) unitVec  ( 1 ... N ) ) )
249203uvcendim 19404 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( (flds  QQ )  e. NzRing  /\  (
1 ... N )  e. 
Fin )  ->  (
1 ... N )  ~~  ran  ( (flds  QQ ) unitVec  ( 1 ... N ) ) )
250164, 24, 249mp2an 676 . . . . . . . . . . . . . . . . . . 19  |-  ( 1 ... N )  ~~  ran  ( (flds  QQ ) unitVec  ( 1 ... N ) )
251250ensymi 7630 . . . . . . . . . . . . . . . . . 18  |-  ran  (
(flds  QQ ) unitVec  ( 1 ... N
) )  ~~  (
1 ... N )
252 domentr 7639 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 0 ... N
)  ~<_  ran  ( (flds  QQ ) unitVec  ( 1 ... N ) )  /\  ran  (
(flds  QQ ) unitVec  ( 1 ... N
) )  ~~  (
1 ... N ) )  ->  ( 0 ... N )  ~<_  ( 1 ... N ) )
253 hashdom 12565 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 0 ... N
)  e.  Fin  /\  ( 1 ... N
)  e.  Fin )  ->  ( ( # `  (
0 ... N ) )  <_  ( # `  (
1 ... N ) )  <-> 
( 0 ... N
)  ~<_  ( 1 ... N ) ) )
25428, 24, 253mp2an 676 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
# `  ( 0 ... N ) )  <_ 
( # `  ( 1 ... N ) )  <-> 
( 0 ... N
)  ~<_  ( 1 ... N ) )
255 hashfz0 12609 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( N  e.  NN0  ->  ( # `  ( 0 ... N
) )  =  ( N  +  1 ) )
2562, 255syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( # `  (
0 ... N ) )  =  ( N  + 
1 ) )
257 hashfz1 12536 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( N  e.  NN0  ->  ( # `  ( 1 ... N
) )  =  N )
2582, 257syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( # `  (
1 ... N ) )  =  N )
259256, 258breq12d 4436 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( # `  (
0 ... N ) )  <_  ( # `  (
1 ... N ) )  <-> 
( N  +  1 )  <_  N )
)
260254, 259syl5bbr 262 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( 0 ... N )  ~<_  ( 1 ... N )  <->  ( N  +  1 )  <_  N ) )
261252, 260syl5ib 222 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ( 0 ... N )  ~<_  ran  ( (flds  QQ ) unitVec  ( 1 ... N ) )  /\  ran  ( (flds  QQ ) unitVec  ( 1 ... N ) )  ~~  ( 1 ... N
) )  ->  ( N  +  1 )  <_  N ) )
262251, 261mpan2i 681 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( 0 ... N )  ~<_  ran  (
(flds  QQ ) unitVec  ( 1 ... N
) )  ->  ( N  +  1 )  <_  N ) )
263248, 262syl5 33 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( 0 ... N )  ~~  ran  ( k  e.  ( 0 ... N ) 
|->  ( n  e.  ( 1 ... N ) 
|->  C ) )  /\  ran  ( k  e.  ( 0 ... N ) 
|->  ( n  e.  ( 1 ... N ) 
|->  C ) )  ~<_  ran  ( (flds  QQ ) unitVec  ( 1 ... N ) ) )  ->  ( N  + 
1 )  <_  N
) )
264263expd 437 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 0 ... N )  ~~  ran  ( k  e.  ( 0 ... N ) 
|->  ( n  e.  ( 1 ... N ) 
|->  C ) )  -> 
( ran  ( k  e.  ( 0 ... N
)  |->  ( n  e.  ( 1 ... N
)  |->  C ) )  ~<_  ran  ( (flds  QQ ) unitVec  ( 1 ... N ) )  ->  ( N  + 
1 )  <_  N
) ) )
265247, 264syl5 33 . . . . . . . . . . . . . 14  |-  ( 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  ( (flds  QQ ) unitVec  ( 1 ... N ) )  ->  ( N  + 
1 )  <_  N
) ) )
266265com23 81 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ran  ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )  ~<_  ran  ( (flds  QQ ) unitVec  ( 1 ... N ) )  ->  ( (
k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) ) : ( 0 ... N )
-1-1-> _V  ->  ( N  +  1 )  <_  N ) ) )
267243, 266syl5 33 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( v  ~<_  ran  ( (flds  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 ) ) )
268267expdimp 438 . . . . . . . . . . 11  |-  ( (
ph  /\  v  ~<_  ran  (
(flds  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 ) ) )
269241, 268sylan2 476 . . . . . . . . . 10  |-  ( (
ph  /\  v  e.  ~P ran  ( (flds  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 )
) )
270269adantrd 469 . . . . . . . . 9  |-  ( (
ph  /\  v  e.  ~P ran  ( (flds  QQ ) unitVec  ( 1 ... N ) ) )  ->  ( ( ran  ( k  e.  ( 0 ... N ) 
|->  ( n  e.  ( 1 ... N ) 
|->  C ) )  ~~  v  /\  ( v  u.  (/) )  e.  (mrInd `  ( LSubSp `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) ) )  ->  ( ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) ) : ( 0 ... N ) -1-1-> _V  ->  ( N  +  1 )  <_  N )
) )
271270rexlimdva 2914 . . . . . . . 8  |-  ( ph  ->  ( E. v  e. 
~P  ran  ( (flds  QQ ) unitVec  ( 1 ... N ) ) ( ran  (
k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )  ~~  v  /\  ( v  u.  (/) )  e.  (mrInd `  ( LSubSp `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) ) ) )  ->  (
( k  e.  ( 0 ... N ) 
|->  ( n  e.  ( 1 ... N ) 
|->  C ) ) : ( 0 ... N
) -1-1-> _V  ->  ( N  +  1 )  <_  N ) ) )
272236, 271syld 45 . . . . . . 7  |-  ( ph  ->  ( ran  ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )  e.  (LIndS `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) )  ->  ( ( k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) ) : ( 0 ... N ) -1-1-> _V  ->  ( N  +  1 )  <_  N )
) )
273272impd 432 . . . . . 6  |-  ( ph  ->  ( ( ran  (
k  e.  ( 0 ... N )  |->  ( n  e.  ( 1 ... N )  |->  C ) )  e.  (LIndS `  ( (flds  QQ ) freeLMod  ( 1 ... N ) ) )  /\  ( k  e.  ( 0 ... N
)  |->  ( n  e.  ( 1 ... N
)  |->  C ) ) : ( 0 ... N ) -1-1-> _V )  ->  ( N  +  1 )  <_  N )
)
274273ancomsd 455 . . . . 5  |-  ( 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 `  (
(flds  QQ ) freeLMod  ( 1 ... N
) ) ) )  ->  ( N  + 
1 )  <_  N
) )
275182, 274sylbird 238 . . . 4  |-  ( 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 )
)
2769, 275mt3d 128 . . 3  |-  ( 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 )
277 eldifsn 4125 . . . . 5  |-  ( w  e.  ( ( QQ 
^m  ( 0 ... N ) )  \  { ( ( 0 ... N )  X. 
{ 0 } ) } )  <->  ( w  e.  ( QQ  ^m  (
0 ... N ) )  /\  w  =/=  (
( 0 ... N
)  X.  { 0 } ) ) )
27844anim1i 570 . . . . 5  |-  ( ( w  e.  ( QQ 
^m  ( 0 ... N ) )  /\  w  =/=  ( ( 0 ... N )  X. 
{ 0 } ) )  ->  ( w : ( 0 ... N ) --> QQ  /\  w  =/=  ( ( 0 ... N )  X. 
{ 0 } ) ) )
279277, 278sylbi 198 . . . 4  |-  ( w  e.  ( ( QQ 
^m  ( 0 ... N ) )  \  { ( ( 0 ... N )  X. 
{ 0 } ) } )  ->  (
w : ( 0 ... N ) --> QQ 
/\  w  =/=  (
( 0 ... N
)  X.  { 0 } ) ) )
28097a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  ->  QQ  C_  CC )
2812adantr 466 . . . . . . . . 9  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  ->  N  e.  NN0 )
282280, 281, 56elplyd 23155 . . . . . . . 8  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  -> 
( y  e.  CC  |->  sum_ k  e.  ( 0 ... N ) ( ( w `  k
)  x.  ( y ^ k ) ) )  e.  (Poly `  QQ ) )
283282adantrr 721 . . . . . . 7  |-  ( (
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 ) )
284 uzdisj 11875 . . . . . . . . . . . . . . . . . 18  |-  ( ( 0 ... ( ( N  +  1 )  -  1 ) )  i^i  ( ZZ>= `  ( N  +  1 ) ) )  =  (/)
2852nn0cnd 10935 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  N  e.  CC )
286 pncan1 10051 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  CC  ->  (
( N  +  1 )  -  1 )  =  N )
287285, 286syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( N  + 
1 )  -  1 )  =  N )
288287oveq2d 6322 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( 0 ... (
( N  +  1 )  -  1 ) )  =  ( 0 ... N ) )
289288ineq1d 3663 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( 0 ... ( ( N  + 
1 )  -  1 ) )  i^i  ( ZZ>=
`  ( N  + 
1 ) ) )  =  ( ( 0 ... N )  i^i  ( ZZ>= `  ( N  +  1 ) ) ) )
290284, 289syl5eqr 2477 . . . . . . . . . . . . . . . . 17  |-  ( ph  -> 
(/)  =  ( ( 0 ... N )  i^i  ( ZZ>= `  ( N  +  1 ) ) ) )
291290eqcomd 2430 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 0 ... N )  i^i  ( ZZ>=
`  ( N  + 
1 ) ) )  =  (/) )
292134fconst 5786 . . . . . . . . . . . . . . . . . 18  |-  ( (
ZZ>= `  ( N  + 
1 ) )  X. 
{ 0 } ) : ( ZZ>= `  ( N  +  1 ) ) --> { 0 }
293 snssi 4144 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  e.  QQ  ->  { 0 }  C_  QQ )
294101, 102, 293mp2b 10 . . . . . . . . . . . . . . . . . . 19  |-  { 0 }  C_  QQ
295294, 97sstri 3473 . . . . . . . . . . . . . . . . . 18  |-  { 0 }  C_  CC
296 fss 5754 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ZZ>= `  ( N  +  1 ) )  X.  { 0 } ) : (
ZZ>= `  ( N  + 
1 ) ) --> { 0 }  /\  {
0 }  C_  CC )  ->  ( ( ZZ>= `  ( N  +  1
) )  X.  {
0 } ) : ( ZZ>= `  ( N  +  1 ) ) --> CC )
297292, 295, 296mp2an 676 . . . . . . . . . . . . . . . . 17  |-  ( (
ZZ>= `  ( N  + 
1 ) )  X. 
{ 0 } ) : ( ZZ>= `  ( N  +  1 ) ) --> CC
298 fun 5763 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) )
299297, 298mpanl2 685 . . . . . . . . . . . . . . . 16  |-  ( ( 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 ) )
300291, 299sylan2 476 . . . . . . . . . . . . . . 15  |-  ( ( w : ( 0 ... N ) --> QQ 
/\  ph )  ->  (
w  u.  ( (
ZZ>= `  ( N  + 
1 ) )  X. 
{ 0 } ) ) : ( ( 0 ... N )  u.  ( ZZ>= `  ( N  +  1 ) ) ) --> ( QQ  u.  CC ) )
301300ancoms 454 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  w :
( 0 ... N
) --> QQ )  -> 
( w  u.  (
( ZZ>= `  ( N  +  1 ) )  X.  { 0 } ) ) : ( ( 0 ... N
)  u.  ( ZZ>= `  ( N  +  1
) ) ) --> ( QQ  u.  CC ) )
302 nn0uz 11201 . . . . . . . . . . . . . . . . . 18  |-  NN0  =  ( ZZ>= `  0 )
3036, 302syl6eleq 2517 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( N  +  1 )  e.  ( ZZ>= ` 
0 ) )
304 uzsplit 11874 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  +  1 )  e.  ( ZZ>= `  0
)  ->  ( ZZ>= ` 
0 )  =  ( ( 0 ... (
( N  +  1 )  -  1 ) )  u.  ( ZZ>= `  ( N  +  1
) ) ) )
305303, 304syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ZZ>= `  0 )  =  ( ( 0 ... ( ( N  +  1 )  - 
1 ) )  u.  ( ZZ>= `  ( N  +  1 ) ) ) )
306302, 305syl5eq 2475 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  NN0  =  ( ( 0 ... ( ( N  +  1 )  -  1 ) )  u.  ( ZZ>= `  ( N  +  1 ) ) ) )
307288uneq1d 3619 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( 0 ... ( ( N  + 
1 )  -  1 ) )  u.  ( ZZ>=
`  ( N  + 
1 ) ) )  =  ( ( 0 ... N )  u.  ( ZZ>= `  ( N  +  1 ) ) ) )
308306, 307eqtr2d 2464 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 0 ... N )  u.  ( ZZ>=
`  ( N  + 
1 ) ) )  =  NN0 )
309 ssequn1 3636 . . . . . . . . . . . . . . . . . 18  |-  ( QQ  C_  CC  <->  ( QQ  u.  CC )  =  CC )
31097, 309mpbi 211 . . . . . . . . . . . . . . . . 17  |-  ( QQ  u.  CC )  =  CC
311310a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( QQ  u.  CC )  =  CC )
312308, 311feq23d 5741 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( (