This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lbsdiflsp0

Description: The linear spans of two disjunct independent sets only have a trivial intersection. This can be seen as the opposite direction of lindsun . (Contributed by Thierry Arnoux, 17-May-2023)

Ref Expression
Hypotheses lbsdiflsp0.j 
|- J = ( LBasis ` W )
lbsdiflsp0.n 
|- N = ( LSpan ` W )
lbsdiflsp0.1 
|- .0. = ( 0g ` W )
Assertion lbsdiflsp0 
|- ( ( W e. LVec /\ B e. J /\ V C_ B ) -> ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) = { .0. } )

Proof

Step Hyp Ref Expression
1 lbsdiflsp0.j 
 |-  J = ( LBasis ` W )
2 lbsdiflsp0.n 
 |-  N = ( LSpan ` W )
3 lbsdiflsp0.1 
 |-  .0. = ( 0g ` W )
4 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) )
5 fveq2 
 |-  ( u = v -> ( a ` u ) = ( a ` v ) )
6 id 
 |-  ( u = v -> u = v )
7 5 6 oveq12d 
 |-  ( u = v -> ( ( a ` u ) ( .s ` W ) u ) = ( ( a ` v ) ( .s ` W ) v ) )
8 7 cbvmptv 
 |-  ( u e. V |-> ( ( a ` u ) ( .s ` W ) u ) ) = ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) )
9 8 oveq2i 
 |-  ( W gsum ( u e. V |-> ( ( a ` u ) ( .s ` W ) u ) ) ) = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) )
10 4 9 eqtr4di 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> x = ( W gsum ( u e. V |-> ( ( a ` u ) ( .s ` W ) u ) ) ) )
11 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) -> a finSupp ( 0g ` ( Scalar ` W ) ) )
12 simpr 
 |-  ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) -> b finSupp ( 0g ` ( Scalar ` W ) ) )
13 simp-8l 
 |-  ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) -> W e. LVec )
14 simplr 
 |-  ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) -> B e. J )
15 14 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) -> B e. J )
16 simpr 
 |-  ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) -> V C_ B )
17 16 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) -> V C_ B )
18 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) -> a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) )
19 fvexd 
 |-  ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) -> ( Base ` ( Scalar ` W ) ) e. _V )
20 14 16 ssexd 
 |-  ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) -> V e. _V )
21 19 20 elmapd 
 |-  ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) -> ( a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) <-> a : V --> ( Base ` ( Scalar ` W ) ) ) )
22 21 biimpa 
 |-  ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) -> a : V --> ( Base ` ( Scalar ` W ) ) )
23 13 15 17 18 22 syl1111anc 
 |-  ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) -> a : V --> ( Base ` ( Scalar ` W ) ) )
24 simplr 
 |-  ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) -> b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) )
25 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
26 25 ad2antrr 
 |-  ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) -> W e. LMod )
27 eqid 
 |-  ( Base ` W ) = ( Base ` W )
28 27 1 lbsss 
 |-  ( B e. J -> B C_ ( Base ` W ) )
29 28 ad2antlr 
 |-  ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) -> B C_ ( Base ` W ) )
30 29 ssdifssd 
 |-  ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) -> ( B \ V ) C_ ( Base ` W ) )
31 3 27 2 0ellsp 
 |-  ( ( W e. LMod /\ ( B \ V ) C_ ( Base ` W ) ) -> .0. e. ( N ` ( B \ V ) ) )
32 26 30 31 syl2anc 
 |-  ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) -> .0. e. ( N ` ( B \ V ) ) )
33 32 elfvexd 
 |-  ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) -> ( B \ V ) e. _V )
34 19 33 elmapd 
 |-  ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) -> ( b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) <-> b : ( B \ V ) --> ( Base ` ( Scalar ` W ) ) ) )
35 34 biimpa 
 |-  ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) -> b : ( B \ V ) --> ( Base ` ( Scalar ` W ) ) )
36 13 15 17 24 35 syl1111anc 
 |-  ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) -> b : ( B \ V ) --> ( Base ` ( Scalar ` W ) ) )
37 disjdif 
 |-  ( V i^i ( B \ V ) ) = (/)
38 37 a1i 
 |-  ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) -> ( V i^i ( B \ V ) ) = (/) )
39 23 36 38 fun2d 
 |-  ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) -> ( a u. b ) : ( V u. ( B \ V ) ) --> ( Base ` ( Scalar ` W ) ) )
