Skip to content

Instantly share code, notes, and snippets.

@tirix

tirix/dimkerim.mmp

Created May 22, 2023 15:17
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save tirix/9e0d04f303b7f8a69a270f1598bfac2f to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save tirix/9e0d04f303b7f8a69a270f1598bfac2f to your computer and use it in GitHub Desktop.
Download ZIP
dimkerim.mmp
Raw
dimkerim.mmp
$theorem dimkerim
* Given a homomorphism of vector spaces ` F ` over ` W ` , the dimension of
the vector space ` W ` 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
h1::dimkerim.1 |- .0. = ( 0g ` U )
h2::dimkerim.k |- K = ( V |`s ( `' F " { .0. } ) )
h3::dimkerim.i |- I = ( U |`s ran F )
4:1,2:kerlmhm |- ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> K e. LVec )
5:3:imlmhm |- ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> I e. LVec )
6::eqid |- ( LBasis ` K ) = ( LBasis ` K )
7::eqid |- ( LBasis ` I ) = ( LBasis ` I )
8::eqid |- ( Base ` V ) = ( Base ` V )
9::eqid |- ( Base ` U ) = ( Base ` U )
10::eqid |- ( LBasis ` V ) = ( LBasis ` V )
11::eqid |- ( LSpan ` V ) = ( LSpan ` V )
12::eqid |- ( LSSum ` V ) = ( LSSum ` V )
13::eqid |- ( Base ` K ) = ( Base ` K )
14::eqid |- ( LSubSp ` V ) = ( LSubSp ` V )
15::eqid |- ( `' F " { .0. } ) = ( `' F " { .0. } )
16::eqid |- ( LSpan ` U ) = ( LSpan ` U )
17::eqid |- ( LSpan ` I ) = ( LSpan ` I )
18::eqid |- ( LSubSp ` U ) = ( LSubSp ` U )
19::eqid |- ( LSpan ` K ) = ( LSpan ` K )
20::eqid |- ( +g ` U ) = ( +g ` U )
21::eqid |- ( .s ` U ) = ( .s ` U )
22:6:lbsex |- ( K e. LVec -> ( LBasis ` K ) =/= (/) )
23:7:lbsex |- ( I e. LVec -> ( LBasis ` I ) =/= (/) )
24::n0 |- ( ( LBasis ` K ) =/= (/) <-> E. w w e. ( LBasis ` K ) )
25:4,22:syl |- ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> ( LBasis ` K ) =/= (/) )
26:5,23:syl |- ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> ( LBasis ` I ) =/= (/) )
27:25,24:sylib |- ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> E. w w e. ( LBasis ` K ) )
28:6:dimval |- ( ( K e. LVec /\ w e. ( LBasis ` K ) ) -> ( dim ` K ) = ( # ` w ) )
29:3,9:ressbas2 |- ( ran F C_ ( Base ` U ) -> ran F = ( Base ` I ) )
30:8,9:lmhmf |- ( F e. ( V LMHom U ) -> F : ( Base ` V ) --> ( Base ` U ) )
31::frn |- ( F : ( Base ` V ) --> ( Base ` U ) -> ran F C_ ( Base ` U ) )
32:30,31,29:3syl |- ( F e. ( V LMHom U ) -> ran F = ( Base ` I ) )
33::eqid |- ( Base ` I ) = ( Base ` I )
34::dffn4 |- ( F Fn ( Base ` V ) <-> F : ( Base ` V ) -onto-> ran F )
35::ffn |- ( F : ( Base ` V ) --> ( Base ` U ) -> F Fn ( Base ` V ) )
36:35,34:sylib |- ( F : ( Base ` V ) --> ( Base ` U ) -> F : ( Base ` V ) -onto-> ran F )
37:30,36:syl |- ( F e. ( V LMHom U ) -> F : ( Base ` V ) -onto-> ran F )
38:8,10,11:islbs4 |- ( ( w u. ( b \ w ) ) e. ( LBasis ` V ) <-> ( ( w u. ( b \ w ) ) e. ( LIndS ` V ) /\ ( ( LSpan ` V ) ` ( w u. ( b \ w ) ) ) = ( Base ` V ) ) )
39:10:dimval |- ( ( V e. LVec /\ ( w u. ( b \ w ) ) e. ( LBasis ` V ) ) -> ( dim ` V ) = ( # ` ( w u. ( b \ w ) ) ) )
*
40::hashunx |- ( ( w e. ( LBasis ` K ) /\ ( b \ w ) e. _V /\ ( w i^i ( b \ w ) ) = (/) ) -> ( # ` ( w u. ( b \ w ) ) ) = ( ( # ` w ) +e ( # ` ( b \ w ) ) ) )
41::vex |- b e. _V
42:41:difexi |- ( b \ w ) e. _V
*
43:10:dimval |- ( ( V e. LVec /\ ( w u. ( b \ w ) ) e. ( LBasis ` V ) ) -> ( dim ` V ) = ( # ` ( w u. ( b \ w ) ) ) )
44:8,10,11:islbs4 |- ( ( w u. ( b \ w ) ) e. ( LBasis ` V ) <-> ( ( w u. ( b \ w ) ) e. ( LIndS ` V ) /\ ( ( LSpan ` V ) ` ( w u. ( b \ w ) ) ) = ( Base ` V ) ) )
45:8,11,12: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 ) ) ) )
46:13,6:lbsss |- ( w e. ( LBasis ` K ) -> w C_ ( Base ` K ) )
47::lveclmod |- ( V e. LVec -> V e. LMod )
48:2,8:ressbasss |- ( Base ` K ) C_ ( Base ` V )
49::elpwi |- ( ( b \ w ) e. ~P ( Base ` V ) -> ( b \ w ) C_ ( Base ` V ) )
50:8,14,11:lspcl |- ( ( V e. LMod /\ ( b \ w ) C_ ( Base ` V ) ) -> ( ( LSpan ` V ) ` ( b \ w ) ) e. ( LSubSp ` V ) )
51:8,11,16:lmhmlsp |- ( ( F e. ( V LMHom U ) /\ ( b \ w ) C_ ( Base ` V ) ) -> ( F " ( ( LSpan ` V ) ` ( b \ w ) ) ) = ( ( LSpan ` U ) ` ( F " ( b \ w ) ) ) )
52::lmhmlmod2 |- ( F e. ( V LMHom U ) -> U e. LMod )
53::lmhmrnlss |- ( F e. ( V LMHom U ) -> ran F e. ( LSubSp ` U ) )
* 700:8,11,16:lmhmlsp |- ( ( F e. ( V LMHom U ) /\ ( b \ w ) C_ ( Base ` V ) ) -> ( F " ( ( LSpan ` V ) ` ( b \ w ) ) ) = ( ( LSpan ` U ) ` ( F " ( b \ w ) ) ) )
54:13,6,19:lbssp |- ( w e. ( LBasis ` K ) -> ( ( LSpan ` K ) ` w ) = ( Base ` K ) )
55:2,11,19,14:lsslsp
|- ( ( V e. LMod /\ ( `' F " { .0. } ) e. ( LSubSp ` V ) /\ w C_ ( `' F " { .0. } ) ) -> ( ( LSpan ` V ) ` w ) = ( ( LSpan ` K ) ` w ) )
56:15,1,14:lmhmkerlss
|- ( F e. ( V LMHom U ) -> ( `' F " { .0. } ) e. ( LSubSp ` V ) )
57:2,8:ressbas2 |- ( ( `' F " { .0. } ) C_ ( Base ` V ) -> ( `' F " { .0. } ) = ( Base ` K ) )
58:2,8:ressbasss |- ( Base ` K ) C_ ( Base ` V )
59:8,14:lssss |- ( ( `' F " { .0. } ) e. ( LSubSp ` V ) -> ( `' F " { .0. } ) C_ ( Base ` V ) )
60:8,11:lspssv |- ( ( V e. LMod /\ ( b \ w ) C_ ( Base ` V ) ) -> ( ( LSpan ` V ) ` ( b \ w ) ) C_ ( Base ` V ) )
61::eqid |- ( .s ` V ) = ( .s ` V )
62::eqid |- ( Scalar ` V ) = ( Scalar ` V )
63::eqid |- ( Base ` ( Scalar ` V ) ) = ( Base ` ( Scalar ` V ) )
64::eqid |- ( 0g ` ( Scalar ` V ) ) = ( 0g ` ( Scalar ` V ) )
65:8,61,11,62,63,64:islinds2
|- ( V e. LVec -> ( ( w u. ( b \ w ) ) e. ( LIndS ` V ) <-> ( ( w u. ( b \ w ) ) C_ ( Base ` V ) /\ A. c e. ( w u. ( b \ w ) ) A. k e. ( ( Base ` ( Scalar ` V ) ) \ { ( 0g ` ( Scalar ` V ) ) } ) -. ( k ( .s ` V ) c ) e. ( ( LSpan ` V ) ` ( ( w u. ( b \ w ) ) \ { c } ) ) ) ) )
66:65:biimpar |- ( ( V e. LVec /\ ( ( w u. ( b \ w ) ) C_ ( Base ` V ) /\ A. c e. ( w u. ( b \ w ) ) A. k e. ( ( Base ` ( Scalar ` V ) ) \ { ( 0g ` ( Scalar ` V ) ) } ) -. ( k ( .s ` V ) c ) e. ( ( LSpan ` V ) ` ( ( w u. ( b \ w ) ) \ { c } ) ) ) ) -> ( w u. ( b \ w ) ) e. ( LIndS ` V ) )
67::eqid |- ( +g ` V ) = ( +g ` V )
68:67,12:lsmelval |- ( ( ( `' F " { .0. } ) e. ( SubGrp ` V ) /\ ( ( LSpan ` V ) ` ( b \ w ) ) e. ( SubGrp ` V ) ) -> ( ( k ( .s ` V ) c ) e. ( ( `' F " { .0. } ) ( LSSum ` V ) ( ( LSpan ` V ) ` ( b \ w ) ) ) <-> E. x e. ( `' F " { .0. } ) E. y e. ( ( LSpan ` V ) ` ( b \ w ) ) ( k ( .s ` V ) c ) = ( x ( +g ` V ) y ) ) )
69:68:biimpa |- ( ( ( ( `' F " { .0. } ) e. ( SubGrp ` V ) /\ ( ( LSpan ` V ) ` ( b \ w ) ) e. ( SubGrp ` V ) ) /\ ( k ( .s ` V ) c ) e. ( ( `' F " { .0. } ) ( LSSum ` V ) ( ( LSpan ` V ) ` ( b \ w ) ) ) ) -> E. x e. ( `' F " { .0. } ) E. y e. ( ( LSpan ` V ) ` ( b \ w ) ) ( k ( .s ` V ) c ) = ( x ( +g ` V ) y ) )
70:14:lsssubg |- ( ( V e. LMod /\ ( `' F " { .0. } ) e. ( LSubSp ` V ) ) -> ( `' F " { .0. } ) e. ( SubGrp ` V ) )
71:14:lsssubg |- ( ( V e. LMod /\ ( ( LSpan ` V ) ` ( b \ w ) ) e. ( LSubSp ` V ) ) -> ( ( LSpan ` V ) ` ( b \ w ) ) e. ( SubGrp ` V ) )
72:8,62,61,63:lmodvscl
|- ( ( V e. LMod /\ k e. ( Base ` ( Scalar ` V ) ) /\ c e. ( Base ` V ) ) -> ( k ( .s ` V ) c ) e. ( Base ` V ) )
*
73:14,2:lsslinds |- ( ( V e. LMod /\ ( `' F " { .0. } ) e. ( LSubSp ` V ) /\ w C_ ( `' F " { .0. } ) ) -> ( w e. ( LIndS ` K ) <-> w e. ( LIndS ` V ) ) )
74:73:biimpa |- ( ( ( V e. LMod /\ ( `' F " { .0. } ) e. ( LSubSp ` V ) /\ w C_ ( `' F " { .0. } ) ) /\ w e. ( LIndS ` K ) ) -> w e. ( LIndS ` V ) )
75::simpr |- ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> w e. ( LBasis ` K ) )
76:6:lbslinds |- ( LBasis ` K ) C_ ( LIndS ` K )
77:76,75:sseldi |- ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> w e. ( LIndS ` K ) )
78::lveclmod |- ( V e. LVec -> V e. LMod )
79:78:ad2antrr |- ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> V e. LMod )
80:15,1,14:lmhmkerlss
|- ( F e. ( V LMHom U ) -> ( `' F " { .0. } ) e. ( LSubSp ` V ) )
81:80:ad2antlr |- ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> ( `' F " { .0. } ) e. ( LSubSp ` V ) )
82:2,8:ressbas2 |- ( ( `' F " { .0. } ) C_ ( Base ` V ) -> ( `' F " { .0. } ) = ( Base ` K ) )
83::eqid |- ( Base ` K ) = ( Base ` K )
84:13,6:lbsss |- ( w e. ( LBasis ` K ) -> w C_ ( Base ` K ) )
85::cnvimass |- ( `' F " { .0. } ) C_ dom F
86:15,85:eqsstri |- ( `' F " { .0. } ) C_ dom F
87::eqid |- ( Base ` U ) = ( Base ` U )
88:8,9:lmhmf |- ( F e. ( V LMHom U ) -> F : ( Base ` V ) --> ( Base ` U ) )
89:88:fdmd |- ( F e. ( V LMHom U ) -> dom F = ( Base ` V ) )
90:86,89:syl5sseq |- ( F e. ( V LMHom U ) -> ( `' F " { .0. } ) C_ ( Base ` V ) )
91:90,82:syl |- ( F e. ( V LMHom U ) -> ( `' F " { .0. } ) = ( Base ` K ) )
92:91:ad2antlr |- ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> ( `' F " { .0. } ) = ( Base ` K ) )
93:75,84:syl |- ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> w C_ ( Base ` K ) )
94:93,92:sseqtr4d |- ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> w C_ ( `' F " { .0. } ) )
95:79,81,94,77,74:syl31anc
|- ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> w e. ( LIndS ` V ) )
96:10:islinds4 |- ( V e. LVec -> ( w e. ( LIndS ` V ) <-> E. b e. ( LBasis ` V ) w C_ b ) )
97:96: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 ) )
98:95,97:mpbid |- ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> E. b e. ( LBasis ` V ) w C_ b )
99::lindsss |- ( ( V e. LMod /\ b e. ( LIndS ` V ) /\ ( b \ w ) C_ b ) -> ( b \ w ) e. ( LIndS ` V ) )
100:79:ad2antrr |- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> V e. LMod )
101::simplr |- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> b e. ( LBasis ` V ) )
102:10:lbslinds |- ( LBasis ` V ) C_ ( LIndS ` V )
103:102,101:sseldi |- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> b e. ( LIndS ` V ) )
104::difssd |- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( b \ w ) C_ b )
105:100,103,104,99: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 ) )
106::simpr |- ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ d = ( b \ w ) ) -> d = ( b \ w ) )
107:106:fveq2d |- ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ d = ( b \ w ) ) -> ( ( LSpan ` V ) ` d ) = ( ( LSpan ` V ) ` ( b \ w ) ) )
108:107:reseq2d |- ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ d = ( b \ w ) ) -> ( F |` ( ( LSpan ` V ) ` d ) ) = ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) )
109::eqidd |- ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ d = ( b \ w ) ) -> ran F = ran F )
110:108,107,109:f1oeq123d
|- ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ d = ( b \ w ) ) -> ( ( F |` ( ( LSpan ` V ) ` d ) ) : ( ( LSpan ` V ) ` d ) -1-1-onto-> ran F <-> ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) : ( ( LSpan ` V ) ` ( b \ w ) ) -1-1-onto-> ran F ) )
111:107:ineq1d |- ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ d = ( b \ w ) ) -> ( ( ( LSpan ` V ) ` d ) i^i ( `' F " { .0. } ) ) = ( ( ( LSpan ` V ) ` ( b \ w ) ) i^i ( `' F " { .0. } ) ) )
112:111:eqeq1d |- ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ d = ( b \ w ) ) -> ( ( ( ( LSpan ` V ) ` d ) i^i ( `' F " { .0. } ) ) = { ( 0g ` V ) } <-> ( ( ( LSpan ` V ) ` ( b \ w ) ) i^i ( `' F " { .0. } ) ) = { ( 0g ` V ) } ) )
113::eqid |- ( Base ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) = ( Base ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) )
114::eqid |- ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) = ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) )
115::eqid |- ( 0g ` V ) = ( 0g ` V )
116:114,8,115: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 ) ) ) ) )
117::eqid |- ( 0g ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) = ( 0g ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) )
118:113,9,117,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 ) ) ) ) } ) )
119:118: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 ) )
120:114: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 ) )
121::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 )
122::lmghm |- ( F e. ( V LMHom U ) -> F e. ( V GrpHom U ) )
123:122: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 ) )
124:8,14,11:lspcl |- ( ( V e. LMod /\ ( b \ w ) C_ ( Base ` V ) ) -> ( ( LSpan ` V ) ` ( b \ w ) ) e. ( LSubSp ` V ) )
125:114,14:lsslmod |- ( ( V e. LMod /\ ( ( LSpan ` V ) ` ( b \ w ) ) e. ( LSubSp ` V ) ) -> ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) e. LMod )
126:14:lsssubg |- ( ( V e. LMod /\ ( ( LSpan ` V ) ` ( b \ w ) ) e. ( LSubSp ` V ) ) -> ( ( LSpan ` V ) ` ( b \ w ) ) e. ( SubGrp ` V ) )
127:8,10:lbsss |- ( b e. ( LBasis ` V ) -> b C_ ( Base ` V ) )
128:101,127:syl |- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> b C_ ( Base ` V ) )
129:104,128: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 ) )
130:100,129,124: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 ) )
131:100,130,126: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 ) )
132:123,131,120: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 ) )
133::grpmnd |- ( V e. Grp -> V e. Mnd )
134::lmodgrp |- ( V e. LMod -> V e. Grp )
135:100,134,133:3syl
|- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> V e. Mnd )
136:115,8,11:0ellsp
|- ( ( V e. LMod /\ ( b \ w ) C_ ( Base ` V ) ) -> ( 0g ` V ) e. ( ( LSpan ` V ) ` ( b \ w ) ) )
137:100,129,136: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 ) ) )
138::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 ) ) ) )
139:114,8:ressbas2 |- ( ( ( LSpan ` V ) ` ( b \ w ) ) C_ ( Base ` V ) -> ( ( LSpan ` V ) ` ( b \ w ) ) = ( Base ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) )
140:8,11:lspssv |- ( ( V e. LMod /\ ( b \ w ) C_ ( Base ` V ) ) -> ( ( LSpan ` V ) ` ( b \ w ) ) C_ ( Base ` V ) )
141:100,129,140: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 ) )
142:141,139: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 ) ) ) ) )
143:135,137,141,116: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 ) ) ) ) )
144:143: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 ) ) ) ) } )
145:87:a1i |- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( Base ` U ) = ( Base ` U ) )
146:138,142,145: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 ) ) )
147::fnssres |- ( ( F Fn ( Base ` V ) /\ ( ( LSpan ` V ) ` ( b \ w ) ) C_ ( Base ` V ) ) -> ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) Fn ( ( LSpan ` V ) ` ( b \ w ) ) )
148:88: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 ) )
149:148:ffnd |- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> F Fn ( Base ` V ) )
150:149,141,147: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 ) ) )
151::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. ) )
152:151: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. } )
153::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 )
154:137: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 ) ) )
155:115,1:ghmid |- ( F e. ( V GrpHom U ) -> ( F ` ( 0g ` V ) ) = .0. )
156:122,155:syl |- ( F e. ( V LMHom U ) -> ( F ` ( 0g ` V ) ) = .0. )
157:156:ad4antlr |- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( F ` ( 0g ` V ) ) = .0. )
158:154,157: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. )
159:153,158,152: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. } )
160:150,137,159: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. } ) )
161:160: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. } ) )
162::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. ) ) )
163::velsn |- ( x e. { ( 0g ` V ) } <-> x = ( 0g ` V ) )
164:162: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. ) )
165:150: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 |` ( ( LSpan ` V ) ` ( b \ w ) ) ) Fn ( ( LSpan ` V ) ` ( b \ w ) ) )
166::simpr |- ( ( ( ( ( ( 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 |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " { .0. } ) )
167:165,166,164:syl2anc
|- ( ( ( ( ( ( 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. ) )
168:167: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. )
169:167: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 ) ) )
170:169: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 ) )
171:170,168: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. )
172::fniniseg |- ( F Fn ( Base ` V ) -> ( x e. ( `' F " { .0. } ) <-> ( x e. ( Base ` V ) /\ ( F ` x ) = .0. ) ) )
173:172:biimpar |- ( ( F Fn ( Base ` V ) /\ ( x e. ( Base ` V ) /\ ( F ` x ) = .0. ) ) -> x e. ( `' F " { .0. } ) )
174:149: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 ) )
175:141: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 ) )
176:175,169: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 ) )
177:174,176,171,173: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. } ) )
178:177,15:syl6eleqr
|- ( ( ( ( ( ( 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. } ) )
179::eqid |- ( LSSum ` V ) = ( LSSum ` V )
180:8,11,12: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 ) ) ) )
181:94:ad2antrr |- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> w C_ ( `' F " { .0. } ) )
182:90: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 ) )
183:181,182:sstrd |- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> w C_ ( Base ` V ) )
184:100,183,129,180: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 ) ) ) )
185::undif |- ( w C_ b <-> ( w u. ( b \ w ) ) = b )
186::simpr |- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> w C_ b )
187:186,185: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 )
188:187: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 ) )
189:8,10,11:islbs4 |- ( b e. ( LBasis ` V ) <-> ( b e. ( LIndS ` V ) /\ ( ( LSpan ` V ) ` b ) = ( Base ` V ) ) )
190:189:simprbi |- ( b e. ( LBasis ` V ) -> ( ( LSpan ` V ) ` b ) = ( Base ` V ) )
191:101,190: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 ) )
192:184,188,191: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 ) ) ) )
193::fvelrnb |- ( F Fn ( Base ` V ) -> ( y e. ran F <-> E. x e. ( Base ` V ) ( F ` x ) = y ) )
194:193:biimpa |- ( ( F Fn ( Base ` V ) /\ y e. ran F ) -> E. x e. ( Base ` V ) ( F ` x ) = y )
195::imassrn |- ( F " ( ( LSpan ` V ) ` ( b \ w ) ) ) C_ ran F
196:195: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 )
197::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 ) )
198:192: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 ) ) ) )
199:197,198: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 ) ) ) )
200::eqid |- ( +g ` V ) = ( +g ` V )
201:8,67,12: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 ) ) )
202:201: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 ) )
203::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 )
204:8,11:lspss |- ( ( V e. LMod /\ b C_ ( Base ` V ) /\ w C_ b ) -> ( ( LSpan ` V ) ` w ) C_ ( ( LSpan ` V ) ` b ) )
205:203,78:syl |- ( ( ( ( ( ( ( ( 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. LMod )
206:100,128,186,204: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 ) )
207:206,191: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 ) )
208:207: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 ) )
209:141: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 ) )
210:203,208,209,199,202: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 ) )
*
211:149: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 ) )
212::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 ) ) )
213:209: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 ) )
214:213,212: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 ) )
215:211,214,212: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 ) ) ) )
216::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 ) )
217:216: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 ) ) )
218::eqid |- ( +g ` U ) = ( +g ` U )
219:8,67,20: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 ) ) )
220:123: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 ) )
221::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 ) )
222: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 ) /\ u e. ( ( LSpan ` V ) ` w ) ) /\ v e. ( ( LSpan ` V ) ` ( b \ w ) ) ) /\ x = ( u ( +g ` V ) v ) ) -> ( ( LSpan ` V ) ` w ) C_ ( Base ` V ) )
223:222,221: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 ) )
224:220,223,214,219: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 ) ) )
225::eqid |- ( LSpan ` K ) = ( LSpan ` K )
226:2,11,19,14:lsslsp
|- ( ( V e. LMod /\ ( `' F " { .0. } ) e. ( LSubSp ` V ) /\ w C_ ( `' F " { .0. } ) ) -> ( ( LSpan ` V ) ` w ) = ( ( LSpan ` K ) ` w ) )
227:13,6,19:lbssp |- ( w e. ( LBasis ` K ) -> ( ( LSpan ` K ) ` w ) = ( Base ` K ) )
228:75,227:syl |- ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> ( ( LSpan ` K ) ` w ) = ( Base ` K ) )
229:79,81,94,226:syl3anc
|- ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> ( ( LSpan ` V ) ` w ) = ( ( LSpan ` K ) ` w ) )
230:228,229,92:3eqtr4d
|- ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> ( ( LSpan ` V ) ` w ) = ( `' F " { .0. } ) )
231:230: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. } ) )
232:221,231: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. } ) )
233:232,15:syl6eleq
|- ( ( ( ( ( ( ( ( ( ( ( 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. } ) )
234::fniniseg |- ( F Fn ( Base ` V ) -> ( u e. ( `' F " { .0. } ) <-> ( u e. ( Base ` V ) /\ ( F ` u ) = .0. ) ) )
235:234:simplbda |- ( ( F Fn ( Base ` V ) /\ u e. ( `' F " { .0. } ) ) -> ( F ` u ) = .0. )
236:211,233,235: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. )
237:236: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 ) ) )
238:9,20,1:grplid |- ( ( U e. Grp /\ ( F ` v ) e. ( Base ` U ) ) -> ( .0. ( +g ` U ) ( F ` v ) ) = ( F ` v ) )
239::lmhmlvec2 |- ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> U e. LVec )
240::lveclmod |- ( U e. LVec -> U e. LMod )
241::lmodgrp |- ( U e. LMod -> U e. Grp )
242:239,240,241:3syl
|- ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> U e. Grp )
243:242: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 )
244:148: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 ) )
245:244,214: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 ) )
247:243,245,238: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 ) )
248:217,224: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 ) )
249::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 )
250:237,248,247: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 ) )
251:249,250: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 ) )
252:251,215: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 ) ) ) )
253:252,210: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 ) ) ) )
254:149,194: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 )
255:253,254: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 ) ) ) )
256:255:ex |- ( ( ( ( ( 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 ) ) ) ) )
257:256:ssrdv |- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ran F C_ ( F " ( ( LSpan ` V ) ` ( b \ w ) ) ) )
258:196,257: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 ) ) ) = ran F )
259::simpr |- ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ x e. ( ( ( LSpan ` V ) ` ( b \ w ) ) i^i ( `' F " { .0. } ) ) ) -> x e. ( ( ( LSpan ` V ) ` ( b \ w ) ) i^i ( `' F " { .0. } ) ) )
260:259:elin2d |- ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ x e. ( ( ( LSpan ` V ) ` ( b \ w ) ) i^i ( `' F " { .0. } ) ) ) -> x e. ( `' F " { .0. } ) )
261:259:elin1d |- ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ x e. ( ( ( LSpan ` V ) ` ( b \ w ) ) i^i ( `' F " { .0. } ) ) ) -> x e. ( ( LSpan ` V ) ` ( b \ w ) ) )
* d3:: |- ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ x e. ( ( ( LSpan ` V ) ` ( b \ w ) ) i^i ( `' F " { .0. } ) ) ) -> x = ( 0g ` V ) )
* d2:d3,c106:sylibr |- ( ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) /\ x e. ( ( ( LSpan ` V ) ` ( b \ w ) ) i^i ( `' F " { .0. } ) ) ) -> x e. { ( 0g ` V ) } )
* d1:d2:ex |- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( x e. ( ( ( LSpan ` V ) ` ( b \ w ) ) i^i ( `' F " { .0. } ) ) -> x e. { ( 0g ` V ) } ) )
* 202:d1:ssrdv |- ( ( ( ( ( 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. } ) ) C_ { ( 0g ` V ) } )
* 203:c3,c1,c5:c0ellsp |- ( ( V e. LMod /\ w C_ ( Base ` V ) ) -> ( 0g ` V ) e. ( ( LSpan ` V ) ` w ) )
* 204:c44,c126,c203: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 ) ` w ) )
262:230: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. } ) )
* 206:c204,c205:eleqtrd
|- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( 0g ` V ) e. ( `' F " { .0. } ) )
* 207:c80,c206:elind |- ( ( ( ( ( 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 ) ) i^i ( `' F " { .0. } ) ) )
* 208:c207:snssd |- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> { ( 0g ` V ) } C_ ( ( ( LSpan ` V ) ` ( b \ w ) ) i^i ( `' F " { .0. } ) ) )
263:10,11,115:lbsdiflsp0
|- ( ( V e. LVec /\ b e. ( LBasis ` V ) /\ w C_ b ) -> ( ( ( LSpan ` V ) ` ( b \ w ) ) i^i ( ( LSpan ` V ) ` w ) ) = { ( 0g ` V ) } )
264::incom |- ( ( ( LSpan ` V ) ` ( b \ w ) ) i^i ( ( LSpan ` V ) ` w ) ) = ( ( ( LSpan ` V ) ` w ) i^i ( ( LSpan ` V ) ` ( b \ w ) ) )
265:263: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 ) } )
266:262: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. } ) ) )
267:266,265: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 ) } )
268:267: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 ) } )
269:169,178: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. } ) ) )
*d17:: |- ( ( ( ( ( ( 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 = ( 0g ` V ) )
270:269,268: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 ) } )
271:270: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 ) } ) )
272:271: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 ) } )
273:272,161: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 ) } )
274:273,144: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 ) ) ) ) } )
275:132,274,119: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 ) )
276:275,146: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 ) )
277::df-ima |- ( F " ( ( LSpan ` V ) ` ( b \ w ) ) ) = ran ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) )
278:8,11,16:lmhmlsp
|- ( ( F e. ( V LMHom U ) /\ ( b \ w ) C_ ( Base ` V ) ) -> ( F " ( ( LSpan ` V ) ` ( b \ w ) ) ) = ( ( LSpan ` U ) ` ( F " ( b \ w ) ) ) )
279:277,258:syl5eqr
|- ( ( ( ( ( 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 )
280:279: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 ) )
281::ssidd |- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ran F C_ ran F )
282:279,281:eqsstrd
|- ( ( ( ( ( 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 )
283:276,282,121: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 )
284::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 ) ) ) )
285:283,284: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 ) ) ) )
286:285,280: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 )
*
287::n0 |- ( ( w i^i ( b \ w ) ) =/= (/) <-> E. x x e. ( w i^i ( b \ w ) ) )
288::fniniseg |- ( F Fn ( Base ` V ) -> ( x e. ( `' F " { .0. } ) <-> ( x e. ( Base ` V ) /\ ( F ` x ) = .0. ) ) )
289:288:simplbda |- ( ( F Fn ( Base ` V ) /\ x e. ( `' F " { .0. } ) ) -> ( F ` x ) = .0. )
290::fvex |- ( Base ` V ) e. _V
291::lmhmlvec2 |- ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> U e. LVec )
292::nne |- ( -. ( w i^i ( b \ w ) ) =/= (/) <-> ( w i^i ( b \ w ) ) = (/) )
*
293:62,63,8,61,21:lmhmlin
|- ( ( F e. ( V LMHom U ) /\ k e. ( Base ` ( Scalar ` V ) ) /\ c e. ( Base ` V ) ) -> ( F ` ( k ( .s ` V ) c ) ) = ( k ( .s ` U ) ( F ` c ) ) )
*
294:8,67,20:ghmlin |- ( ( F e. ( V GrpHom U ) /\ x e. ( Base ` V ) /\ y e. ( Base ` V ) ) -> ( F ` ( x ( +g ` V ) y ) ) = ( ( F ` x ) ( +g ` U ) ( F ` y ) ) )
295::lmghm |- ( F e. ( V LMHom U ) -> F e. ( V GrpHom U ) )
296::fniniseg |- ( F Fn ( Base ` V ) -> ( x e. ( `' F " { .0. } ) <-> ( x e. ( Base ` V ) /\ ( F ` x ) = .0. ) ) )
297:9,20,1:grplid |- ( ( U e. Grp /\ ( F ` y ) e. ( Base ` U ) ) -> ( .0. ( +g ` U ) ( F ` y ) ) = ( F ` y ) )
298::lmodgrp |- ( U e. LMod -> U e. Grp )
299:52:adantl |- ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> U e. LMod )
300:299,298:syl |- ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> U e. Grp )
301::eqid |- ( 0g ` V ) = ( 0g ` V )
302:6:lbslinds |- ( LBasis ` K ) C_ ( LIndS ` K )
303:14,2:lsslinds |- ( ( V e. LMod /\ ( `' F " { .0. } ) e. ( LSubSp ` V ) /\ w C_ ( `' F " { .0. } ) ) -> ( w e. ( LIndS ` K ) <-> w e. ( LIndS ` V ) ) )
304::eqid |- ( Base ` ( V |`s D ) ) = ( Base ` ( V |`s D ) )
305::eqid |- ( Base ` ( Base ` U ) ) = ( Base ` ( Base ` U ) )
306:304,305:lindsmm
|- ( ( ( F |` D ) e. ( ( V |`s D ) LMHom ( Base ` U ) ) /\ ( F |` D ) : ( Base ` ( V |`s D ) ) -1-1-> ( Base ` ( Base ` U ) ) /\ ( b \ w ) C_ ( Base ` ( V |`s D ) ) ) -> ( ( b \ w ) e. ( LIndS ` ( V |`s D ) ) <-> ( ( F |` D ) " ( b \ w ) ) e. ( LIndS ` ( Base ` U ) ) ) )
307::eqid |- ( LBasis ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) = ( LBasis ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) )
308:307,7: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 ) )
310:4:ad3antrrr |- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> K e. LVec )
311:5:ad3antrrr |- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> I e. LVec )
312:75:ad2antrr |- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> w e. ( LBasis ` K ) )
313::simp-4l |- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> V e. LVec )
314::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 ) )
315:42:a1i |- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( b \ w ) e. _V )
316::f1of1 |- ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) : ( ( LSpan ` V ) ` ( b \ w ) ) -1-1-onto-> ran F -> ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) : ( ( LSpan ` V ) ` ( b \ w ) ) -1-1-> ran F )
318::eqid |- ( Base ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) = ( Base ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) )
319:318,33: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 ) ) )
321::eqid |- ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) = ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) )
322:14,321: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 ) )
323:8,14,11:lspcl |- ( ( V e. LMod /\ ( b \ w ) C_ ( Base ` V ) ) -> ( ( LSpan ` V ) ` ( b \ w ) ) e. ( LSubSp ` V ) )
324:313,47:syl |- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> V e. LMod )
325:8:linds1 |- ( ( b \ w ) e. ( LIndS ` V ) -> ( b \ w ) C_ ( Base ` V ) )
326:105,325: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 ) )
327:324,326,323: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 ) )
328:314,327,322: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 ) )
329:3,18: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 ) ) )
330:329: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 ) )
331:314,52:syl |- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> U e. LMod )
332:314,53: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 ) )
333::resss |- ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) C_ F
334::rnss |- ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) C_ F -> ran ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) C_ ran F )
* 251::rnresss |- ran ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) C_ ran F
335:331,332,282,328,330: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 ) )
336:314,32:syl |- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ran F = ( Base ` I ) )
337::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 ) ) ) )
338:321,8:ressbas2 |- ( ( ( LSpan ` V ) ` ( b \ w ) ) C_ ( Base ` V ) -> ( ( LSpan ` V ) ` ( b \ w ) ) = ( Base ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) )
339:324,326,60: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 ) )
340:339,338: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 ) ) ) ) )
341:337,340,336: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 ) ) )
342:286,341: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 ) )
343:335,342,319: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 ) )
344:8,11:lspssid |- ( ( V e. LMod /\ ( b \ w ) C_ ( Base ` V ) ) -> ( b \ w ) C_ ( ( LSpan ` V ) ` ( b \ w ) ) )
345:324,326,344: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 ) ) )
346::eqid |- ( LSpan ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) ) = ( LSpan ` ( V |`s ( ( LSpan ` V ) ` ( b \ w ) ) ) )
347:318,307,346: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 ) ) ) ) ) )
348:14,321: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 ) ) )
349:348: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 ) ) ) ) )
350:100,130,345,105,349: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 ) ) ) ) )
351:321,11,346,14: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 ) ) )
352:324,327,345,351: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 ) ) )
353:352:eqcomd |- ( ( ( ( ( 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 ) ) = ( ( LSpan ` V ) ` ( b \ w ) ) )
354:353,340:eqtrd |- ( ( ( ( ( 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 ) ) ) ) )
355:350,354,347: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 ) ) ) ) )
356::disjdif |- ( w i^i ( b \ w ) ) = (/)
357:356: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 ) ) = (/) )
358:95:ad2antrr |- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> w e. ( LIndS ` V ) )
359:264,265:syl5eqr
|- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( ( ( LSpan ` V ) ` w ) i^i ( ( LSpan ` V ) ` ( b \ w ) ) ) = { ( 0g ` V ) } )
360:11,115,313,358,105,359:lindsun
|- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( w u. ( b \ w ) ) e. ( LIndS ` V ) )
361:8,10,11:islbs4 |- ( ( w u. ( b \ w ) ) e. ( LBasis ` V ) <-> ( ( w u. ( b \ w ) ) e. ( LIndS ` V ) /\ ( ( LSpan ` V ) ` ( w u. ( b \ w ) ) ) = ( Base ` V ) ) )
362:188,191:eqtrd |- ( ( ( ( ( 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 ) ) ) = ( Base ` V ) )
363:360,362,38:sylanbrc
|- ( ( ( ( ( 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 ) )
364:343,355,308: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 ) )
365:7:dimval |- ( ( I e. LVec /\ ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " ( b \ w ) ) e. ( LBasis ` I ) ) -> ( dim ` I ) = ( # ` ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " ( b \ w ) ) ) )
366:311,364,365: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 ) ) ) )
367::hasheni |- ( ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " ( b \ w ) ) ~~ ( b \ w ) -> ( # ` ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) " ( b \ w ) ) ) = ( # ` ( b \ w ) ) )
368::fvex |- ( ( LSpan ` V ) ` ( b \ w ) ) e. _V
369:368:f1oen |- ( ( F |` ( ( LSpan ` V ) ` ( b \ w ) ) ) : ( ( LSpan ` V ) ` ( b \ w ) ) -1-1-onto-> ran F -> ( ( LSpan ` V ) ` ( b \ w ) ) ~~ ran F )
370::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 ) )
371:370,367: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 ) ) )
372:283,345,105,371: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 ) ) )
373:366,372:eqtrd |- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( dim ` I ) = ( # ` ( b \ w ) ) )
374:310,312,28:syl2anc
|- ( ( ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) /\ b e. ( LBasis ` V ) ) /\ w C_ b ) -> ( dim ` K ) = ( # ` w ) )
375:374,373: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 ) ) ) )
376:313,363,43: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 ) ) ) )
377:312,315,357,40: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 ) ) ) )
378:377,376,375: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 ) ) )
379:378,98:r19.29a |- ( ( ( V e. LVec /\ F e. ( V LMHom U ) ) /\ w e. ( LBasis ` K ) ) -> ( dim ` V ) = ( ( dim ` K ) +e ( dim ` I ) ) )
380:379:ex |- ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> ( w e. ( LBasis ` K ) -> ( dim ` V ) = ( ( dim ` K ) +e ( dim ` I ) ) ) )
381:380:exlimdv |- ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> ( E. w w e. ( LBasis ` K ) -> ( dim ` V ) = ( ( dim ` K ) +e ( dim ` I ) ) ) )
qed:27,381:mpd |- ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> ( dim ` V ) = ( ( dim ` K ) +e ( dim ` I ) ) )
$= ( clvec wcel clmhm co wa vw cv clbs cfv wex cldim cxad wceq c0 wne kerlmhm
eqid lbsex syl n0 sylib vb wss cdif cun chash cvv cin simpr ad2antrr vex
difexi a1i disjdif hashunx syl3anc simp-4l clinds clspn cbs c0g clmod ccnv
csn cima clss lveclmod lmhmkerlss ad2antlr lbsss cdm cnvimass eqsstri lmhmf
fdmd syl5sseq ressbas2 sseqtr4d lbslinds sseldi w3a lsslinds biimpa syl31anc
simplr difssd lindsss incom lbsdiflsp0 ad5ant145 syl5eqr lindsun undif
fveq2d islbs4 simprbi eqtrd sylanbrc dimval syl2anc ad3antrrr cres imlmhm
cress clmim wf1o crn simp-4r lmhmlmod2 lmhmrnlss df-ima imassrn vy vx vu vv
cplusg wfn wf ad4antlr ffnd ad6antr simpllr lbssp lsslsp 3eqtr4d ad8antr
eleqtrd syl6eleq fniniseg simplbda oveq1d cghm lmghm lspss sseqtrd sseldd
sstrd lspssv ghmlin eqtr2d cgrp lmhmlvec2 lmodgrp 3syl ad9antr ffvelrnd
grplid 3eqtr3d eqtr3d fnfvimad eqeltrd clsm wrex simp-7l lsmsp2 3eqtrrd
lsmelvalx r19.29vva fvelrnb sylan r19.29a ex ssrdv eqssd ssidd eqsstrd
linds1 lspcl reslmhm reslmhm2b wf1 csubg lsssubg resghm fnssres adantr
simpld fvresd simprd biimpar syl12anc syl6eleqr elind ineq2d 0ellsp fvexd
ghmid elsng elpreimad snssd cmnd grpmnd ress0g sneqd kerf1ghm eqidd f1eq123d
mpbird f1ssr f1f1orn f1oeq3d mpbid frn f1oeq123d islmim lspssid eqcomd
lmimlbs cen wbr f1imaeng hasheni oveq12d wb islinds4 exlimdv mpd ) EJKZBEALM
ZKZNZOPZDQRZKZOSZETRZDTRZCTRZUAMZUBZUYKUYMUCUDZUYOUYKDJKZVUAABDEFGHUEUYMDUYM
UFUGUHOUYMUIUJUYKUYNUYTOUYKUYNUYTUYKUYNNZUYLUKPZULZUYTUKEQRZVUCVUDVUFKZNZVUE
NZUYLVUDUYLUMZUNZUORZUYLUORZVUJUORZUAMZUYPUYSVUIUYNVUJUPKZUYLVUJUQZUCUBZVULV
UOUBVUCUYNVUGVUEUYKUYNURUSVUPVUIVUDUYLUKUTVAVBVURVUIUYLVUDVCVBUYLVUJUYMUPVDV
EVUIUYHVUKVUFKZUYPVULUBUYHUYJUYNVUGVUEVFVUIVUKEVGRZKVUKEVHRZRZEVIRZUBVUSVUIU
YLVVAVUJEEVJRZVVAUFVVDUFUYHUYJUYNVUGVUEVFVUCUYLVUTKZVUGVUEVUCEVKKZBVLZFVMZVN
ZEVORZKZUYLVVIULZUYLDVGRZKZVVEUYHVVFUYJUYNEVPUSUYJVVKUYHUYNEAVVJBVVIFVVIUFGV
VJUFVQVRVUCUYLDVIRZVVIVUCUYNUYLVVOULZUYKUYNURUYLUYMVVODVVOUFUYMUFVSUHUYJVVIV
VOUBZUYHUYNUYJVVIVVCULZVVQUYJBVTZVVIVVCVVIVVIVVSVVIUFBVVHWAWBUYJVVCAVIRZBVVC
VVTEABVVCUFVVTUFWCWDWEVVIVVCDEHVVCUFWFUHVRWGVUCUYMVVMUYLUYMDUYMUFWHUYKUYNURW
IVVFVVKVVLWJZVVNVVEVVIVVJUYLEDVVJUFHWKWLWMUSVUIVVFVUDVUTKZVUJVUDULZVUJVUTKZV
UCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUFVUTVUDVUFEVUFUFWHVUCVUGVUEWNWIVUIVUDUYLW
OVUDVUJEWPVEVUIUYLVVARZVUJVVARZUQVWFVWEUQZVVDVMZVWFVWEWQUYHVUGVUEVWGVWHUBZUY
JUYNVUDVUFVVAUYLEVVDVUFUFVVAUFVVDUFWRWSWTXAVUIVVBVUDVVARZVVCVUIVUKVUDVVAVUIV
UEVUKVUDUBZVUHVUEURUYLVUDXBUJXCVUIVUGVWJVVCUBZVUCVUGVUEWNVUGVWBVWLVVCVUFVVAE
VUDVVCUFVUFUFVVAUFXDXEUHXFVVCVUFVVAEVUKVVCUFVUFUFVVAUFXDXGVUKEVUFVUFUFXHXIVU
IUYQVUMUYRVUNUAVUIVUBUYNUYQVUMUBUYKVUBUYNVUGVUEABDEFGHUEXJVUCUYNVUGVUEUYKUYN
URUSUYLDUYMUYMUFXHXIVUIUYRBVWFXKZVUJVNZUORZVUNVUICJKZVWNCQRZKZUYRVWOUBUYKVWP
UYNVUGVUEABCEIXLXJVUIVWMEVWFXMMZCXNMZKZVUJVWSQRZKZVWRVUIVWMVWSCLMZKZVWSVIRZC
VIRZVWMXOZVXAVUIAVKKZBXPZAVORZKZVWMXPZVXJULZVWMVWSALMZKZVXEVUIUYJVXIUYHUYJUY
NVUGVUEXQEABXRUHVUIUYJVXLUYHUYJUYNVUGVUEXQEABXSUHVUIVXMVXJVXJVUIVXMBVWFVNZVX
JBVWFXTVUIVXQVXJVXQVXJULZVUIBVWFYAVBVUIYBVXJVXQVUIYBPZVXJKZVXSVXQKZVUIVXTNZY
CPZBRZVXSUBZVYAYCVVCVYBVYCVVCKZNZVYENZVYCYDPZYEPZEYFRZMZUBZVYAYDYEVWEVWFVYHV
YIVWEKZNZVYJVWFKZNZVYMNZVXSVYJBRZVXQVYRVYDVXSVYSVYGVYEVYNVYPVYMXQVYRVYIBRZVY
SAYFRZMZFVYSWUAMZVYDVYSVYRVYTFVYSWUAVYRBVVCYGZVYIVVIKZVYTFUBZVUIWUDVXTVYFVYE
VYNVYPVYMVUIVVCVVTBUYJVVCVVTBYHZUYHUYNVUGVUEVVCVVTEABVVCUFVVTUFWCYIYJYKVYRVY
IVVIVVIVYRVYIVWEVVIVYHVYNVYPVYMYLVUCVWEVVIUBZVUGVUEVXTVYFVYEVYNVYPVYMVUCUYLD
VHRZRZVVOVWEVVIVUCUYNWUJVVOUBZUYKUYNURUYLUYMWUIVVODVVOUFUYMUFWUIUFYMUHVUCVVF
VVKVVLVWEWUJUBZUYHVVFUYJUYNEVPUSUYJVVKUYHUYNEAVVJBVVIFVVIUFGVVJUFVQVRVUCUYLV
VOVVIVUCUYNVVPUYKUYNURUYLUYMVVODVVOUFUYMUFVSUHUYJVVQUYHUYNUYJVVRVVQUYJVVSVVI
VVCVVIVVIVVSVVIUFBVVHWAWBUYJVVCVVTBVVCVVTEABVVCUFVVTUFWCWDWEVVIVVCDEHVVCUFWF
UHVRWGVVIUYLVVJVVAWUIEDHVVAUFWUIUFVVJUFYNVEUYJVVQUYHUYNUYJVVRVVQUYJVVSVVIVVC
VVIVVIVVSVVIUFBVVHWAWBUYJVVCVVTBVVCVVTEABVVCUFVVTUFWCWDWEVVIVVCDEHVVCUFWFUHV
RYOYPYQVVIUFYRWUDWUEVYIVVCKZWUFVVCFVYIBYSYTXIUUAVYRVYDVYLBRZWUBVYRVYCVYLBVYQ
VYMURXCVYRBEAUUBMZKZWUMVYJVVCKZWUNWUBUBZVUIWUPVXTVYFVYEVYNVYPVYMUYJWUPUYHUYN
VUGVUEEABUUCYIYKVYRVWEVVCVYIVYHVWEVVCULZVYNVYPVYMVUIWUSVXTVYFVYEVUIVWEVWJVVC
VUIVVFVUDVVCULZVUEVWEVWJULZVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUGWUTVUCVUGVUE
WNVUDVUFVVCEVVCUFVUFUFVSUHVUHVUEURUYLVUDVVAVVCEVVCUFVVAUFUUDVEVUIVUGVWLVUCVU
GVUEWNVUGVWBVWLVVCVUFVVAEVUDVVCUFVUFUFVVAUFXDXEUHUUEXJXJVYHVYNVYPVYMYLUUFVYR
VWFVVCVYJVYHVWFVVCULZVYNVYPVYMVUIWVBVXTVYFVYEVUIVVFVUJVVCULZWVBVUCVVFVUGVUEU
YHVVFUYJUYNEVPUSUSVUIVUJVUDVVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUF
VUFUFVSUHUUGVUJVVAVVCEVVCUFVVAUFUUHXIXJXJVYOVYPVYMWNUUFVYKWUAEAVYIBVYJVVCVVC
UFVYKUFWUAUFUUIVEUUJVYRAUUKKZVYSVVTKZWUCVYSUBZUYKWVDUYNVUGVUEVXTVYFVYEVYNVYP
VYMUYKAJKZVXIWVDABEUULAVPAUUMUUNUUOVYRVVCVVTVYJBVUIWUGVXTVYFVYEVYNVYPVYMUYJW
UGUYHUYNVUGVUEVVCVVTEABVVCUFVVTUFWCYIYKVYRVWFVVCVYJVYHWVBVYNVYPVYMVUIWVBVXTV
YFVYEVUIVVFWVCWVBVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUJVUDVVCVUIVUDUYLWOVUIVU
GWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGVUJVVAVVCEVVCUFVVAUFUUHXIXJXJVYOVY
PVYMWNUUFUUPVVTWUAAVYSFVVTUFWUAUFGUUQXIUURUUSVYRVVCVYJVWFBVUIWUDVXTVYFVYEVYN
VYPVYMVUIVVCVVTBUYJWUGUYHUYNVUGVUEVVCVVTEABVVCUFVVTUFWCYIYJYKVYRVWFVVCVYJVYH
WVBVYNVYPVYMVUIWVBVXTVYFVYEVUIVVFWVCWVBVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUJ
VUDVVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGVUJVVAVVCEVV
CUFVVAUFUUHXIXJXJVYOVYPVYMWNUUFVYOVYPVYMWNUUTUVAVYHUYHWUSWVBVYCVWEVWFEUVBRZM
ZKZVYMYEVWFUVCZYDVWEUVCZUYHUYJUYNVUGVUEVXTVYFVYEUVDVUIWUSVXTVYFVYEVUIVWEVWJV
VCVUIVVFWUTVUEWVAVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUGWUTVUCVUGVUEWNVUDVUFVV
CEVVCUFVUFUFVSUHVUHVUEURUYLVUDVVAVVCEVVCUFVVAUFUUDVEVUIVUGVWLVUCVUGVUEWNVUGV
WBVWLVVCVUFVVAEVUDVVCUFVUFUFVVAUFXDXEUHUUEXJVUIWVBVXTVYFVYEVUIVVFWVCWVBVUCVV
FVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUJVUDVVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFV
VCEVVCUFVUFUFVSUHUUGVUJVVAVVCEVVCUFVVAUFUUHXIXJVYHVYCVVCWVIVYBVYFVYEWNVUIVVC
WVIUBZVXTVYFVYEVUIWVIVVBVWJVVCVUIVVFUYLVVCULZWVCWVIVVBUBZVUCVVFVUGVUEUYHVVFU
YJUYNEVPUSUSVUIUYLVVIVVCVUCVVLVUGVUEVUCUYLVVOVVIVUCUYNVVPUYKUYNURUYLUYMVVODV
VOUFUYMUFVSUHUYJVVQUYHUYNUYJVVRVVQUYJVVSVVIVVCVVIVVIVVSVVIUFBVVHWAWBUYJVVCVV
TBVVCVVTEABVVCUFVVTUFWCWDWEVVIVVCDEHVVCUFWFUHVRWGUSUYJVVRUYHUYNVUGVUEUYJVVSV
VIVVCVVIVVIVVSVVIUFBVVHWAWBUYJVVCVVTBVVCVVTEABVVCUFVVTUFWCWDWEYIUUGVUIVUJVUD
VVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGWVHUYLVUJVVAVVC
EVVCUFVVAUFWVHUFUVEVEVUIVUKVUDVVAVUIVUEVWKVUHVUEURUYLVUDXBUJXCVUIVUGVWLVUCVU
GVUEWNVUGVWBVWLVVCVUFVVAEVUDVVCUFVUFUFVVAUFXDXEUHUVFXJYQUYHWUSWVBWJZWVJWVLYD
YEVVCVYKWVHVWEVWFEJVYCVVCUFVYKUFWVHUFUVGWLWMUVHVUIWUDVXTVYEYCVVCUVCZVUIVVCVV
TBUYJWUGUYHUYNVUGVUEVVCVVTEABVVCUFVVTUFWCYIYJWUDVXTWVQYCVVCVXSBUVIWLUVJUVKUV
LUVMUVNWTVUIVXJUVOUVPVUIUYJVWFVVJKZVXPUYHUYJUYNVUGVUEXQVUIVVFWVCWVRVUIUYHVVF
UYHUYJUYNVUGVUEVFEVPUHVUIVWDWVCVUIVVFVWBVWCVWDVUCVVFVUGVUEUYHVVFUYJUYNEVPUSU
SVUIVUFVUTVUDVUFEVUFUFWHVUCVUGVUEWNWIVUIVUDUYLWOVUDVUJEWPVEVVCEVUJVVCUFUVQUH
VVJVUJVVAVVCEVVCUFVVJUFVVAUFUVRXIVWSEAVVJBVWFVVJUFVWSUFUVSXIVXIVXLVXNWJVXPVX
EVWSACVWMVXKVXJIVXKUFUVTWLWMVUIVWFVXJVWMXOZVXHVUIVWFVXMVWMXOZWVSVUIVWFVXJVWM
UWAZWVTVUIVWFVVTVWMUWAZVXNWWAVUIWWBVXFVVTVWMUWAZVUIVWMVWSAUUBMZKZVWMVLZVVHVN
ZVWSVJRZVMZUBZWWCVUIWUPVWFEUWBRZKZWWEUYJWUPUYHUYNVUGVUEEABUUCYIVUIVVFWVRWWLV
UCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVVFWVCWVRVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUI
VUJVUDVVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGVVJVUJVVA
VVCEVVCUFVVJUFVVAUFUVRXIVVJVWFEVVJUFUWCXIEAVWSBVWFVWSUFUWDXIVUIWWGVWHWWIVUIW
WGVWHVUIYCWWGVWHVUIVYCWWGKZVYCVWHKZVUIWWMNZVYCVWFVVIUQZVWHWWOVWFVVIVYCWWOVYC
VWFKZVYCVWMRZFUBZWWOVWMVWFYGZWWMWWQWWSNZVUIWWTWWMVUIWUDWVBWWTVUIVVCVVTBUYJWU
GUYHUYNVUGVUEVVCVVTEABVVCUFVVTUFWCYIYJVUIVVFWVCWVBVUCVVFVUGVUEUYHVVFUYJUYNEV
PUSUSVUIVUJVUDVVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGV
UJVVAVVCEVVCUFVVAUFUUHXIVVCVWFBUWEXIUWFVUIWWMURWWTWWMWXAVWFFVYCVWMYSWLXIUWGW
WOVYCVVIVVIWWOWUDVYFVYDFUBZVYCVVIKZVUIWUDWWMVUIVVCVVTBUYJWUGUYHUYNVUGVUEVVCV
VTEABVVCUFVVTUFWCYIYJUWFWWOVWFVVCVYCVUIWVBWWMVUIVVFWVCWVBVUCVVFVUGVUEUYHVVFU
YJUYNEVPUSUSVUIVUJVUDVVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFV
SUHUUGVUJVVAVVCEVVCUFVVAUFUUHXIUWFWWOWWQWWSWWOWWTWWMWXAVUIWWTWWMVUIWUDWVBWWT
VUIVVCVVTBUYJWUGUYHUYNVUGVUEVVCVVTEABVVCUFVVTUFWCYIYJVUIVVFWVCWVBVUCVVFVUGVU
EUYHVVFUYJUYNEVPUSUSVUIVUJVUDVVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVC
UFVUFUFVSUHUUGVUJVVAVVCEVVCUFVVAUFUUHXIVVCVWFBUWEXIUWFVUIWWMURWWTWWMWXAVWFFV
YCVWMYSWLXIUWGUUFWWOWWRVYDFWWOVYCVWFBWWOWWQWWSWWOWWTWWMWXAVUIWWTWWMVUIWUDWVB
WWTVUIVVCVVTBUYJWUGUYHUYNVUGVUEVVCVVTEABVVCUFVVTUFWCYIYJVUIVVFWVCWVBVUCVVFVU
GVUEUYHVVFUYJUYNEVPUSUSVUIVUJVUDVVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCE
VVCUFVUFUFVSUHUUGVUJVVAVVCEVVCUFVVAUFUUHXIVVCVWFBUWEXIUWFVUIWWMURWWTWWMWXAVW
FFVYCVWMYSWLXIUWGUWHWWOWWQWWSWWOWWTWWMWXAVUIWWTWWMVUIWUDWVBWWTVUIVVCVVTBUYJW
UGUYHUYNVUGVUEVVCVVTEABVVCUFVVTUFWCYIYJVUIVVFWVCWVBVUCVVFVUGVUEUYHVVFUYJUYNE
VPUSUSVUIVUJVUDVVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUG
VUJVVAVVCEVVCUFVVAUFUUHXIVVCVWFBUWEXIUWFVUIWWMURWWTWWMWXAVWFFVYCVWMYSWLXIUWI
UUSWUDWXCVYFWXBNZVVCFVYCBYSUWJUWKVVIUFUWLUWMVUIWWPVWHUBZWWMVUIVWGWWPVWHVUIVW
EVVIVWFVUCWUHVUGVUEVUCWUJVVOVWEVVIVUCUYNWUKUYKUYNURUYLUYMWUIVVODVVOUFUYMUFWU
IUFYMUHVUCVVFVVKVVLWULUYHVVFUYJUYNEVPUSUYJVVKUYHUYNEAVVJBVVIFVVIUFGVVJUFVQVR
VUCUYLVVOVVIVUCUYNVVPUYKUYNURUYLUYMVVODVVOUFUYMUFVSUHUYJVVQUYHUYNUYJVVRVVQUY
JVVSVVIVVCVVIVVIVVSVVIUFBVVHWAWBUYJVVCVVTBVVCVVTEABVVCUFVVTUFWCWDWEVVIVVCDEH
VVCUFWFUHVRWGVVIUYLVVJVVAWUIEDHVVAUFWUIUFVVJUFYNVEUYJVVQUYHUYNUYJVVRVVQUYJVV
SVVIVVCVVIVVIVVSVVIUFBVVHWAWBUYJVVCVVTBVVCVVTEABVVCUFVVTUFWCWDWEVVIVVCDEHVVC
UFWFUHVRYOUSUWNUYHVUGVUEVWIUYJUYNVUDVUFVVAUYLEVVDVUFUFVVAUFVVDUFWRWSUUSUWFYQ
UVLUVMVUIVVDWWGVUIVWFVVDVVHVWMVUIWUDWVBWWTVUIVVCVVTBUYJWUGUYHUYNVUGVUEVVCVVT
EABVVCUFVVTUFWCYIYJVUIVVFWVCWVBVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUJVUDVVCVU
IVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGVUJVVAVVCEVVCUFVVAUF
UUHXIVVCVWFBUWEXIVUIVVFWVCVVDVWFKZVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUJVUDVV
CVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGVVCVUJVVAEVVDVVDU
FVVCUFVVAUFUWOXIVUIVVDVWMRZUPKZWXGFUBZWXGVVHKZVUIVVDVWMUWPVUIWXGVVDBRZFVUIVV
DVWFBVUIVVFWVCWXFVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUJVUDVVCVUIVUDUYLWOVUIVU
GWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGVVCVUJVVAEVVDVVDUFVVCUFVVAUFUWOXIU
WHUYJWXKFUBZUYHUYNVUGVUEUYJWUPWXLEABUUCEABVVDFVVDUFGUWQUHYIXFWXHWXJWXIWXGFUP
UWRUWJXIUWSUWTUVNVUIVVDWWHVUIEUXAKZWXFWVBVVDWWHUBZVUIVVFEUUKKZWXMVUCVVFVUGVU
EUYHVVFUYJUYNEVPUSUSEUUMEUXBUUNVUIVVFWVCWXFVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVU
IVUJVUDVVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGVVCVUJVV
AEVVDVVDUFVVCUFVVAUFUWOXIVUIVVFWVCWVBVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUJVU
DVVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGVUJVVAVVCEVVCU
FVVAUFUUHXIVWFVVCEVWSVVDVWSUFVVCUFVVDUFUXCVEUXDXFWWEWWCWWJVXFVVTVWSAVWMWWHFV
XFUFVVTUFWWHUFGUXEUWJXIVUIVWFVXFVVTVVTVWMVWMVUIVWMUXFVUIWVBVWFVXFUBZVUIVVFWV
CWVBVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUJVUDVVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUE
WNVUDVUFVVCEVVCUFVUFUFVSUHUUGVUJVVAVVCEVVCUFVVAUFUUHXIVWFVVCVWSEVWSUFVVCUFWF
UHVVTVVTUBZVUIVVTUFVBUXGUXHVUIVXMVXJVXJVUIVXMVXQVXJBVWFXTVUIVXQVXJVXRVUIBVWF
YAVBVUIYBVXJVXQVUIVXTVYAVYBVYEVYAYCVVCVYHVYMVYAYDYEVWEVWFVYRVXSVYSVXQVYRVYDV
XSVYSVYGVYEVYNVYPVYMXQVYRWUBWUCVYDVYSVYRVYTFVYSWUAVYRWUDWUEWUFVUIWUDVXTVYFVY
EVYNVYPVYMVUIVVCVVTBUYJWUGUYHUYNVUGVUEVVCVVTEABVVCUFVVTUFWCYIYJYKVYRVYIVVIVV
IVYRVYIVWEVVIVYHVYNVYPVYMYLVUCWUHVUGVUEVXTVYFVYEVYNVYPVYMVUCWUJVVOVWEVVIVUCU
YNWUKUYKUYNURUYLUYMWUIVVODVVOUFUYMUFWUIUFYMUHVUCVVFVVKVVLWULUYHVVFUYJUYNEVPU
SUYJVVKUYHUYNEAVVJBVVIFVVIUFGVVJUFVQVRVUCUYLVVOVVIVUCUYNVVPUYKUYNURUYLUYMVVO
DVVOUFUYMUFVSUHUYJVVQUYHUYNUYJVVRVVQUYJVVSVVIVVCVVIVVIVVSVVIUFBVVHWAWBUYJVVC
VVTBVVCVVTEABVVCUFVVTUFWCWDWEVVIVVCDEHVVCUFWFUHVRWGVVIUYLVVJVVAWUIEDHVVAUFWU
IUFVVJUFYNVEUYJVVQUYHUYNUYJVVRVVQUYJVVSVVIVVCVVIVVIVVSVVIUFBVVHWAWBUYJVVCVVT
BVVCVVTEABVVCUFVVTUFWCWDWEVVIVVCDEHVVCUFWFUHVRYOYPYQVVIUFYRWUDWUEWUMWUFVVCFV
YIBYSYTXIUUAVYRVYDWUNWUBVYRVYCVYLBVYQVYMURXCVYRWUPWUMWUQWURVUIWUPVXTVYFVYEVY
NVYPVYMUYJWUPUYHUYNVUGVUEEABUUCYIYKVYRVWEVVCVYIVYHWUSVYNVYPVYMVUIWUSVXTVYFVY
EVUIVWEVWJVVCVUIVVFWUTVUEWVAVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUGWUTVUCVUGVU
EWNVUDVUFVVCEVVCUFVUFUFVSUHVUHVUEURUYLVUDVVAVVCEVVCUFVVAUFUUDVEVUIVUGVWLVUCV
UGVUEWNVUGVWBVWLVVCVUFVVAEVUDVVCUFVUFUFVVAUFXDXEUHUUEXJXJVYHVYNVYPVYMYLUUFVY
RVWFVVCVYJVYHWVBVYNVYPVYMVUIWVBVXTVYFVYEVUIVVFWVCWVBVUCVVFVUGVUEUYHVVFUYJUYN
EVPUSUSVUIVUJVUDVVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUU
GVUJVVAVVCEVVCUFVVAUFUUHXIXJXJVYOVYPVYMWNUUFVYKWUAEAVYIBVYJVVCVVCUFVYKUFWUAU
FUUIVEUUJVYRWVDWVEWVFUYKWVDUYNVUGVUEVXTVYFVYEVYNVYPVYMUYKWVGVXIWVDABEUULAVPA
UUMUUNUUOVYRVVCVVTVYJBVUIWUGVXTVYFVYEVYNVYPVYMUYJWUGUYHUYNVUGVUEVVCVVTEABVVC
UFVVTUFWCYIYKVYRVWFVVCVYJVYHWVBVYNVYPVYMVUIWVBVXTVYFVYEVUIVVFWVCWVBVUCVVFVUG
VUEUYHVVFUYJUYNEVPUSUSVUIVUJVUDVVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEV
VCUFVUFUFVSUHUUGVUJVVAVVCEVVCUFVVAUFUUHXIXJXJVYOVYPVYMWNUUFUUPVVTWUAAVYSFVVT
UFWUAUFGUUQXIUURUUSVYRVVCVYJVWFBVUIWUDVXTVYFVYEVYNVYPVYMVUIVVCVVTBUYJWUGUYHU
YNVUGVUEVVCVVTEABVVCUFVVTUFWCYIYJYKVYRVWFVVCVYJVYHWVBVYNVYPVYMVUIWVBVXTVYFVY
EVUIVVFWVCWVBVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUJVUDVVCVUIVUDUYLWOVUIVUGWUT
VUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGVUJVVAVVCEVVCUFVVAUFUUHXIXJXJVYOVYPVYM
WNUUFVYOVYPVYMWNUUTUVAVYHUYHWUSWVBWVJWVLUYHUYJUYNVUGVUEVXTVYFVYEUVDVUIWUSVXT
VYFVYEVUIVWEVWJVVCVUIVVFWUTVUEWVAVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUGWUTVUC
VUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHVUHVUEURUYLVUDVVAVVCEVVCUFVVAUFUUDVEVUIVUGVW
LVUCVUGVUEWNVUGVWBVWLVVCVUFVVAEVUDVVCUFVUFUFVVAUFXDXEUHUUEXJVUIWVBVXTVYFVYEV
UIVVFWVCWVBVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUJVUDVVCVUIVUDUYLWOVUIVUGWUTVU
CVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGVUJVVAVVCEVVCUFVVAUFUUHXIXJVYHVYCVVCWVIV
YBVYFVYEWNVUIWVMVXTVYFVYEVUIWVIVVBVWJVVCVUIVVFWVNWVCWVOVUCVVFVUGVUEUYHVVFUYJ
UYNEVPUSUSVUIUYLVVIVVCVUCVVLVUGVUEVUCUYLVVOVVIVUCUYNVVPUYKUYNURUYLUYMVVODVVO
UFUYMUFVSUHUYJVVQUYHUYNUYJVVRVVQUYJVVSVVIVVCVVIVVIVVSVVIUFBVVHWAWBUYJVVCVVTB
VVCVVTEABVVCUFVVTUFWCWDWEVVIVVCDEHVVCUFWFUHVRWGUSUYJVVRUYHUYNVUGVUEUYJVVSVVI
VVCVVIVVIVVSVVIUFBVVHWAWBUYJVVCVVTBVVCVVTEABVVCUFVVTUFWCWDWEYIUUGVUIVUJVUDVV
CVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGWVHUYLVUJVVAVVCEV
VCUFVVAUFWVHUFUVEVEVUIVUKVUDVVAVUIVUEVWKVUHVUEURUYLVUDXBUJXCVUIVUGVWLVUCVUGV
UEWNVUGVWBVWLVVCVUFVVAEVUDVVCUFVUFUFVVAUFXDXEUHUVFXJYQWVPWVJWVLYDYEVVCVYKWVH
VWEVWFEJVYCVVCUFVYKUFWVHUFUVGWLWMUVHVUIWUDVXTWVQVUIVVCVVTBUYJWUGUYHUYNVUGVUE
VVCVVTEABVVCUFVVTUFWCYIYJWUDVXTWVQYCVVCVXSBUVIWLUVJUVKUVLUVMUVNWTVUIVXJUVOUV
PVWFVVTVXJVWMUXIXIVWFVXJVWMUXJUHVUIVXMVXJVWFVWMVUIVXMVXQVXJBVWFXTVUIVXQVXJVX
RVUIBVWFYAVBVUIYBVXJVXQVUIVXTVYAVYBVYEVYAYCVVCVYHVYMVYAYDYEVWEVWFVYRVXSVYSVX
QVYRVYDVXSVYSVYGVYEVYNVYPVYMXQVYRWUBWUCVYDVYSVYRVYTFVYSWUAVYRWUDWUEWUFVUIWUD
VXTVYFVYEVYNVYPVYMVUIVVCVVTBUYJWUGUYHUYNVUGVUEVVCVVTEABVVCUFVVTUFWCYIYJYKVYR
VYIVVIVVIVYRVYIVWEVVIVYHVYNVYPVYMYLVUCWUHVUGVUEVXTVYFVYEVYNVYPVYMVUCWUJVVOVW
EVVIVUCUYNWUKUYKUYNURUYLUYMWUIVVODVVOUFUYMUFWUIUFYMUHVUCVVFVVKVVLWULUYHVVFUY
JUYNEVPUSUYJVVKUYHUYNEAVVJBVVIFVVIUFGVVJUFVQVRVUCUYLVVOVVIVUCUYNVVPUYKUYNURU
YLUYMVVODVVOUFUYMUFVSUHUYJVVQUYHUYNUYJVVRVVQUYJVVSVVIVVCVVIVVIVVSVVIUFBVVHWA
WBUYJVVCVVTBVVCVVTEABVVCUFVVTUFWCWDWEVVIVVCDEHVVCUFWFUHVRWGVVIUYLVVJVVAWUIED
HVVAUFWUIUFVVJUFYNVEUYJVVQUYHUYNUYJVVRVVQUYJVVSVVIVVCVVIVVIVVSVVIUFBVVHWAWBU
YJVVCVVTBVVCVVTEABVVCUFVVTUFWCWDWEVVIVVCDEHVVCUFWFUHVRYOYPYQVVIUFYRWUDWUEWUM
WUFVVCFVYIBYSYTXIUUAVYRVYDWUNWUBVYRVYCVYLBVYQVYMURXCVYRWUPWUMWUQWURVUIWUPVXT
VYFVYEVYNVYPVYMUYJWUPUYHUYNVUGVUEEABUUCYIYKVYRVWEVVCVYIVYHWUSVYNVYPVYMVUIWUS
VXTVYFVYEVUIVWEVWJVVCVUIVVFWUTVUEWVAVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUGWUT
VUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHVUHVUEURUYLVUDVVAVVCEVVCUFVVAUFUUDVEVUIVU
GVWLVUCVUGVUEWNVUGVWBVWLVVCVUFVVAEVUDVVCUFVUFUFVVAUFXDXEUHUUEXJXJVYHVYNVYPVY
MYLUUFVYRVWFVVCVYJVYHWVBVYNVYPVYMVUIWVBVXTVYFVYEVUIVVFWVCWVBVUCVVFVUGVUEUYHV
VFUYJUYNEVPUSUSVUIVUJVUDVVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUF
UFVSUHUUGVUJVVAVVCEVVCUFVVAUFUUHXIXJXJVYOVYPVYMWNUUFVYKWUAEAVYIBVYJVVCVVCUFV
YKUFWUAUFUUIVEUUJVYRWVDWVEWVFUYKWVDUYNVUGVUEVXTVYFVYEVYNVYPVYMUYKWVGVXIWVDAB
EUULAVPAUUMUUNUUOVYRVVCVVTVYJBVUIWUGVXTVYFVYEVYNVYPVYMUYJWUGUYHUYNVUGVUEVVCV
VTEABVVCUFVVTUFWCYIYKVYRVWFVVCVYJVYHWVBVYNVYPVYMVUIWVBVXTVYFVYEVUIVVFWVCWVBV
UCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUJVUDVVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUD
VUFVVCEVVCUFVUFUFVSUHUUGVUJVVAVVCEVVCUFVVAUFUUHXIXJXJVYOVYPVYMWNUUFUUPVVTWUA
AVYSFVVTUFWUAUFGUUQXIUURUUSVYRVVCVYJVWFBVUIWUDVXTVYFVYEVYNVYPVYMVUIVVCVVTBUY
JWUGUYHUYNVUGVUEVVCVVTEABVVCUFVVTUFWCYIYJYKVYRVWFVVCVYJVYHWVBVYNVYPVYMVUIWVB
VXTVYFVYEVUIVVFWVCWVBVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUJVUDVVCVUIVUDUYLWOV
UIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGVUJVVAVVCEVVCUFVVAUFUUHXIXJXJV
YOVYPVYMWNUUFVYOVYPVYMWNUUTUVAVYHUYHWUSWVBWVJWVLUYHUYJUYNVUGVUEVXTVYFVYEUVDV
UIWUSVXTVYFVYEVUIVWEVWJVVCVUIVVFWUTVUEWVAVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIV
UGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHVUHVUEURUYLVUDVVAVVCEVVCUFVVAUFUUDVE
VUIVUGVWLVUCVUGVUEWNVUGVWBVWLVVCVUFVVAEVUDVVCUFVUFUFVVAUFXDXEUHUUEXJVUIWVBVX
TVYFVYEVUIVVFWVCWVBVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUJVUDVVCVUIVUDUYLWOVUI
VUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGVUJVVAVVCEVVCUFVVAUFUUHXIXJVYHVY
CVVCWVIVYBVYFVYEWNVUIWVMVXTVYFVYEVUIWVIVVBVWJVVCVUIVVFWVNWVCWVOVUCVVFVUGVUEU
YHVVFUYJUYNEVPUSUSVUIUYLVVIVVCVUCVVLVUGVUEVUCUYLVVOVVIVUCUYNVVPUYKUYNURUYLUY
MVVODVVOUFUYMUFVSUHUYJVVQUYHUYNUYJVVRVVQUYJVVSVVIVVCVVIVVIVVSVVIUFBVVHWAWBUY
JVVCVVTBVVCVVTEABVVCUFVVTUFWCWDWEVVIVVCDEHVVCUFWFUHVRWGUSUYJVVRUYHUYNVUGVUEU
YJVVSVVIVVCVVIVVIVVSVVIUFBVVHWAWBUYJVVCVVTBVVCVVTEABVVCUFVVTUFWCWDWEYIUUGVUI
VUJVUDVVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGWVHUYLVUJ
VVAVVCEVVCUFVVAUFWVHUFUVEVEVUIVUKVUDVVAVUIVUEVWKVUHVUEURUYLVUDXBUJXCVUIVUGVW
LVUCVUGVUEWNVUGVWBVWLVVCVUFVVAEVUDVVCUFVUFUFVVAUFXDXEUHUVFXJYQWVPWVJWVLYDYEV
VCVYKWVHVWEVWFEJVYCVVCUFVYKUFWVHUFUVGWLWMUVHVUIWUDVXTWVQVUIVVCVVTBUYJWUGUYHU
YNVUGVUEVVCVVTEABVVCUFVVTUFWCYIYJWUDVXTWVQYCVVCVXSBUVIWLUVJUVKUVLUVMUVNWTUXK
UXLVUIVWFVXFVXJVXGVWMVWMVUIVWMUXFVUIWVBWXPVUIVVFWVCWVBVUIUYHVVFUYHUYJUYNVUGV
UEVFEVPUHVUIVWDWVCVUIVVFVWBVWCVWDVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUFVUTVUD
VUFEVUFUFWHVUCVUGVUEWNWIVUIVUDUYLWOVUDVUJEWPVEVVCEVUJVVCUFUVQUHVUJVVAVVCEVVC
UFVVAUFUUHXIVWFVVCVWSEVWSUFVVCUFWFUHVUIUYJVXJVXGUBZUYHUYJUYNVUGVUEXQUYJWUGVX
JVVTULWXRVVCVVTEABVVCUFVVTUFWCVVCVVTBUXMVXJVVTCAIVVTUFWFUUNUHUXNUXLVXFVXGVWS
CVWMVXFUFVXGUFUXOXGVUIVUJVWSVGRZKZVUJVWSVHRZRZVXFUBVXCVUIVVFWVRVUJVWFULZVWDW
XTVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVVFWVCWVRVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUS
VUIVUJVUDVVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGVVJVUJ
VVAVVCEVVCUFVVJUFVVAUFUVRXIVUIVVFWVCWYCVUIUYHVVFUYHUYJUYNVUGVUEVFEVPUHVUIVWD
WVCVUIVVFVWBVWCVWDVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUFVUTVUDVUFEVUFUFWHVUCV
UGVUEWNWIVUIVUDUYLWOVUDVUJEWPVEVVCEVUJVVCUFUVQUHVUJVVAVVCEVVCUFVVAUFUXPXIVUI
VVFVWBVWCVWDVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUFVUTVUDVUFEVUFUFWHVUCVUGVUEW
NWIVUIVUDUYLWOVUDVUJEWPVEVVFWVRWYCWJWXTVWDVWFVVJVUJEVWSVVJUFVWSUFWKUWJWMVUIW
YBVWFVXFVUIVWFWYBVUIVVFWVRWYCVWFWYBUBVUIUYHVVFUYHUYJUYNVUGVUEVFEVPUHVUIVVFWV
CWVRVUIUYHVVFUYHUYJUYNVUGVUEVFEVPUHVUIVWDWVCVUIVVFVWBVWCVWDVUCVVFVUGVUEUYHVV
FUYJUYNEVPUSUSVUIVUFVUTVUDVUFEVUFUFWHVUCVUGVUEWNWIVUIVUDUYLWOVUDVUJEWPVEVVCE
VUJVVCUFUVQUHVVJVUJVVAVVCEVVCUFVVJUFVVAUFUVRXIVUIVVFWVCWYCVUIUYHVVFUYHUYJUYN
VUGVUEVFEVPUHVUIVWDWVCVUIVVFVWBVWCVWDVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUFVU
TVUDVUFEVUFUFWHVUCVUGVUEWNWIVUIVUDUYLWOVUDVUJEWPVEVVCEVUJVVCUFUVQUHVUJVVAVVC
EVVCUFVVAUFUXPXIVWFVUJVVJVVAWYAEVWSVWSUFVVAUFWYAUFVVJUFYNVEUXQVUIWVBWXPVUIVV
FWVCWVBVUIUYHVVFUYHUYJUYNVUGVUEVFEVPUHVUIVWDWVCVUIVVFVWBVWCVWDVUCVVFVUGVUEUY
HVVFUYJUYNEVPUSUSVUIVUFVUTVUDVUFEVUFUFWHVUCVUGVUEWNWIVUIVUDUYLWOVUDVUJEWPVEV
VCEVUJVVCUFUVQUHVUJVVAVVCEVVCUFVVAUFUUHXIVWFVVCVWSEVWSUFVVCUFWFUHXFVXFVXBWYA
VWSVUJVXFUFVXBUFWYAUFXDXGVUJVWSCVWMVXBVWQVXBUFVWQUFUXRXIVWNCVWQVWQUFXHXIVUIW
WAWYCVWDVWOVUNUBZVUIWWBVXNWWAVUIWWBWWCVUIWWEWWJWWCVUIWUPWWLWWEUYJWUPUYHUYNVU
GVUEEABUUCYIVUIVVFWVRWWLVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVVFWVCWVRVUCVVFVUG
VUEUYHVVFUYJUYNEVPUSUSVUIVUJVUDVVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEV
VCUFVUFUFVSUHUUGVVJVUJVVAVVCEVVCUFVVJUFVVAUFUVRXIVVJVWFEVVJUFUWCXIEAVWSBVWFV
WSUFUWDXIVUIWWGVWHWWIVUIWWGVWHVUIYCWWGVWHVUIWWMWWNWWOVYCWWPVWHWWOVWFVVIVYCWW
OWWQWWSWWOWWTWWMWXAVUIWWTWWMVUIWUDWVBWWTVUIVVCVVTBUYJWUGUYHUYNVUGVUEVVCVVTEA
BVVCUFVVTUFWCYIYJVUIVVFWVCWVBVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUJVUDVVCVUIV
UDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGVUJVVAVVCEVVCUFVVAUFUU
HXIVVCVWFBUWEXIUWFVUIWWMURWWTWWMWXAVWFFVYCVWMYSWLXIUWGWWOVYCVVIVVIWWOWUDVYFW
XBWXCVUIWUDWWMVUIVVCVVTBUYJWUGUYHUYNVUGVUEVVCVVTEABVVCUFVVTUFWCYIYJUWFWWOVWF
VVCVYCVUIWVBWWMVUIVVFWVCWVBVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUJVUDVVCVUIVUD
UYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGVUJVVAVVCEVVCUFVVAUFUUHX
IUWFWWOWWQWWSWWOWWTWWMWXAVUIWWTWWMVUIWUDWVBWWTVUIVVCVVTBUYJWUGUYHUYNVUGVUEVV
CVVTEABVVCUFVVTUFWCYIYJVUIVVFWVCWVBVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUJVUDV
VCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGVUJVVAVVCEVVCUFV
VAUFUUHXIVVCVWFBUWEXIUWFVUIWWMURWWTWWMWXAVWFFVYCVWMYSWLXIUWGUUFWWOWWRVYDFWWO
VYCVWFBWWOWWQWWSWWOWWTWWMWXAVUIWWTWWMVUIWUDWVBWWTVUIVVCVVTBUYJWUGUYHUYNVUGVU
EVVCVVTEABVVCUFVVTUFWCYIYJVUIVVFWVCWVBVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUJV
UDVVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGVUJVVAVVCEVVC
UFVVAUFUUHXIVVCVWFBUWEXIUWFVUIWWMURWWTWWMWXAVWFFVYCVWMYSWLXIUWGUWHWWOWWQWWSW
WOWWTWWMWXAVUIWWTWWMVUIWUDWVBWWTVUIVVCVVTBUYJWUGUYHUYNVUGVUEVVCVVTEABVVCUFVV
TUFWCYIYJVUIVVFWVCWVBVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUJVUDVVCVUIVUDUYLWOV
UIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGVUJVVAVVCEVVCUFVVAUFUUHXIVVCVW
FBUWEXIUWFVUIWWMURWWTWWMWXAVWFFVYCVWMYSWLXIUWIUUSWUDWXCWXDVVCFVYCBYSUWJUWKVV
IUFUWLUWMVUIWXEWWMVUIVWGWWPVWHVUIVWEVVIVWFVUCWUHVUGVUEVUCWUJVVOVWEVVIVUCUYNW
UKUYKUYNURUYLUYMWUIVVODVVOUFUYMUFWUIUFYMUHVUCVVFVVKVVLWULUYHVVFUYJUYNEVPUSUY
JVVKUYHUYNEAVVJBVVIFVVIUFGVVJUFVQVRVUCUYLVVOVVIVUCUYNVVPUYKUYNURUYLUYMVVODVV
OUFUYMUFVSUHUYJVVQUYHUYNUYJVVRVVQUYJVVSVVIVVCVVIVVIVVSVVIUFBVVHWAWBUYJVVCVVT
BVVCVVTEABVVCUFVVTUFWCWDWEVVIVVCDEHVVCUFWFUHVRWGVVIUYLVVJVVAWUIEDHVVAUFWUIUF
VVJUFYNVEUYJVVQUYHUYNUYJVVRVVQUYJVVSVVIVVCVVIVVIVVSVVIUFBVVHWAWBUYJVVCVVTBVV
CVVTEABVVCUFVVTUFWCWDWEVVIVVCDEHVVCUFWFUHVRYOUSUWNUYHVUGVUEVWIUYJUYNVUDVUFVV
AUYLEVVDVUFUFVVAUFVVDUFWRWSUUSUWFYQUVLUVMVUIVVDWWGVUIVWFVVDVVHVWMVUIWUDWVBWW
TVUIVVCVVTBUYJWUGUYHUYNVUGVUEVVCVVTEABVVCUFVVTUFWCYIYJVUIVVFWVCWVBVUCVVFVUGV
UEUYHVVFUYJUYNEVPUSUSVUIVUJVUDVVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVV
CUFVUFUFVSUHUUGVUJVVAVVCEVVCUFVVAUFUUHXIVVCVWFBUWEXIVUIVVFWVCWXFVUCVVFVUGVUE
UYHVVFUYJUYNEVPUSUSVUIVUJVUDVVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCU
FVUFUFVSUHUUGVVCVUJVVAEVVDVVDUFVVCUFVVAUFUWOXIVUIWXHWXIWXJVUIVVDVWMUWPVUIWXG
WXKFVUIVVDVWFBVUIVVFWVCWXFVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUJVUDVVCVUIVUDU
YLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGVVCVUJVVAEVVDVVDUFVVCUFVV
AUFUWOXIUWHUYJWXLUYHUYNVUGVUEUYJWUPWXLEABUUCEABVVDFVVDUFGUWQUHYIXFWXHWXJWXIW
XGFUPUWRUWJXIUWSUWTUVNVUIVVDWWHVUIWXMWXFWVBWXNVUIVVFWXOWXMVUCVVFVUGVUEUYHVVF
UYJUYNEVPUSUSEUUMEUXBUUNVUIVVFWVCWXFVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUJVUD
VVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGVVCVUJVVAEVVDVV
DUFVVCUFVVAUFUWOXIVUIVVFWVCWVBVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUJVUDVVCVUI
VUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGVUJVVAVVCEVVCUFVVAUFU
UHXIVWFVVCEVWSVVDVWSUFVVCUFVVDUFUXCVEUXDXFWWEWWCWWJVXFVVTVWSAVWMWWHFVXFUFVVT
UFWWHUFGUXEUWJXIVUIVWFVXFVVTVVTVWMVWMVUIVWMUXFVUIWVBWXPVUIVVFWVCWVBVUCVVFVUG
VUEUYHVVFUYJUYNEVPUSUSVUIVUJVUDVVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEV
VCUFVUFUFVSUHUUGVUJVVAVVCEVVCUFVVAUFUUHXIVWFVVCVWSEVWSUFVVCUFWFUHWXQVUIVVTUF
VBUXGUXHVUIVXMVXJVXJVUIVXMVXQVXJBVWFXTVUIVXQVXJVXRVUIBVWFYAVBVUIYBVXJVXQVUIV
XTVYAVYBVYEVYAYCVVCVYHVYMVYAYDYEVWEVWFVYRVXSVYSVXQVYRVYDVXSVYSVYGVYEVYNVYPVY
MXQVYRWUBWUCVYDVYSVYRVYTFVYSWUAVYRWUDWUEWUFVUIWUDVXTVYFVYEVYNVYPVYMVUIVVCVVT
BUYJWUGUYHUYNVUGVUEVVCVVTEABVVCUFVVTUFWCYIYJYKVYRVYIVVIVVIVYRVYIVWEVVIVYHVYN
VYPVYMYLVUCWUHVUGVUEVXTVYFVYEVYNVYPVYMVUCWUJVVOVWEVVIVUCUYNWUKUYKUYNURUYLUYM
WUIVVODVVOUFUYMUFWUIUFYMUHVUCVVFVVKVVLWULUYHVVFUYJUYNEVPUSUYJVVKUYHUYNEAVVJB
VVIFVVIUFGVVJUFVQVRVUCUYLVVOVVIVUCUYNVVPUYKUYNURUYLUYMVVODVVOUFUYMUFVSUHUYJV
VQUYHUYNUYJVVRVVQUYJVVSVVIVVCVVIVVIVVSVVIUFBVVHWAWBUYJVVCVVTBVVCVVTEABVVCUFV
VTUFWCWDWEVVIVVCDEHVVCUFWFUHVRWGVVIUYLVVJVVAWUIEDHVVAUFWUIUFVVJUFYNVEUYJVVQU
YHUYNUYJVVRVVQUYJVVSVVIVVCVVIVVIVVSVVIUFBVVHWAWBUYJVVCVVTBVVCVVTEABVVCUFVVTU
FWCWDWEVVIVVCDEHVVCUFWFUHVRYOYPYQVVIUFYRWUDWUEWUMWUFVVCFVYIBYSYTXIUUAVYRVYDW
UNWUBVYRVYCVYLBVYQVYMURXCVYRWUPWUMWUQWURVUIWUPVXTVYFVYEVYNVYPVYMUYJWUPUYHUYN
VUGVUEEABUUCYIYKVYRVWEVVCVYIVYHWUSVYNVYPVYMVUIWUSVXTVYFVYEVUIVWEVWJVVCVUIVVF
WUTVUEWVAVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFV
UFUFVSUHVUHVUEURUYLVUDVVAVVCEVVCUFVVAUFUUDVEVUIVUGVWLVUCVUGVUEWNVUGVWBVWLVVC
VUFVVAEVUDVVCUFVUFUFVVAUFXDXEUHUUEXJXJVYHVYNVYPVYMYLUUFVYRVWFVVCVYJVYHWVBVYN
VYPVYMVUIWVBVXTVYFVYEVUIVVFWVCWVBVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUJVUDVVC
VUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGVUJVVAVVCEVVCUFVVA
UFUUHXIXJXJVYOVYPVYMWNUUFVYKWUAEAVYIBVYJVVCVVCUFVYKUFWUAUFUUIVEUUJVYRWVDWVEW
VFUYKWVDUYNVUGVUEVXTVYFVYEVYNVYPVYMUYKWVGVXIWVDABEUULAVPAUUMUUNUUOVYRVVCVVTV
YJBVUIWUGVXTVYFVYEVYNVYPVYMUYJWUGUYHUYNVUGVUEVVCVVTEABVVCUFVVTUFWCYIYKVYRVWF
VVCVYJVYHWVBVYNVYPVYMVUIWVBVXTVYFVYEVUIVVFWVCWVBVUCVVFVUGVUEUYHVVFUYJUYNEVPU
SUSVUIVUJVUDVVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGVUJ
VVAVVCEVVCUFVVAUFUUHXIXJXJVYOVYPVYMWNUUFUUPVVTWUAAVYSFVVTUFWUAUFGUUQXIUURUUS
VYRVVCVYJVWFBVUIWUDVXTVYFVYEVYNVYPVYMVUIVVCVVTBUYJWUGUYHUYNVUGVUEVVCVVTEABVV
CUFVVTUFWCYIYJYKVYRVWFVVCVYJVYHWVBVYNVYPVYMVUIWVBVXTVYFVYEVUIVVFWVCWVBVUCVVF
VUGVUEUYHVVFUYJUYNEVPUSUSVUIVUJVUDVVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVV
CEVVCUFVUFUFVSUHUUGVUJVVAVVCEVVCUFVVAUFUUHXIXJXJVYOVYPVYMWNUUFVYOVYPVYMWNUUT
UVAVYHUYHWUSWVBWVJWVLUYHUYJUYNVUGVUEVXTVYFVYEUVDVUIWUSVXTVYFVYEVUIVWEVWJVVCV
UIVVFWUTVUEWVAVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIVUGWUTVUCVUGVUEWNVUDVUFVVCEV
VCUFVUFUFVSUHVUHVUEURUYLVUDVVAVVCEVVCUFVVAUFUUDVEVUIVUGVWLVUCVUGVUEWNVUGVWBV
WLVVCVUFVVAEVUDVVCUFVUFUFVVAUFXDXEUHUUEXJVUIWVBVXTVYFVYEVUIVVFWVCWVBVUCVVFVU
GVUEUYHVVFUYJUYNEVPUSUSVUIVUJVUDVVCVUIVUDUYLWOVUIVUGWUTVUCVUGVUEWNVUDVUFVVCE
VVCUFVUFUFVSUHUUGVUJVVAVVCEVVCUFVVAUFUUHXIXJVYHVYCVVCWVIVYBVYFVYEWNVUIWVMVXT
VYFVYEVUIWVIVVBVWJVVCVUIVVFWVNWVCWVOVUCVVFVUGVUEUYHVVFUYJUYNEVPUSUSVUIUYLVVI
VVCVUCVVLVUGVUEVUCUYLVVOVVIVUCUYNVVPUYKUYNURUYLUYMVVODVVOUFUYMUFVSUHUYJVVQUY
HUYNUYJVVRVVQUYJVVSVVIVVCVVIVVIVVSVVIUFBVVHWAWBUYJVVCVVTBVVCVVTEABVVCUFVVTUF
WCWDWEVVIVVCDEHVVCUFWFUHVRWGUSUYJVVRUYHUYNVUGVUEUYJVVSVVIVVCVVIVVIVVSVVIUFBV
VHWAWBUYJVVCVVTBVVCVVTEABVVCUFVVTUFWCWDWEYIUUGVUIVUJVUDVVCVUIVUDUYLWOVUIVUGW
UTVUCVUGVUEWNVUDVUFVVCEVVCUFVUFUFVSUHUUGWVHUYLVUJVVAVVCEVVCUFVVAUFWVHUFUVEVE
VUIVUKVUDVVAVUIVUEVWKVUHVUEURUYLVUDXBUJXCVUIVUGVWLVUCVUGVUEWNVUGVWBVWLVVCVUF
VVAEVUDVVCUFVUFUFVVAUFXDXEUHUVFXJYQWVPWVJWVLYDYEVVCVYKWVHVWEVWFEJVYCVVCUFVYK
UFWVHUFUVGWLWMUVHVUIWUDVXTWVQVUIVVCVVTBUYJWUGUYHUYNVUGVUEVVCVVTEABVVCUFVVTUF
WCYIYJWUDVXTWVQYCVVCVXSBUVIWLUVJUVKUVLUVMUVNWTVUIVXJUVOUVPVWFVVTVXJVWMUXIXIV
UIVVFWVCWYCVUIUYHVVFUYHUYJUYNVUGVUEVFEVPUHVUIVWDWVCVUIVVFVWBVWCVWDVUCVVFVUGV
UEUYHVVFUYJUYNEVPUSUSVUIVUFVUTVUDVUFEVUFUFWHVUCVUGVUEWNWIVUIVUDUYLWOVUDVUJEW
PVEVVCEVUJVVCUFUVQUHVUJVVAVVCEVVCUFVVAUFUXPXIVUIVVFVWBVWCVWDVUCVVFVUGVUEUYHV
VFUYJUYNEVPUSUSVUIVUFVUTVUDVUFEVUFUFWHVUCVUGVUEWNWIVUIVUDUYLWOVUDVUJEWPVEWWA
WYCVWDWJVWNVUJUXSUXTWYDVWFVXJVUJVWMVUTUYAVWNVUJUYBUHVEXFUYCYOVUCVVEVUEUKVUFU
VCZVUCVVFVVKVVLVVNVVEUYHVVFUYJUYNEVPUSUYJVVKUYHUYNEAVVJBVVIFVVIUFGVVJUFVQVRV
UCUYLVVOVVIVUCUYNVVPUYKUYNURUYLUYMVVODVVOUFUYMUFVSUHUYJVVQUYHUYNUYJVVRVVQUYJ
VVSVVIVVCVVIVVIVVSVVIUFBVVHWAWBUYJVVCVVTBVVCVVTEABVVCUFVVTUFWCWDWEVVIVVCDEHV
VCUFWFUHVRWGVUCUYMVVMUYLUYMDUYMUFWHUYKUYNURWIVWAVVNVVEVVIVVJUYLEDVVJUFHWKWLW
MUYHVVEWYEUYDUYJUYNVUFEUYLUKVUFUFUYEUSUXLUVKUVLUYFUYG $.
$d K w
$d k w
$d b k
$d b c
$d c w
$d c k
$d V k
$d V c
$d x y
$d V x
$d V y
$d F x
$d F y
$d .0. x
$d .0. y
$d b x
$d b y
$d w x
$d w y
$d k x
$d k y
$d c x
$d c y
$d V b
$d b w
$d U x
$d K x
$d U y
$d K y
$d K b
$d I b
$d F b
$d U b
$d V w
$d I w
$d F w
$d U w
$d V u
$d V v
$d u v
$d u w
$d u x
$d v w
$d v x
$d b u
$d b v
$d u y
$d F u
$d F v
$d v y
$d U u
$d U v
$d K u
$d K v
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment