MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  islindf4 Structured version   Visualization version   Unicode version
Theorem islindf4 20177
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 4324 . . . . 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 1100 . . . . . . . . . . . . . . . 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 802 . . . . . . . . . . . . . . . 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 6357 . . . . . . . . . . . . . . . . . 18 |- ( ( F : I --> B /\ j e. I ) -> ( F ` j ) e. B )
543ad2antl3 1225 . . . . . . . . . . . . . . . . 17 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( F ` j ) e. B )
65adantr 481 . . . . . . . . . . . . . . . 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 2622 . . . . . . . . . . . . . . . . 17 |- ( invg ` W ) = ( invg ` W )
11 eqid 2622 . . . . . . . . . . . . . . . . 17 |- ( invg ` R ) = ( invg ` R )
12 eqid 2622 . . . . . . . . . . . . . . . . 17 |- ( Base ` R ) = ( Base ` R )
137, 8, 9, 10, 11, 12lmodvsinv 19036 . . . . . . . . . . . . . . . 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 1326 . . . . . . . . . . . . . . 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 2624 . . . . . . . . . . . . . 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 18870 . . . . . . . . . . . . . . . 16 |- ( W e. LMod -> W e. Grp )
172, 16syl 17 . . . . . . . . . . . . . . 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 18880 . . . . . . . . . . . . . . . 16 |- ( ( W e. LMod /\ l e. ( Base ` R ) /\ ( F ` j ) e. B ) -> ( l .x. ( F ` j ) ) e. B )
192, 3, 6, 18syl3anc 1326 . . . . . . . . . . . . . . 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 18911 . . . . . . . . . . . . . . . . 17 |- ( W e. LMod -> W e. CMnd )
222, 21syl 17 . . . . . . . . . . . . . . . 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 1101 . . . . . . . . . . . . . . . . 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 4808 . . . . . . . . . . . . . . . . 17 |- ( I e. X -> ( I \ { j } ) e. _V )
2523, 24syl 17 . . . . . . . . . . . . . . . 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 803 . . . . . . . . . . . . . . . . . 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 7879 . . . . . . . . . . . . . . . . . 18 |- ( y e. ( ( Base ` R ) ^m ( I \ { j } ) ) -> y : ( I \ { j } ) --> ( Base ` R ) )
2826, 27syl 17 . . . . . . . . . . . . . . . . 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 1102 . . . . . . . . . . . . . . . . . 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 3737 . . . . . . . . . . . . . . . . . 18 |- ( I \ { j } ) C_ I
31 fssres 6070 . . . . . . . . . . . . . . . . . 18 |- ( ( F : I --> B /\ ( I \ { j } ) C_ I ) -> ( F |` ( I \ { j } ) ) : ( I \ { j } ) --> B )
3229, 30, 31sylancl 694 . . . . . . . . . . . . . . . . 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 18902 . . . . . . . . . . . . . . . 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 796 . . . . . . . . . . . . . . . . 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 18903 . . . . . . . . . . . . . . . 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 18316 . . . . . . . . . . . . . . 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 2622 . . . . . . . . . . . . . . . 16 |- ( +g ` W ) = ( +g ` W )
397, 38, 20, 10grpinvid2 17471 . . . . . . . . . . . . . . 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 1326 . . . . . . . . . . . . . 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 792 . . . . . . . . . . . . . . . . . . 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 6452 . . . . . . . . . . . . . . . . . . 19 |- ( ( y : ( I \ { j } ) --> ( Base ` R ) /\ j e. I /\ l e. ( Base ` R ) ) -> ( y u. { <. j , l >. } ) : I --> ( Base ` R ) )
4328, 41, 3, 42syl3anc 1326 . . . . . . . . . . . . . . . . . 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 18902 . . . . . . . . . . . . . . . . 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 477 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> j e. I )
46 simpl 473 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) -> l e. ( Base ` R ) )
4745, 46anim12i 590 . . . . . . . . . . . . . . . . . . . . . 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 7881 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y e. ( ( Base ` R ) ^m ( I \ { j } ) ) -> Fun y )
49 fdm 6051 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( y : ( I \ { j } ) --> ( Base ` R ) -> dom y = ( I \ { j } ) )
50 neldifsnd 4322 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( dom y = ( I \ { j } ) -> -. j e. ( I \ { j } ) )
51 df-nel 2898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( j e/ dom y <-> -. j e. dom y )
52 eleq2 2690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( dom y = ( I \ { j } ) -> ( j e. dom y <-> j e. ( I \ { j } ) ) )
5352notbid 308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( dom y = ( I \ { j } ) -> ( -. j e. dom y <-> -. j e. ( I \ { j } ) ) )
5451, 53syl5bb 272 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( dom y = ( I \ { j } ) -> ( j e/ dom y <-> -. j e. ( I \ { j } ) ) )
5550, 54mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( dom y = ( I \ { j } ) -> j e/ dom y )
5649, 55syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y : ( I \ { j } ) --> ( Base ` R ) -> j e/ dom y )
5727, 56syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y e. ( ( Base ` R ) ^m ( I \ { j } ) ) -> j e/ dom y )
5848, 57jca 554 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y e. ( ( Base ` R ) ^m ( I \ { j } ) ) -> ( Fun y /\ j e/ dom y ) )
5958adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( l e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( I \ { j } ) ) ) -> ( Fun y /\ j e/ dom y ) )
6059adantl 482 . . . . . . . . . . . . . . . . . . . . . 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 554 . . . . . . . . . . . . . . . . . . . . 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 8299 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( j e. I /\ l e. ( Base ` R ) ) /\ ( Fun y /\ j e/ dom y ) ) -> ( ( y u. { <. j , l >. } ) finSupp Y <-> y finSupp Y ) )
6362bicomd 213 . . . . . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . . . . 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 219 . . . . . . . . . . . . . . . . . . 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 649 . . . . . . . . . . . . . . . . . 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 18903 . . . . . . . . . . . . . . . . 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 3805 . . . . . . . . . . . . . . . . . . 19 |- ( ( I \ { j } ) i^i { j } ) = ( { j } i^i ( I \ { j } ) )
69 disjdif 4040 . . . . . . . . . . . . . . . . . . 19 |- ( { j } i^i ( I \ { j } ) ) = (/)
7068, 69eqtri 2644 . . . . . . . . . . . . . . . . . 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 4341 . . . . . . . . . . . . . . . . . . 19 |- ( j e. I -> ( ( I \ { j } ) u. { j } ) = I )
7372eqcomd 2628 . . . . . . . . . . . . . . . . . 18 |- ( j e. I -> I = ( ( I \ { j } ) u. { j } ) )
7441, 73syl 17 . . . . . . . . . . . . . . . . 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 18328 . . . . . . . . . . . . . . . 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 3203 . . . . . . . . . . . . . . . . . . . . 21 |- y e. _V
77 snex 4908 . . . . . . . . . . . . . . . . . . . . 21 |- { <. j , l >. } e. _V
7876, 77unex 6956 . . . . . . . . . . . . . . . . . . . 20 |- ( y u. { <. j , l >. } ) e. _V
79 simpl3 1066 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> F : I --> B )
80 simpl2 1065 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> I e. X )
81 fex 6490 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( F : I --> B /\ I e. X ) -> F e. _V )
8279, 80, 81syl2anc 693 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> F e. _V )
8382adantr 481 . . . . . . . . . . . . . . . . . . . 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 7163 . . . . . . . . . . . . . . . . . . . 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 695 . . . . . . . . . . . . . . . . . . 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 6045 . . . . . . . . . . . . . . . . . . . . . 22 |- ( y : ( I \ { j } ) --> ( Base ` R ) -> y Fn ( I \ { j } ) )
8728, 86syl 17 . . . . . . . . . . . . . . . . . . . . 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 4321 . . . . . . . . . . . . . . . . . . . . 21 |- -. j e. ( I \ { j } )
89 fsnunres 6454 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( y Fn ( I \ { j } ) /\ -. j e. ( I \ { j } ) ) -> ( ( y u. { <. j , l >. } ) |` ( I \ { j } ) ) = y )
9087, 88, 89sylancl 694 . . . . . . . . . . . . . . . . . . . 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 6665 . . . . . . . . . . . . . . . . . . 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 2656 . . . . . . . . . . . . . . . . . 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 6666 . . . . . . . . . . . . . . . . 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 6045 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( y u. { <. j , l >. } ) oF .x. F ) : I --> B -> ( ( y u. { <. j , l >. } ) oF .x. F ) Fn I )
9544, 94syl 17 . . . . . . . . . . . . . . . . . . . . 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 6425 . . . . . . . . . . . . . . . . . . . . 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 693 . . . . . . . . . . . . . . . . . . . 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 6045 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( y u. { <. j , l >. } ) : I --> ( Base ` R ) -> ( y u. { <. j , l >. } ) Fn I )
9943, 98syl 17 . . . . . . . . . . . . . . . . . . . . . . . 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 6045 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( F : I --> B -> F Fn I )
10129, 100syl 17 . . . . . . . . . . . . . . . . . . . . . . . 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 6911 . . . . . . . . . . . . . . . . . . . . . . . 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 1327 . . . . . . . . . . . . . . . . . . . . . . 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 5990 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( y Fn ( I \ { j } ) -> dom y = ( I \ { j } ) )
105104eleq2d 2687 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y Fn ( I \ { j } ) -> ( j e. dom y <-> j e. ( I \ { j } ) ) )
10688, 105mtbiri 317 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y Fn ( I \ { j } ) -> -. j e. dom y )
107 vex 3203 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- j e. _V
108 vex 3203 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- l e. _V
109 fsnunfv 6453 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( j e. _V /\ l e. _V /\ -. j e. dom y ) -> ( ( y u. { <. j , l >. } ) ` j ) = l )
110107, 108, 109mp3an12 1414 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( -. j e. dom y -> ( ( y u. { <. j , l >. } ) ` j ) = l )
11187, 106, 1103syl 18 . . . . . . . . . . . . . . . . . . . . . . . 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 6665 . . . . . . . . . . . . . . . . . . . . . . 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 2656 . . . . . . . . . . . . . . . . . . . . . 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 4409 . . . . . . . . . . . . . . . . . . . . 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 4189 . . . . . . . . . . . . . . . . . . . 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 6678 . . . . . . . . . . . . . . . . . . . . . 22 |- ( l .x. ( F ` j ) ) e. _V
117 fmptsn 6433 . . . . . . . . . . . . . . . . . . . . . 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 708 . . . . . . . . . . . . . . . . . . . . 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 2660 . . . . . . . . . . . . . . . . . . 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 6666 . . . . . . . . . . . . . . . . . 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 18208 . . . . . . . . . . . . . . . . . . . 20 |- ( W e. CMnd -> W e. Mnd )
12322, 122syl 17 . . . . . . . . . . . . . . . . . . 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 2623 . . . . . . . . . . . . . . . . . . . 20 |- ( x = j -> ( l .x. ( F ` j ) ) = ( l .x. ( F ` j ) ) )
1267, 125gsumsn 18354 . . . . . . . . . . . . . . . . . . 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 1326 . . . . . . . . . . . . . . . . . 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 2656 . . . . . . . . . . . . . . . . 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 6668 . . . . . . . . . . . . . . . 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 2657 . . . . . . . . . . . . . . 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 2624 . . . . . . . . . . . . . 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 294 . . . . . . . . . . . . 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 2628 . . . . . . . . . . . . . 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 2624 . . . . . . . . . . . . 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 334 . . . . . . . . . . . 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 680 . . . . . . . . . . 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 723 . . . . . . . . . 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 462 . . . . . . . . . . 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 213 . . . . . . . . . . 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 331 . . . . . . . . . 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 300 . . . . . . . . 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 2988 . . . . . . . 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 4656 . . . . . . . . . . 11 |- ( x = ( y u. { <. j , l >. } ) -> ( x finSupp Y <-> ( y u. { <. j , l >. } ) finSupp Y ) )
145 oveq1 6657 . . . . . . . . . . . . . 14 |- ( x = ( y u. { <. j , l >. } ) -> ( x oF .x. F ) = ( ( y u. { <. j , l >. } ) oF .x. F ) )
146145oveq2d 6666 . . . . . . . . . . . . 13 |- ( x = ( y u. { <. j , l >. } ) -> ( W gsumg ( x oF .x. F ) ) = ( W gsumg ( ( y u. { <. j , l >. } ) oF .x. F ) ) )
147146eqeq1d 2624 . . . . . . . . . . . 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 6190 . . . . . . . . . . . . 13 |- ( x = ( y u. { <. j , l >. } ) -> ( x ` j ) = ( ( y u. { <. j , l >. } ) ` j ) )
149148eqeq1d 2624 . . . . . . . . . . . 12 |- ( x = ( y u. { <. j , l >. } ) -> ( ( x ` j ) = Y <-> ( ( y u. { <. j , l >. } ) ` j ) = Y ) )
150147, 149imbi12d 334 . . . . . . . . . . 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 334 . . . . . . . . . 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 7907 . . . . . . . . 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 482 . . . . . . . 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 271 . . . . . . 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 4656 . . . . . . . 8 |- ( z = x -> ( z finSupp Y <-> x finSupp Y ) )
156155ralrab 3368 . . . . . . 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 278 . . . . . 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 5431 . . . . . . . . . . . . 13 |- ( ( F |` ( I \ { j } ) ) " ( I \ { j } ) ) = ( F " ( I \ { j } ) )
159158eqcomi 2631 . . . . . . . . . . . 12 |- ( F " ( I \ { j } ) ) = ( ( F |` ( I \ { j } ) ) " ( I \ { j } ) )
160159fveq2i 6194 . . . . . . . . . . 11 |- ( ( LSpan ` W ) ` ( F " ( I \ { j } ) ) ) = ( ( LSpan ` W ) ` ( ( F |` ( I \ { j } ) ) " ( I \ { j } ) ) )
161160eleq2i 2693 . . . . . . . . . 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 2622 . . . . . . . . . . 11 |- ( LSpan ` W ) = ( LSpan ` W )
16379, 30, 31sylancl 694 . . . . . . . . . . 11 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> ( F |` ( I \ { j } ) ) : ( I \ { j } ) --> B )
164 simpl1 1064 . . . . . . . . . . 11 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> W e. LMod )
165243ad2ant2 1083 . . . . . . . . . . . 12 |- ( ( W e. LMod /\ I e. X /\ F : I --> B ) -> ( I \ { j } ) e. _V )
166165adantr 481 . . . . . . . . . . 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 20141 . . . . . . . . . 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 272 . . . . . . . . 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 331 . . . . . . . 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 3023 . . . . . . . 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 278 . . . . . . 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 2986 . . . . . 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 6201 . . . . . . . . . . . 12 |- (Scalar ` W ) e. _V
1748, 173eqeltri 2697 . . . . . . . . . . 11 |- R e. _V
175 eqid 2622 . . . . . . . . . . . 12 |- ( R freeLMod I ) = ( R freeLMod I )
176 eqid 2622 . . . . . . . . . . . 12 |- { z e. ( ( Base ` R ) ^m I ) | z finSupp Y } = { z e. ( ( Base ` R ) ^m I ) | z finSupp Y }
177175, 12, 34, 176frlmbas 20099 . . . . . . . . . . 11 |- ( ( R e. _V /\ I e. X ) -> { z e. ( ( Base ` R ) ^m I ) | z finSupp Y } = ( Base ` ( R freeLMod I ) ) )
178174, 177mpan 706 . . . . . . . . . 10 |- ( I e. X -> { z e. ( ( Base ` R ) ^m I ) | z finSupp Y } = ( Base ` ( R freeLMod I ) ) )
1791783ad2ant2 1083 . . . . . . . . 9 |- ( ( W e. LMod /\ I e. X /\ F : I --> B ) -> { z e. ( ( Base ` R ) ^m I ) | z finSupp Y } = ( Base ` ( R freeLMod I ) ) )
180179adantr 481 . . . . . . . 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 2675 . . . . . . 7 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) -> L = { z e. ( ( Base ` R ) ^m I ) | z finSupp Y } )
183182raleqdv 3144 . . . . . 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 300 . . . . 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 272 . . . 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 18872 . . . . . . . 8 |- ( W e. LMod -> R e. Grp )
18712, 34, 11grpinvnzcl 17487 . . . . . . . 8 |- ( ( R e. Grp /\ l e. ( ( Base ` R ) \ { Y } ) ) -> ( ( invg ` R ) ` l ) e. ( ( Base ` R ) \ { Y } ) )
188186, 187sylan 488 . . . . . . 7 |- ( ( W e. LMod /\ l e. ( ( Base ` R ) \ { Y } ) ) -> ( ( invg ` R ) ` l ) e. ( ( Base ` R ) \ { Y } ) )
18912, 34, 11grpinvnzcl 17487 . . . . . . . . 9 |- ( ( R e. Grp /\ k e. ( ( Base ` R ) \ { Y } ) ) -> ( ( invg ` R ) ` k ) e. ( ( Base ` R ) \ { Y } ) )
190186, 189sylan 488 . . . . . . . 8 |- ( ( W e. LMod /\ k e. ( ( Base ` R ) \ { Y } ) ) -> ( ( invg ` R ) ` k ) e. ( ( Base ` R ) \ { Y } ) )
191 eldifi 3732 . . . . . . . . . 10 |- ( k e. ( ( Base ` R ) \ { Y } ) -> k e. ( Base ` R ) )
19212, 11grpinvinv 17482 . . . . . . . . . 10 |- ( ( R e. Grp /\ k e. ( Base ` R ) ) -> ( ( invg ` R ) ` ( ( invg ` R ) ` k ) ) = k )
193186, 191, 192syl2an 494 . . . . . . . . 9 |- ( ( W e. LMod /\ k e. ( ( Base ` R ) \ { Y } ) ) -> ( ( invg ` R ) ` ( ( invg ` R ) ` k ) ) = k )
194193eqcomd 2628 . . . . . . . 8 |- ( ( W e. LMod /\ k e. ( ( Base ` R ) \ { Y } ) ) -> k = ( ( invg ` R ) ` ( ( invg ` R ) ` k ) ) )
195 fveq2 6191 . . . . . . . . . 10 |- ( l = ( ( invg ` R ) ` k ) -> ( ( invg ` R ) ` l ) = ( ( invg ` R ) ` ( ( invg ` R ) ` k ) ) )
196195eqeq2d 2632 . . . . . . . . 9 |- ( l = ( ( invg ` R ) ` k ) -> ( k = ( ( invg ` R ) ` l ) <-> k = ( ( invg ` R ) ` ( ( invg ` R ) ` k ) ) ) )
197196rspcev 3309 . . . . . . . 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 693 . . . . . . 7 |- ( ( W e. LMod /\ k e. ( ( Base ` R ) \ { Y } ) ) -> E. l e. ( ( Base ` R ) \ { Y } ) k = ( ( invg ` R ) ` l ) )
199 oveq1 6657 . . . . . . . . . 10 |- ( k = ( ( invg ` R ) ` l ) -> ( k .x. ( F ` j ) ) = ( ( ( invg ` R ) ` l ) .x. ( F ` j ) ) )
200199eleq1d 2686 . . . . . . . . 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 308 . . . . . . . 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 482 . . . . . . 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 4879 . . . . . 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 1082 . . . . 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 481 . . . 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 792 . . . . . . . 8 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ x e. L ) -> j e. I )
207 fvex 6201 . . . . . . . . . 10 |- ( 0g ` R ) e. _V
20834, 207eqeltri 2697 . . . . . . . . 9 |- Y e. _V
209208fvconst2 6469 . . . . . . . 8 |- ( j e. I -> ( ( I X. { Y } ) ` j ) = Y )
210206, 209syl 17 . . . . . . 7 |- ( ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ j e. I ) /\ x e. L ) -> ( ( I X. { Y } ) ` j ) = Y )
211210eqeq2d 2632 . . . . . 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 330 . . . . 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 2985 . . . 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 300 . . 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 2985 . 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 20153 . 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 20104 . . . . . . . 8 |- ( ( I e. X /\ x e. L ) -> x : I --> ( Base ` R ) )
2182173ad2antl2 1224 . . . . . . 7 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ x e. L ) -> x : I --> ( Base ` R ) )
219 ffn 6045 . . . . . . 7 |- ( x : I --> ( Base ` R ) -> x Fn I )
220218, 219syl 17 . . . . . 6 |- ( ( ( W e. LMod /\ I e. X /\ F : I --> B ) /\ x e. L ) -> x Fn I )
221 fnconstg 6093 . . . . . . 7 |- ( Y e. _V -> ( I X. { Y } ) Fn I )
222208, 221ax-mp 5 . . . . . 6 |- ( I X. { Y } ) Fn I
223 eqfnfv 6311 . . . . . 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 694 . . . . 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 330 . . . 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 2985 . . 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 2960 . . . . 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 2980 . . . 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 3098 . . . 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 266 . . 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 276 . 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 300 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 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   e/ wnel 2897   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   \ cdif 3571   u. cun 3572   i^i cin 3573   C_ wss 3574   (/)c0 3915   {csn 4177   <.cop 4183   class class class wbr 4653   |-> cmpt 4729   X. cxp 5112   dom cdm 5114   |` cres 5116   "cima 5117   Fun wfun 5882   Fn wfn 5883   -->wf 5884   ` cfv 5888  (class class class)co 6650   oFcof 6895   ^m cmap 7857   finSupp cfsupp 8275   Basecbs 15857   +g cplusg 15941  Scalarcsca 15944   .scvsca 15945   0gc0g 16100   gsumg cgsu 16101   Mndcmnd 17294   Grpcgrp 17422   invgcminusg 17423  CMndccmn 18193   LModclmod 18863   LSpanclspn 18971   freeLMod cfrlm 20090   LIndF clindf 20143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-sup 8348  df-oi 8415  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-fz 12327  df-fzo 12466  df-seq 12802  df-hash 13118  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-hom 15966  df-cco 15967  df-0g 16102  df-gsum 16103  df-prds 16108  df-pws 16110  df-mre 16246  df-mrc 16247  df-acs 16249  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-mhm 17335  df-submnd 17336  df-grp 17425  df-minusg 17426  df-sbg 17427  df-mulg 17541  df-subg 17591  df-ghm 17658  df-cntz 17750  df-cmn 18195  df-abl 18196  df-mgp 18490  df-ur 18502  df-ring 18549  df-subrg 18778  df-lmod 18865  df-lss 18933  df-lsp 18972  df-lmhm 19022  df-lbs 19075  df-sra 19172  df-rgmod 19173  df-nzr 19258  df-dsmm 20076  df-frlm 20091  df-uvc 20122  df-lindf 20145
This theorem is referenced by:  islindf5  20178  matunitlindflem1  33405  aacllem  42547
  Copyright terms: Public domain W3C validator