40 undif 
 |-  ( V C_ B <-> ( V u. ( B \ V ) ) = B )
41 17 40 sylib 
 |-  ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) -> ( V u. ( B \ V ) ) = B )
42 41 feq2d 
 |-  ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) -> ( ( a u. b ) : ( V u. ( B \ V ) ) --> ( Base ` ( Scalar ` W ) ) <-> ( a u. b ) : B --> ( Base ` ( Scalar ` W ) ) ) )
43 39 42 mpbid 
 |-  ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) -> ( a u. b ) : B --> ( Base ` ( Scalar ` W ) ) )
44 43 ffund 
 |-  ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) -> Fun ( a u. b ) )
45 44 fsuppunbi 
 |-  ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) -> ( ( a u. b ) finSupp ( 0g ` ( Scalar ` W ) ) <-> ( a finSupp ( 0g ` ( Scalar ` W ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) ) )
46 11 12 45 mpbir2and 
 |-  ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) -> ( a u. b ) finSupp ( 0g ` ( Scalar ` W ) ) )
47 46 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( a u. b ) finSupp ( 0g ` ( Scalar ` W ) ) )
48 eqid 
 |-  ( +g ` W ) = ( +g ` W )
49 lmodcmn 
 |-  ( W e. LMod -> W e. CMnd )
50 25 49 syl 
 |-  ( W e. LVec -> W e. CMnd )
51 50 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> W e. CMnd )
52 14 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> B e. J )
53 26 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. B ) -> W e. LMod )
54 elmapfn 
 |-  ( a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) -> a Fn V )
55 54 ad6antlr 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> a Fn V )
56 55 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. V ) -> a Fn V )
57 elmapfn 
 |-  ( b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) -> b Fn ( B \ V ) )
58 57 ad3antlr 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> b Fn ( B \ V ) )
59 58 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. V ) -> b Fn ( B \ V ) )
60 37 a1i 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. V ) -> ( V i^i ( B \ V ) ) = (/) )
61 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. V ) -> u e. V )
62 fvun1 
 |-  ( ( a Fn V /\ b Fn ( B \ V ) /\ ( ( V i^i ( B \ V ) ) = (/) /\ u e. V ) ) -> ( ( a u. b ) ` u ) = ( a ` u ) )
63 56 59 60 61 62 syl112anc 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. V ) -> ( ( a u. b ) ` u ) = ( a ` u ) )
64 63 adantlr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. B ) /\ u e. V ) -> ( ( a u. b ) ` u ) = ( a ` u ) )
65 23 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. B ) /\ u e. V ) -> a : V --> ( Base ` ( Scalar ` W ) ) )
66 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. B ) /\ u e. V ) -> u e. V )
67 65 66 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. B ) /\ u e. V ) -> ( a ` u ) e. ( Base ` ( Scalar ` W ) ) )
68 64 67 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. B ) /\ u e. V ) -> ( ( a u. b ) ` u ) e. ( Base ` ( Scalar ` W ) ) )
69 55 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. ( B \ V ) ) -> a Fn V )
70 58 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. ( B \ V ) ) -> b Fn ( B \ V ) )
71 37 a1i 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. ( B \ V ) ) -> ( V i^i ( B \ V ) ) = (/) )
72 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. ( B \ V ) ) -> u e. ( B \ V ) )
73 fvun2 
 |-  ( ( a Fn V /\ b Fn ( B \ V ) /\ ( ( V i^i ( B \ V ) ) = (/) /\ u e. ( B \ V ) ) ) -> ( ( a u. b ) ` u ) = ( b ` u ) )
74 69 70 71 72 73 syl112anc 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. ( B \ V ) ) -> ( ( a u. b ) ` u ) = ( b ` u ) )
75 74 adantlr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. B ) /\ u e. ( B \ V ) ) -> ( ( a u. b ) ` u ) = ( b ` u ) )
76 36 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. B ) /\ u e. ( B \ V ) ) -> b : ( B \ V ) --> ( Base ` ( Scalar ` W ) ) )
77 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. B ) /\ u e. ( B \ V ) ) -> u e. ( B \ V ) )
78 76 77 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. B ) /\ u e. ( B \ V ) ) -> ( b ` u ) e. ( Base ` ( Scalar ` W ) ) )
79 75 78 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. B ) /\ u e. ( B \ V ) ) -> ( ( a u. b ) ` u ) e. ( Base ` ( Scalar ` W ) ) )
80 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. B ) -> u e. B )
81 40 biimpi 
 |-  ( V C_ B -> ( V u. ( B \ V ) ) = B )
