Metamath Proof Explorer

Theorem dimkerim

Description: Given a linear map F between vector spaces V and U , the dimension of the vector space V is the sum of the dimension of F 's kernel and the dimension of F 's image. Second part of theorem 5.3 in Lang p. 141 This can also be described as the Rank-nullity theorem, ( dimI ) being the rank of F (the dimension of its image), and ( dimK ) its nullity (the dimension of its kernel). (Contributed by Thierry Arnoux, 17-May-2023)

Ref Expression
Hypotheses dimkerim.0 
|- .0. = ( 0g ` U )
dimkerim.k 
|- K = ( V |`s ( `' F " { .0. } ) )
dimkerim.i 
|- I = ( U |`s ran F )
Assertion dimkerim 
|- ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> ( dim ` V ) = ( ( dim ` K ) +e ( dim ` I ) ) )

Proof

Step Hyp Ref Expression
1 dimkerim.0 
 |-  .0. = ( 0g ` U )
2 dimkerim.k 
 |-  K = ( V |`s ( `' F " { .0. } ) )
3 dimkerim.i 
 |-  I = ( U |`s ran F )
4 1 2 kerlmhm 
 |-  ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> K e. LVec )
5 eqid 
 |-  ( LBasis ` K ) = ( LBasis ` K )
6 5 lbsex 
 |-  ( K e. LVec -> ( LBasis ` K ) =/= (/) )
7 4 6 syl 
 |-  ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> ( LBasis ` K ) =/= (/) )
8 n0 
 |-  ( ( LBasis ` K ) =/= (/) <-> E. w w e. ( LBasis ` K ) )
9 7 8 sylib 
 |-  ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> E. w w e. ( LBasis ` K ) )
10 simpllr 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> w e. ( LBasis ` K ) )
11 vex 
 |-  b e. _V
12 11 difexi 
 |-  ( b \ w ) e. _V
13 12 a1i 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( b \ w ) e. _V )
14 disjdif 
 |-  ( w i^i ( b \ w ) ) = (/)
15 14 a1i 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( w i^i ( b \ w ) ) = (/) )
16 hashunx 
 |-  ( ( w e. ( LBasis ` K ) /\ ( b \ w ) e. _V /\ ( w i^i ( b \ w ) ) = (/) ) -> ( # ` ( w u. ( b \ w ) ) ) = ( ( # ` w ) +e ( # ` ( b \ w ) ) ) )
17 10 13 15 16 syl3anc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( # ` ( w u. ( b \ w ) ) ) = ( ( # ` w ) +e ( # ` ( b \ w ) ) ) )
18 simp-4l 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> V e. LVec )
19 simpr 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> w C_ b )
20 undif 
 |-  ( w C_ b <-> ( w u. ( b \ w ) ) = b )
21 19 20 sylib 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( w u. ( b \ w ) ) = b )
22 simplr 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> b e. ( LBasis ` V ) )
23 21 22 eqeltrd 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( w u. ( b \ w ) ) e. ( LBasis ` V ) )
24 eqid 
 |-  ( LBasis ` V ) = ( LBasis ` V )
25 24 dimval 
 |-  ( ( V e. LVec /\ ( w u. ( b \ w ) ) e. ( LBasis ` V ) ) -> ( dim ` V ) = ( # ` ( w u. ( b \ w ) ) ) )
26 18 23 25 syl2anc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( dim ` V ) = ( # ` ( w u. ( b \ w ) ) ) )
27 4 ad3antrrr 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> K e. LVec )
28 5 dimval 
 |-  ( ( K e. LVec /\ w e. ( LBasis ` K ) ) -> ( dim ` K ) = ( # ` w ) )
29 27 10 28 syl2anc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( dim ` K ) = ( # ` w ) )
30 3 imlmhm 
 |-  ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> I e. LVec )
31 30 ad3antrrr 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> I e. LVec )
32 simp-4r 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> F e. ( V LMHom U ) )
33 lmhmlmod2 
 |-  ( F e. ( V LMHom U ) -> U e. LMod )
34 32 33 syl 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> U e. LMod )
35 lmhmrnlss 
 |-  ( F e. ( V LMHom U ) -> ran F e. ( LSubSp ` U ) )
36 32 35 syl 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ran F e. ( LSubSp ` U ) )
37 df-ima 
 |-  ( F " ( ( LSpan ` V ) ` ( b \ w ) ) ) = ran ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) )
38 imassrn 
 |-  ( F " ( ( LSpan ` V ) ` ( b \ w ) ) ) C_ ran F
39 38 a1i 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( F " ( ( LSpan ` V ) ` ( b \ w ) ) ) C_ ran F )
40 37 39 eqsstrrid 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ran ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) C_ ran F )
41 lveclmod 
 |-  ( V e. LVec -> V e. LMod )
42 41 ad4antr 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> V e. LMod )
43 24 lbslinds 
 |-  ( LBasis ` V ) C_ ( LIndS ` V )
44 43 22 sseldi 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> b e. ( LIndS ` V ) )
45 difssd 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( b \ w ) C_ b )
46 lindsss 
 |-  ( ( V e. LMod /\ b e. ( LIndS ` V ) /\ ( b \ w ) C_ b ) -> ( b \ w ) e. ( LIndS ` V ) )
47 42 44 45 46 syl3anc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( b \ w ) e. ( LIndS ` V ) )
48 eqid 
 |-  ( Base ` V ) = ( Base ` V )
