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 } ) ) ) ) |