82 81 ad8antlr 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( V u. ( B \ V ) ) = B )
83 82 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> B = ( V u. ( B \ V ) ) )
84 83 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. B ) -> B = ( V u. ( B \ V ) ) )
85 80 84 eleqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. B ) -> u e. ( V u. ( B \ V ) ) )
86 elun 
 |-  ( u e. ( V u. ( B \ V ) ) <-> ( u e. V \/ u e. ( B \ V ) ) )
87 85 86 sylib 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. B ) -> ( u e. V \/ u e. ( B \ V ) ) )
88 68 79 87 mpjaodan 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. B ) -> ( ( a u. b ) ` u ) e. ( Base ` ( Scalar ` W ) ) )
89 29 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. B ) -> B C_ ( Base ` W ) )
90 89 80 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. B ) -> u e. ( Base ` W ) )
91 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
92 eqid 
 |-  ( .s ` W ) = ( .s ` W )
93 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
94 27 91 92 93 lmodvscl 
 |-  ( ( W e. LMod /\ ( ( a u. b ) ` u ) e. ( Base ` ( Scalar ` W ) ) /\ u e. ( Base ` W ) ) -> ( ( ( a u. b ) ` u ) ( .s ` W ) u ) e. ( Base ` W ) )
95 53 88 90 94 syl3anc 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. B ) -> ( ( ( a u. b ) ` u ) ( .s ` W ) u ) e. ( Base ` W ) )
96 simp-9l 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> W e. LVec )
97 96 25 syl 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> W e. LMod )
98 eqidd 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( Scalar ` W ) = ( Scalar ` W ) )
99 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
100 43 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( a u. b ) : B --> ( Base ` ( Scalar ` W ) ) )
101 100 feqmptd 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( a u. b ) = ( u e. B |-> ( ( a u. b ) ` u ) ) )
102 101 47 eqbrtrrd 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( u e. B |-> ( ( a u. b ) ` u ) ) finSupp ( 0g ` ( Scalar ` W ) ) )
103 52 97 98 27 88 90 3 99 92 102 mptscmfsupp0 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( u e. B |-> ( ( ( a u. b ) ` u ) ( .s ` W ) u ) ) finSupp .0. )
104 37 a1i 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( V i^i ( B \ V ) ) = (/) )
105 27 3 48 51 52 95 103 104 83 gsumsplit2 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( W gsum ( u e. B |-> ( ( ( a u. b ) ` u ) ( .s ` W ) u ) ) ) = ( ( W gsum ( u e. V |-> ( ( ( a u. b ) ` u ) ( .s ` W ) u ) ) ) ( +g ` W ) ( W gsum ( u e. ( B \ V ) |-> ( ( ( a u. b ) ` u ) ( .s ` W ) u ) ) ) ) )
106 63 oveq1d 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. V ) -> ( ( ( a u. b ) ` u ) ( .s ` W ) u ) = ( ( a ` u ) ( .s ` W ) u ) )
107 106 mpteq2dva 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( u e. V |-> ( ( ( a u. b ) ` u ) ( .s ` W ) u ) ) = ( u e. V |-> ( ( a ` u ) ( .s ` W ) u ) ) )
108 107 oveq2d 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( W gsum ( u e. V |-> ( ( ( a u. b ) ` u ) ( .s ` W ) u ) ) ) = ( W gsum ( u e. V |-> ( ( a ` u ) ( .s ` W ) u ) ) ) )
109 74 oveq1d 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. ( B \ V ) ) -> ( ( ( a u. b ) ` u ) ( .s ` W ) u ) = ( ( b ` u ) ( .s ` W ) u ) )
110 109 mpteq2dva 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( u e. ( B \ V ) |-> ( ( ( a u. b ) ` u ) ( .s ` W ) u ) ) = ( u e. ( B \ V ) |-> ( ( b ` u ) ( .s ` W ) u ) ) )
111 110 oveq2d 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( W gsum ( u e. ( B \ V ) |-> ( ( ( a u. b ) ` u ) ( .s ` W ) u ) ) ) = ( W gsum ( u e. ( B \ V ) |-> ( ( b ` u ) ( .s ` W ) u ) ) ) )
112 108 111 oveq12d 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( ( W gsum ( u e. V |-> ( ( ( a u. b ) ` u ) ( .s ` W ) u ) ) ) ( +g ` W ) ( W gsum ( u e. ( B \ V ) |-> ( ( ( a u. b ) ` u ) ( .s ` W ) u ) ) ) ) = ( ( W gsum ( u e. V |-> ( ( a ` u ) ( .s ` W ) u ) ) ) ( +g ` W ) ( W gsum ( u e. ( B \ V ) |-> ( ( b ` u ) ( .s ` W ) u ) ) ) ) )
113 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) )
114 fveq2 
 |-  ( u = v -> ( b ` u ) = ( b ` v ) )