49 48 linds1 
 |-  ( ( b \ w ) e. ( LIndS ` V ) -> ( b \ w ) C_ ( Base ` V ) )
50 47 49 syl 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( b \ w ) C_ ( Base ` V ) )
51 eqid 
 |-  ( LSubSp ` V ) = ( LSubSp ` V )
52 eqid 
 |-  ( LSpan ` V ) = ( LSpan ` V )
53 48 51 52 lspcl 
 |-  ( ( V e. LMod /\ ( b \ w ) C_ ( Base ` V ) ) -> ( ( LSpan ` V ) ` ( b \ w ) ) e. ( LSubSp ` V ) )
54 42 50 53 syl2anc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( LSpan ` V ) ` ( b \ w ) ) e. ( LSubSp ` V ) )
55 eqid 
 |-  ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) = ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) )
56 51 55 reslmhm 
 |-  ( ( F e. ( V LMHom U ) /\ ( ( LSpan ` V ) ` ( b \ w ) ) e. ( LSubSp ` V ) ) -> ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) e. ( ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) LMHom U ) )
57 32 54 56 syl2anc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) e. ( ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) LMHom U ) )
58 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
59 3 58 reslmhm2b 
 |-  ( ( U e. LMod /\ ran F e. ( LSubSp ` U ) /\ ran ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) C_ ran F ) -> ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) e. ( ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) LMHom U ) <-> ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) e. ( ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) LMHom I ) ) )
60 59 biimpa 
 |-  ( ( ( U e. LMod /\ ran F e. ( LSubSp ` U ) /\ ran ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) C_ ran F ) /\ ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) e. ( ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) LMHom U ) ) -> ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) e. ( ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) LMHom I ) )
61 34 36 40 57 60 syl31anc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) e. ( ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) LMHom I ) )
62 lmghm 
 |-  ( F e. ( V LMHom U ) -> F e. ( V GrpHom U ) )
63 62 ad4antlr 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> F e. ( V GrpHom U ) )
64 48 24 lbsss 
 |-  ( b e. ( LBasis ` V ) -> b C_ ( Base ` V ) )
65 22 64 syl 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> b C_ ( Base ` V ) )
66 45 65 sstrd 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( b \ w ) C_ ( Base ` V ) )
67 42 66 53 syl2anc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( LSpan ` V ) ` ( b \ w ) ) e. ( LSubSp ` V ) )
68 51 lsssubg 
 |-  ( ( V e. LMod /\ ( ( LSpan ` V ) ` ( b \ w ) ) e. ( LSubSp ` V ) ) -> ( ( LSpan ` V ) ` ( b \ w ) ) e. ( SubGrp ` V ) )
69 42 67 68 syl2anc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( LSpan ` V ) ` ( b \ w ) ) e. ( SubGrp ` V ) )
70 55 resghm 
 |-  ( ( F e. ( V GrpHom U ) /\ ( ( LSpan ` V ) ` ( b \ w ) ) e. ( SubGrp ` V ) ) -> ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) e. ( ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) GrpHom U ) )
71 63 69 70 syl2anc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) e. ( ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) GrpHom U ) )
72 eqid 
 |-  ( Base ` U ) = ( Base ` U )
73 48 72 lmhmf 
 |-  ( F e. ( V LMHom U ) -> F : ( Base ` V ) --> ( Base ` U ) )
74 73 ad4antlr 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> F : ( Base ` V ) --> ( Base ` U ) )
75 74 ffnd 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> F Fn ( Base ` V ) )
76 48 52 lspssv 
 |-  ( ( V e. LMod /\ ( b \ w ) C_ ( Base ` V ) ) -> ( ( LSpan ` V ) ` ( b \ w ) ) C_ ( Base ` V ) )
77 42 66 76 syl2anc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( LSpan ` V ) ` ( b \ w ) ) C_ ( Base ` V ) )
78 fnssres 
 |-  ( ( F Fn ( Base ` V ) /\ ( ( LSpan ` V ) ` ( b \ w ) ) C_ ( Base ` V ) ) -> ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) Fn ( ( LSpan ` V ) ` ( b \ w ) ) )
79 75 77 78 syl2anc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) Fn ( ( LSpan ` V ) ` ( b \ w ) ) )
80 fniniseg 
 |-  ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) Fn ( ( LSpan ` V ) ` ( b \ w ) ) -> ( x e. ( `' ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " { .0. } ) <-> ( x e. ( ( LSpan ` V ) ` ( b \ w ) ) /\ ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) ` x ) = .0. ) ) )
81 80 biimpa 
 |-  ( ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) Fn ( ( LSpan ` V ) ` ( b \ w ) ) /\ x e. ( `' ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " { .0. } ) ) -> ( x e. ( ( LSpan ` V ) ` ( b \ w ) ) /\ ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) ` x ) = .0. ) )
82 79 81 sylan 
 |-  ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ x e. ( `' ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " { .0. } ) ) -> ( x e. ( ( LSpan ` V ) ` ( b \ w ) ) /\ ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) ` x ) = .0. ) )
