:: 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

theorem :: VECTSP12:1

for K being Field
for V, W being finite-dimensional VectSp of K
for A being Subset of V
for B being Basis of V
for T being linear-transformation of V,W
for l being Linear_Combination of B \ A st A is Basis of (ker T) & A c= B holds
T . (Sum l) = Sum (T @* l)

proof end;

HM11: for F being Field
for X, Y being VectSp of F
for T being linear-transformation of X,Y
for A being Subset of X st T is bijective & A is Basis of X holds
T .: A is Basis of Y

proof end;

theorem HM12: :: VECTSP12:2

for F being Field
for X, Y being VectSp of F
for T being linear-transformation of X,Y
for A being Subset of X st T is bijective holds
( A is Basis of X iff T .: A is Basis of Y )

proof end;

HM13: for F being Field
for X, Y being VectSp of F
for T being linear-transformation of X,Y st T is bijective & X is finite-dimensional holds
Y is finite-dimensional

proof end;

theorem HM151: :: VECTSP12:3

for F being Field
for X, Y being VectSp of F
for T being linear-transformation of X,Y st T is bijective holds
( X is finite-dimensional iff Y is finite-dimensional )

proof end;

theorem HM15: :: VECTSP12:4

for F being Field
for X being finite-dimensional VectSp of F
for Y being VectSp of F
for T being linear-transformation of X,Y st T is bijective holds
( Y is finite-dimensional & dim X = dim Y )

proof end;

theorem :: VECTSP12:5

for F being Field
for X, Y being VectSp of F
for l being Linear_Combination of X
for T being linear-transformation of X,Y st T is one-to-one holds
T @ l = T @* l

proof end;

theorem FRds1: :: VECTSP12:6

for K being Field
for V being VectSp of K
for W1, W2 being Subspace of V
for I1 being Basis of W1
for I2 being Basis of W2 st V is_the_direct_sum_of W1,W2 holds
I1 /\ I2 = {}

proof end;

theorem FRds2: :: VECTSP12:7

for K being Field
for V being VectSp of K
for W1, W2 being Subspace of V
for I1 being Basis of W1
for I2 being Basis of W2
for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds
Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)

proof end;

theorem FRds3: :: VECTSP12:8

for K being Field
for V being VectSp of K
for W1, W2 being Subspace of V
for I1 being Basis of W1
for I2 being Basis of W2
for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds
I is linearly-independent

proof end;

theorem :: VECTSP12:9

for K being Field
for V being VectSp of K
for W1, W2 being Subspace of V
for I1 being Basis of W1
for I2 being Basis of W2 st W1 /\ W2 = (0). V holds
I1 \/ I2 is Basis of (W1 + W2)

proof end;

theorem Th38A: :: VECTSP12:10

for K being Field
for V being finite-dimensional VectSp of K
for W being Subspace of V ex S being Linear_Compl of W ex 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 ) )

proof end;

theorem :: VECTSP12:11

for K being Field
for V being finite-dimensional VectSp of K
for W being Subspace of V holds
( VectQuot (V,W) is finite-dimensional & (dim (VectQuot (V,W))) + (dim W) = dim V )

proof end;

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 A1: the carrier of W c= the carrier of (ker f) ;

func QFunctional (f,W) -> linear-transformation of (VectQuot (V,W)),U means :Def12: :: VECTSP12:def 1
for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
it . A = f . a;

existence
ex b₁ being linear-transformation of (VectQuot (V,W)),U st
for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
b₁ . A = f . a

proof end;

uniqueness
for b₁, b₂ being linear-transformation of (VectQuot (V,W)),U st ( for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
b₁ . A = f . a ) & ( for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
b₂ . A = f . a ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def12 defines QFunctional VECTSP12:def 1 :
for K being Ring
for V, U being VectSp of K
for W being Subspace of V
for f being linear-transformation of V,U st the carrier of W c= the carrier of (ker f) holds
for b₆ being linear-transformation of (VectQuot (V,W)),U holds
( b₆ = QFunctional (f,W) iff for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
b₆ . A = f . a );

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));

