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 incom 
 |-  ( ( I \ { j } ) i^i { j } ) = ( { j } i^i ( I \ { j } ) )
69 disjdif 
 |-  ( { j } i^i ( I \ { j } ) ) = (/)
70 68 69 eqtri 
 |-  ( ( I \ { j } ) i^i { j } ) = (/)
71 70 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 } ) = (/) )
72 difsnid 
 |-  ( j e. I -> ( ( I \ { j } ) u. { j } ) = I )
73 72 eqcomd 
 |-  ( j e. I -> I = ( ( I \ { j } ) u. { j } ) )
74 42 73 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 } ) )
75 1 4 39 24 25 45 67 71 74 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 } ) ) ) )
76 vex 
 |-  y e. _V
77 snex 
 |-  { <. j , l >. } e. _V
78 76 77 unex 
 |-  ( y u. { <. j , l >. } ) e. _V
79 simpl3 
 |-  ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> F : I --> B )
80 simpl2 
 |-  ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> I e. X )
81 fex 
 |-  ( ( F : I --> B /\ I e. X ) -> F e. _V )
82 79 80 81 syl2anc 
 |-  ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> F e. _V )
83 82 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 )
84 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 } ) ) ) )
85 78 83 84 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 } ) ) ) )
86 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 } ) )
87 neldifsn 
 |-  -. j e. ( I \ { j } )
88 fsnunres 
 |-  ( ( y Fn ( I \ { j } ) /\ -. j e. ( I \ { j } ) ) -> ( ( y u. { <. j , l >. } ) |` ( I \ { j } ) ) = y )
89 86 87 88 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 )
90 89 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 } ) ) ) )
91 85 90 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 } ) ) ) )
92 91 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 } ) ) ) ) )
93 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 )
94 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 ) >. } )
95 93 42 94 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 ) >. } )
96 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 )
97 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 )
98 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 ) ) )
99 96 97 25 42 98 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 ) ) )
100 fndm 
 |-  ( y Fn ( I \ { j } ) -> dom y = ( I \ { j } ) )
101 100 eleq2d 
 |-  ( y Fn ( I \ { j } ) -> ( j e. dom y <-> j e. ( I \ { j } ) ) )
102 87 101 mtbiri 
 |-  ( y Fn ( I \ { j } ) -> -. j e. dom y )
103 vex 
 |-  j e. _V
104 vex 
 |-  l e. _V
105 fsnunfv 
 |-  ( ( j e. _V /\ l e. _V /\ -. j e. dom y ) -> ( ( y u. { <. j , l >. } ) ` j ) = l )
106 103 104 105 mp3an12 
 |-  ( -. j e. dom y -> ( ( y u. { <. j , l >. } ) ` j ) = l )
107 86 102 106 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 )
108 107 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 ) ) )
109 99 108 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 ) ) )
110 109 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 ) ) >. )
111 110 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 ) ) >. } )
112 ovex 
 |-  ( l .x. ( F ` j ) ) e. _V
