MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  islindf4 Structured version   Unicode version

Theorem islindf4 18740
Description: A family is independent iff it has no nontrivial representations of zero. (Contributed by Stefan O'Rear, 28-Feb-2015.)
Hypotheses
Ref Expression
islindf4.b  |-  B  =  ( Base `  W
)
islindf4.r  |-  R  =  (Scalar `  W )
islindf4.t  |-  .x.  =  ( .s `  W )
islindf4.z  |-  .0.  =  ( 0g `  W )
islindf4.y  |-  Y  =  ( 0g `  R
)
islindf4.l  |-  L  =  ( Base `  ( R freeLMod  I ) )
Assertion
Ref Expression
islindf4  |-  ( ( W  e.  LMod  /\  I  e.  X  /\  F :
I --> B )  -> 
( F LIndF  W  <->  A. x  e.  L  ( ( W  gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  x  =  ( I  X.  { Y } ) ) ) )
Distinct variable groups:    x, B    x, F    x, I    x, L    x, R    x,  .x.    x, W    x, X    x, Y    x,  .0.

Proof of Theorem islindf4
Dummy variables  j 
k  l  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 raldifsni 4163 . . . . 5  |-  ( A. l  e.  ( ( Base `  R )  \  { Y } )  -.  ( ( ( invg `  R ) `
 l )  .x.  ( F `  j ) )  e.  ( (
LSpan `  W ) `  ( F " ( I 
\  { j } ) ) )  <->  A. l  e.  ( Base `  R
) ( ( ( ( invg `  R ) `  l
)  .x.  ( F `  j ) )  e.  ( ( LSpan `  W
) `  ( F " ( I  \  {
j } ) ) )  ->  l  =  Y ) )
2 simpll1 1035 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  W  e.  LMod )
3 simprll 761 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  l  e.  ( Base `  R
) )
4 ffvelrn 6030 . . . . . . . . . . . . . . . . . 18  |-  ( ( F : I --> B  /\  j  e.  I )  ->  ( F `  j
)  e.  B )
543ad2antl3 1160 . . . . . . . . . . . . . . . . 17  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  ->  ( F `  j )  e.  B
)
65adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  ( F `  j )  e.  B )
7 islindf4.b . . . . . . . . . . . . . . . . 17  |-  B  =  ( Base `  W
)
8 islindf4.r . . . . . . . . . . . . . . . . 17  |-  R  =  (Scalar `  W )
9 islindf4.t . . . . . . . . . . . . . . . . 17  |-  .x.  =  ( .s `  W )
10 eqid 2467 . . . . . . . . . . . . . . . . 17  |-  ( invg `  W )  =  ( invg `  W )
11 eqid 2467 . . . . . . . . . . . . . . . . 17  |-  ( invg `  R )  =  ( invg `  R )
12 eqid 2467 . . . . . . . . . . . . . . . . 17  |-  ( Base `  R )  =  (
Base `  R )
137, 8, 9, 10, 11, 12lmodvsinv 17551 . . . . . . . . . . . . . . . 16  |-  ( ( W  e.  LMod  /\  l  e.  ( Base `  R
)  /\  ( F `  j )  e.  B
)  ->  ( (
( invg `  R ) `  l
)  .x.  ( F `  j ) )  =  ( ( invg `  W ) `  (
l  .x.  ( F `  j ) ) ) )
142, 3, 6, 13syl3anc 1228 . . . . . . . . . . . . . . 15  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
( ( invg `  R ) `  l
)  .x.  ( F `  j ) )  =  ( ( invg `  W ) `  (
l  .x.  ( F `  j ) ) ) )
1514eqeq1d 2469 . . . . . . . . . . . . . 14  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
( ( ( invg `  R ) `
 l )  .x.  ( F `  j ) )  =  ( W 
gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) )  <->  ( ( invg `  W ) `
 ( l  .x.  ( F `  j ) ) )  =  ( W  gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) ) ) )
16 lmodgrp 17388 . . . . . . . . . . . . . . . 16  |-  ( W  e.  LMod  ->  W  e. 
Grp )
172, 16syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  W  e.  Grp )
187, 8, 9, 12lmodvscl 17398 . . . . . . . . . . . . . . . 16  |-  ( ( W  e.  LMod  /\  l  e.  ( Base `  R
)  /\  ( F `  j )  e.  B
)  ->  ( l  .x.  ( F `  j
) )  e.  B
)
192, 3, 6, 18syl3anc 1228 . . . . . . . . . . . . . . 15  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
l  .x.  ( F `  j ) )  e.  B )
20 islindf4.z . . . . . . . . . . . . . . . 16  |-  .0.  =  ( 0g `  W )
21 lmodcmn 17427 . . . . . . . . . . . . . . . . 17  |-  ( W  e.  LMod  ->  W  e. CMnd
)
222, 21syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  W  e. CMnd )
23 simpll2 1036 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  I  e.  X )
24 difexg 4601 . . . . . . . . . . . . . . . . 17  |-  ( I  e.  X  ->  (
I  \  { j } )  e.  _V )
2523, 24syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
I  \  { j } )  e.  _V )
26 simprlr 762 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )
27 elmapi 7452 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  ( ( Base `  R )  ^m  (
I  \  { j } ) )  -> 
y : ( I 
\  { j } ) --> ( Base `  R
) )
2826, 27syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  y : ( I  \  { j } ) --> ( Base `  R
) )
29 simpll3 1037 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  F : I --> B )
30 difss 3636 . . . . . . . . . . . . . . . . . 18  |-  ( I 
\  { j } )  C_  I
31 fssres 5757 . . . . . . . . . . . . . . . . . 18  |-  ( ( F : I --> B  /\  ( I  \  { j } )  C_  I
)  ->  ( F  |`  ( I  \  {
j } ) ) : ( I  \  { j } ) --> B )
3229, 30, 31sylancl 662 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  ( F  |`  ( I  \  { j } ) ) : ( I 
\  { j } ) --> B )
338, 12, 9, 7, 2, 28, 32, 25lcomf 17417 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
y  oF  .x.  ( F  |`  ( I 
\  { j } ) ) ) : ( I  \  {
j } ) --> B )
34 islindf4.y . . . . . . . . . . . . . . . . 17  |-  Y  =  ( 0g `  R
)
35 simprr 756 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  y finSupp  Y )
368, 12, 9, 7, 2, 28, 32, 25, 20, 34, 35lcomfsupp 17419 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
y  oF  .x.  ( F  |`  ( I 
\  { j } ) ) ) finSupp  .0.  )
377, 20, 22, 25, 33, 36gsumcl 16794 . . . . . . . . . . . . . . 15  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  ( W  gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) )  e.  B )
38 eqid 2467 . . . . . . . . . . . . . . . 16  |-  ( +g  `  W )  =  ( +g  `  W )
397, 38, 20, 10grpinvid2 15970 . . . . . . . . . . . . . . 15  |-  ( ( W  e.  Grp  /\  ( l  .x.  ( F `  j )
)  e.  B  /\  ( W  gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) )  e.  B )  ->  ( ( ( invg `  W
) `  ( l  .x.  ( F `  j
) ) )  =  ( W  gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) )  <->  ( ( W 
gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) ) ( +g  `  W
) ( l  .x.  ( F `  j ) ) )  =  .0.  ) )
4017, 19, 37, 39syl3anc 1228 . . . . . . . . . . . . . 14  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
( ( invg `  W ) `  (
l  .x.  ( F `  j ) ) )  =  ( W  gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) )  <->  ( ( W  gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) ) ( +g  `  W
) ( l  .x.  ( F `  j ) ) )  =  .0.  ) )
41 simplr 754 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  j  e.  I )
42 fsnunf2 6111 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y : ( I 
\  { j } ) --> ( Base `  R
)  /\  j  e.  I  /\  l  e.  (
Base `  R )
)  ->  ( y  u.  { <. j ,  l
>. } ) : I --> ( Base `  R
) )
4328, 41, 3, 42syl3anc 1228 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
y  u.  { <. j ,  l >. } ) : I --> ( Base `  R ) )
448, 12, 9, 7, 2, 43, 29, 23lcomf 17417 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
( y  u.  { <. j ,  l >. } )  oF  .x.  F ) : I --> B )
45 simpr 461 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  ->  j  e.  I )
46 simpl 457 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  ->  l  e.  ( Base `  R
) )
4745, 46anim12i 566 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( l  e.  ( Base `  R
)  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) ) )  -> 
( j  e.  I  /\  l  e.  ( Base `  R ) ) )
48 elmapfun 7454 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  ( ( Base `  R )  ^m  (
I  \  { j } ) )  ->  Fun  y )
49 fdm 5741 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y : ( I  \  { j } ) --> ( Base `  R
)  ->  dom  y  =  ( I  \  {
j } ) )
50 neldifsnd 4161 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( dom  y  =  ( I 
\  { j } )  ->  -.  j  e.  ( I  \  {
j } ) )
51 df-nel 2665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( j  e/  dom  y  <->  -.  j  e.  dom  y )
52 eleq2 2540 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( dom  y  =  ( I 
\  { j } )  ->  ( j  e.  dom  y  <->  j  e.  ( I  \  { j } ) ) )
5352notbid 294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( dom  y  =  ( I 
\  { j } )  ->  ( -.  j  e.  dom  y  <->  -.  j  e.  ( I  \  {
j } ) ) )
5451, 53syl5bb 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( dom  y  =  ( I 
\  { j } )  ->  ( j  e/  dom  y  <->  -.  j  e.  ( I  \  {
j } ) ) )
5550, 54mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( dom  y  =  ( I 
\  { j } )  ->  j  e/  dom  y )
5649, 55syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y : ( I  \  { j } ) --> ( Base `  R
)  ->  j  e/  dom  y )
5727, 56syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  ( ( Base `  R )  ^m  (
I  \  { j } ) )  -> 
j  e/  dom  y )
5848, 57jca 532 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  ( ( Base `  R )  ^m  (
I  \  { j } ) )  -> 
( Fun  y  /\  j  e/  dom  y ) )
5958adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  ->  ( Fun  y  /\  j  e/  dom  y ) )
6059adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( l  e.  ( Base `  R
)  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) ) )  -> 
( Fun  y  /\  j  e/  dom  y ) )
6147, 60jca 532 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( l  e.  ( Base `  R
)  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) ) )  -> 
( ( j  e.  I  /\  l  e.  ( Base `  R
) )  /\  ( Fun  y  /\  j  e/  dom  y ) ) )
62 funsnfsupp 7865 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( j  e.  I  /\  l  e.  ( Base `  R ) )  /\  ( Fun  y  /\  j  e/  dom  y
) )  ->  (
( y  u.  { <. j ,  l >. } ) finSupp  Y  <->  y finSupp  Y ) )
6362bicomd 201 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( j  e.  I  /\  l  e.  ( Base `  R ) )  /\  ( Fun  y  /\  j  e/  dom  y
) )  ->  (
y finSupp  Y  <->  ( y  u. 
{ <. j ,  l
>. } ) finSupp  Y ) )
6461, 63syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( l  e.  ( Base `  R
)  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) ) )  -> 
( y finSupp  Y  <->  ( y  u.  { <. j ,  l
>. } ) finSupp  Y ) )
6564biimpd 207 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( l  e.  ( Base `  R
)  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) ) )  -> 
( y finSupp  Y  ->  ( y  u.  { <. j ,  l >. } ) finSupp  Y ) )
6665impr 619 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
y  u.  { <. j ,  l >. } ) finSupp  Y )
678, 12, 9, 7, 2, 43, 29, 23, 20, 34, 66lcomfsupp 17419 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
( y  u.  { <. j ,  l >. } )  oF  .x.  F ) finSupp  .0.  )
68 incom 3696 . . . . . . . . . . . . . . . . . . 19  |-  ( ( I  \  { j } )  i^i  {
j } )  =  ( { j }  i^i  ( I  \  { j } ) )
69 disjdif 3905 . . . . . . . . . . . . . . . . . . 19  |-  ( { j }  i^i  (
I  \  { j } ) )  =  (/)
7068, 69eqtri 2496 . . . . . . . . . . . . . . . . . 18  |-  ( ( I  \  { j } )  i^i  {
j } )  =  (/)
7170a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
( I  \  {
j } )  i^i 
{ j } )  =  (/) )
72 difsnid 4179 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  I  ->  (
( I  \  {
j } )  u. 
{ j } )  =  I )
7372eqcomd 2475 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  I  ->  I  =  ( ( I 
\  { j } )  u.  { j } ) )
7441, 73syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  I  =  ( ( I 
\  { j } )  u.  { j } ) )
757, 20, 38, 22, 23, 44, 67, 71, 74gsumsplit 16817 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  ( W  gsumg  ( ( y  u. 
{ <. j ,  l
>. } )  oF  .x.  F ) )  =  ( ( W 
gsumg  ( ( ( y  u.  { <. j ,  l >. } )  oF  .x.  F
)  |`  ( I  \  { j } ) ) ) ( +g  `  W ) ( W 
gsumg  ( ( ( y  u.  { <. j ,  l >. } )  oF  .x.  F
)  |`  { j } ) ) ) )
76 vex 3121 . . . . . . . . . . . . . . . . . . . . 21  |-  y  e. 
_V
77 snex 4694 . . . . . . . . . . . . . . . . . . . . 21  |-  { <. j ,  l >. }  e.  _V
7876, 77unex 6593 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  u.  { <. j ,  l >. } )  e.  _V
79 simpl3 1001 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  ->  F :
I --> B )
80 simpl2 1000 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  ->  I  e.  X )
81 fex 6144 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F : I --> B  /\  I  e.  X )  ->  F  e.  _V )
8279, 80, 81syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  ->  F  e.  _V )
8382adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  F  e.  _V )
84 offres 6790 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( y  u.  { <. j ,  l >. } )  e.  _V  /\  F  e.  _V )  ->  ( ( ( y  u.  { <. j ,  l >. } )  oF  .x.  F
)  |`  ( I  \  { j } ) )  =  ( ( ( y  u.  { <. j ,  l >. } )  |`  (
I  \  { j } ) )  oF  .x.  ( F  |`  ( I  \  {
j } ) ) ) )
8578, 83, 84sylancr 663 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
( ( y  u. 
{ <. j ,  l
>. } )  oF  .x.  F )  |`  ( I  \  { j } ) )  =  ( ( ( y  u.  { <. j ,  l >. } )  |`  ( I  \  {
j } ) )  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) )
86 ffn 5737 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y : ( I  \  { j } ) --> ( Base `  R
)  ->  y  Fn  ( I  \  { j } ) )
8728, 86syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  y  Fn  ( I  \  {
j } ) )
88 neldifsn 4160 . . . . . . . . . . . . . . . . . . . . 21  |-  -.  j  e.  ( I  \  {
j } )
89 fsnunres 6113 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  Fn  ( I 
\  { j } )  /\  -.  j  e.  ( I  \  {
j } ) )  ->  ( ( y  u.  { <. j ,  l >. } )  |`  ( I  \  {
j } ) )  =  y )
9087, 88, 89sylancl 662 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
( y  u.  { <. j ,  l >. } )  |`  (
I  \  { j } ) )  =  y )
9190oveq1d 6310 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
( ( y  u. 
{ <. j ,  l
>. } )  |`  (
I  \  { j } ) )  oF  .x.  ( F  |`  ( I  \  {
j } ) ) )  =  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) )
9285, 91eqtrd 2508 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
( ( y  u. 
{ <. j ,  l
>. } )  oF  .x.  F )  |`  ( I  \  { j } ) )  =  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) )
9392oveq2d 6311 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  ( W  gsumg  ( ( ( y  u.  { <. j ,  l >. } )  oF  .x.  F
)  |`  ( I  \  { j } ) ) )  =  ( W  gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) ) )
94 ffn 5737 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( y  u.  { <. j ,  l >. } )  oF  .x.  F ) : I --> B  ->  (
( y  u.  { <. j ,  l >. } )  oF  .x.  F )  Fn  I )
9544, 94syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
( y  u.  { <. j ,  l >. } )  oF  .x.  F )  Fn  I )
96 fnressn 6084 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( y  u. 
{ <. j ,  l
>. } )  oF  .x.  F )  Fn  I  /\  j  e.  I )  ->  (
( ( y  u. 
{ <. j ,  l
>. } )  oF  .x.  F )  |`  { j } )  =  { <. j ,  ( ( ( y  u.  { <. j ,  l >. } )  oF  .x.  F
) `  j ) >. } )
9795, 41, 96syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
( ( y  u. 
{ <. j ,  l
>. } )  oF  .x.  F )  |`  { j } )  =  { <. j ,  ( ( ( y  u.  { <. j ,  l >. } )  oF  .x.  F
) `  j ) >. } )
98 ffn 5737 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( y  u.  { <. j ,  l >. } ) : I --> ( Base `  R )  ->  (
y  u.  { <. j ,  l >. } )  Fn  I )
9943, 98syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
y  u.  { <. j ,  l >. } )  Fn  I )
100 ffn 5737 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( F : I --> B  ->  F  Fn  I )
10129, 100syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  F  Fn  I )
102 fnfvof 6548 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( y  u. 
{ <. j ,  l
>. } )  Fn  I  /\  F  Fn  I
)  /\  ( I  e.  X  /\  j  e.  I ) )  -> 
( ( ( y  u.  { <. j ,  l >. } )  oF  .x.  F
) `  j )  =  ( ( ( y  u.  { <. j ,  l >. } ) `
 j )  .x.  ( F `  j ) ) )
10399, 101, 23, 41, 102syl22anc 1229 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
( ( y  u. 
{ <. j ,  l
>. } )  oF  .x.  F ) `  j )  =  ( ( ( y  u. 
{ <. j ,  l
>. } ) `  j
)  .x.  ( F `  j ) ) )
104 fndm 5686 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  Fn  ( I  \  { j } )  ->  dom  y  =  ( I  \  { j } ) )
105104eleq2d 2537 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  Fn  ( I  \  { j } )  ->  ( j  e. 
dom  y  <->  j  e.  ( I  \  { j } ) ) )
10688, 105mtbiri 303 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  Fn  ( I  \  { j } )  ->  -.  j  e.  dom  y )
107 vex 3121 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  j  e. 
_V
108 vex 3121 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  l  e. 
_V
109 fsnunfv 6112 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( j  e.  _V  /\  l  e.  _V  /\  -.  j  e.  dom  y )  ->  ( ( y  u.  { <. j ,  l >. } ) `
 j )  =  l )
110107, 108, 109mp3an12 1314 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( -.  j  e.  dom  y  ->  ( ( y  u. 
{ <. j ,  l
>. } ) `  j
)  =  l )
11187, 106, 1103syl 20 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
( y  u.  { <. j ,  l >. } ) `  j
)  =  l )
112111oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
( ( y  u. 
{ <. j ,  l
>. } ) `  j
)  .x.  ( F `  j ) )  =  ( l  .x.  ( F `  j )
) )
113103, 112eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
( ( y  u. 
{ <. j ,  l
>. } )  oF  .x.  F ) `  j )  =  ( l  .x.  ( F `
 j ) ) )