83 82 simpld 
 |-  ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ x e. ( `' ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " { .0. } ) ) -> x e. ( ( LSpan ` V ) ` ( b \ w ) ) )
84 75 adantr 
 |-  ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ x e. ( `' ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " { .0. } ) ) -> F Fn ( Base ` V ) )
85 77 adantr 
 |-  ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ x e. ( `' ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " { .0. } ) ) -> ( ( LSpan ` V ) ` ( b \ w ) ) C_ ( Base ` V ) )
86 85 83 sseldd 
 |-  ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ x e. ( `' ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " { .0. } ) ) -> x e. ( Base ` V ) )
87 83 fvresd 
 |-  ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ x e. ( `' ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " { .0. } ) ) -> ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) ` x ) = ( F ` x ) )
88 82 simprd 
 |-  ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ x e. ( `' ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " { .0. } ) ) -> ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) ` x ) = .0. )
89 87 88 eqtr3d 
 |-  ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ x e. ( `' ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " { .0. } ) ) -> ( F ` x ) = .0. )
90 fniniseg 
 |-  ( F Fn ( Base ` V ) -> ( x e. ( `' F " { .0. } ) <-> ( x e. ( Base ` V ) /\ ( F ` x ) = .0. ) ) )
91 90 biimpar 
 |-  ( ( F Fn ( Base ` V ) /\ ( x e. ( Base ` V ) /\ ( F ` x ) = .0. ) ) -> x e. ( `' F " { .0. } ) )
92 84 86 89 91 syl12anc 
 |-  ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ x e. ( `' ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " { .0. } ) ) -> x e. ( `' F " { .0. } ) )
93 83 92 elind 
 |-  ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ x e. ( `' ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " { .0. } ) ) -> x e. ( ( ( LSpan ` V ) ` ( b \ w ) ) i^i ( `' F " { .0. } ) ) )
94 simpr 
 |-  ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> w e. ( LBasis ` K ) )
95 eqid 
 |-  ( Base ` K ) = ( Base ` K )
96 eqid 
 |-  ( LSpan ` K ) = ( LSpan ` K )
97 95 5 96 lbssp 
 |-  ( w e. ( LBasis ` K ) -> ( ( LSpan ` K ) ` w ) = ( Base ` K ) )
98 94 97 syl 
 |-  ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> ( ( LSpan ` K ) ` w ) = ( Base ` K ) )
99 41 ad2antrr 
 |-  ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> V e. LMod )
100 eqid 
 |-  ( `' F " { .0. } ) = ( `' F " { .0. } )
101 100 1 51 lmhmkerlss 
 |-  ( F e. ( V LMHom U ) -> ( `' F " { .0. } ) e. ( LSubSp ` V ) )
102 101 ad2antlr 
 |-  ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> ( `' F " { .0. } ) e. ( LSubSp ` V ) )
103 95 5 lbsss 
 |-  ( w e. ( LBasis ` K ) -> w C_ ( Base ` K ) )
104 94 103 syl 
 |-  ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> w C_ ( Base ` K ) )
105 cnvimass 
 |-  ( `' F " { .0. } ) C_ dom F
106 105 73 fssdm 
 |-  ( F e. ( V LMHom U ) -> ( `' F " { .0. } ) C_ ( Base ` V ) )
107 2 48 ressbas2 
 |-  ( ( `' F " { .0. } ) C_ ( Base ` V ) -> ( `' F " { .0. } ) = ( Base ` K ) )
108 106 107 syl 
 |-  ( F e. ( V LMHom U ) -> ( `' F " { .0. } ) = ( Base ` K ) )
109 108 ad2antlr 
 |-  ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> ( `' F " { .0. } ) = ( Base ` K ) )
110 104 109 sseqtrrd 
 |-  ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> w C_ ( `' F " { .0. } ) )
111 2 52 96 51 lsslsp 
 |-  ( ( V e. LMod /\ ( `' F " { .0. } ) e. ( LSubSp ` V ) /\ w C_ ( `' F " { .0. } ) ) -> ( ( LSpan ` V ) ` w ) = ( ( LSpan ` K ) ` w ) )
112 99 102 110 111 syl3anc 
 |-  ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> ( ( LSpan ` V ) ` w ) = ( ( LSpan ` K ) ` w ) )
113 98 112 109 3eqtr4d 
 |-  ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> ( ( LSpan ` V ) ` w ) = ( `' F " { .0. } ) )
114 113 ad2antrr 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( LSpan ` V ) ` w ) = ( `' F " { .0. } ) )
115 114 ineq2d 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( ( LSpan ` V ) ` ( b \ w ) ) i^i ( ( LSpan ` V ) ` w ) ) = ( ( ( LSpan ` V ) ` ( b \ w ) ) i^i ( `' F " { .0. } ) ) )
116 eqid 
 |-  ( 0g ` V ) = ( 0g ` V )
117 24 52 116 lbsdiflsp0 
 |-  ( ( V e. LVec /\ b e. ( LBasis ` V ) /\ w C_ b ) -> ( ( ( LSpan ` V ) ` ( b \ w ) ) i^i ( ( LSpan ` V ) ` w ) ) = { ( 0g ` V ) } )
118 117 ad5ant145 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( ( LSpan ` V ) ` ( b \ w ) ) i^i ( ( LSpan ` V ) ` w ) ) = { ( 0g ` V ) } )
119 115 118 eqtr3d 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( ( LSpan ` V ) ` ( b \ w ) ) i^i ( `' F " { .0. } ) ) = { ( 0g ` V ) } )
120 119 adantr 
 |-  ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ x e. ( `' ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " { .0. } ) ) -> ( ( ( LSpan ` V ) ` ( b \ w ) ) i^i ( `' F " { .0. } ) ) = { ( 0g ` V ) } )
121 93 120 eleqtrd 
 |-  ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ x e. ( `' ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " { .0. } ) ) -> x e. { ( 0g ` V ) } )
122 121 ex 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( x e. ( `' ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " { .0. } ) -> x e. { ( 0g ` V ) } ) )
123 122 ssrdv 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( `' ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " { .0. } ) C_ { ( 0g ` V ) } )
124 116 48 52 0ellsp 
 |-  ( ( V e. LMod /\ ( b \ w ) C_ ( Base ` V ) ) -> ( 0g ` V ) e. ( ( LSpan ` V ) ` ( b \ w ) ) )
125 42 66 124 syl2anc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( 0g ` V ) e. ( ( LSpan ` V ) ` ( b \ w ) ) )
126 fvexd 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) ` ( 0g ` V ) ) e. _V )
127 125 fvresd 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) ` ( 0g ` V ) ) = ( F ` ( 0g ` V ) ) )
128 116 1 ghmid 
 |-  ( F e. ( V GrpHom U ) -> ( F ` ( 0g ` V ) ) = .0. )
129 62 128 syl 
 |-  ( F e. ( V LMHom U ) -> ( F ` ( 0g ` V ) ) = .0. )
130 129 ad4antlr 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( F ` ( 0g ` V ) ) = .0. )
131 127 130 eqtrd 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) ` ( 0g ` V ) ) = .0. )
132 elsng 
 |-  ( ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) ` ( 0g ` V ) ) e. _V -> ( ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) ` ( 0g ` V ) ) e. { .0. } <-> ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) ` ( 0g ` V ) ) = .0. ) )
133 132 biimpar 
 |-  ( ( ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) ` ( 0g ` V ) ) e. _V /\ ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) ` ( 0g ` V ) ) = .0. ) -> ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) ` ( 0g ` V ) ) e. { .0. } )
134 126 131 133 syl2anc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) ` ( 0g ` V ) ) e. { .0. } )
135 79 125 134 elpreimad 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( 0g ` V ) e. ( `' ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " { .0. } ) )
136 135 snssd 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> { ( 0g ` V ) } C_ ( `' ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " { .0. } ) )
137 123 136 eqssd 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( `' ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " { .0. } ) = { ( 0g ` V ) } )
138 lmodgrp 
 |-  ( V e. LMod -> V e. Grp )
139 grpmnd 
 |-  ( V e. Grp -> V e. Mnd )
140 42 138 139 3syl 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> V e. Mnd )
141 55 48 116 ress0g 
 |-  ( ( V e. Mnd /\ ( 0g ` V ) e. ( ( LSpan ` V ) ` ( b \ w ) ) /\ ( ( LSpan ` V ) ` ( b \ w ) ) C_ ( Base ` V ) ) -> ( 0g ` V ) = ( 0g ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) )
142 140 125 77 141 syl3anc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( 0g ` V ) = ( 0g ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) )
143 142 sneqd 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> { ( 0g ` V ) } = { ( 0g ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) } )
144 137 143 eqtrd 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( `' ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " { .0. } ) = { ( 0g ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) } )
145 eqid 
 |-  ( Base ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) = ( Base ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) )
146 eqid 
 |-  ( 0g ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) = ( 0g ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) )
147 145 72 146 1 kerf1ghm 
 |-  ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) e. ( ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) GrpHom U ) -> ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) : ( Base ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) -1-1-> ( Base ` U ) <-> ( `' ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " { .0. } ) = { ( 0g ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) } ) )
148 147 biimpar 
 |-  ( ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) e. ( ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) GrpHom U ) /\ ( `' ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " { .0. } ) = { ( 0g ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) } ) -> ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) : ( Base ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) -1-1-> ( Base ` U ) )
149 71 144 148 syl2anc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) : ( Base ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) -1-1-> ( Base ` U ) )
150 eqidd 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) = ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) )
151 55 48 ressbas2 
 |-  ( ( ( LSpan ` V ) ` ( b \ w ) ) C_ ( Base ` V ) -> ( ( LSpan ` V ) ` ( b \ w ) ) = ( Base ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) )
152 77 151 syl 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( LSpan ` V ) ` ( b \ w ) ) = ( Base ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) )
153 eqidd 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( Base ` U ) = ( Base ` U ) )
154 150 152 153 f1eq123d 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) : ( ( LSpan ` V ) ` ( b \ w ) ) -1-1-> ( Base ` U ) <-> ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) : ( Base ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) -1-1-> ( Base ` U ) ) )
155 149 154 mpbird 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) : ( ( LSpan ` V ) ` ( b \ w ) ) -1-1-> ( Base ` U ) )
156 f1ssr 
 |-  ( ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) : ( ( LSpan ` V ) ` ( b \ w ) ) -1-1-> ( Base ` U ) /\ ran ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) C_ ran F ) -> ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) : ( ( LSpan ` V ) ` ( b \ w ) ) -1-1-> ran F )