115 114 6 oveq12d 
 |-  ( u = v -> ( ( b ` u ) ( .s ` W ) u ) = ( ( b ` v ) ( .s ` W ) v ) )
116 115 cbvmptv 
 |-  ( u e. ( B \ V ) |-> ( ( b ` u ) ( .s ` W ) u ) ) = ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) )
117 116 oveq2i 
 |-  ( W gsum ( u e. ( B \ V ) |-> ( ( b ` u ) ( .s ` W ) u ) ) ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) )
118 113 117 eqtr4di 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( ( invg ` W ) ` x ) = ( W gsum ( u e. ( B \ V ) |-> ( ( b ` u ) ( .s ` W ) u ) ) ) )
119 10 118 oveq12d 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( x ( +g ` W ) ( ( invg ` W ) ` x ) ) = ( ( W gsum ( u e. V |-> ( ( a ` u ) ( .s ` W ) u ) ) ) ( +g ` W ) ( W gsum ( u e. ( B \ V ) |-> ( ( b ` u ) ( .s ` W ) u ) ) ) ) )
120 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
121 96 25 120 3syl 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> W e. Grp )
122 16 29 sstrd 
 |-  ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) -> V C_ ( Base ` W ) )
123 27 2 lspssv 
 |-  ( ( W e. LMod /\ V C_ ( Base ` W ) ) -> ( N ` V ) C_ ( Base ` W ) )
124 26 122 123 syl2anc 
 |-  ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) -> ( N ` V ) C_ ( Base ` W ) )
125 124 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( N ` V ) C_ ( Base ` W ) )
126 simpr 
 |-  ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) -> x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) )
