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

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 sselid 
 |-  ( ( ( ( ( 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 75 77 fnssresd 
 |-  ( ( ( ( ( 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 ) ) )
79 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. ) ) )
80 79 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. ) )
81 78 80 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. ) )
82 81 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 ) ) )
83 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 ) )
84 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 ) )
85 84 82 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 ) )
86 82 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 ) )
87 81 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. )
88 86 87 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. )
89 fniniseg 
 |-  ( F Fn ( Base ` V ) -> ( x e. ( `' F " { .0. } ) <-> ( x e. ( Base ` V ) /\ ( F ` x ) = .0. ) ) )
90 89 biimpar 
 |-  ( ( F Fn ( Base ` V ) /\ ( x e. ( Base ` V ) /\ ( F ` x ) = .0. ) ) -> x e. ( `' F " { .0. } ) )
91 83 85 88 90 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. } ) )
92 82 91 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. } ) ) )
93 simpr 
 |-  ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> w e. ( LBasis ` K ) )
94 eqid 
 |-  ( Base ` K ) = ( Base ` K )
95 eqid 
 |-  ( LSpan ` K ) = ( LSpan ` K )
96 94 5 95 lbssp 
 |-  ( w e. ( LBasis ` K ) -> ( ( LSpan ` K ) ` w ) = ( Base ` K ) )
97 93 96 syl 
 |-  ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> ( ( LSpan ` K ) ` w ) = ( Base ` K ) )
98 41 ad2antrr 
 |-  ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> V e. LMod )
99 eqid 
 |-  ( `' F " { .0. } ) = ( `' F " { .0. } )
100 99 1 51 lmhmkerlss 
 |-  ( F e. ( V LMHom U ) -> ( `' F " { .0. } ) e. ( LSubSp ` V ) )
101 100 ad2antlr 
 |-  ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> ( `' F " { .0. } ) e. ( LSubSp ` V ) )
102 94 5 lbsss 
 |-  ( w e. ( LBasis ` K ) -> w C_ ( Base ` K ) )
103 93 102 syl 
 |-  ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> w C_ ( Base ` K ) )
104 cnvimass 
 |-  ( `' F " { .0. } ) C_ dom F
105 104 73 fssdm 
 |-  ( F e. ( V LMHom U ) -> ( `' F " { .0. } ) C_ ( Base ` V ) )
106 2 48 ressbas2 
 |-  ( ( `' F " { .0. } ) C_ ( Base ` V ) -> ( `' F " { .0. } ) = ( Base ` K ) )
107 105 106 syl 
 |-  ( F e. ( V LMHom U ) -> ( `' F " { .0. } ) = ( Base ` K ) )
108 107 ad2antlr 
 |-  ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> ( `' F " { .0. } ) = ( Base ` K ) )
109 103 108 sseqtrrd 
 |-  ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> w C_ ( `' F " { .0. } ) )
110 2 52 95 51 lsslsp 
 |-  ( ( V e. LMod /\ ( `' F " { .0. } ) e. ( LSubSp ` V ) /\ w C_ ( `' F " { .0. } ) ) -> ( ( LSpan ` K ) ` w ) = ( ( LSpan ` V ) ` w ) )
111 110 eqcomd 
 |-  ( ( V e. LMod /\ ( `' F " { .0. } ) e. ( LSubSp ` V ) /\ w C_ ( `' F " { .0. } ) ) -> ( ( LSpan ` V ) ` w ) = ( ( LSpan ` K ) ` w ) )
112 98 101 109 111 syl3anc 
 |-  ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> ( ( LSpan ` V ) ` w ) = ( ( LSpan ` K ) ` w ) )
113 97 112 108 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 92 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 78 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 189 lvecgrpd 
 |-  ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> U e. Grp )
191 190 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 )
192 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 ) )
193 192 183 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ( ( ( ( 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 ) )
194 72 185 1 191 193 grplidd 
 |-  ( ( ( ( ( ( ( ( ( ( ( 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 ) )
195 168 188 194 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 ) )
196 160 195 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 ) )
197 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 ) ) ) )
198 196 197 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 ) ) ) )
199 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 )
200 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 ) )
201 109 ad2antrr 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> w C_ ( `' F " { .0. } ) )
202 105 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 ) )
203 201 202 sstrd 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> w C_ ( Base ` V ) )
204 eqid 
 |-  ( LSSum ` V ) = ( LSSum ` V )
205 48 52 204 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 ) ) ) )
206 42 203 66 205 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 ) ) ) )
207 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 ) )
208 206 207 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 ) ) ) )
209 208 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 ) ) ) )
210 200 209 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 ) ) ) )
211 48 184 204 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 ) ) )
212 211 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 ) )
213 199 177 180 210 212 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 ) )
214 198 213 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 ) ) ) )
215 fvelrnb 
 |-  ( F Fn ( Base ` V ) -> ( y e. ran F <-> E. x e. ( Base ` V ) ( F ` x ) = y ) )