157 155 40 156 syl2anc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) : ( ( LSpan ` V ) ` ( b \ w ) ) -1-1-> ran F )
158 f1f1orn 
 |-  ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) : ( ( LSpan ` V ) ` ( b \ w ) ) -1-1-> ran F -> ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) : ( ( LSpan ` V ) ` ( b \ w ) ) -1-1-onto-> ran ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) )
159 157 158 syl 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) : ( ( LSpan ` V ) ` ( b \ w ) ) -1-1-onto-> ran ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) )
160 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) /\ u e. ( ( LSpan ` V ) ` w ) ) /\ v e. ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ x = ( u ( +g ` V ) v ) ) -> ( F ` x ) = y )
161 75 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) /\ u e. ( ( LSpan ` V ) ` w ) ) /\ v e. ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ x = ( u ( +g ` V ) v ) ) -> F Fn ( Base ` V ) )
162 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) /\ u e. ( ( LSpan ` V ) ` w ) ) /\ v e. ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ x = ( u ( +g ` V ) v ) ) -> u e. ( ( LSpan ` V ) ` w ) )
163 113 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) /\ u e. ( ( LSpan ` V ) ` w ) ) /\ v e. ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ x = ( u ( +g ` V ) v ) ) -> ( ( LSpan ` V ) ` w ) = ( `' F " { .0. } ) )
164 162 163 eleqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) /\ u e. ( ( LSpan ` V ) ` w ) ) /\ v e. ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ x = ( u ( +g ` V ) v ) ) -> u e. ( `' F " { .0. } ) )
165 fniniseg 
 |-  ( F Fn ( Base ` V ) -> ( u e. ( `' F " { .0. } ) <-> ( u e. ( Base ` V ) /\ ( F ` u ) = .0. ) ) )
166 165 simplbda 
 |-  ( ( F Fn ( Base ` V ) /\ u e. ( `' F " { .0. } ) ) -> ( F ` u ) = .0. )
