:: Isomorphism Theorem on Vector Spaces over a Ring :: by Yuichi Futa and Yasunari Shidama :: :: Received August 30, 2017 :: Copyright (c) 2017-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies VECTSP_1, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCSDOM, FINSET_1, CARD_1, CARD_3, ARYTM_3, ARYTM_1, MOD_3, FINSEQ_1, VALUED_1, SUPINF_2, MSSUBFAM, STRUCT_0, RLSUB_1, RLSUB_2, RLVECT_2, SETWISEO, ORDINAL4, RLVECT_3, UNIALG_1, RANKNULL, UPROOTS, VECTSP10, ZMODUL05, QC_LANG1, RLVECT_5, ALGSTR_0, VECTSP12, GROUP_2, PRVECT_1, PRVECT_2, BINOP_1, NUMBERS, RLVECT_1, ZFMISC_1, NAT_1, FUNCT_6, FINSEQOP, MESFUNC1, PRVECT_3; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, BINOP_1, FINSET_1, CARD_1, ORDINAL1, CARD_3, XCMPLX_0, NUMBERS, FINSEQ_1, FINSEQOP, STRUCT_0, SETWISEO, ALGSTR_0, RLVECT_1, VECTSP_1, MOD_2, RLVECT_2, VECTSP_4, VECTSP_5, VECTSP_6, MATRLIN, VECTSP_7, VECTSP_9, VECTSP10, PRVECT_1, PRVECT_2, PRVECT_3, RANKNULL, ZMODUL05, ZMODUL07; constructors RELSET_1, REALSET1, FINSEQOP, RLVECT_2, VECTSP_9, WELLORD2, SETWISEO, PRVECT_2, ZMODUL05, ZMODUL07, PRVECT_3; registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, FINSET_1, RLVECT_1, CARD_3, FINSEQ_1, PRVECT_1, PRVECT_2, XREAL_0, STRUCT_0, MATRLIN, RANKNULL, VECTSP_9, VECTSP_1, FUNCT_2, ALGSTR_0, PRVECT_3; requirements BOOLE, SUBSET, NUMERALS; begin :: 1. Bijective linear transformation reserve K,F for Ring; reserve V,W for VectSp of K; reserve l for Linear_Combination of V; reserve T for linear-transformation of V,W; theorem :: VECTSP12:1 for K being Field, V,W being finite-dimensional VectSp of K, A being Subset of V, B being Basis of V, T being linear-transformation of V, W, l being Linear_Combination of B \ A st A is Basis of ker T & A c= B holds T.(Sum l) = Sum(T@*l); theorem :: VECTSP12:2 for F being Field, X, Y being VectSp of F, T being linear-transformation of X, Y, A being Subset of X st T is bijective holds A is Basis of X iff T.: A is Basis of Y; theorem :: VECTSP12:3 for F being Field, X, Y being VectSp of F, T being linear-transformation of X, Y st T is bijective holds X is finite-dimensional iff Y is finite-dimensional; theorem :: VECTSP12:4 for F being Field, X being finite-dimensional VectSp of F, Y being VectSp of F, T being linear-transformation of X, Y st T is bijective holds Y is finite-dimensional & dim(X) = dim(Y); theorem :: VECTSP12:5 for F being Field, X, Y being VectSp of F, l being Linear_Combination of X, T being linear-transformation of X, Y st T is one-to-one holds T @ l = T @* l; begin :: 2. Properties of linear combinations on modules over a ring theorem :: VECTSP12:6 for K being Field,V being VectSp of K, W1, W2 being Subspace of V, I1 being Basis of W1, I2 being Basis of W2 st V is_the_direct_sum_of W1,W2 holds I1 /\ I2 = {}; theorem :: VECTSP12:7 for K being Field,V being VectSp of K, W1, W2 being Subspace of V, I1 being Basis of W1, I2 being Basis of W2, I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds Lin(I) = the ModuleStr of V; theorem :: VECTSP12:8 for K being Field,V being VectSp of K, W1, W2 being Subspace of V, I1 being Basis of W1, I2 being Basis of W2, I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds I is linearly-independent; theorem :: VECTSP12:9 for K being Field,V being VectSp of K, W1, W2 being Subspace of V, I1 being Basis of W1,I2 being Basis of W2 st W1 /\ W2 = (0).V holds I1 \/ I2 is Basis of W1+W2; begin :: 3. 1st isomorphism theorem theorem :: VECTSP12:10 for K being Field for V being finite-dimensional VectSp of K, W being Subspace of V holds ex S being Linear_Compl of W, T being linear-transformation of S, VectQuot(V,W) st T is bijective & for v being Vector of V st v in S holds T.v = v+ W; theorem :: VECTSP12:11 for K being Field for V being finite-dimensional VectSp of K, W being Subspace of V holds VectQuot(V,W) is finite-dimensional & dim VectQuot(V,W) + dim W = dim V; definition let K be Ring; let V,U be VectSp of K; let W be Subspace of V; let f be linear-transformation of V,U; assume the carrier of W c= the carrier of ker f; func QFunctional(f,W) -> linear-transformation of VectQuot(V,W),U means :: VECTSP12:def 1 for A being Vector of VectQuot(V,W), a being Vector of V st A = a+W holds it.A = f.a; end; definition let K be Ring; let V,U be VectSp of K; let f be linear-transformation of V,U; func CQFunctional(f) -> linear-transformation of VectQuot(V,ker f),U equals :: VECTSP12:def 2 QFunctional(f,ker f); end; registration let K be Ring; let V,U be VectSp of K, f be linear-transformation of V,U; cluster CQFunctional(f) -> one-to-one; end; :: 1st isomorphism theorem theorem :: VECTSP12:12 for K being Ring, V, U being VectSp of K, f being linear-transformation of V,U holds ex T being linear-transformation of VectQuot(V,ker f), im f st T = CQFunctional(f) & T is bijective; definition let K be Ring, V, U, W be VectSp of K, f be linear-transformation of V, U, g be linear-transformation of U, W; redefine func g*f -> linear-transformation of V, W; end; begin :: 4. The product space of vector spaces definition let K be Ring; mode VectorSpace-Sequence of K -> non empty FinSequence means :: VECTSP12:def 3 for S be set st S in rng it holds S is VectSp of K; end; registration let K be Ring; cluster -> AbGroup-yielding for VectorSpace-Sequence of K; end; definition let K be Ring; let G be VectorSpace-Sequence of K; let j be Element of dom G; redefine func G.j -> VectSp of K; end; definition let K be Ring, G be VectorSpace-Sequence of K, j be Element of dom carr G; redefine func G.j -> VectSp of K; end; definition let K be Ring, G be VectorSpace-Sequence of K; func multop G -> MultOps of the carrier of K,carr G means :: VECTSP12:def 4 len it = len carr G & for j being Element of dom carr G holds it.j = the lmult of G.j; end; definition let K be Ring, G be VectorSpace-Sequence of K; func product G -> strict non empty ModuleStr over K equals :: VECTSP12:def 5 ModuleStr (# product carr G, [: addop G :], zeros G, [: multop G :] #); end; registration let K be Ring, G be VectorSpace-Sequence of K; cluster product G -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital; end; begin :: 5. Cartesian product of vector spaces reserve K for Ring; definition let K be Ring, G,F be non empty ModuleStr over K; func prod_MLT(G,F) -> Function of [:the carrier of K , [:the carrier of G,the carrier of F:] :], [:the carrier of G,the carrier of F:] means :: VECTSP12:def 6 for r being Element of K, g be Vector of G, f being Vector of F holds it.(r,[g,f]) = [r*g,r*f]; end; definition let K be Ring; let G,F be non empty ModuleStr over K; func [:G,F:] -> strict non empty ModuleStr over K equals :: VECTSP12:def 7 ModuleStr (# [:the carrier of G,the carrier of F:], prod_ADD(G,F), prod_ZERO(G,F), prod_MLT(G,F) #); end; registration let K be Ring; let G,F be Abelian non empty ModuleStr over K; cluster [:G,F:] -> Abelian; end; registration let K be Ring; let G,F be add-associative non empty ModuleStr over K; cluster [:G,F:] -> add-associative; end; registration let K be Ring; let G, F be right_zeroed non empty ModuleStr over K; cluster [:G,F:] -> right_zeroed; end; registration let K be Ring; let G,F be right_complementable non empty ModuleStr over K; cluster [:G,F:] -> right_complementable; end; theorem :: VECTSP12:13 for G, F being non empty ModuleStr over K holds ( for x being set holds (x is Vector of [:G,F:] iff ex x1 being Vector of G, x2 being Vector of F st x=[x1,x2]) ) & ( for x, y being Vector of [:G,F:], x1, y1 being Vector of G, x2, y2 being Vector of F st x = [x1,x2] & y = [y1,y2] holds x+y = [x1+y1,x2+y2] ) & 0.[:G,F:] = [0.G,0.F] & ( for x being Vector of [:G,F:], x1 being Vector of G, x2 be Vector of F, a being Element of K st x = [x1,x2] holds a*x = [a*x1,a*x2] ); theorem :: VECTSP12:14 for G,F being add-associative right_zeroed right_complementable non empty ModuleStr over K, x being Vector of [:G,F:], x1 being Vector of G, x2 be Vector of F st x = [x1,x2] holds -x = [-x1,-x2]; registration let K be Ring; let G, F be vector-distributive non empty ModuleStr over K; cluster [:G,F:] -> vector-distributive; end; registration let K be Ring; let G, F be scalar-distributive non empty ModuleStr over K; cluster [:G,F:] -> scalar-distributive; end; registration let K be Ring; let G,F be scalar-associative non empty ModuleStr over K; cluster [:G,F:] -> scalar-associative; end; registration let K be Ring; let G, F be scalar-unital non empty ModuleStr over K; cluster [:G,F:] -> scalar-unital; end; definition let K be Ring; let G be VectSp of K; redefine func <* G *> -> VectorSpace-Sequence of K; end; definition let K be Ring; let G, F be VectSp of K; redefine func <* G,F *> -> VectorSpace-Sequence of K; end; theorem :: VECTSP12:15 for X being VectSp of K holds ex I being Function of X, product <*X*> st I is one-to-one onto & ( for x being Vector of X holds I.x = <*x*> ) & ( for v, w being Vector of X holds I.(v+w) = I.v + I.w ) & ( for v being Vector of X, r being Element of the carrier of K holds I.(r*v) = r*(I.v) ) & I.(0.X) = 0.product <*X*>; definition let K be Ring; let G, F be VectorSpace-Sequence of K; redefine func G^F -> VectorSpace-Sequence of K; end; theorem :: VECTSP12:16 for X, Y being VectSp of K holds ex I being Function of [:X,Y:],product <*X,Y*> st I is one-to-one onto & ( for x being Vector of X, y be Vector of Y holds I.(x,y) = <*x,y*> ) & ( for v, w being Vector of [:X,Y:] holds I.(v+w)=(I.v) + (I.w) ) & ( for v being Vector of [:X,Y:], r being Element of K holds I.(r*v) = r*(I.v) ) & I.(0.[:X,Y:]) = 0.product <*X,Y*>; theorem :: VECTSP12:17 for X, Y being VectorSpace-Sequence of K holds ex I being Function of [:product X,product Y:],product (X^Y) st I is one-to-one onto & ( for x being Vector of product X, y being Vector of product Y holds ex x1, y1 being FinSequence st x = x1 & y = y1 & I.(x,y) = x1^y1 ) & ( for v, w being Vector of [:product X,product Y:] holds I.(v+w) = I.v + I.w ) & ( for v being Vector of [:product X,product Y:], r be Element of the carrier of K holds I.(r*v) = r*(I.v) ) & I.(0.[:product X,product Y:]) = 0.product (X^Y); theorem :: VECTSP12:18 for G, F being VectSp of K holds ( for x being set holds ( x is Vector of product <*G,F*> iff ex x1 being Vector of G, x2 being Vector of F st x=<* x1,x2 *> ) ) & ( for x, y being Vector of product <*G,F*>, x1, y1 being Vector of G, x2, y2 being Vector of F st x = <*x1,x2*> & y = <*y1,y2*> holds x+y = <*x1+y1,x2+y2*> ) & 0.(product <*G,F*>) = <* 0.G,0.F *> & ( for x being Vector of product <*G,F*>, x1 being Vector of G, x2 being Vector of F st x = <* x1,x2 *> holds -x = <* -x1,-x2 *> ) & ( for x being Vector of product <*G,F*>, x1 being Vector of G, x2 being Vector of F, a being Element of K st x = <*x1,x2*> holds a*x = <* a*x1,a*x2 *> );