114113opeq2d 4226 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  <. j ,  ( ( ( y  u.  { <. j ,  l >. } )  oF  .x.  F
) `  j ) >.  =  <. j ,  ( l  .x.  ( F `
 j ) )
>. )
115114sneqd 4045 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  { <. j ,  ( ( ( y  u.  { <. j ,  l >. } )  oF  .x.  F
) `  j ) >. }  =  { <. j ,  ( l  .x.  ( F `  j ) ) >. } )
116 ovex 6320 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( l 
.x.  ( F `  j ) )  e. 
_V
117 fmptsn 6092 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( j  e.  _V  /\  ( l  .x.  ( F `  j )
)  e.  _V )  ->  { <. j ,  ( l  .x.  ( F `
 j ) )
>. }  =  ( x  e.  { j } 
|->  ( l  .x.  ( F `  j )
) ) )
118107, 116, 117mp2an 672 . . . . . . . . . . . . . . . . . . . . 21  |-  { <. j ,  ( l  .x.  ( F `  j ) ) >. }  =  ( x  e.  { j }  |->  ( l  .x.  ( F `  j ) ) )
119118a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  { <. j ,  ( l  .x.  ( F `  j ) ) >. }  =  ( x  e.  { j }  |->  ( l  .x.  ( F `  j ) ) ) )
12097, 115, 1193eqtrd 2512 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
( ( y  u. 
{ <. j ,  l
>. } )  oF  .x.  F )  |`  { j } )  =  ( x  e. 
{ j }  |->  ( l  .x.  ( F `
 j ) ) ) )