167 161 164 166 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) /\ u e. ( ( LSpan ` V ) ` w ) ) /\ v e. ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ x = ( u ( +g ` V ) v ) ) -> ( F ` u ) = .0. )
168 167 oveq1d 
 |-  ( ( ( ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) /\ u e. ( ( LSpan ` V ) ` w ) ) /\ v e. ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ x = ( u ( +g ` V ) v ) ) -> ( ( F ` u ) ( +g ` U ) ( F ` v ) ) = ( .0. ( +g ` U ) ( F ` v ) ) )
169 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) /\ u e. ( ( LSpan ` V ) ` w ) ) /\ v e. ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ x = ( u ( +g ` V ) v ) ) -> x = ( u ( +g ` V ) v ) )
170 169 fveq2d 
 |-  ( ( ( ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) /\ u e. ( ( LSpan ` V ) ` w ) ) /\ v e. ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ x = ( u ( +g ` V ) v ) ) -> ( F ` x ) = ( F ` ( u ( +g ` V ) v ) ) )
171 63 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) /\ u e. ( ( LSpan ` V ) ` w ) ) /\ v e. ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ x = ( u ( +g ` V ) v ) ) -> F e. ( V GrpHom U ) )
172 48 52 lspss 
 |-  ( ( V e. LMod /\ b C_ ( Base ` V ) /\ w C_ b ) -> ( ( LSpan ` V ) ` w ) C_ ( ( LSpan ` V ) ` b ) )
173 42 65 19 172 syl3anc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( LSpan ` V ) ` w ) C_ ( ( LSpan ` V ) ` b ) )
174 48 24 52 lbssp 
 |-  ( b e. ( LBasis ` V ) -> ( ( LSpan ` V ) ` b ) = ( Base ` V ) )
175 22 174 syl 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( LSpan ` V ) ` b ) = ( Base ` V ) )
176 173 175 sseqtrd 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( LSpan ` V ) ` w ) C_ ( Base ` V ) )
177 176 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) -> ( ( LSpan ` V ) ` w ) C_ ( Base ` V ) )
178 177 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) /\ u e. ( ( LSpan ` V ) ` w ) ) /\ v e. ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ x = ( u ( +g ` V ) v ) ) -> ( ( LSpan ` V ) ` w ) C_ ( Base ` V ) )
179 178 162 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) /\ u e. ( ( LSpan ` V ) ` w ) ) /\ v e. ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ x = ( u ( +g ` V ) v ) ) -> u e. ( Base ` V ) )
180 77 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) -> ( ( LSpan ` V ) ` ( b \ w ) ) C_ ( Base ` V ) )
181 180 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) /\ u e. ( ( LSpan ` V ) ` w ) ) /\ v e. ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ x = ( u ( +g ` V ) v ) ) -> ( ( LSpan ` V ) ` ( b \ w ) ) C_ ( Base ` V ) )
182 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) /\ u e. ( ( LSpan ` V ) ` w ) ) /\ v e. ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ x = ( u ( +g ` V ) v ) ) -> v e. ( ( LSpan ` V ) ` ( b \ w ) ) )
183 181 182 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) /\ u e. ( ( LSpan ` V ) ` w ) ) /\ v e. ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ x = ( u ( +g ` V ) v ) ) -> v e. ( Base ` V ) )
184 eqid 
 |-  ( +g ` V ) = ( +g ` V )
185 eqid 
 |-  ( +g ` U ) = ( +g ` U )
186 48 184 185 ghmlin 
 |-  ( ( F e. ( V GrpHom U ) /\ u e. ( Base ` V ) /\ v e. ( Base ` V ) ) -> ( F ` ( u ( +g ` V ) v ) ) = ( ( F ` u ) ( +g ` U ) ( F ` v ) ) )
