:: Isomorphism Theorem on Vector Spaces over a Ring
:: by Yuichi Futa and Yasunari Shidama
::
:: 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 b1 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
b1 . A = f . a
proof end;
uniqueness
for b1, b2 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
b1 . A = f . a ) & ( for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
b2 . A = f . a ) holds
b1 = b2
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 b6 being linear-transformation of (VectQuot (V,W)),U holds
( b6 = QFunctional (f,W) iff for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
b6 . 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;
coherence
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 b1 being non empty FinSequence st
for S being set st S in rng b1 holds
S is VectSp of K
proof end;
end;

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

registration
let K be Ring;
coherence
for b1 being VectorSpace-Sequence of K holds b1 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 b1 being MultOps of the carrier of K, carr G st
( len b1 = len (carr G) & ( for j being Element of dom (carr G) holds b1 . j = the lmult of (G . j) ) )
proof end;
uniqueness
for b1, b2 being MultOps of the carrier of K, carr G st len b1 = len (carr G) & ( for j being Element of dom (carr G) holds b1 . j = the lmult of (G . j) ) & len b2 = len (carr G) & ( for j being Element of dom (carr G) holds b2 . j = the lmult of (G . j) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines multop VECTSP12:def 4 :
for K being Ring
for G being VectorSpace-Sequence of K
for b3 being MultOps of the carrier of K, carr G holds
( b3 = multop G iff ( len b3 = len (carr G) & ( for j being Element of dom (carr G) holds b3 . 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)),[:():],(),[:():] #);
coherence
ModuleStr(# (product (carr 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)),[:():],(),[:():] #);

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
( ([:():] . (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
([:():] . (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
( ([:():] . (r,v)) . i = the lmult of (G . i) . (r,(v . i)) & ( for vi being Vector of (G . i) st vi = v . i holds
([:():] . (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;
coherence
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 b1 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 b1 . (r,[g,f]) = [(r * g),(r * f)]
proof end;
uniqueness
for b1, b2 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 b1 . (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 b2 . (r,[g,f]) = [(r * g),(r * f)] ) holds
b1 = b2
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 b4 being Function of [: the carrier of K,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] holds
( b4 = prod_MLT (G,F) iff for r being Element of K
for g being Vector of G
for f being Vector of F holds b4 . (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;
correctness
coherence
;
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;
correctness
coherence ;
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 ;

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;
correctness
coherence ;
proof end;
end;

registration
let K be Ring;
let G, F be non empty scalar-distributive ModuleStr over K;
correctness
coherence ;
proof end;
end;

registration
let K be Ring;
let G, F be non empty scalar-associative ModuleStr over K;
correctness
coherence ;
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,() 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. () )
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 ^ Y)) st
( I is one-to-one & I is onto & ( for x being Vector of ()
for y being Vector of () ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Vector of [:(),():] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of [:(),():]
for r being Element of the carrier of K holds I . (r * v) = r * (I . v) ) & I . (0. [:(),():]) = 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;