Metamath Proof Explorer

Theorem islindf4

Description: A family is independent iff it has no nontrivial representations of zero. (Contributed by Stefan O'Rear, 28-Feb-2015)

Ref Expression
Hypotheses 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 islindf4 
|- ( ( W e. LMod /\ I e. X /\ F : I --> B ) -> ( F LIndF W <-> A. x e. L ( ( W gsum ( x oF .x. F ) ) = .0. -> x = ( I X. { Y } ) ) ) )

Proof

Step Hyp Ref Expression
1 islindf4.b 
 |-  B = ( Base ` W )
2 islindf4.r 
 |-  R = ( Scalar ` W )
3 islindf4.t 
 |-  .x. = ( .s ` W )
4 islindf4.z 
 |-  .0. = ( 0g ` W )
5 islindf4.y 
 |-  Y = ( 0g ` R )
6 islindf4.l 
 |-  L = ( Base ` ( R freeLMod I ) )
7 raldifsni 
 |-  ( 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 ) )
8 simpll1 
 |-  ( ( ( ( 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 )
9 simprll 
 |-  ( ( ( ( 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 ) )
10 ffvelrn 
 |-  ( ( F : I --> B /\ j e. I ) -> ( F ` j ) e. B )
11 10 3ad2antl3 
 |-  ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( F ` j ) e. B )
12 11 adantr 
 |-  ( ( ( ( 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 )
13 eqid 
 |-  ( invg ` W ) = ( invg ` W )
14 eqid 
 |-  ( invg ` R ) = ( invg ` R )
15 eqid 
 |-  ( Base ` R ) = ( Base ` R )
16 1 2 3 13 14 15 lmodvsinv 
 |-  ( ( W e. LMod /\ l e. ( Base ` R ) /\ ( F ` j ) e. B ) -> ( ( ( invg ` R ) ` l ) .x. ( F ` j ) ) = ( ( invg ` W ) ` ( l .x. ( F ` j ) ) ) )
17 8 9 12 16 syl3anc 
 |-  ( ( ( ( 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 ) ) ) )
18 17 eqeq1d 
 |-  ( ( ( ( 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 gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) <-> ( ( invg ` W ) ` ( l .x. ( F ` j ) ) ) = ( W gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) ) )
19 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
20 8 19 syl 
 |-  ( ( ( ( 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 )
21 1 2 3 15 lmodvscl 
 |-  ( ( W e. LMod /\ l e. ( Base ` R ) /\ ( F ` j ) e. B ) -> ( l .x. ( F ` j ) ) e. B )
22 8 9 12 21 syl3anc 
 |-  ( ( ( ( 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 )
23 lmodcmn 
 |-  ( W e. LMod -> W e. CMnd )
24 8 23 syl 
 |-  ( ( ( ( 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 )
25 simpll2 
 |-  ( ( ( ( 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 )
26 difexg 
 |-  ( I e. X -> ( I \ { j } ) e. _V )
27 25 26 syl 
 |-  ( ( ( ( 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 )
28 simprlr 
 |-  ( ( ( ( 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 } ) ) )
29 elmapi 
 |-  ( y e. ( ( Base ` R ) ^m ( I \ { j } ) ) -> y : ( I \ { j } ) --> ( Base ` R ) )
30 28 29 syl 
 |-  ( ( ( ( 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 ) )
31 simpll3 
 |-  ( ( ( ( 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 )
32 difss 
 |-  ( I \ { j } ) C_ I
33 fssres 
 |-  ( ( F : I --> B /\ ( I \ { j } ) C_ I ) -> ( F |` ( I \ { j } ) ) : ( I \ { j } ) --> B )
34 31 32 33 sylancl 
 |-  ( ( ( ( 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 )
35 2 15 3 1 8 30 34 27 lcomf 
 |-  ( ( ( ( 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 )
36 simprr 
 |-  ( ( ( ( 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 )
37 2 15 3 1 8 30 34 27 4 5 36 lcomfsupp 
 |-  ( ( ( ( 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. )
38 1 4 24 27 35 37 gsumcl 
 |-  ( ( ( ( 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 gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) e. B )
39 eqid 
 |-  ( +g ` W ) = ( +g ` W )
40 1 39 4 13 grpinvid2 
 |-  ( ( W e. Grp /\ ( l .x. ( F ` j ) ) e. B /\ ( W gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) e. B ) -> ( ( ( invg ` W ) ` ( l .x. ( F ` j ) ) ) = ( W gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) <-> ( ( W gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) ( +g ` W ) ( l .x. ( F ` j ) ) ) = .0. ) )
41 20 22 38 40 syl3anc 
 |-  ( ( ( ( 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 gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) <-> ( ( W gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) ( +g ` W ) ( l .x. ( F ` j ) ) ) = .0. ) )
42 simplr 
 |-  ( ( ( ( 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 )
43 fsnunf2 
 |-  ( ( y : ( I \ { j } ) --> ( Base ` R ) /\ j e. I /\ l e. ( Base ` R ) ) -> ( y u. { <. j , l >. } ) : I --> ( Base ` R ) )
44 30 42 9 43 syl3anc 
 |-  ( ( ( ( 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 ) )
45 2 15 3 1 8 44 31 25 lcomf 
 |-  ( ( ( ( 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 )
46 simpr 
 |-  ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> j e. I )
47 simpl 
 |-  ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) -> l e. ( Base ` R ) )
48 46 47 anim12i 
 |-  ( ( ( ( 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 ) ) )
49 elmapfun 
 |-  ( y e. ( ( Base ` R ) ^m ( I \ { j } ) ) -> Fun y )
50 fdm 
 |-  ( y : ( I \ { j } ) --> ( Base ` R ) -> dom y = ( I \ { j } ) )
51 neldifsnd 
 |-  ( dom y = ( I \ { j } ) -> -. j e. ( I \ { j } ) )
52 df-nel 
 |-  ( j e/ dom y <-> -. j e. dom y )
53 eleq2 
 |-  ( dom y = ( I \ { j } ) -> ( j e. dom y <-> j e. ( I \ { j } ) ) )
54 53 notbid 
 |-  ( dom y = ( I \ { j } ) -> ( -. j e. dom y <-> -. j e. ( I \ { j } ) ) )
55 52 54 syl5bb 
 |-  ( dom y = ( I \ { j } ) -> ( j e/ dom y <-> -. j e. ( I \ { j } ) ) )
56 51 55 mpbird 
 |-  ( dom y = ( I \ { j } ) -> j e/ dom y )
57 29 50 56 3syl 
 |-  ( y e. ( ( Base ` R ) ^m ( I \ { j } ) ) -> j e/ dom y )
58 49 57 jca 
 |-  ( y e. ( ( Base ` R ) ^m ( I \ { j } ) ) -> ( Fun y /\ j e/ dom y ) )
59 58 adantl 
 |-  ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) -> ( Fun y /\ j e/ dom y ) )
60 59 adantl 
 |-  ( ( ( ( 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 ) )
61 48 60 jca 
 |-  ( ( ( ( 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 
 |-  ( ( ( j e. I /\ l e. ( Base ` R ) ) /\ ( Fun y /\ j e/ dom y ) ) -> ( ( y u. { <. j , l >. } ) finSupp Y <-> y finSupp Y ) )
63 62 bicomd 
 |-  ( ( ( j e. I /\ l e. ( Base ` R ) ) /\ ( Fun y /\ j e/ dom y ) ) -> ( y finSupp Y <-> ( y u. { <. j , l >. } ) finSupp Y ) )
64 61 63 syl 
 |-  ( ( ( ( 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 ) )
65 64 biimpd 
 |-  ( ( ( ( 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 ) )
66 65 impr 
 |-  ( ( ( ( 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 )
67 2 15 3 1 8 44 31 25 4 5 66 lcomfsupp 
 |-  ( ( ( ( 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 disjdifr 
 |-  ( ( I \ { j } ) i^i { j } ) = (/)
69 68 a1i 
 |-  ( ( ( ( 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 } ) = (/) )
70 difsnid 
 |-  ( j e. I -> ( ( I \ { j } ) u. { j } ) = I )
71 70 eqcomd 
 |-  ( j e. I -> I = ( ( I \ { j } ) u. { j } ) )
72 42 71 syl 
 |-  ( ( ( ( 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 } ) )
73 1 4 39 24 25 45 67 69 72 gsumsplit 
 |-  ( ( ( ( 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 gsum ( ( y u. { <. j , l >. } ) oF .x. F ) ) = ( ( W gsum ( ( ( y u. { <. j , l >. } ) oF .x. F ) |` ( I \ { j } ) ) ) ( +g ` W ) ( W gsum ( ( ( y u. { <. j , l >. } ) oF .x. F ) |` { j } ) ) ) )
74 vex 
 |-  y e. _V
75 snex 
 |-  { <. j , l >. } e. _V
76 74 75 unex 
 |-  ( y u. { <. j , l >. } ) e. _V
77 simpl3 
 |-  ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> F : I --> B )
78 simpl2 
 |-  ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> I e. X )
79 77 78 fexd 
 |-  ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> F e. _V )
80 79 adantr 
 |-  ( ( ( ( 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 )
81 offres 
 |-  ( ( ( 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 } ) ) ) )
82 76 80 81 sylancr 
 |-  ( ( ( ( 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 } ) ) ) )
83 30 ffnd 
 |-  ( ( ( ( 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 } ) )
84 neldifsn 
 |-  -. j e. ( I \ { j } )
85 fsnunres 
 |-  ( ( y Fn ( I \ { j } ) /\ -. j e. ( I \ { j } ) ) -> ( ( y u. { <. j , l >. } ) |` ( I \ { j } ) ) = y )
86 83 84 85 sylancl 
 |-  ( ( ( ( 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 )
87 86 oveq1d 
 |-  ( ( ( ( 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 } ) ) ) )
88 82 87 eqtrd 
 |-  ( ( ( ( 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 } ) ) ) )
89 88 oveq2d 
 |-  ( ( ( ( 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 gsum ( ( ( y u. { <. j , l >. } ) oF .x. F ) |` ( I \ { j } ) ) ) = ( W gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) )
90 45 ffnd 
 |-  ( ( ( ( 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 )
91 fnressn 
 |-  ( ( ( ( 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 ) >. } )
92 90 42 91 syl2anc 
 |-  ( ( ( ( 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 ) >. } )
93 44 ffnd 
 |-  ( ( ( ( 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 )
94 31 ffnd 
 |-  ( ( ( ( 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 )
95 fnfvof 
 |-  ( ( ( ( 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 ) ) )
96 93 94 25 42 95 syl22anc 
 |-  ( ( ( ( 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 ) ) )
97 fndm 
 |-  ( y Fn ( I \ { j } ) -> dom y = ( I \ { j } ) )
98 97 eleq2d 
 |-  ( y Fn ( I \ { j } ) -> ( j e. dom y <-> j e. ( I \ { j } ) ) )
99 84 98 mtbiri 
 |-  ( y Fn ( I \ { j } ) -> -. j e. dom y )
100 vex 
 |-  j e. _V
101 vex 
 |-  l e. _V
102 fsnunfv 
 |-  ( ( j e. _V /\ l e. _V /\ -. j e. dom y ) -> ( ( y u. { <. j , l >. } ) ` j ) = l )
103 100 101 102 mp3an12 
 |-  ( -. j e. dom y -> ( ( y u. { <. j , l >. } ) ` j ) = l )
104 83 99 103 3syl 
 |-  ( ( ( ( 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 )
105 104 oveq1d 
 |-  ( ( ( ( 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 ) ) )
106 96 105 eqtrd 
 |-  ( ( ( ( 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 ) ) )
107 106 opeq2d 
 |-  ( ( ( ( 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 ) ) >. )
108 107 sneqd 
 |-  ( ( ( ( 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 ) ) >. } )
109 ovex 
 |-  ( l .x. ( F ` j ) ) e. _V
110 fmptsn 
 |-  ( ( j e. _V /\ ( l .x. ( F ` j ) ) e. _V ) -> { <. j , ( l .x. ( F ` j ) ) >. } = ( x e. { j } |-> ( l .x. ( F ` j ) ) ) )
111 100 109 110 mp2an 
 |-  { <. j , ( l .x. ( F ` j ) ) >. } = ( x e. { j } |-> ( l .x. ( F ` j ) ) )
112 111 a1i 
 |-  ( ( ( ( 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 ) ) ) )
113 92 108 112 3eqtrd 
 |-  ( ( ( ( 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 ) ) ) )
114 113 oveq2d 
 |-  ( ( ( ( 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 gsum ( ( ( y u. { <. j , l >. } ) oF .x. F ) |` { j } ) ) = ( W gsum ( x e. { j } |-> ( l .x. ( F ` j ) ) ) ) )
115 cmnmnd 
 |-  ( W e. CMnd -> W e. Mnd )
116 8 23 115 3syl 
 |-  ( ( ( ( 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 )
117 100 a1i 
 |-  ( ( ( ( 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 )
118 eqidd 
 |-  ( x = j -> ( l .x. ( F ` j ) ) = ( l .x. ( F ` j ) ) )
119 1 118 gsumsn 
 |-  ( ( W e. Mnd /\ j e. _V /\ ( l .x. ( F ` j ) ) e. B ) -> ( W gsum ( x e. { j } |-> ( l .x. ( F ` j ) ) ) ) = ( l .x. ( F ` j ) ) )
120 116 117 22 119 syl3anc 
 |-  ( ( ( ( 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 gsum ( x e. { j } |-> ( l .x. ( F ` j ) ) ) ) = ( l .x. ( F ` j ) ) )
121 114 120 eqtrd 
 |-  ( ( ( ( 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 gsum ( ( ( y u. { <. j , l >. } ) oF .x. F ) |` { j } ) ) = ( l .x. ( F ` j ) ) )
122 89 121 oveq12d 
 |-  ( ( ( ( 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 gsum ( ( ( y u. { <. j , l >. } ) oF .x. F ) |` ( I \ { j } ) ) ) ( +g ` W ) ( W gsum ( ( ( y u. { <. j , l >. } ) oF .x. F ) |` { j } ) ) ) = ( ( W gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) ( +g ` W ) ( l .x. ( F ` j ) ) ) )
123 73 122 eqtr2d 
 |-  ( ( ( ( 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 gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) ( +g ` W ) ( l .x. ( F ` j ) ) ) = ( W gsum ( ( y u. { <. j , l >. } ) oF .x. F ) ) )
124 123 eqeq1d 
 |-  ( ( ( ( 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 gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) ( +g ` W ) ( l .x. ( F ` j ) ) ) = .0. <-> ( W gsum ( ( y u. { <. j , l >. } ) oF .x. F ) ) = .0. ) )
125 18 41 124 3bitrd 
 |-  ( ( ( ( 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 gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) <-> ( W gsum ( ( y u. { <. j , l >. } ) oF .x. F ) ) = .0. ) )
126 104 eqcomd 
 |-  ( ( ( ( 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 ) )
127 126 eqeq1d 
 |-  ( ( ( ( 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 ) )
128 125 127 imbi12d 
 |-  ( ( ( ( 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 gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) -> l = Y ) <-> ( ( W gsum ( ( y u. { <. j , l >. } ) oF .x. F ) ) = .0. -> ( ( y u. { <. j , l >. } ) ` j ) = Y ) ) )
129 128 anassrs 
 |-  ( ( ( ( ( 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 gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) -> l = Y ) <-> ( ( W gsum ( ( y u. { <. j , l >. } ) oF .x. F ) ) = .0. -> ( ( y u. { <. j , l >. } ) ` j ) = Y ) ) )
130 129 pm5.74da 
 |-  ( ( ( ( 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 gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) -> l = Y ) ) <-> ( y finSupp Y -> ( ( W gsum ( ( y u. { <. j , l >. } ) oF .x. F ) ) = .0. -> ( ( y u. { <. j , l >. } ) ` j ) = Y ) ) ) )
131 impexp 
 |-  ( ( ( y finSupp Y /\ ( ( ( invg ` R ) ` l ) .x. ( F ` j ) ) = ( W gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) ) -> l = Y ) <-> ( y finSupp Y -> ( ( ( ( invg ` R ) ` l ) .x. ( F ` j ) ) = ( W gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) -> l = Y ) ) )
132 131 a1i 
 |-  ( ( ( ( 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 gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) ) -> l = Y ) <-> ( y finSupp Y -> ( ( ( ( invg ` R ) ` l ) .x. ( F ` j ) ) = ( W gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) -> l = Y ) ) ) )
133 64 bicomd 
 |-  ( ( ( ( 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 ) )
134 133 imbi1d 
 |-  ( ( ( ( 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 gsum ( ( y u. { <. j , l >. } ) oF .x. F ) ) = .0. -> ( ( y u. { <. j , l >. } ) ` j ) = Y ) ) <-> ( y finSupp Y -> ( ( W gsum ( ( y u. { <. j , l >. } ) oF .x. F ) ) = .0. -> ( ( y u. { <. j , l >. } ) ` j ) = Y ) ) ) )
135 130 132 134 3bitr4d 
 |-  ( ( ( ( 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 gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) ) -> l = Y ) <-> ( ( y u. { <. j , l >. } ) finSupp Y -> ( ( W gsum ( ( y u. { <. j , l >. } ) oF .x. F ) ) = .0. -> ( ( y u. { <. j , l >. } ) ` j ) = Y ) ) ) )
136 135 2ralbidva 
 |-  ( ( ( 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 gsum ( 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 gsum ( ( y u. { <. j , l >. } ) oF .x. F ) ) = .0. -> ( ( y u. { <. j , l >. } ) ` j ) = Y ) ) ) )
137 breq1 
 |-  ( x = ( y u. { <. j , l >. } ) -> ( x finSupp Y <-> ( y u. { <. j , l >. } ) finSupp Y ) )
138 oveq1 
 |-  ( x = ( y u. { <. j , l >. } ) -> ( x oF .x. F ) = ( ( y u. { <. j , l >. } ) oF .x. F ) )
139 138 oveq2d 
 |-  ( x = ( y u. { <. j , l >. } ) -> ( W gsum ( x oF .x. F ) ) = ( W gsum ( ( y u. { <. j , l >. } ) oF .x. F ) ) )
140 139 eqeq1d 
 |-  ( x = ( y u. { <. j , l >. } ) -> ( ( W gsum ( x oF .x. F ) ) = .0. <-> ( W gsum ( ( y u. { <. j , l >. } ) oF .x. F ) ) = .0. ) )
141 fveq1 
 |-  ( x = ( y u. { <. j , l >. } ) -> ( x ` j ) = ( ( y u. { <. j , l >. } ) ` j ) )
142 141 eqeq1d 
 |-  ( x = ( y u. { <. j , l >. } ) -> ( ( x ` j ) = Y <-> ( ( y u. { <. j , l >. } ) ` j ) = Y ) )
143 140 142 imbi12d 
 |-  ( x = ( y u. { <. j , l >. } ) -> ( ( ( W gsum ( x oF .x. F ) ) = .0. -> ( x ` j ) = Y ) <-> ( ( W gsum ( ( y u. { <. j , l >. } ) oF .x. F ) ) = .0. -> ( ( y u. { <. j , l >. } ) ` j ) = Y ) ) )
144 137 143 imbi12d 
 |-  ( x = ( y u. { <. j , l >. } ) -> ( ( x finSupp Y -> ( ( W gsum ( x oF .x. F ) ) = .0. -> ( x ` j ) = Y ) ) <-> ( ( y u. { <. j , l >. } ) finSupp Y -> ( ( W gsum ( ( y u. { <. j , l >. } ) oF .x. F ) ) = .0. -> ( ( y u. { <. j , l >. } ) ` j ) = Y ) ) ) )
145 144 ralxpmap 
 |-  ( j e. I -> ( A. x e. ( ( Base ` R ) ^m I ) ( x finSupp Y -> ( ( W gsum ( 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 gsum ( ( y u. { <. j , l >. } ) oF .x. F ) ) = .0. -> ( ( y u. { <. j , l >. } ) ` j ) = Y ) ) ) )
146 145 adantl 
 |-  ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( A. x e. ( ( Base ` R ) ^m I ) ( x finSupp Y -> ( ( W gsum ( 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 gsum ( ( y u. { <. j , l >. } ) oF .x. F ) ) = .0. -> ( ( y u. { <. j , l >. } ) ` j ) = Y ) ) ) )
147 136 146 bitr4d 
 |-  ( ( ( 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 gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) ) -> l = Y ) <-> A. x e. ( ( Base ` R ) ^m I ) ( x finSupp Y -> ( ( W gsum ( x oF .x. F ) ) = .0. -> ( x ` j ) = Y ) ) ) )
148 breq1 
 |-  ( z = x -> ( z finSupp Y <-> x finSupp Y ) )
149 148 ralrab 
 |-  ( A. x e. { z e. ( ( Base ` R ) ^m I ) | z finSupp Y } ( ( W gsum ( x oF .x. F ) ) = .0. -> ( x ` j ) = Y ) <-> A. x e. ( ( Base ` R ) ^m I ) ( x finSupp Y -> ( ( W gsum ( x oF .x. F ) ) = .0. -> ( x ` j ) = Y ) ) )
150 147 149 bitr4di 
 |-  ( ( ( 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 gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) ) -> l = Y ) <-> A. x e. { z e. ( ( Base ` R ) ^m I ) | z finSupp Y } ( ( W gsum ( x oF .x. F ) ) = .0. -> ( x ` j ) = Y ) ) )
151 resima 
 |-  ( ( F |` ( I \ { j } ) ) " ( I \ { j } ) ) = ( F " ( I \ { j } ) )
152 151 eqcomi 
 |-  ( F " ( I \ { j } ) ) = ( ( F |` ( I \ { j } ) ) " ( I \ { j } ) )
153 152 fveq2i 
 |-  ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) = ( ( LSpan ` W ) ` ( ( F |` ( I \ { j } ) ) " ( I \ { j } ) ) )
154 153 eleq2i 
 |-  ( ( ( ( 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 } ) ) ) )
155 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
156 77 32 33 sylancl 
 |-  ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( F |` ( I \ { j } ) ) : ( I \ { j } ) --> B )
157 simpl1 
 |-  ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> W e. LMod )
158 26 3ad2ant2 
 |-  ( ( W e. LMod /\ I e. X /\ F : I --> B ) -> ( I \ { j } ) e. _V )
159 158 adantr 
 |-  ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( I \ { j } ) e. _V )
160 155 1 15 2 5 3 156 157 159 ellspd 
 |-  ( ( ( 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 gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) ) ) )
161 154 160 syl5bb 
 |-  ( ( ( 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 gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) ) ) )
162 161 imbi1d 
 |-  ( ( ( 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 gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) ) -> l = Y ) ) )
163 r19.23v 
 |-  ( A. y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ( ( y finSupp Y /\ ( ( ( invg ` R ) ` l ) .x. ( F ` j ) ) = ( W gsum ( 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 gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) ) -> l = Y ) )
164 162 163 bitr4di 
 |-  ( ( ( 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 gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) ) -> l = Y ) ) )
165 164 ralbidv 
 |-  ( ( ( 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 gsum ( y oF .x. ( F |` ( I \ { j } ) ) ) ) ) -> l = Y ) ) )
166 2 fvexi 
 |-  R e. _V
167 eqid 
 |-  ( R freeLMod I ) = ( R freeLMod I )
168 eqid 
 |-  { z e. ( ( Base ` R ) ^m I ) | z finSupp Y } = { z e. ( ( Base ` R ) ^m I ) | z finSupp Y }
169 167 15 5 168 frlmbas 
 |-  ( ( R e. _V /\ I e. X ) -> { z e. ( ( Base ` R ) ^m I ) | z finSupp Y } = ( Base ` ( R freeLMod I ) ) )
170 166 169 mpan 
 |-  ( I e. X -> { z e. ( ( Base ` R ) ^m I ) | z finSupp Y } = ( Base ` ( R freeLMod I ) ) )
171 170 3ad2ant2 
 |-  ( ( W e. LMod /\ I e. X /\ F : I --> B ) -> { z e. ( ( Base ` R ) ^m I ) | z finSupp Y } = ( Base ` ( R freeLMod I ) ) )
172 171 adantr 
 |-  ( ( ( 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 ) ) )
173 6 172 eqtr4id 
 |-  ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> L = { z e. ( ( Base ` R ) ^m I ) | z finSupp Y } )
174 173 raleqdv 
 |-  ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( A. x e. L ( ( W gsum ( x oF .x. F ) ) = .0. -> ( x ` j ) = Y ) <-> A. x e. { z e. ( ( Base ` R ) ^m I ) | z finSupp Y } ( ( W gsum ( x oF .x. F ) ) = .0. -> ( x ` j ) = Y ) ) )
175 150 165 174 3bitr4d 
 |-  ( ( ( 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 gsum ( x oF .x. F ) ) = .0. -> ( x ` j ) = Y ) ) )
176 7 175 syl5bb 
 |-  ( ( ( 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 gsum ( x oF .x. F ) ) = .0. -> ( x ` j ) = Y ) ) )
177 2 lmodfgrp 
 |-  ( W e. LMod -> R e. Grp )
178 15 5 14 grpinvnzcl 
 |-  ( ( R e. Grp /\ l e. ( ( Base ` R ) \ { Y } ) ) -> ( ( invg ` R ) ` l ) e. ( ( Base ` R ) \ { Y } ) )
179 177 178 sylan 
 |-  ( ( W e. LMod /\ l e. ( ( Base ` R ) \ { Y } ) ) -> ( ( invg ` R ) ` l ) e. ( ( Base ` R ) \ { Y } ) )
180 15 5 14 grpinvnzcl 
 |-  ( ( R e. Grp /\ k e. ( ( Base ` R ) \ { Y } ) ) -> ( ( invg ` R ) ` k ) e. ( ( Base ` R ) \ { Y } ) )
181 177 180 sylan 
 |-  ( ( W e. LMod /\ k e. ( ( Base ` R ) \ { Y } ) ) -> ( ( invg ` R ) ` k ) e. ( ( Base ` R ) \ { Y } ) )
182 eldifi 
 |-  ( k e. ( ( Base ` R ) \ { Y } ) -> k e. ( Base ` R ) )
183 15 14 grpinvinv 
 |-  ( ( R e. Grp /\ k e. ( Base ` R ) ) -> ( ( invg ` R ) ` ( ( invg ` R ) ` k ) ) = k )
184 177 182 183 syl2an 
 |-  ( ( W e. LMod /\ k e. ( ( Base ` R ) \ { Y } ) ) -> ( ( invg ` R ) ` ( ( invg ` R ) ` k ) ) = k )
185 184 eqcomd 
 |-  ( ( W e. LMod /\ k e. ( ( Base ` R ) \ { Y } ) ) -> k = ( ( invg ` R ) ` ( ( invg ` R ) ` k ) ) )
186 fveq2 
 |-  ( l = ( ( invg ` R ) ` k ) -> ( ( invg ` R ) ` l ) = ( ( invg ` R ) ` ( ( invg ` R ) ` k ) ) )
187 186 rspceeqv 
 |-  ( ( ( ( invg ` R ) ` k ) e. ( ( Base ` R ) \ { Y } ) /\ k = ( ( invg ` R ) ` ( ( invg ` R ) ` k ) ) ) -> E. l e. ( ( Base ` R ) \ { Y } ) k = ( ( invg ` R ) ` l ) )
188 181 185 187 syl2anc 
 |-  ( ( W e. LMod /\ k e. ( ( Base ` R ) \ { Y } ) ) -> E. l e. ( ( Base ` R ) \ { Y } ) k = ( ( invg ` R ) ` l ) )
189 oveq1 
 |-  ( k = ( ( invg ` R ) ` l ) -> ( k .x. ( F ` j ) ) = ( ( ( invg ` R ) ` l ) .x. ( F ` j ) ) )
190 189 eleq1d 
 |-  ( 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 } ) ) ) ) )
191 190 notbid 
 |-  ( 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 } ) ) ) ) )
192 191 adantl 
 |-  ( ( 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 } ) ) ) ) )
193 179 188 192 ralxfrd 
 |-  ( 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 } ) ) ) ) )
194 193 3ad2ant1 
 |-  ( ( 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 } ) ) ) ) )
195 194 adantr 
 |-  ( ( ( 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 } ) ) ) ) )
196 simplr 
 |-  ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ x e. L ) -> j e. I )
197 5 fvexi 
 |-  Y e. _V
198 197 fvconst2 
 |-  ( j e. I -> ( ( I X. { Y } ) ` j ) = Y )
199 196 198 syl 
 |-  ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ x e. L ) -> ( ( I X. { Y } ) ` j ) = Y )
200 199 eqeq2d 
 |-  ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ x e. L ) -> ( ( x ` j ) = ( ( I X. { Y } ) ` j ) <-> ( x ` j ) = Y ) )
201 200 imbi2d 
 |-  ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ x e. L ) -> ( ( ( W gsum ( x oF .x. F ) ) = .0. -> ( x ` j ) = ( ( I X. { Y } ) ` j ) ) <-> ( ( W gsum ( x oF .x. F ) ) = .0. -> ( x ` j ) = Y ) ) )
202 201 ralbidva 
 |-  ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( A. x e. L ( ( W gsum ( x oF .x. F ) ) = .0. -> ( x ` j ) = ( ( I X. { Y } ) ` j ) ) <-> A. x e. L ( ( W gsum ( x oF .x. F ) ) = .0. -> ( x ` j ) = Y ) ) )
203 176 195 202 3bitr4d 
 |-  ( ( ( 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 gsum ( x oF .x. F ) ) = .0. -> ( x ` j ) = ( ( I X. { Y } ) ` j ) ) ) )
204 203 ralbidva 
 |-  ( ( 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 gsum ( x oF .x. F ) ) = .0. -> ( x ` j ) = ( ( I X. { Y } ) ` j ) ) ) )
205 1 3 155 2 15 5 islindf2 
 |-  ( ( 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 } ) ) ) ) )
206 167 15 6 frlmbasf 
 |-  ( ( I e. X /\ x e. L ) -> x : I --> ( Base ` R ) )
207 206 3ad2antl2 
 |-  ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ x e. L ) -> x : I --> ( Base ` R ) )
208 207 ffnd 
 |-  ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ x e. L ) -> x Fn I )
209 fnconstg 
 |-  ( Y e. _V -> ( I X. { Y } ) Fn I )
210 197 209 ax-mp 
 |-  ( I X. { Y } ) Fn I
211 eqfnfv 
 |-  ( ( x Fn I /\ ( I X. { Y } ) Fn I ) -> ( x = ( I X. { Y } ) <-> A. j e. I ( x ` j ) = ( ( I X. { Y } ) ` j ) ) )
212 208 210 211 sylancl 
 |-  ( ( ( 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 ) ) )
213 212 imbi2d 
 |-  ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ x e. L ) -> ( ( ( W gsum ( x oF .x. F ) ) = .0. -> x = ( I X. { Y } ) ) <-> ( ( W gsum ( x oF .x. F ) ) = .0. -> A. j e. I ( x ` j ) = ( ( I X. { Y } ) ` j ) ) ) )
214 213 ralbidva 
 |-  ( ( W e. LMod /\ I e. X /\ F : I --> B ) -> ( A. x e. L ( ( W gsum ( x oF .x. F ) ) = .0. -> x = ( I X. { Y } ) ) <-> A. x e. L ( ( W gsum ( x oF .x. F ) ) = .0. -> A. j e. I ( x ` j ) = ( ( I X. { Y } ) ` j ) ) ) )
215 r19.21v 
 |-  ( A. j e. I ( ( W gsum ( x oF .x. F ) ) = .0. -> ( x ` j ) = ( ( I X. { Y } ) ` j ) ) <-> ( ( W gsum ( x oF .x. F ) ) = .0. -> A. j e. I ( x ` j ) = ( ( I X. { Y } ) ` j ) ) )
216 215 ralbii 
 |-  ( A. x e. L A. j e. I ( ( W gsum ( x oF .x. F ) ) = .0. -> ( x ` j ) = ( ( I X. { Y } ) ` j ) ) <-> A. x e. L ( ( W gsum ( x oF .x. F ) ) = .0. -> A. j e. I ( x ` j ) = ( ( I X. { Y } ) ` j ) ) )
217 ralcom 
 |-  ( A. x e. L A. j e. I ( ( W gsum ( x oF .x. F ) ) = .0. -> ( x ` j ) = ( ( I X. { Y } ) ` j ) ) <-> A. j e. I A. x e. L ( ( W gsum ( x oF .x. F ) ) = .0. -> ( x ` j ) = ( ( I X. { Y } ) ` j ) ) )
218 216 217 bitr3i 
 |-  ( A. x e. L ( ( W gsum ( x oF .x. F ) ) = .0. -> A. j e. I ( x ` j ) = ( ( I X. { Y } ) ` j ) ) <-> A. j e. I A. x e. L ( ( W gsum ( x oF .x. F ) ) = .0. -> ( x ` j ) = ( ( I X. { Y } ) ` j ) ) )
219 214 218 bitrdi 
 |-  ( ( W e. LMod /\ I e. X /\ F : I --> B ) -> ( A. x e. L ( ( W gsum ( x oF .x. F ) ) = .0. -> x = ( I X. { Y } ) ) <-> A. j e. I A. x e. L ( ( W gsum ( x oF .x. F ) ) = .0. -> ( x ` j ) = ( ( I X. { Y } ) ` j ) ) ) )
220 204 205 219 3bitr4d 
 |-  ( ( W e. LMod /\ I e. X /\ F : I --> B ) -> ( F LIndF W <-> A. x e. L ( ( W gsum ( x oF .x. F ) ) = .0. -> x = ( I X. { Y } ) ) ) )