127 126 elin2d 
 |-  ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) -> x e. ( N ` V ) )
128 127 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> x e. ( N ` V ) )
129 125 128 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> x e. ( Base ` W ) )
130 eqid 
 |-  ( invg ` W ) = ( invg ` W )
131 27 48 3 130 grprinv 
 |-  ( ( W e. Grp /\ x e. ( Base ` W ) ) -> ( x ( +g ` W ) ( ( invg ` W ) ` x ) ) = .0. )
132 121 129 131 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( x ( +g ` W ) ( ( invg ` W ) ` x ) ) = .0. )
133 112 119 132 3eqtr2d 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( ( W gsum ( u e. V |-> ( ( ( a u. b ) ` u ) ( .s ` W ) u ) ) ) ( +g ` W ) ( W gsum ( u e. ( B \ V ) |-> ( ( ( a u. b ) ` u ) ( .s ` W ) u ) ) ) ) = .0. )
134 105 133 eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( W gsum ( u e. B |-> ( ( ( a u. b ) ` u ) ( .s ` W ) u ) ) ) = .0. )
135 breq1 
 |-  ( c = ( a u. b ) -> ( c finSupp ( 0g ` ( Scalar ` W ) ) <-> ( a u. b ) finSupp ( 0g ` ( Scalar ` W ) ) ) )
136 fveq1 
 |-  ( c = ( a u. b ) -> ( c ` u ) = ( ( a u. b ) ` u ) )
137 136 oveq1d 
 |-  ( c = ( a u. b ) -> ( ( c ` u ) ( .s ` W ) u ) = ( ( ( a u. b ) ` u ) ( .s ` W ) u ) )
138 137 mpteq2dv 
 |-  ( c = ( a u. b ) -> ( u e. B |-> ( ( c ` u ) ( .s ` W ) u ) ) = ( u e. B |-> ( ( ( a u. b ) ` u ) ( .s ` W ) u ) ) )
139 138 oveq2d 
 |-  ( c = ( a u. b ) -> ( W gsum ( u e. B |-> ( ( c ` u ) ( .s ` W ) u ) ) ) = ( W gsum ( u e. B |-> ( ( ( a u. b ) ` u ) ( .s ` W ) u ) ) ) )
140 139 eqeq1d 
 |-  ( c = ( a u. b ) -> ( ( W gsum ( u e. B |-> ( ( c ` u ) ( .s ` W ) u ) ) ) = .0. <-> ( W gsum ( u e. B |-> ( ( ( a u. b ) ` u ) ( .s ` W ) u ) ) ) = .0. ) )
141 135 140 anbi12d 
 |-  ( c = ( a u. b ) -> ( ( c finSupp ( 0g ` ( Scalar ` W ) ) /\ ( W gsum ( u e. B |-> ( ( c ` u ) ( .s ` W ) u ) ) ) = .0. ) <-> ( ( a u. b ) finSupp ( 0g ` ( Scalar ` W ) ) /\ ( W gsum ( u e. B |-> ( ( ( a u. b ) ` u ) ( .s ` W ) u ) ) ) = .0. ) ) )
142 eqeq1 
 |-  ( c = ( a u. b ) -> ( c = ( B X. { ( 0g ` ( Scalar ` W ) ) } ) <-> ( a u. b ) = ( B X. { ( 0g ` ( Scalar ` W ) ) } ) ) )
143 141 142 imbi12d 
 |-  ( c = ( a u. b ) -> ( ( ( c finSupp ( 0g ` ( Scalar ` W ) ) /\ ( W gsum ( u e. B |-> ( ( c ` u ) ( .s ` W ) u ) ) ) = .0. ) -> c = ( B X. { ( 0g ` ( Scalar ` W ) ) } ) ) <-> ( ( ( a u. b ) finSupp ( 0g ` ( Scalar ` W ) ) /\ ( W gsum ( u e. B |-> ( ( ( a u. b ) ` u ) ( .s ` W ) u ) ) ) = .0. ) -> ( a u. b ) = ( B X. { ( 0g ` ( Scalar ` W ) ) } ) ) ) )
144 1 lbslinds 
 |-  J C_ ( LIndS ` W )
145 144 14 sselid 
 |-  ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) -> B e. ( LIndS ` W ) )
146 27 93 91 92 3 99 islinds5 
 |-  ( ( W e. LMod /\ B C_ ( Base ` W ) ) -> ( B e. ( LIndS ` W ) <-> A. c e. ( ( Base ` ( Scalar ` W ) ) ^m B ) ( ( c finSupp ( 0g ` ( Scalar ` W ) ) /\ ( W gsum ( u e. B |-> ( ( c ` u ) ( .s ` W ) u ) ) ) = .0. ) -> c = ( B X. { ( 0g ` ( Scalar ` W ) ) } ) ) ) )
147 146 biimpa 
 |-  ( ( ( W e. LMod /\ B C_ ( Base ` W ) ) /\ B e. ( LIndS ` W ) ) -> A. c e. ( ( Base ` ( Scalar ` W ) ) ^m B ) ( ( c finSupp ( 0g ` ( Scalar ` W ) ) /\ ( W gsum ( u e. B |-> ( ( c ` u ) ( .s ` W ) u ) ) ) = .0. ) -> c = ( B X. { ( 0g ` ( Scalar ` W ) ) } ) ) )
148 26 29 145 147 syl21anc 
 |-  ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) -> A. c e. ( ( Base ` ( Scalar ` W ) ) ^m B ) ( ( c finSupp ( 0g ` ( Scalar ` W ) ) /\ ( W gsum ( u e. B |-> ( ( c ` u ) ( .s ` W ) u ) ) ) = .0. ) -> c = ( B X. { ( 0g ` ( Scalar ` W ) ) } ) ) )
149 148 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> A. c e. ( ( Base ` ( Scalar ` W ) ) ^m B ) ( ( c finSupp ( 0g ` ( Scalar ` W ) ) /\ ( W gsum ( u e. B |-> ( ( c ` u ) ( .s ` W ) u ) ) ) = .0. ) -> c = ( B X. { ( 0g ` ( Scalar ` W ) ) } ) ) )
150 fvexd 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( Base ` ( Scalar ` W ) ) e. _V )
151 150 52 elmapd 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( ( a u. b ) e. ( ( Base ` ( Scalar ` W ) ) ^m B ) <-> ( a u. b ) : B --> ( Base ` ( Scalar ` W ) ) ) )
152 100 151 mpbird 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( a u. b ) e. ( ( Base ` ( Scalar ` W ) ) ^m B ) )
153 143 149 152 rspcdva 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( ( ( a u. b ) finSupp ( 0g ` ( Scalar ` W ) ) /\ ( W gsum ( u e. B |-> ( ( ( a u. b ) ` u ) ( .s ` W ) u ) ) ) = .0. ) -> ( a u. b ) = ( B X. { ( 0g ` ( Scalar ` W ) ) } ) ) )
154 47 134 153 mp2and 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( a u. b ) = ( B X. { ( 0g ` ( Scalar ` W ) ) } ) )
155 154 reseq1d 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( ( a u. b ) |` V ) = ( ( B X. { ( 0g ` ( Scalar ` W ) ) } ) |` V ) )
156 fnunres1 
 |-  ( ( a Fn V /\ b Fn ( B \ V ) /\ ( V i^i ( B \ V ) ) = (/) ) -> ( ( a u. b ) |` V ) = a )
157 55 58 104 156 syl3anc 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( ( a u. b ) |` V ) = a )
158 xpssres 
 |-  ( V C_ B -> ( ( B X. { ( 0g ` ( Scalar ` W ) ) } ) |` V ) = ( V X. { ( 0g ` ( Scalar ` W ) ) } ) )
159 158 ad8antlr 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( ( B X. { ( 0g ` ( Scalar ` W ) ) } ) |` V ) = ( V X. { ( 0g ` ( Scalar ` W ) ) } ) )
160 155 157 159 3eqtr3d 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> a = ( V X. { ( 0g ` ( Scalar ` W ) ) } ) )
161 160 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. V ) -> a = ( V X. { ( 0g ` ( Scalar ` W ) ) } ) )
162 161 fveq1d 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. V ) -> ( a ` u ) = ( ( V X. { ( 0g ` ( Scalar ` W ) ) } ) ` u ) )
163 fvex 
 |-  ( 0g ` ( Scalar ` W ) ) e. _V
164 163 fvconst2 
 |-  ( u e. V -> ( ( V X. { ( 0g ` ( Scalar ` W ) ) } ) ` u ) = ( 0g ` ( Scalar ` W ) ) )
165 61 164 syl 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. V ) -> ( ( V X. { ( 0g ` ( Scalar ` W ) ) } ) ` u ) = ( 0g ` ( Scalar ` W ) ) )
166 162 165 eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. V ) -> ( a ` u ) = ( 0g ` ( Scalar ` W ) ) )
167 166 oveq1d 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. V ) -> ( ( a ` u ) ( .s ` W ) u ) = ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) u ) )
168 122 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. V ) -> V C_ ( Base ` W ) )
169 168 61 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. V ) -> u e. ( Base ` W ) )
170 27 91 92 99 3 lmod0vs 
 |-  ( ( W e. LMod /\ u e. ( Base ` W ) ) -> ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) u ) = .0. )
171 97 169 170 syl2an2r 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. V ) -> ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) u ) = .0. )
172 167 171 eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) /\ u e. V ) -> ( ( a ` u ) ( .s ` W ) u ) = .0. )
173 172 mpteq2dva 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( u e. V |-> ( ( a ` u ) ( .s ` W ) u ) ) = ( u e. V |-> .0. ) )
174 173 oveq2d 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( W gsum ( u e. V |-> ( ( a ` u ) ( .s ` W ) u ) ) ) = ( W gsum ( u e. V |-> .0. ) ) )
175 cmnmnd 
 |-  ( W e. CMnd -> W e. Mnd )
176 51 175 syl 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> W e. Mnd )
177 128 elfvexd 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> V e. _V )
178 3 gsumz 
 |-  ( ( W e. Mnd /\ V e. _V ) -> ( W gsum ( u e. V |-> .0. ) ) = .0. )
179 176 177 178 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> ( W gsum ( u e. V |-> .0. ) ) = .0. )
180 10 174 179 3eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ b finSupp ( 0g ` ( Scalar ` W ) ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) -> x = .0. )
181 180 anasss 
 |-  ( ( ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) /\ b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ) /\ ( b finSupp ( 0g ` ( Scalar ` W ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) ) -> x = .0. )
182 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
183 27 182 2 lspcl 
 |-  ( ( W e. LMod /\ ( B \ V ) C_ ( Base ` W ) ) -> ( N ` ( B \ V ) ) e. ( LSubSp ` W ) )
184 26 30 183 syl2anc 
 |-  ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) -> ( N ` ( B \ V ) ) e. ( LSubSp ` W ) )
185 184 adantr 
 |-  ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) -> ( N ` ( B \ V ) ) e. ( LSubSp ` W ) )
186 182 lsssubg 
 |-  ( ( W e. LMod /\ ( N ` ( B \ V ) ) e. ( LSubSp ` W ) ) -> ( N ` ( B \ V ) ) e. ( SubGrp ` W ) )
187 26 185 186 syl2an2r 
 |-  ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) -> ( N ` ( B \ V ) ) e. ( SubGrp ` W ) )
188 126 elin1d 
 |-  ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) -> x e. ( N ` ( B \ V ) ) )
189 130 subginvcl 
 |-  ( ( ( N ` ( B \ V ) ) e. ( SubGrp ` W ) /\ x e. ( N ` ( B \ V ) ) ) -> ( ( invg ` W ) ` x ) e. ( N ` ( B \ V ) ) )
190 187 188 189 syl2anc 
 |-  ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) -> ( ( invg ` W ) ` x ) e. ( N ` ( B \ V ) ) )
191 2 27 93 91 99 92 26 30 ellspds 
 |-  ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) -> ( ( ( invg ` W ) ` x ) e. ( N ` ( B \ V ) ) <-> E. b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ( b finSupp ( 0g ` ( Scalar ` W ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) ) )
192 191 biimpa 
 |-  ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ ( ( invg ` W ) ` x ) e. ( N ` ( B \ V ) ) ) -> E. b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ( b finSupp ( 0g ` ( Scalar ` W ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) )
193 190 192 syldan 
 |-  ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) -> E. b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ( b finSupp ( 0g ` ( Scalar ` W ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) )
194 193 ad3antrrr 
 |-  ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) -> E. b e. ( ( Base ` ( Scalar ` W ) ) ^m ( B \ V ) ) ( b finSupp ( 0g ` ( Scalar ` W ) ) /\ ( ( invg ` W ) ` x ) = ( W gsum ( v e. ( B \ V ) |-> ( ( b ` v ) ( .s ` W ) v ) ) ) ) )
195 181 194 r19.29a 
 |-  ( ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ a finSupp ( 0g ` ( Scalar ` W ) ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) -> x = .0. )
196 195 anasss 
 |-  ( ( ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) /\ a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ) /\ ( a finSupp ( 0g ` ( Scalar ` W ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) ) -> x = .0. )
197 2 27 93 91 99 92 26 122 ellspds 
 |-  ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) -> ( x e. ( N ` V ) <-> E. a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ( a finSupp ( 0g ` ( Scalar ` W ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) ) )
198 197 biimpa 
 |-  ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( N ` V ) ) -> E. a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ( a finSupp ( 0g ` ( Scalar ` W ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) )
199 127 198 syldan 
 |-  ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) -> E. a e. ( ( Base ` ( Scalar ` W ) ) ^m V ) ( a finSupp ( 0g ` ( Scalar ` W ) ) /\ x = ( W gsum ( v e. V |-> ( ( a ` v ) ( .s ` W ) v ) ) ) ) )
200 196 199 r19.29a 
 |-  ( ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) /\ x e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) ) -> x = .0. )
201 3 27 2 0ellsp 
 |-  ( ( W e. LMod /\ V C_ ( Base ` W ) ) -> .0. e. ( N ` V ) )
202 26 122 201 syl2anc 
 |-  ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) -> .0. e. ( N ` V ) )
203 32 202 elind 
 |-  ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) -> .0. e. ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) )
204 200 203 eqsnd 
 |-  ( ( ( W e. LVec /\ B e. J ) /\ V C_ B ) -> ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) = { .0. } )
205 204 3impa 
 |-  ( ( W e. LVec /\ B e. J /\ V C_ B ) -> ( ( N ` ( B \ V ) ) i^i ( N ` V ) ) = { .0. } )