187 171 179 183 186 syl3anc 
 |-  ( ( ( ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) /\ u e. ( ( LSpan ` V ) ` w ) ) /\ v e. ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ x = ( u ( +g ` V ) v ) ) -> ( F ` ( u ( +g ` V ) v ) ) = ( ( F ` u ) ( +g ` U ) ( F ` v ) ) )
188 170 187 eqtr2d 
 |-  ( ( ( ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) /\ u e. ( ( LSpan ` V ) ` w ) ) /\ v e. ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ x = ( u ( +g ` V ) v ) ) -> ( ( F ` u ) ( +g ` U ) ( F ` v ) ) = ( F ` x ) )
189 lmhmlvec2 
 |-  ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> U e. LVec )
190 lveclmod 
 |-  ( U e. LVec -> U e. LMod )
191 lmodgrp 
 |-  ( U e. LMod -> U e. Grp )
192 189 190 191 3syl 
 |-  ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> U e. Grp )
193 192 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) /\ u e. ( ( LSpan ` V ) ` w ) ) /\ v e. ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ x = ( u ( +g ` V ) v ) ) -> U e. Grp )
194 74 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) /\ u e. ( ( LSpan ` V ) ` w ) ) /\ v e. ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ x = ( u ( +g ` V ) v ) ) -> F : ( Base ` V ) --> ( Base ` U ) )
195 194 183 ffvelrnd 
 |-  ( ( ( ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) /\ u e. ( ( LSpan ` V ) ` w ) ) /\ v e. ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ x = ( u ( +g ` V ) v ) ) -> ( F ` v ) e. ( Base ` U ) )
196 72 185 1 grplid 
 |-  ( ( U e. Grp /\ ( F ` v ) e. ( Base ` U ) ) -> ( .0. ( +g ` U ) ( F ` v ) ) = ( F ` v ) )
197 193 195 196 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) /\ u e. ( ( LSpan ` V ) ` w ) ) /\ v e. ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ x = ( u ( +g ` V ) v ) ) -> ( .0. ( +g ` U ) ( F ` v ) ) = ( F ` v ) )
198 168 188 197 3eqtr3d 
 |-  ( ( ( ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) /\ u e. ( ( LSpan ` V ) ` w ) ) /\ v e. ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ x = ( u ( +g ` V ) v ) ) -> ( F ` x ) = ( F ` v ) )
199 160 198 eqtr3d 
 |-  ( ( ( ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) /\ u e. ( ( LSpan ` V ) ` w ) ) /\ v e. ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ x = ( u ( +g ` V ) v ) ) -> y = ( F ` v ) )
200 161 183 182 fnfvimad 
 |-  ( ( ( ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) /\ u e. ( ( LSpan ` V ) ` w ) ) /\ v e. ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ x = ( u ( +g ` V ) v ) ) -> ( F ` v ) e. ( F " ( ( LSpan ` V ) ` ( b \ w ) ) ) )
201 199 200 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) /\ u e. ( ( LSpan ` V ) ` w ) ) /\ v e. ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ x = ( u ( +g ` V ) v ) ) -> y e. ( F " ( ( LSpan ` V ) ` ( b \ w ) ) ) )
202 simp-7l 
 |-  ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) -> V e. LVec )
203 simplr 
 |-  ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) -> x e. ( Base ` V ) )
204 110 ad2antrr 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> w C_ ( `' F " { .0. } ) )
205 106 ad4antlr 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( `' F " { .0. } ) C_ ( Base ` V ) )
206 204 205 sstrd 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> w C_ ( Base ` V ) )
207 eqid 
 |-  ( LSSum ` V ) = ( LSSum ` V )
208 48 52 207 lsmsp2 
 |-  ( ( V e. LMod /\ w C_ ( Base ` V ) /\ ( b \ w ) C_ ( Base ` V ) ) -> ( ( ( LSpan ` V ) ` w ) ( LSSum ` V ) ( ( LSpan ` V ) ` ( b \ w ) ) ) = ( ( LSpan ` V ) ` ( w u. ( b \ w ) ) ) )
209 42 206 66 208 syl3anc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( ( LSpan ` V ) ` w ) ( LSSum ` V ) ( ( LSpan ` V ) ` ( b \ w ) ) ) = ( ( LSpan ` V ) ` ( w u. ( b \ w ) ) ) )
210 21 fveq2d 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( LSpan ` V ) ` ( w u. ( b \ w ) ) ) = ( ( LSpan ` V ) ` b ) )
211 209 210 175 3eqtrrd 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( Base ` V ) = ( ( ( LSpan ` V ) ` w ) ( LSSum ` V ) ( ( LSpan ` V ) ` ( b \ w ) ) ) )
212 211 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) -> ( Base ` V ) = ( ( ( LSpan ` V ) ` w ) ( LSSum ` V ) ( ( LSpan ` V ) ` ( b \ w ) ) ) )
213 203 212 eleqtrd 
 |-  ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) -> x e. ( ( ( LSpan ` V ) ` w ) ( LSSum ` V ) ( ( LSpan ` V ) ` ( b \ w ) ) ) )
214 48 184 207 lsmelvalx 
 |-  ( ( V e. LVec /\ ( ( LSpan ` V ) ` w ) C_ ( Base ` V ) /\ ( ( LSpan ` V ) ` ( b \ w ) ) C_ ( Base ` V ) ) -> ( x e. ( ( ( LSpan ` V ) ` w ) ( LSSum ` V ) ( ( LSpan ` V ) ` ( b \ w ) ) ) <-> E. u e. ( ( LSpan ` V ) ` w ) E. v e. ( ( LSpan ` V ) ` ( b \ w ) ) x = ( u ( +g ` V ) v ) ) )