113 fmptsn 
 |-  ( ( j e. _V /\ ( l .x. ( F ` j ) ) e. _V ) -> { <. j , ( l .x. ( F ` j ) ) >. } = ( x e. { j } |-> ( l .x. ( F ` j ) ) ) )
114 103 112 113 mp2an 
 |-  { <. j , ( l .x. ( F ` j ) ) >. } = ( x e. { j } |-> ( l .x. ( F ` j ) ) )
115 114 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 ) ) ) )
116 95 111 115 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 ) ) ) )
117 116 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 ) ) ) ) )
118 cmnmnd 
 |-  ( W e. CMnd -> W e. Mnd )
119 8 23 118 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 )
120 103 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 )
121 eqidd 
 |-  ( x = j -> ( l .x. ( F ` j ) ) = ( l .x. ( F ` j ) ) )
122 1 121 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 ) ) )
123 119 120 22 122 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 ) ) )
124 117 123 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 ) ) )
125 92 124 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 ) ) ) )
126 75 125 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 ) ) )
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 ) ) -> ( ( ( 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. ) )
128 18 41 127 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. ) )
129 107 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 ) )
130 129 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 ) )
131 128 130 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 ) ) )
132 131 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 ) ) )
133 132 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 ) ) ) )
134 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 ) ) )
135 134 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 ) ) ) )
136 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 ) )
137 136 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 ) ) ) )
138 133 135 137 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 ) ) ) )
139 138 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 ) ) ) )
140 breq1 
 |-  ( x = ( y u. { <. j , l >. } ) -> ( x finSupp Y <-> ( y u. { <. j , l >. } ) finSupp Y ) )
141 oveq1 
 |-  ( x = ( y u. { <. j , l >. } ) -> ( x oF .x. F ) = ( ( y u. { <. j , l >. } ) oF .x. F ) )
142 141 oveq2d 
 |-  ( x = ( y u. { <. j , l >. } ) -> ( W gsum ( x oF .x. F ) ) = ( W gsum ( ( y u. { <. j , l >. } ) oF .x. F ) ) )
143 142 eqeq1d 
 |-  ( x = ( y u. { <. j , l >. } ) -> ( ( W gsum ( x oF .x. F ) ) = .0. <-> ( W gsum ( ( y u. { <. j , l >. } ) oF .x. F ) ) = .0. ) )
144 fveq1 
 |-  ( x = ( y u. { <. j , l >. } ) -> ( x ` j ) = ( ( y u. { <. j , l >. } ) ` j ) )
145 144 eqeq1d 
 |-  ( x = ( y u. { <. j , l >. } ) -> ( ( x ` j ) = Y <-> ( ( y u. { <. j , l >. } ) ` j ) = Y ) )
146 143 145 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 ) ) )
147 140 146 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 ) ) ) )
148 147 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 ) ) ) )
149 148 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 ) ) ) )
150 139 149 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 ) ) ) )
151 breq1 
 |-  ( z = x -> ( z finSupp Y <-> x finSupp Y ) )
152 151 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 ) ) )
153 150 152 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 ) ) )
154 resima 
 |-  ( ( F |` ( I \ { j } ) ) " ( I \ { j } ) ) = ( F " ( I \ { j } ) )
155 154 eqcomi 
 |-  ( F " ( I \ { j } ) ) = ( ( F |` ( I \ { j } ) ) " ( I \ { j } ) )
156 155 fveq2i 
 |-  ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) = ( ( LSpan ` W ) ` ( ( F |` ( I \ { j } ) ) " ( I \ { j } ) ) )
157 156 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 } ) ) ) )
158 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
159 79 32 33 sylancl 
 |-  ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( F |` ( I \ { j } ) ) : ( I \ { j } ) --> B )
160 simpl1 
 |-  ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> W e. LMod )
161 26 3ad2ant2 
 |-  ( ( W e. LMod /\ I e. X /\ F : I --> B ) -> ( I \ { j } ) e. _V )
162 161 adantr 
 |-  ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( I \ { j } ) e. _V )
163 158 1 15 2 5 3 159 160 162 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 } ) ) ) ) ) ) )
164 157 163 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 } ) ) ) ) ) ) )
165 164 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 ) ) )
166 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 ) )
167 165 166 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 ) ) )
168 167 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 ) ) )
169 2 fvexi 
 |-  R e. _V
170 eqid 
 |-  ( R freeLMod I ) = ( R freeLMod I )
171 eqid 
 |-  { z e. ( ( Base ` R ) ^m I ) | z finSupp Y } = { z e. ( ( Base ` R ) ^m I ) | z finSupp Y }