coherence
QFunctional (f,(ker f)) is linear-transformation of (VectQuot (V,(ker f))),U ;

end;

:: deftheorem defines CQFunctional VECTSP12:def 2 :
for K being Ring
for V, U being VectSp of K
for f being linear-transformation of V,U holds CQFunctional f = QFunctional (f,(ker f));

registration

let K be Ring;
let V, U be VectSp of K;
let f be linear-transformation of V,U;

cluster CQFunctional f -> one-to-one ;

coherence
CQFunctional f is one-to-one

proof end;

end;

:: 1st isomorphism theorem

theorem :: VECTSP12:12

for K being Ring
for V, U being VectSp of K
for f being linear-transformation of V,U ex T being linear-transformation of (VectQuot (V,(ker f))),(im f) st
( T = CQFunctional f & T is bijective )

proof end;

definition

let K be Ring;
let V, U, W be VectSp of K;
let f be linear-transformation of V,U;
let g be linear-transformation of U,W;
:: original: (#)
redefine func g * f -> linear-transformation of V,W;
correctness
coherence
f (#) g is linear-transformation of V,W;

proof end;

end;

definition

let K be Ring;

mode VectorSpace-Sequence of K -> non empty FinSequence means :Def3: :: VECTSP12:def 3
for S being set st S in rng it holds
S is VectSp of K;

existence
ex b₁ being non empty FinSequence st
for S being set st S in rng b₁ holds
S is VectSp of K

proof end;

end;

:: deftheorem Def3 defines VectorSpace-Sequence VECTSP12:def 3 :
for K being Ring
for b₂ being non empty FinSequence holds
( b₂ is VectorSpace-Sequence of K iff for S being set st S in rng b₂ holds
S is VectSp of K );

registration

let K be Ring;

cluster -> AbGroup-yielding for VectorSpace-Sequence of K;

coherence
for b₁ being VectorSpace-Sequence of K holds b₁ is AbGroup-yielding

proof end;

end;

definition

let K be Ring;
let G be VectorSpace-Sequence of K;
let j be Element of dom G;
:: original: .
redefine func G . j -> VectSp of K;
coherence
G . j is VectSp of K

proof end;

end;

definition

let K be Ring;
let G be VectorSpace-Sequence of K;
let j be Element of dom (carr G);
:: original: .
redefine func G . j -> VectSp of K;
coherence
G . j is VectSp of K

proof end;

end;

definition

let K be Ring;
let G be VectorSpace-Sequence of K;

func multop G -> MultOps of the carrier of K, carr G means :Def8: :: VECTSP12:def 4
( len it = len (carr G) & ( for j being Element of dom (carr G) holds it . j = the lmult of (G . j) ) );

existence
ex b₁ being MultOps of the carrier of K, carr G st
( len b₁ = len (carr G) & ( for j being Element of dom (carr G) holds b₁ . j = the lmult of (G . j) ) )

proof end;

uniqueness
for b₁, b₂ being MultOps of the carrier of K, carr G st len b₁ = len (carr G) & ( for j being Element of dom (carr G) holds b₁ . j = the lmult of (G . j) ) & len b₂ = len (carr G) & ( for j being Element of dom (carr G) holds b₂ . j = the lmult of (G . j) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines multop VECTSP12:def 4 :
for K being Ring
for G being VectorSpace-Sequence of K
for b₃ being MultOps of the carrier of K, carr G holds
( b₃ = multop G iff ( len b₃ = len (carr G) & ( for j being Element of dom (carr G) holds b₃ . j = the lmult of (G . j) ) ) );

definition

let K be Ring;
let G be VectorSpace-Sequence of K;

func product G -> non empty strict ModuleStr over K equals :: VECTSP12:def 5
ModuleStr(# (product (carr G)),[:(addop G):],(zeros G),[:(multop G):] #);

coherence
ModuleStr(# (product (carr G)),[:(addop G):],(zeros G),[:(multop G):] #) is non empty strict ModuleStr over K ;

end;

:: deftheorem defines product VECTSP12:def 5 :
for K being Ring
for G being VectorSpace-Sequence of K holds product G = ModuleStr(# (product (carr G)),[:(addop G):],(zeros G),[:(multop G):] #);

Lm3: for K being Ring
for G being VectorSpace-Sequence of K
for v1, w1 being Element of product (carr G)
for i being Element of dom (carr G) holds
( ([:(addop G):] . (v1,w1)) . i = the addF of (G . i) . ((v1 . i),(w1 . i)) & ( for vi, wi being Vector of (G . i) st vi = v1 . i & wi = w1 . i holds
([:(addop G):] . (v1,w1)) . i = vi + wi ) )

proof end;

Lm4: for K being Ring
for G being VectorSpace-Sequence of K
for r being Element of K
for v being Element of product (carr G)
for i being Element of dom (carr G) holds
( ([:(multop G):] . (r,v)) . i = the lmult of (G . i) . (r,(v . i)) & ( for vi being Vector of (G . i) st vi = v . i holds
([:(multop G):] . (r,v)) . i = r * vi ) )

proof end;

Lm5: for K being Ring
for G being VectorSpace-Sequence of K holds
( product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital )

proof end;

registration

let K be Ring;
let G be VectorSpace-Sequence of K;

cluster product G -> non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence
( product G is Abelian & product G is add-associative & product G is right_zeroed & product G is right_complementable & product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital )

proof end;

end;

definition

let K be Ring;
let 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 :YDef2: :: VECTSP12:def 6
for r being Element of K
for g being Vector of G
for f being Vector of F holds it . (r,[g,f]) = [(r * g),(r * f)];

existence
ex b₁ being Function of [: the carrier of K,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] st
for r being Element of K
for g being Vector of G
for f being Vector of F holds b₁ . (r,[g,f]) = [(r * g),(r * f)]

proof end;

uniqueness
for b₁, b₂ being Function of [: the carrier of K,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] st ( for r being Element of K
for g being Vector of G
for f being Vector of F holds b₁ . (r,[g,f]) = [(r * g),(r * f)] ) & ( for r being Element of K
for g being Vector of G
for f being Vector of F holds b₂ . (r,[g,f]) = [(r * g),(r * f)] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem YDef2 defines prod_MLT VECTSP12:def 6 :
for K being Ring
for G, F being non empty ModuleStr over K
for b₄ being Function of [: the carrier of K,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] holds
( b₄ = prod_MLT (G,F) iff for r being Element of K
for g being Vector of G
for f being Vector of F holds b₄ . (r,[g,f]) = [(r * g),(r * f)] );

definition

let K be Ring;
let G, F be non empty ModuleStr over K;

func [:G,F:] -> non empty strict 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)) #);

correctness
coherence
ModuleStr(# [: the carrier of G, the carrier of F:],(prod_ADD (G,F)),(prod_ZERO (G,F)),(prod_MLT (G,F)) #) is non empty strict ModuleStr over K;

proof end;

end;

:: deftheorem defines [: VECTSP12:def 7 :
for K being Ring
for G, F being non empty ModuleStr over K holds [:G,F:] = ModuleStr(# [: the carrier of G, the carrier of F:],(prod_ADD (G,F)),(prod_ZERO (G,F)),(prod_MLT (G,F)) #);

registration

let K be Ring;
let G, F be non empty Abelian ModuleStr over K;

cluster [:G,F:] -> non empty Abelian strict ;

correctness
coherence
[:G,F:] is Abelian ;

proof end;

end;

registration

let K be Ring;
let G, F be non empty add-associative ModuleStr over K;

cluster [:G,F:] -> non empty add-associative strict ;

correctness
coherence
[:G,F:] is add-associative ;

proof end;

end;

registration

let K be Ring;
let G, F be non empty right_zeroed ModuleStr over K;

cluster [:G,F:] -> non empty right_zeroed strict ;

correctness
coherence
[:G,F:] is right_zeroed ;

proof end;

end;

registration

let K be Ring;
let G, F be non empty right_complementable ModuleStr over K;

cluster [:G,F:] -> non empty right_complementable strict ;

correctness
coherence
[:G,F:] is right_complementable ;

proof end;

end;

theorem :: VECTSP12:13

for K being Ring
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 ex x2 being Vector of F st x = [x1,x2] ) ) & ( for x, y being Vector of [:G,F:]
for x1, y1 being Vector of G
for 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:]
for x1 being Vector of G
for x2 being Vector of F
for a being Element of K st x = [x1,x2] holds
a * x = [(a * x1),(a * x2)] ) ) by YDef2, PRVECT_3:def 1, SUBSET_1:43;

theorem :: VECTSP12:14

for K being Ring
for G, F being non empty right_complementable add-associative right_zeroed ModuleStr over K
for x being Vector of [:G,F:]
for x1 being Vector of G
for x2 being Vector of F st x = [x1,x2] holds
- x = [(- x1),(- x2)]

proof end;

registration

let K be Ring;
let G, F be non empty vector-distributive ModuleStr over K;

cluster [:G,F:] -> non empty strict vector-distributive ;

correctness
coherence
[:G,F:] is vector-distributive ;

proof end;

end;

registration

let K be Ring;
let G, F be non empty scalar-distributive ModuleStr over K;

cluster [:G,F:] -> non empty strict scalar-distributive ;

correctness
coherence
[:G,F:] is scalar-distributive ;

proof end;

end;

registration

let K be Ring;
let G, F be non empty scalar-associative ModuleStr over K;

cluster [:G,F:] -> non empty strict scalar-associative ;

correctness
coherence
[:G,F:] is scalar-associative ;

proof end;

end;

registration

let K be Ring;
let G, F be non empty scalar-unital ModuleStr over K;

cluster [:G,F:] -> non empty strict scalar-unital ;

correctness
coherence
[:G,F:] is scalar-unital ;

proof end;

end;

definition

let K be Ring;
let G be VectSp of K;
:: original: <*
redefine func <*G*> -> VectorSpace-Sequence of K;
correctness
coherence
<*G*> is VectorSpace-Sequence of K;

proof end;

end;

definition

let K be Ring;
let G, F be VectSp of K;
:: original: <*
redefine func <*G,F*> -> VectorSpace-Sequence of K;
correctness
coherence
<*G,F*> is VectorSpace-Sequence of K;

proof end;

end;

theorem :: VECTSP12:15

for K being Ring
for X being VectSp of K ex I being Function of X,(product <*X*>) st
( I is one-to-one & I is 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
for r being Element of the carrier of K holds I . (r * v) = r * (I . v) ) & I . (0. X) = 0. (product <*X*>) )

proof end;

definition

let K be Ring;
let G, F be VectorSpace-Sequence of K;
:: original: ^
redefine func G ^ F -> VectorSpace-Sequence of K;
correctness
coherence
G ^ F is VectorSpace-Sequence of K;

proof end;

end;

theorem Th12: :: VECTSP12:16

for K being Ring
for X, Y being VectSp of K ex I being Function of [:X,Y:],(product <*X,Y*>) st
( I is one-to-one & I is onto & ( for x being Vector of X
for y being 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:]
for r being Element of K holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y:]) = 0. (product <*X,Y*>) )

proof end;

theorem :: VECTSP12:17

for K being Ring
for X, Y being VectorSpace-Sequence of K ex I being Function of [:(product X),(product Y):],(product (X ^ Y)) st
( I is one-to-one & I is onto & ( for x being Vector of (product X)
for y being Vector of (product Y) 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):]
for r being Element of the carrier of K holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) )

proof end;

theorem :: VECTSP12:18

for K being Ring
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 ex x2 being Vector of F st x = <*x1,x2*> ) ) & ( for x, y being Vector of (product <*G,F*>)
for x1, y1 being Vector of G
for 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*>)
for x1 being Vector of G
for x2 being Vector of F st x = <*x1,x2*> holds
- x = <*(- x1),(- x2)*> ) & ( for x being Vector of (product <*G,F*>)
for x1 being Vector of G
for x2 being Vector of F
for a being Element of K st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*> ) )

proof end;