216 215 biimpa 
 |-  ( ( F Fn ( Base ` V ) /\ y e. ran F ) -> E. x e. ( Base ` V ) ( F ` x ) = y )
217 75 216 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 )
218 214 217 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 ) ) ) )
219 39 218 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 )
220 37 219 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 )
221 220 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 ) )
222 159 221 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 )
223 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 ) )
224 223 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 ) ) ) ) )
225 frn 
 |-  ( F : ( Base ` V ) --> ( Base ` U ) -> ran F C_ ( Base ` U ) )
226 3 72 ressbas2 
 |-  ( ran F C_ ( Base ` U ) -> ran F = ( Base ` I ) )
227 32 73 225 226 4syl 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ran F = ( Base ` I ) )
228 150 224 227 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 ) ) )
229 222 228 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 ) )
230 eqid 
 |-  ( Base ` I ) = ( Base ` I )
231 145 230 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 ) ) )
232 61 229 231 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 ) )
233 48 52 lspssid 
 |-  ( ( V e. LMod /\ ( b \ w ) C_ ( Base ` V ) ) -> ( b \ w ) C_ ( ( LSpan ` V ) ` ( b \ w ) ) )
234 42 50 233 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 ) ) )
235 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 ) ) )
236 235 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 ) ) ) ) )
237 42 67 234 47 236 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 ) ) ) ) )
238 eqid 
 |-  ( LSpan ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) = ( LSpan ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) )
239 55 52 238 51 lsslsp 
 |-  ( ( V e. LMod /\ ( ( LSpan ` V ) ` ( b \ w ) ) e. ( LSubSp ` V ) /\ ( b \ w ) C_ ( ( LSpan ` V ) ` ( b \ w ) ) ) -> ( ( LSpan ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) ` ( b \ w ) ) = ( ( LSpan ` V ) ` ( b \ w ) ) )
240 239 eqcomd 
 |-  ( ( 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 ) ) )
241 42 54 234 240 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 ) ) )
242 241 224 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 ) ) ) ) )
243 eqid 
 |-  ( LBasis ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) = ( LBasis ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) )
244 145 243 238 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 ) ) ) ) ) )
245 237 242 244 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 ) ) ) ) )
246 eqid 
 |-  ( LBasis ` I ) = ( LBasis ` I )
247 243 246 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 ) )
248 232 245 247 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 ) )
249 246 dimval 
 |-  ( ( I e. LVec /\ ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " ( b \ w ) ) e. ( LBasis ` I ) ) -> ( dim ` I ) = ( # ` ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " ( b \ w ) ) ) )
250 31 248 249 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 ) ) ) )
251 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 ) )
252 hasheni 
 |-  ( ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " ( b \ w ) ) ~~ ( b \ w ) -> ( # ` ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " ( b \ w ) ) ) = ( # ` ( b \ w ) ) )
253 251 252 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 ) ) )
254 157 234 47 253 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 ) ) )
255 250 254 eqtrd 
 |-  ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( dim ` I ) = ( # ` ( b \ w ) ) )
256 29 255 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 ) ) ) )
257 17 26 256 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 ) ) )
258 5 lbslinds 
 |-  ( LBasis ` K ) C_ ( LIndS ` K )
259 258 93 sselid 
 |-  ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> w e. ( LIndS ` K ) )
260 51 2 lsslinds 
 |-  ( ( V e. LMod /\ ( `' F " { .0. } ) e. ( LSubSp ` V ) /\ w C_ ( `' F " { .0. } ) ) -> ( w e. ( LIndS ` K ) <-> w e. ( LIndS ` V ) ) )
261 260 biimpa 
 |-  ( ( ( V e. LMod /\ ( `' F " { .0. } ) e. ( LSubSp ` V ) /\ w C_ ( `' F " { .0. } ) ) /\ w e. ( LIndS ` K ) ) -> w e. ( LIndS ` V ) )
262 98 101 109 259 261 syl31anc 
 |-  ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> w e. ( LIndS ` V ) )
263 24 islinds4 
 |-  ( V e. LVec -> ( w e. ( LIndS ` V ) <-> E. b e. ( LBasis ` V ) w C_ b ) )
264 263 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 ) )
265 262 264 mpbid 
 |-  ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> E. b e. ( LBasis ` V ) w C_ b )
266 257 265 r19.29a 
 |-  ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> ( dim ` V ) = ( ( dim ` K ) +e ( dim ` I ) ) )
267 9 266 exlimddv 
 |-  ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> ( dim ` V ) = ( ( dim ` K ) +e ( dim ` I ) ) )