172 170 15 5 171 frlmbas 
 |-  ( ( R e. _V /\ I e. X ) -> { z e. ( ( Base ` R ) ^m I ) | z finSupp Y } = ( Base ` ( R freeLMod I ) ) )
173 169 172 mpan 
 |-  ( I e. X -> { z e. ( ( Base ` R ) ^m I ) | z finSupp Y } = ( Base ` ( R freeLMod I ) ) )
174 173 3ad2ant2 
 |-  ( ( W e. LMod /\ I e. X /\ F : I --> B ) -> { z e. ( ( Base ` R ) ^m I ) | z finSupp Y } = ( Base ` ( R freeLMod I ) ) )
175 174 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 ) ) )
176 6 175 eqtr4id 
 |-  ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> L = { z e. ( ( Base ` R ) ^m I ) | z finSupp Y } )
177 176 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 ) ) )
178 153 168 177 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 ) ) )
179 7 178 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 ) ) )
180 2 lmodfgrp 
 |-  ( W e. LMod -> R e. Grp )
181 15 5 14 grpinvnzcl 
 |-  ( ( R e. Grp /\ l e. ( ( Base ` R ) \ { Y } ) ) -> ( ( invg ` R ) ` l ) e. ( ( Base ` R ) \ { Y } ) )
182 180 181 sylan 
 |-  ( ( W e. LMod /\ l e. ( ( Base ` R ) \ { Y } ) ) -> ( ( invg ` R ) ` l ) e. ( ( Base ` R ) \ { Y } ) )
183 15 5 14 grpinvnzcl 
 |-  ( ( R e. Grp /\ k e. ( ( Base ` R ) \ { Y } ) ) -> ( ( invg ` R ) ` k ) e. ( ( Base ` R ) \ { Y } ) )
184 180 183 sylan 
 |-  ( ( W e. LMod /\ k e. ( ( Base ` R ) \ { Y } ) ) -> ( ( invg ` R ) ` k ) e. ( ( Base ` R ) \ { Y } ) )
185 eldifi 
 |-  ( k e. ( ( Base ` R ) \ { Y } ) -> k e. ( Base ` R ) )
186 15 14 grpinvinv 
 |-  ( ( R e. Grp /\ k e. ( Base ` R ) ) -> ( ( invg ` R ) ` ( ( invg ` R ) ` k ) ) = k )
187 180 185 186 syl2an 
 |-  ( ( W e. LMod /\ k e. ( ( Base ` R ) \ { Y } ) ) -> ( ( invg ` R ) ` ( ( invg ` R ) ` k ) ) = k )
188 187 eqcomd 
 |-  ( ( W e. LMod /\ k e. ( ( Base ` R ) \ { Y } ) ) -> k = ( ( invg ` R ) ` ( ( invg ` R ) ` k ) ) )
189 fveq2 
 |-  ( l = ( ( invg ` R ) ` k ) -> ( ( invg ` R ) ` l ) = ( ( invg ` R ) ` ( ( invg ` R ) ` k ) ) )
190 189 rspceeqv 
 |-  ( ( ( ( invg ` R ) ` k ) e. ( ( Base ` R ) \ { Y } ) /\ k = ( ( invg ` R ) ` ( ( invg ` R ) ` k ) ) ) -> E. l e. ( ( Base ` R ) \ { Y } ) k = ( ( invg ` R ) ` l ) )
191 184 188 190 syl2anc 
 |-  ( ( W e. LMod /\ k e. ( ( Base ` R ) \ { Y } ) ) -> E. l e. ( ( Base ` R ) \ { Y } ) k = ( ( invg ` R ) ` l ) )
192 oveq1 
 |-  ( k = ( ( invg ` R ) ` l ) -> ( k .x. ( F ` j ) ) = ( ( ( invg ` R ) ` l ) .x. ( F ` j ) ) )
193 192 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 } ) ) ) ) )
194 193 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 } ) ) ) ) )
195 194 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 } ) ) ) ) )
196 182 191 195 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 } ) ) ) ) )
197 196 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 } ) ) ) ) )
198 197 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 } ) ) ) ) )
199 simplr 
 |-  ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ x e. L ) -> j e. I )
200 5 fvexi 
 |-  Y e. _V
201 200 fvconst2 
 |-  ( j e. I -> ( ( I X. { Y } ) ` j ) = Y )
202 199 201 syl 
 |-  ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ x e. L ) -> ( ( I X. { Y } ) ` j ) = Y )
203 202 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 ) )
204 203 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 ) ) )
205 204 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 ) ) )
206 179 198 205 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 ) ) ) )
207 206 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 ) ) ) )
208 1 3 158 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 } ) ) ) ) )
209 170 15 6 frlmbasf 
 |-  ( ( I e. X /\ x e. L ) -> x : I --> ( Base ` R ) )
210 209 3ad2antl2 
 |-  ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ x e. L ) -> x : I --> ( Base ` R ) )
211 210 ffnd 
 |-  ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ x e. L ) -> x Fn I )
212 fnconstg 
 |-  ( Y e. _V -> ( I X. { Y } ) Fn I )
213 200 212 ax-mp 
 |-  ( I X. { Y } ) Fn I
214 eqfnfv 
 |-  ( ( x Fn I /\ ( I X. { Y } ) Fn I ) -> ( x = ( I X. { Y } ) <-> A. j e. I ( x ` j ) = ( ( I X. { Y } ) ` j ) ) )
215 211 213 214 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 ) ) )
216 215 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 ) ) ) )
217 216 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 ) ) ) )
218 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 ) ) )
219 218 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 ) ) )
220 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 ) ) )
221 219 220 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 ) ) )
222 217 221 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 ) ) ) )
223 207 208 222 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 } ) ) ) )