Created
May 22, 2023 15:17
-
-
Save tirix/9e0d04f303b7f8a69a270f1598bfac2f to your computer and use it in GitHub Desktop.
dimkerim.mmp
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| $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