215 214 biimpa 
 |-  ( ( ( V e. LVec /\ ( ( LSpan ` V ) ` w ) C_ ( Base ` V ) /\ ( ( LSpan ` V ) ` ( b \ w ) ) C_ ( Base ` V ) ) /\ x e. ( ( ( LSpan ` V ) ` w ) ( LSSum ` V ) ( ( LSpan ` V ) ` ( b \ w ) ) ) ) -> E. u e. ( ( LSpan ` V ) ` w ) E. v e. ( ( LSpan ` V ) ` ( b \ w ) ) x = ( u ( +g ` V ) v ) )
216 202 177 180 213 215 syl31anc 
 |-  ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) -> E. u e. ( ( LSpan ` V ) ` w ) E. v e. ( ( LSpan ` V ) ` ( b \ w ) ) x = ( u ( +g ` V ) v ) )
217 201 216 r19.29vva 
 |-  ( ( ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) /\ x e. ( Base ` V ) ) /\ ( F ` x ) = y ) -> y e. ( F " ( ( LSpan ` V ) ` ( b \ w ) ) ) )
218 fvelrnb 
 |-  ( F Fn ( Base ` V ) -> ( y e. ran F <-> E. x e. ( Base ` V ) ( F ` x ) = y ) )
219 218 biimpa 
 |-  ( ( F Fn ( Base ` V ) /\ y e. ran F ) -> E. x e. ( Base ` V ) ( F ` x ) = y )
220 75 219 sylan 
 |-  ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) -> E. x e. ( Base ` V ) ( F ` x ) = y )
221 217 220 r19.29a 
 |-  ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ y e. ran F ) -> y e. ( F " ( ( LSpan ` V ) ` ( b \ w ) ) ) )
222 39 221 eqelssd 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( F " ( ( LSpan ` V ) ` ( b \ w ) ) ) = ran F )
223 37 222 eqtr3id 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ran ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) = ran F )
224 223 f1oeq3d 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) : ( ( LSpan ` V ) ` ( b \ w ) ) -1-1-onto-> ran ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) <-> ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) : ( ( LSpan ` V ) ` ( b \ w ) ) -1-1-onto-> ran F ) )
225 159 224 mpbid 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) : ( ( LSpan ` V ) ` ( b \ w ) ) -1-1-onto-> ran F )
226 42 50 76 syl2anc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( LSpan ` V ) ` ( b \ w ) ) C_ ( Base ` V ) )
227 226 151 syl 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( LSpan ` V ) ` ( b \ w ) ) = ( Base ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) )
228 frn 
 |-  ( F : ( Base ` V ) --> ( Base ` U ) -> ran F C_ ( Base ` U ) )
229 3 72 ressbas2 
 |-  ( ran F C_ ( Base ` U ) -> ran F = ( Base ` I ) )
230 73 228 229 3syl 
 |-  ( F e. ( V LMHom U ) -> ran F = ( Base ` I ) )
231 32 230 syl 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ran F = ( Base ` I ) )
232 150 227 231 f1oeq123d 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) : ( ( LSpan ` V ) ` ( b \ w ) ) -1-1-onto-> ran F <-> ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) : ( Base ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) -1-1-onto-> ( Base ` I ) ) )
233 225 232 mpbid 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) : ( Base ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) -1-1-onto-> ( Base ` I ) )
234 eqid 
 |-  ( Base ` I ) = ( Base ` I )
235 145 234 islmim 
 |-  ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) e. ( ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) LMIso I ) <-> ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) e. ( ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) LMHom I ) /\ ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) : ( Base ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) -1-1-onto-> ( Base ` I ) ) )