121120oveq2d 6311 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  ( W  gsumg  ( ( ( y  u.  { <. j ,  l >. } )  oF  .x.  F
)  |`  { j } ) )  =  ( W  gsumg  ( x  e.  {
j }  |->  ( l 
.x.  ( F `  j ) ) ) ) )
122 cmnmnd 16684 . . . . . . . . . . . . . . . . . . . 20  |-  ( W  e. CMnd  ->  W  e.  Mnd )
12322, 122syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  W  e.  Mnd )
124107a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  j  e.  _V )
125 eqidd 2468 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  j  ->  (
l  .x.  ( F `  j ) )  =  ( l  .x.  ( F `  j )
) )
1267, 125gsumsn 16852 . . . . . . . . . . . . . . . . . . 19  |-  ( ( W  e.  Mnd  /\  j  e.  _V  /\  (
l  .x.  ( F `  j ) )  e.  B )  ->  ( W  gsumg  ( x  e.  {
j }  |->  ( l 
.x.  ( F `  j ) ) ) )  =  ( l 
.x.  ( F `  j ) ) )
127123, 124, 19, 126syl3anc 1228 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  ( W  gsumg  ( x  e.  {
j }  |->  ( l 
.x.  ( F `  j ) ) ) )  =  ( l 
.x.  ( F `  j ) ) )
128121, 127eqtrd 2508 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  ( W  gsumg  ( ( ( y  u.  { <. j ,  l >. } )  oF  .x.  F
)  |`  { j } ) )  =  ( l  .x.  ( F `
 j ) ) )
12993, 128oveq12d 6313 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
( W  gsumg  ( ( ( y  u.  { <. j ,  l >. } )  oF  .x.  F
)  |`  ( I  \  { j } ) ) ) ( +g  `  W ) ( W 
gsumg  ( ( ( y  u.  { <. j ,  l >. } )  oF  .x.  F
)  |`  { j } ) ) )  =  ( ( W  gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) ) ( +g  `  W ) ( l  .x.  ( F `  j )
) ) )
13075, 129eqtr2d 2509 . . . . . . . . . . . . . . 15  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
( W  gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) ) ( +g  `  W
) ( l  .x.  ( F `  j ) ) )  =  ( W  gsumg  ( ( y  u. 
{ <. j ,  l
>. } )  oF  .x.  F ) ) )
131130eqeq1d 2469 . . . . . . . . . . . . . 14  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
( ( W  gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) ) ( +g  `  W ) ( l  .x.  ( F `  j )
) )  =  .0.  <->  ( W  gsumg  ( ( y  u. 
{ <. j ,  l
>. } )  oF  .x.  F ) )  =  .0.  ) )
13215, 40, 1313bitrd 279 . . . . . . . . . . . . 13  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
( ( ( invg `  R ) `
 l )  .x.  ( F `  j ) )  =  ( W 
gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) )  <->  ( W  gsumg  ( ( y  u.  { <. j ,  l >. } )  oF  .x.  F
) )  =  .0.  ) )
133111eqcomd 2475 . . . . . . . . . . . . . 14  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  l  =  ( ( y  u.  { <. j ,  l >. } ) `
 j ) )
134133eqeq1d 2469 . . . . . . . . . . . . 13  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
l  =  Y  <->  ( (
y  u.  { <. j ,  l >. } ) `
 j )  =  Y ) )
135132, 134imbi12d 320 . . . . . . . . . . . 12  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( (
l  e.  ( Base `  R )  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) )  /\  y finSupp  Y ) )  ->  (
( ( ( ( invg `  R
) `  l )  .x.  ( F `  j
) )  =  ( W  gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) )  ->  l  =  Y )  <->  ( ( W  gsumg  ( ( y  u. 
{ <. j ,  l
>. } )  oF  .x.  F ) )  =  .0.  ->  (
( y  u.  { <. j ,  l >. } ) `  j
)  =  Y ) ) )
136135anassrs 648 . . . . . . . . . . 11  |-  ( ( ( ( ( W  e.  LMod  /\  I  e.  X  /\  F :
I --> B )  /\  j  e.  I )  /\  ( l  e.  (
Base `  R )  /\  y  e.  (
( Base `  R )  ^m  ( I  \  {
j } ) ) ) )  /\  y finSupp  Y )  ->  ( (
( ( ( invg `  R ) `
 l )  .x.  ( F `  j ) )  =  ( W 
gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) )  ->  l  =  Y )  <->  ( ( W  gsumg  ( ( y  u. 
{ <. j ,  l
>. } )  oF  .x.  F ) )  =  .0.  ->  (
( y  u.  { <. j ,  l >. } ) `  j
)  =  Y ) ) )
137136pm5.74da 687 . . . . . . . . . 10  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( l  e.  ( Base `  R
)  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) ) )  -> 
( ( y finSupp  Y  ->  ( ( ( ( invg `  R
) `  l )  .x.  ( F `  j
) )  =  ( W  gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) )  ->  l  =  Y ) )  <->  ( y finSupp  Y  ->  ( ( W 
gsumg  ( ( y  u. 
{ <. j ,  l
>. } )  oF  .x.  F ) )  =  .0.  ->  (
( y  u.  { <. j ,  l >. } ) `  j
)  =  Y ) ) ) )
138 impexp 446 . . . . . . . . . . 11  |-  ( ( ( y finSupp  Y  /\  ( ( ( invg `  R ) `
 l )  .x.  ( F `  j ) )  =  ( W 
gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) ) )  ->  l  =  Y )  <->  ( y finSupp  Y  ->  ( ( ( ( invg `  R ) `  l
)  .x.  ( F `  j ) )  =  ( W  gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) )  ->  l  =  Y ) ) )
139138a1i 11 . . . . . . . . . 10  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( l  e.  ( Base `  R
)  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) ) )  -> 
( ( ( y finSupp  Y  /\  ( ( ( invg `  R
) `  l )  .x.  ( F `  j
) )  =  ( W  gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) ) )  ->  l  =  Y )  <->  ( y finSupp  Y  ->  ( ( ( ( invg `  R ) `  l
)  .x.  ( F `  j ) )  =  ( W  gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) )  ->  l  =  Y ) ) ) )
14064bicomd 201 . . . . . . . . . . 11  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( l  e.  ( Base `  R
)  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) ) )  -> 
( ( y  u. 
{ <. j ,  l
>. } ) finSupp  Y  <->  y finSupp  Y ) )
141140imbi1d 317 . . . . . . . . . 10  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( l  e.  ( Base `  R
)  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) ) )  -> 
( ( ( y  u.  { <. j ,  l >. } ) finSupp  Y  ->  ( ( W 
gsumg  ( ( y  u. 
{ <. j ,  l
>. } )  oF  .x.  F ) )  =  .0.  ->  (
( y  u.  { <. j ,  l >. } ) `  j
)  =  Y ) )  <->  ( y finSupp  Y  ->  ( ( W  gsumg  ( ( y  u.  { <. j ,  l >. } )  oF  .x.  F
) )  =  .0. 
->  ( ( y  u. 
{ <. j ,  l
>. } ) `  j
)  =  Y ) ) ) )
142137, 139, 1413bitr4d 285 . . . . . . . . 9  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  ( l  e.  ( Base `  R
)  /\  y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) ) )  -> 
( ( ( y finSupp  Y  /\  ( ( ( invg `  R
) `  l )  .x.  ( F `  j
) )  =  ( W  gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) ) )  ->  l  =  Y )  <->  ( (
y  u.  { <. j ,  l >. } ) finSupp  Y  ->  ( ( W 
gsumg  ( ( y  u. 
{ <. j ,  l
>. } )  oF  .x.  F ) )  =  .0.  ->  (
( y  u.  { <. j ,  l >. } ) `  j
)  =  Y ) ) ) )
1431422ralbidva 2909 . . . . . . . 8  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  ->  ( A. l  e.  ( Base `  R ) A. y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) ( ( y finSupp  Y  /\  ( ( ( invg `  R
) `  l )  .x.  ( F `  j
) )  =  ( W  gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) ) )  ->  l  =  Y )  <->  A. l  e.  ( Base `  R
) A. y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) ( ( y  u.  { <. j ,  l >. } ) finSupp  Y  ->  ( ( W 
gsumg  ( ( y  u. 
{ <. j ,  l
>. } )  oF  .x.  F ) )  =  .0.  ->  (
( y  u.  { <. j ,  l >. } ) `  j
)  =  Y ) ) ) )
144 breq1 4456 . . . . . . . . . . 11  |-  ( x  =  ( y  u. 
{ <. j ,  l
>. } )  ->  (
x finSupp  Y  <->  ( y  u. 
{ <. j ,  l
>. } ) finSupp  Y ) )
145 oveq1 6302 . . . . . . . . . . . . . 14  |-  ( x  =  ( y  u. 
{ <. j ,  l
>. } )  ->  (
x  oF  .x.  F )  =  ( ( y  u.  { <. j ,  l >. } )  oF  .x.  F ) )
146145oveq2d 6311 . . . . . . . . . . . . 13  |-  ( x  =  ( y  u. 
{ <. j ,  l
>. } )  ->  ( W  gsumg  ( x  oF  .x.  F ) )  =  ( W  gsumg  ( ( y  u.  { <. j ,  l >. } )  oF  .x.  F
) ) )
147146eqeq1d 2469 . . . . . . . . . . . 12  |-  ( x  =  ( y  u. 
{ <. j ,  l
>. } )  ->  (
( W  gsumg  ( x  oF  .x.  F ) )  =  .0.  <->  ( W  gsumg  ( ( y  u.  { <. j ,  l >. } )  oF  .x.  F ) )  =  .0.  ) )
148 fveq1 5871 . . . . . . . . . . . . 13  |-  ( x  =  ( y  u. 
{ <. j ,  l
>. } )  ->  (
x `  j )  =  ( ( y  u.  { <. j ,  l >. } ) `
 j ) )
149148eqeq1d 2469 . . . . . . . . . . . 12  |-  ( x  =  ( y  u. 
{ <. j ,  l
>. } )  ->  (
( x `  j
)  =  Y  <->  ( (
y  u.  { <. j ,  l >. } ) `
 j )  =  Y ) )
150147, 149imbi12d 320 . . . . . . . . . . 11  |-  ( x  =  ( y  u. 
{ <. j ,  l
>. } )  ->  (
( ( W  gsumg  ( x  oF  .x.  F
) )  =  .0. 
->  ( x `  j
)  =  Y )  <-> 
( ( W  gsumg  ( ( y  u.  { <. j ,  l >. } )  oF  .x.  F
) )  =  .0. 
->  ( ( y  u. 
{ <. j ,  l
>. } ) `  j
)  =  Y ) ) )
151144, 150imbi12d 320 . . . . . . . . . 10  |-  ( x  =  ( y  u. 
{ <. j ,  l
>. } )  ->  (
( x finSupp  Y  ->  ( ( W  gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  (
x `  j )  =  Y ) )  <->  ( (
y  u.  { <. j ,  l >. } ) finSupp  Y  ->  ( ( W 
gsumg  ( ( y  u. 
{ <. j ,  l
>. } )  oF  .x.  F ) )  =  .0.  ->  (
( y  u.  { <. j ,  l >. } ) `  j
)  =  Y ) ) ) )
152151ralxpmap 7480 . . . . . . . . 9  |-  ( j  e.  I  ->  ( A. x  e.  (
( Base `  R )  ^m  I ) ( x finSupp  Y  ->  ( ( W 
gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  ( x `  j )  =  Y ) )  <->  A. l  e.  ( Base `  R
) A. y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) ( ( y  u.  { <. j ,  l >. } ) finSupp  Y  ->  ( ( W 
gsumg  ( ( y  u. 
{ <. j ,  l
>. } )  oF  .x.  F ) )  =  .0.  ->  (
( y  u.  { <. j ,  l >. } ) `  j
)  =  Y ) ) ) )
153152adantl 466 . . . . . . . 8  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  ->  ( A. x  e.  ( ( Base `  R )  ^m  I ) ( x finSupp  Y  ->  ( ( W 
gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  ( x `  j )  =  Y ) )  <->  A. l  e.  ( Base `  R
) A. y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) ( ( y  u.  { <. j ,  l >. } ) finSupp  Y  ->  ( ( W 
gsumg  ( ( y  u. 
{ <. j ,  l
>. } )  oF  .x.  F ) )  =  .0.  ->  (
( y  u.  { <. j ,  l >. } ) `  j
)  =  Y ) ) ) )
154143, 153bitr4d 256 . . . . . . 7  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  ->  ( A. l  e.  ( Base `  R ) A. y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) ( ( y finSupp  Y  /\  ( ( ( invg `  R
) `  l )  .x.  ( F `  j
) )  =  ( W  gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) ) )  ->  l  =  Y )  <->  A. x  e.  ( ( Base `  R
)  ^m  I )
( x finSupp  Y  ->  ( ( W  gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  (
x `  j )  =  Y ) ) ) )
155 breq1 4456 . . . . . . . 8  |-  ( z  =  x  ->  (
z finSupp  Y  <->  x finSupp  Y ) )
156155ralrab 3270 . . . . . . 7  |-  ( A. x  e.  { z  e.  ( ( Base `  R
)  ^m  I )  |  z finSupp  Y }  (
( W  gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  (
x `  j )  =  Y )  <->  A. x  e.  ( ( Base `  R
)  ^m  I )
( x finSupp  Y  ->  ( ( W  gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  (
x `  j )  =  Y ) ) )
157154, 156syl6bbr 263 . . . . . 6  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  ->  ( A. l  e.  ( Base `  R ) A. y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) ( ( y finSupp  Y  /\  ( ( ( invg `  R
) `  l )  .x.  ( F `  j
) )  =  ( W  gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) ) )  ->  l  =  Y )  <->  A. x  e.  { z  e.  ( ( Base `  R
)  ^m  I )  |  z finSupp  Y }  (
( W  gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  (
x `  j )  =  Y ) ) )
158 resima 5312 . . . . . . . . . . . . 13  |-  ( ( F  |`  ( I  \  { j } ) ) " ( I 
\  { j } ) )  =  ( F " ( I 
\  { j } ) )
159158eqcomi 2480 . . . . . . . . . . . 12  |-  ( F
" ( I  \  { j } ) )  =  ( ( F  |`  ( I  \  { j } ) ) " ( I 
\  { j } ) )
160159fveq2i 5875 . . . . . . . . . . 11  |-  ( (
LSpan `  W ) `  ( F " ( I 
\  { j } ) ) )  =  ( ( LSpan `  W
) `  ( ( F  |`  ( I  \  { j } ) ) " ( I 
\  { j } ) ) )
161160eleq2i 2545 . . . . . . . . . 10  |-  ( ( ( ( invg `  R ) `  l
)  .x.  ( F `  j ) )  e.  ( ( LSpan `  W
) `  ( F " ( I  \  {
j } ) ) )  <->  ( ( ( invg `  R
) `  l )  .x.  ( F `  j
) )  e.  ( ( LSpan `  W ) `  ( ( F  |`  ( I  \  { j } ) ) "
( I  \  {
j } ) ) ) )
162 eqid 2467 . . . . . . . . . . 11  |-  ( LSpan `  W )  =  (
LSpan `  W )
16379, 30, 31sylancl 662 . . . . . . . . . . 11  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  ->  ( F  |`  ( I  \  {
j } ) ) : ( I  \  { j } ) --> B )
164 simpl1 999 . . . . . . . . . . 11  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  ->  W  e.  LMod )
165243ad2ant2 1018 . . . . . . . . . . . 12  |-  ( ( W  e.  LMod  /\  I  e.  X  /\  F :
I --> B )  -> 
( I  \  {
j } )  e. 
_V )
166165adantr 465 . . . . . . . . . . 11  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  ->  ( I  \  { j } )  e.  _V )
167162, 7, 12, 8, 34, 9, 163, 164, 166ellspd 18703 . . . . . . . . . 10  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  ->  ( (
( ( invg `  R ) `  l
)  .x.  ( F `  j ) )  e.  ( ( LSpan `  W
) `  ( ( F  |`  ( I  \  { j } ) ) " ( I 
\  { j } ) ) )  <->  E. y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) ( y finSupp  Y  /\  ( ( ( invg `  R ) `
 l )  .x.  ( F `  j ) )  =  ( W 
gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) ) ) ) )
168161, 167syl5bb 257 . . . . . . . . 9  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  ->  ( (
( ( invg `  R ) `  l
)  .x.  ( F `  j ) )  e.  ( ( LSpan `  W
) `  ( F " ( I  \  {
j } ) ) )  <->  E. y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) ( y finSupp  Y  /\  ( ( ( invg `  R ) `
 l )  .x.  ( F `  j ) )  =  ( W 
gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) ) ) ) )
169168imbi1d 317 . . . . . . . 8  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  ->  ( (
( ( ( invg `  R ) `
 l )  .x.  ( F `  j ) )  e.  ( (
LSpan `  W ) `  ( F " ( I 
\  { j } ) ) )  -> 
l  =  Y )  <-> 
( E. y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) ( y finSupp  Y  /\  ( ( ( invg `  R ) `
 l )  .x.  ( F `  j ) )  =  ( W 
gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) ) )  ->  l  =  Y ) ) )
170 r19.23v 2947 . . . . . . . 8  |-  ( A. y  e.  ( ( Base `  R )  ^m  ( I  \  { j } ) ) ( ( y finSupp  Y  /\  ( ( ( invg `  R ) `
 l )  .x.  ( F `  j ) )  =  ( W 
gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) ) )  ->  l  =  Y )  <->  ( E. y  e.  ( ( Base `  R )  ^m  ( I  \  { j } ) ) ( y finSupp  Y  /\  (
( ( invg `  R ) `  l
)  .x.  ( F `  j ) )  =  ( W  gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) ) )  ->  l  =  Y ) )
171169, 170syl6bbr 263 . . . . . . 7  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  ->  ( (
( ( ( invg `  R ) `
 l )  .x.  ( F `  j ) )  e.  ( (
LSpan `  W ) `  ( F " ( I 
\  { j } ) ) )  -> 
l  =  Y )  <->  A. y  e.  (
( Base `  R )  ^m  ( I  \  {
j } ) ) ( ( y finSupp  Y  /\  ( ( ( invg `  R ) `
 l )  .x.  ( F `  j ) )  =  ( W 
gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) ) )  ->  l  =  Y ) ) )
172171ralbidv 2906 . . . . . 6  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  ->  ( A. l  e.  ( Base `  R ) ( ( ( ( invg `  R ) `  l
)  .x.  ( F `  j ) )  e.  ( ( LSpan `  W
) `  ( F " ( I  \  {
j } ) ) )  ->  l  =  Y )  <->  A. l  e.  ( Base `  R
) A. y  e.  ( ( Base `  R
)  ^m  ( I  \  { j } ) ) ( ( y finSupp  Y  /\  ( ( ( invg `  R
) `  l )  .x.  ( F `  j
) )  =  ( W  gsumg  ( y  oF  .x.  ( F  |`  ( I  \  { j } ) ) ) ) )  ->  l  =  Y ) ) )
173 fvex 5882 . . . . . . . . . . . 12  |-  (Scalar `  W )  e.  _V
1748, 173eqeltri 2551 . . . . . . . . . . 11  |-  R  e. 
_V
175 eqid 2467 . . . . . . . . . . . 12  |-  ( R freeLMod  I )  =  ( R freeLMod  I )
176 eqid 2467 . . . . . . . . . . . 12  |-  { z  e.  ( ( Base `  R )  ^m  I
)  |  z finSupp  Y }  =  { z  e.  ( ( Base `  R
)  ^m  I )  |  z finSupp  Y }
177175, 12, 34, 176frlmbas 18653 . . . . . . . . . . 11  |-  ( ( R  e.  _V  /\  I  e.  X )  ->  { z  e.  ( ( Base `  R
)  ^m  I )  |  z finSupp  Y }  =  ( Base `  ( R freeLMod  I ) ) )
178174, 177mpan 670 . . . . . . . . . 10  |-  ( I  e.  X  ->  { z  e.  ( ( Base `  R )  ^m  I
)  |  z finSupp  Y }  =  ( Base `  ( R freeLMod  I )
) )
1791783ad2ant2 1018 . . . . . . . . 9  |-  ( ( W  e.  LMod  /\  I  e.  X  /\  F :
I --> B )  ->  { z  e.  ( ( Base `  R
)  ^m  I )  |  z finSupp  Y }  =  ( Base `  ( R freeLMod  I ) ) )
180179adantr 465 . . . . . . . 8  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  ->  { z  e.  ( ( Base `  R
)  ^m  I )  |  z finSupp  Y }  =  ( Base `  ( R freeLMod  I ) ) )
181 islindf4.l . . . . . . . 8  |-  L  =  ( Base `  ( R freeLMod  I ) )
182180, 181syl6reqr 2527 . . . . . . 7  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  ->  L  =  { z  e.  ( ( Base `  R
)  ^m  I )  |  z finSupp  Y } )
183182raleqdv 3069 . . . . . 6  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  ->  ( A. x  e.  L  (
( W  gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  (
x `  j )  =  Y )  <->  A. x  e.  { z  e.  ( ( Base `  R
)  ^m  I )  |  z finSupp  Y }  (
( W  gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  (
x `  j )  =  Y ) ) )
184157, 172, 1833bitr4d 285 . . . . 5  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  ->  ( A. l  e.  ( Base `  R ) ( ( ( ( invg `  R ) `  l
)  .x.  ( F `  j ) )  e.  ( ( LSpan `  W
) `  ( F " ( I  \  {
j } ) ) )  ->  l  =  Y )  <->  A. x  e.  L  ( ( W  gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  (
x `  j )  =  Y ) ) )
1851, 184syl5bb 257 . . . 4  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  ->  ( A. l  e.  ( ( Base `  R )  \  { Y } )  -.  ( ( ( invg `  R ) `
 l )  .x.  ( F `  j ) )  e.  ( (
LSpan `  W ) `  ( F " ( I 
\  { j } ) ) )  <->  A. x  e.  L  ( ( W  gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  (
x `  j )  =  Y ) ) )
1868lmodfgrp 17390 . . . . . . . 8  |-  ( W  e.  LMod  ->  R  e. 
Grp )
18712, 34, 11grpinvnzcl 15981 . . . . . . . 8  |-  ( ( R  e.  Grp  /\  l  e.  ( ( Base `  R )  \  { Y } ) )  ->  ( ( invg `  R ) `
 l )  e.  ( ( Base `  R
)  \  { Y } ) )
188186, 187sylan 471 . . . . . . 7  |-  ( ( W  e.  LMod  /\  l  e.  ( ( Base `  R
)  \  { Y } ) )  -> 
( ( invg `  R ) `  l
)  e.  ( (
Base `  R )  \  { Y } ) )
18912, 34, 11grpinvnzcl 15981 . . . . . . . . 9  |-  ( ( R  e.  Grp  /\  k  e.  ( ( Base `  R )  \  { Y } ) )  ->  ( ( invg `  R ) `
 k )  e.  ( ( Base `  R
)  \  { Y } ) )
190186, 189sylan 471 . . . . . . . 8  |-  ( ( W  e.  LMod  /\  k  e.  ( ( Base `  R
)  \  { Y } ) )  -> 
( ( invg `  R ) `  k
)  e.  ( (
Base `  R )  \  { Y } ) )
191 eldifi 3631 . . . . . . . . . 10  |-  ( k  e.  ( ( Base `  R )  \  { Y } )  ->  k  e.  ( Base `  R
) )
19212, 11grpinvinv 15976 . . . . . . . . . 10  |-  ( ( R  e.  Grp  /\  k  e.  ( Base `  R ) )  -> 
( ( invg `  R ) `  (
( invg `  R ) `  k
) )  =  k )
193186, 191, 192syl2an 477 . . . . . . . . 9  |-  ( ( W  e.  LMod  /\  k  e.  ( ( Base `  R
)  \  { Y } ) )  -> 
( ( invg `  R ) `  (
( invg `  R ) `  k
) )  =  k )
194193eqcomd 2475 . . . . . . . 8  |-  ( ( W  e.  LMod  /\  k  e.  ( ( Base `  R
)  \  { Y } ) )  -> 
k  =  ( ( invg `  R
) `  ( ( invg `  R ) `
 k ) ) )
195 fveq2 5872 . . . . . . . . . 10  |-  ( l  =  ( ( invg `  R ) `
 k )  -> 
( ( invg `  R ) `  l
)  =  ( ( invg `  R
) `  ( ( invg `  R ) `
 k ) ) )
196195eqeq2d 2481 . . . . . . . . 9  |-  ( l  =  ( ( invg `  R ) `
 k )  -> 
( k  =  ( ( invg `  R ) `  l
)  <->  k  =  ( ( invg `  R ) `  (
( invg `  R ) `  k
) ) ) )
197196rspcev 3219 . . . . . . . 8  |-  ( ( ( ( invg `  R ) `  k
)  e.  ( (
Base `  R )  \  { Y } )  /\  k  =  ( ( invg `  R ) `  (
( invg `  R ) `  k
) ) )  ->  E. l  e.  (
( Base `  R )  \  { Y } ) k  =  ( ( invg `  R
) `  l )
)
198190, 194, 197syl2anc 661 . . . . . . 7  |-  ( ( W  e.  LMod  /\  k  e.  ( ( Base `  R
)  \  { Y } ) )  ->  E. l  e.  (
( Base `  R )  \  { Y } ) k  =  ( ( invg `  R
) `  l )
)
199 oveq1 6302 . . . . . . . . . 10  |-  ( k  =  ( ( invg `  R ) `
 l )  -> 
( k  .x.  ( F `  j )
)  =  ( ( ( invg `  R ) `  l
)  .x.  ( F `  j ) ) )
200199eleq1d 2536 . . . . . . . . 9  |-  ( k  =  ( ( invg `  R ) `
 l )  -> 
( ( k  .x.  ( F `  j ) )  e.  ( (
LSpan `  W ) `  ( F " ( I 
\  { j } ) ) )  <->  ( (
( invg `  R ) `  l
)  .x.  ( F `  j ) )  e.  ( ( LSpan `  W
) `  ( F " ( I  \  {
j } ) ) ) ) )
201200notbid 294 . . . . . . . 8  |-  ( k  =  ( ( invg `  R ) `
 l )  -> 
( -.  ( k 
.x.  ( F `  j ) )  e.  ( ( LSpan `  W
) `  ( F " ( I  \  {
j } ) ) )  <->  -.  ( (
( invg `  R ) `  l
)  .x.  ( F `  j ) )  e.  ( ( LSpan `  W
) `  ( F " ( I  \  {
j } ) ) ) ) )
202201adantl 466 . . . . . . 7  |-  ( ( W  e.  LMod  /\  k  =  ( ( invg `  R ) `
 l ) )  ->  ( -.  (
k  .x.  ( F `  j ) )  e.  ( ( LSpan `  W
) `  ( F " ( I  \  {
j } ) ) )  <->  -.  ( (
( invg `  R ) `  l
)  .x.  ( F `  j ) )  e.  ( ( LSpan `  W
) `  ( F " ( I  \  {
j } ) ) ) ) )
203188, 198, 202ralxfrd 4667 . . . . . 6  |-  ( W  e.  LMod  ->  ( A. k  e.  ( ( Base `  R )  \  { Y } )  -.  ( k  .x.  ( F `  j )
)  e.  ( (
LSpan `  W ) `  ( F " ( I 
\  { j } ) ) )  <->  A. l  e.  ( ( Base `  R
)  \  { Y } )  -.  (
( ( invg `  R ) `  l
)  .x.  ( F `  j ) )  e.  ( ( LSpan `  W
) `  ( F " ( I  \  {
j } ) ) ) ) )
2042033ad2ant1 1017 . . . . 5  |-  ( ( W  e.  LMod  /\  I  e.  X  /\  F :
I --> B )  -> 
( A. k  e.  ( ( Base `  R
)  \  { Y } )  -.  (
k  .x.  ( F `  j ) )  e.  ( ( LSpan `  W
) `  ( F " ( I  \  {
j } ) ) )  <->  A. l  e.  ( ( Base `  R
)  \  { Y } )  -.  (
( ( invg `  R ) `  l
)  .x.  ( F `  j ) )  e.  ( ( LSpan `  W
) `  ( F " ( I  \  {
j } ) ) ) ) )
205204adantr 465 . . . 4  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  ->  ( A. k  e.  ( ( Base `  R )  \  { Y } )  -.  ( k  .x.  ( F `  j )
)  e.  ( (
LSpan `  W ) `  ( F " ( I 
\  { j } ) ) )  <->  A. l  e.  ( ( Base `  R
)  \  { Y } )  -.  (
( ( invg `  R ) `  l
)  .x.  ( F `  j ) )  e.  ( ( LSpan `  W
) `  ( F " ( I  \  {
j } ) ) ) ) )
206 simplr 754 . . . . . . . 8  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  x  e.  L )  ->  j  e.  I )
207 fvex 5882 . . . . . . . . . 10  |-  ( 0g
`  R )  e. 
_V
20834, 207eqeltri 2551 . . . . . . . . 9  |-  Y  e. 
_V
209208fvconst2 6127 . . . . . . . 8  |-  ( j  e.  I  ->  (
( I  X.  { Y } ) `  j
)  =  Y )
210206, 209syl 16 . . . . . . 7  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  x  e.  L )  ->  (
( I  X.  { Y } ) `  j
)  =  Y )
211210eqeq2d 2481 . . . . . 6  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  x  e.  L )  ->  (
( x `  j
)  =  ( ( I  X.  { Y } ) `  j
)  <->  ( x `  j )  =  Y ) )
212211imbi2d 316 . . . . 5  |-  ( ( ( ( W  e. 
LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  /\  x  e.  L )  ->  (
( ( W  gsumg  ( x  oF  .x.  F
) )  =  .0. 
->  ( x `  j
)  =  ( ( I  X.  { Y } ) `  j
) )  <->  ( ( W  gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  (
x `  j )  =  Y ) ) )
213212ralbidva 2903 . . . 4  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  ->  ( A. x  e.  L  (
( W  gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  (
x `  j )  =  ( ( I  X.  { Y }
) `  j )
)  <->  A. x  e.  L  ( ( W  gsumg  ( x  oF  .x.  F
) )  =  .0. 
->  ( x `  j
)  =  Y ) ) )
214185, 205, 2133bitr4d 285 . . 3  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  j  e.  I
)  ->  ( A. k  e.  ( ( Base `  R )  \  { Y } )  -.  ( k  .x.  ( F `  j )
)  e.  ( (
LSpan `  W ) `  ( F " ( I 
\  { j } ) ) )  <->  A. x  e.  L  ( ( W  gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  (
x `  j )  =  ( ( I  X.  { Y }
) `  j )
) ) )
215214ralbidva 2903 . 2  |-  ( ( W  e.  LMod  /\  I  e.  X  /\  F :
I --> B )  -> 
( A. j  e.  I  A. k  e.  ( ( Base `  R
)  \  { Y } )  -.  (
k  .x.  ( F `  j ) )  e.  ( ( LSpan `  W
) `  ( F " ( I  \  {
j } ) ) )  <->  A. j  e.  I  A. x  e.  L  ( ( W  gsumg  ( x  oF  .x.  F
) )  =  .0. 
->  ( x `  j
)  =  ( ( I  X.  { Y } ) `  j
) ) ) )
2167, 9, 162, 8, 12, 34islindf2 18716 . 2  |-  ( ( W  e.  LMod  /\  I  e.  X  /\  F :
I --> B )  -> 
( F LIndF  W  <->  A. j  e.  I  A. k  e.  ( ( Base `  R
)  \  { Y } )  -.  (
k  .x.  ( F `  j ) )  e.  ( ( LSpan `  W
) `  ( F " ( I  \  {
j } ) ) ) ) )
217175, 12, 181frlmbasf 18661 . . . . . . . 8  |-  ( ( I  e.  X  /\  x  e.  L )  ->  x : I --> ( Base `  R ) )
2182173ad2antl2 1159 . . . . . . 7  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  x  e.  L
)  ->  x :
I --> ( Base `  R
) )
219 ffn 5737 . . . . . . 7  |-  ( x : I --> ( Base `  R )  ->  x  Fn  I )
220218, 219syl 16 . . . . . 6  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  x  e.  L
)  ->  x  Fn  I )
221 fnconstg 5779 . . . . . . 7  |-  ( Y  e.  _V  ->  (
I  X.  { Y } )  Fn  I
)
222208, 221ax-mp 5 . . . . . 6  |-  ( I  X.  { Y }
)  Fn  I
223 eqfnfv 5982 . . . . . 6  |-  ( ( x  Fn  I  /\  ( I  X.  { Y } )  Fn  I
)  ->  ( x  =  ( I  X.  { Y } )  <->  A. j  e.  I  ( x `  j )  =  ( ( I  X.  { Y } ) `  j
) ) )
224220, 222, 223sylancl 662 . . . . 5  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  x  e.  L
)  ->  ( x  =  ( I  X.  { Y } )  <->  A. j  e.  I  ( x `  j )  =  ( ( I  X.  { Y } ) `  j
) ) )
225224imbi2d 316 . . . 4  |-  ( ( ( W  e.  LMod  /\  I  e.  X  /\  F : I --> B )  /\  x  e.  L
)  ->  ( (
( W  gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  x  =  ( I  X.  { Y } ) )  <-> 
( ( W  gsumg  ( x  oF  .x.  F
) )  =  .0. 
->  A. j  e.  I 
( x `  j
)  =  ( ( I  X.  { Y } ) `  j
) ) ) )
226225ralbidva 2903 . . 3  |-  ( ( W  e.  LMod  /\  I  e.  X  /\  F :
I --> B )  -> 
( A. x  e.  L  ( ( W 
gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  x  =  ( I  X.  { Y } ) )  <->  A. x  e.  L  ( ( W  gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  A. j  e.  I  ( x `  j )  =  ( ( I  X.  { Y } ) `  j
) ) ) )
227 r19.21v 2872 . . . . 5  |-  ( A. j  e.  I  (
( W  gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  (
x `  j )  =  ( ( I  X.  { Y }
) `  j )
)  <->  ( ( W 
gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  A. j  e.  I  ( x `  j )  =  ( ( I  X.  { Y } ) `  j
) ) )
228227ralbii 2898 . . . 4  |-  ( A. x  e.  L  A. j  e.  I  (
( W  gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  (
x `  j )  =  ( ( I  X.  { Y }
) `  j )
)  <->  A. x  e.  L  ( ( W  gsumg  ( x  oF  .x.  F
) )  =  .0. 
->  A. j  e.  I 
( x `  j
)  =  ( ( I  X.  { Y } ) `  j
) ) )
229 ralcom 3027 . . . 4  |-  ( A. x  e.  L  A. j  e.  I  (
( W  gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  (
x `  j )  =  ( ( I  X.  { Y }
) `  j )
)  <->  A. j  e.  I  A. x  e.  L  ( ( W  gsumg  ( x  oF  .x.  F
) )  =  .0. 
->  ( x `  j
)  =  ( ( I  X.  { Y } ) `  j
) ) )
230228, 229bitr3i 251 . . 3  |-  ( A. x  e.  L  (
( W  gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  A. j  e.  I  ( x `  j )  =  ( ( I  X.  { Y } ) `  j
) )  <->  A. j  e.  I  A. x  e.  L  ( ( W  gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  (
x `  j )  =  ( ( I  X.  { Y }
) `  j )
) )
231226, 230syl6bb 261 . 2  |-  ( ( W  e.  LMod  /\  I  e.  X  /\  F :
I --> B )  -> 
( A. x  e.  L  ( ( W 
gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  x  =  ( I  X.  { Y } ) )  <->  A. j  e.  I  A. x  e.  L  ( ( W  gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  (
x `  j )  =  ( ( I  X.  { Y }
) `  j )
) ) )
232215, 216, 2313bitr4d 285 1  |-  ( ( W  e.  LMod  /\  I  e.  X  /\  F :
I --> B )  -> 
( F LIndF  W  <->  A. x  e.  L  ( ( W  gsumg  ( x  oF  .x.  F ) )  =  .0.  ->  x  =  ( I  X.  { Y } ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 973    = wceq 1379    e. wcel 1767    e/ wnel 2663   A.wral 2817   E.wrex 2818   {crab 2821   _Vcvv 3118    \ cdif 3478    u. cun 3479    i^i cin 3480    C_ wss 3481   (/)c0 3790   {csn 4033   <.cop 4039   class class class wbr 4453    |-> cmpt 4511    X. cxp 5003   dom cdm 5005    |` cres 5007   "cima 5008   Fun wfun 5588    Fn wfn 5589   -->wf 5590   ` cfv 5594  (class class class)co 6295    oFcof 6533    ^m cmap 7432   finSupp cfsupp 7841   Basecbs 14506   +g cplusg 14571  Scalarcsca 14574   .scvsca 14575   0gc0g 14711    gsumg cgsu 14712   Mndcmnd 15792   Grpcgrp 15924   invgcminusg 15925  CMndccmn 16669   LModclmod 17381   LSpanclspn 17486   freeLMod cfrlm 18644   LIndF clindf 18706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587  ax-inf2 8070  ax-cnex 9560  ax-resscn 9561  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-addrcl 9565  ax-mulcl 9566  ax-mulrcl 9567  ax-mulcom 9568  ax-addass 9569  ax-mulass 9570  ax-distr 9571  ax-i2m1 9572  ax-1ne0 9573  ax-1rid 9574  ax-rnegex 9575  ax-rrecex 9576  ax-cnre 9577  ax-pre-lttri 9578  ax-pre-lttrn 9579  ax-pre-ltadd 9580  ax-pre-mulgt0 9581
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-int 4289  df-iun 4333  df-iin 4334  df-br 4454  df-opab 4512  df-mpt 4513  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-se 4845  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-isom 5603  df-riota 6256  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-of 6535  df-om 6696  df-1st 6795  df-2nd 6796  df-supp 6914  df-recs 7054  df-rdg 7088  df-1o 7142  df-oadd 7146  df-er 7323  df-map 7434  df-ixp 7482  df-en 7529  df-dom 7530  df-sdom 7531  df-fin 7532  df-fsupp 7842  df-sup 7913  df-oi 7947  df-card 8332  df-pnf 9642  df-mnf 9643  df-xr 9644  df-ltxr 9645  df-le 9646  df-sub 9819  df-neg 9820  df-nn 10549  df-2 10606  df-3 10607  df-4 10608  df-5 10609  df-6 10610  df-7 10611  df-8 10612  df-9 10613  df-10 10614  df-n0 10808  df-z 10877  df-dec 10989  df-uz 11095  df-fz 11685  df-fzo 11805  df-seq 12088  df-hash 12386  df-struct 14508  df-ndx 14509  df-slot 14510  df-base 14511  df-sets 14512  df-ress 14513  df-plusg 14584  df-mulr 14585  df-sca 14587  df-vsca 14588  df-ip 14589  df-tset 14590  df-ple 14591  df-ds 14593  df-hom 14595  df-cco 14596  df-0g 14713  df-gsum 14714  df-prds 14719  df-pws 14721  df-mre 14857  df-mrc 14858  df-acs 14860  df-mgm 15745  df-sgrp 15784  df-mnd 15794  df-mhm 15838  df-submnd 15839  df-grp 15928  df-minusg 15929  df-sbg 15930  df-mulg 15931  df-subg 16069  df-ghm 16136  df-cntz 16226  df-cmn 16671  df-abl 16672  df-mgp 17012  df-ur 17024  df-ring 17070  df-subrg 17296  df-lmod 17383  df-lss 17448  df-lsp 17487  df-lmhm 17537  df-lbs 17590  df-sra 17687  df-rgmod 17688  df-nzr 17774  df-dsmm 18630  df-frlm 18645  df-uvc 18681  df-lindf 18708
This theorem is referenced by:  islindf5  18741
  Copyright terms: Public domain W3C validator