236 61 233 235 sylanbrc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) e. ( ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) LMIso I ) )
237 48 52 lspssid 
 |-  ( ( V e. LMod /\ ( b \ w ) C_ ( Base ` V ) ) -> ( b \ w ) C_ ( ( LSpan ` V ) ` ( b \ w ) ) )
238 42 50 237 syl2anc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( b \ w ) C_ ( ( LSpan ` V ) ` ( b \ w ) ) )
239 51 55 lsslinds 
 |-  ( ( V e. LMod /\ ( ( LSpan ` V ) ` ( b \ w ) ) e. ( LSubSp ` V ) /\ ( b \ w ) C_ ( ( LSpan ` V ) ` ( b \ w ) ) ) -> ( ( b \ w ) e. ( LIndS ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) <-> ( b \ w ) e. ( LIndS ` V ) ) )
240 239 biimpar 
 |-  ( ( ( V e. LMod /\ ( ( LSpan ` V ) ` ( b \ w ) ) e. ( LSubSp ` V ) /\ ( b \ w ) C_ ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ ( b \ w ) e. ( LIndS ` V ) ) -> ( b \ w ) e. ( LIndS ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) )
241 42 67 238 47 240 syl31anc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( b \ w ) e. ( LIndS ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) )
242 eqid 
 |-  ( LSpan ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) = ( LSpan ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) )
243 55 52 242 51 lsslsp 
 |-  ( ( V e. LMod /\ ( ( LSpan ` V ) ` ( b \ w ) ) e. ( LSubSp ` V ) /\ ( b \ w ) C_ ( ( LSpan ` V ) ` ( b \ w ) ) ) -> ( ( LSpan ` V ) ` ( b \ w ) ) = ( ( LSpan ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) ` ( b \ w ) ) )
244 42 54 238 243 syl3anc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( LSpan ` V ) ` ( b \ w ) ) = ( ( LSpan ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) ` ( b \ w ) ) )
245 244 227 eqtr3d 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( LSpan ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) ` ( b \ w ) ) = ( Base ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) )
246 eqid 
 |-  ( LBasis ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) = ( LBasis ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) )
247 145 246 242 islbs4 
 |-  ( ( b \ w ) e. ( LBasis ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) <-> ( ( b \ w ) e. ( LIndS ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) /\ ( ( LSpan ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) ` ( b \ w ) ) = ( Base ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) ) )
248 241 245 247 sylanbrc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( b \ w ) e. ( LBasis ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) )
249 eqid 
 |-  ( LBasis ` I ) = ( LBasis ` I )
250 246 249 lmimlbs 
 |-  ( ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) e. ( ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) LMIso I ) /\ ( b \ w ) e. ( LBasis ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) ) -> ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " ( b \ w ) ) e. ( LBasis ` I ) )
251 236 248 250 syl2anc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " ( b \ w ) ) e. ( LBasis ` I ) )
252 249 dimval 
 |-  ( ( I e. LVec /\ ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " ( b \ w ) ) e. ( LBasis ` I ) ) -> ( dim ` I ) = ( # ` ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " ( b \ w ) ) ) )
253 31 251 252 syl2anc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( dim ` I ) = ( # ` ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " ( b \ w ) ) ) )
254 f1imaeng 
 |-  ( ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) : ( ( LSpan ` V ) ` ( b \ w ) ) -1-1-> ran F /\ ( b \ w ) C_ ( ( LSpan ` V ) ` ( b \ w ) ) /\ ( b \ w ) e. ( LIndS ` V ) ) -> ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " ( b \ w ) ) ~~ ( b \ w ) )
255 hasheni 
 |-  ( ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " ( b \ w ) ) ~~ ( b \ w ) -> ( # ` ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " ( b \ w ) ) ) = ( # ` ( b \ w ) ) )
256 254 255 syl 
 |-  ( ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) : ( ( LSpan ` V ) ` ( b \ w ) ) -1-1-> ran F /\ ( b \ w ) C_ ( ( LSpan ` V ) ` ( b \ w ) ) /\ ( b \ w ) e. ( LIndS ` V ) ) -> ( # ` ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " ( b \ w ) ) ) = ( # ` ( b \ w ) ) )
257 157 238 47 256 syl3anc 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( # ` ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " ( b \ w ) ) ) = ( # ` ( b \ w ) ) )
258 253 257 eqtrd 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( dim ` I ) = ( # ` ( b \ w ) ) )
259 29 258 oveq12d 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( dim ` K ) +e ( dim ` I ) ) = ( ( # ` w ) +e ( # ` ( b \ w ) ) ) )
260 17 26 259 3eqtr4d 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( dim ` V ) = ( ( dim ` K ) +e ( dim ` I ) ) )
261 5 lbslinds 
 |-  ( LBasis ` K ) C_ ( LIndS ` K )
262 261 94 sseldi 
 |-  ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> w e. ( LIndS ` K ) )
263 51 2 lsslinds 
 |-  ( ( V e. LMod /\ ( `' F " { .0. } ) e. ( LSubSp ` V ) /\ w C_ ( `' F " { .0. } ) ) -> ( w e. ( LIndS ` K ) <-> w e. ( LIndS ` V ) ) )
264 263 biimpa 
 |-  ( ( ( V e. LMod /\ ( `' F " { .0. } ) e. ( LSubSp ` V ) /\ w C_ ( `' F " { .0. } ) ) /\ w e. ( LIndS ` K ) ) -> w e. ( LIndS ` V ) )
265 99 102 110 262 264 syl31anc 
 |-  ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> w e. ( LIndS ` V ) )
266 24 islinds4 
 |-  ( V e. LVec -> ( w e. ( LIndS ` V ) <-> E. b e. ( LBasis ` V ) w C_ b ) )
267 266 ad2antrr 
 |-  ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> ( w e. ( LIndS ` V ) <-> E. b e. ( LBasis ` V ) w C_ b ) )
268 265 267 mpbid 
 |-  ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> E. b e. ( LBasis ` V ) w C_ b )
269 260 268 r19.29a 
 |-  ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> ( dim ` V ) = ( ( dim ` K ) +e ( dim ` I ) ) )
270 9 269 exlimddv 
 |-  ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> ( dim ` V ) = ( ( dim ` K ) +e ( dim ` I ) ) )