:: Linear Map of Matrices
:: by Karol P\c{a}k
::
:: Received May 13, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


begin

theorem Th1: :: MATRLIN2:1
for K being Field
for V being VectSp of K
for W1, W2, W12 being Subspace of V
for U1, U2 being Subspace of W12 st U1 = W1 & U2 = W2 holds
( W1 /\ W2 = U1 /\ U2 & W1 + W2 = U1 + U2 )
proofend;

theorem Th2: :: MATRLIN2:2
for K being Field
for V being VectSp of K
for W1, W2 being Subspace of V st W1 /\ W2 = (0). V holds
for B1 being linearly-independent Subset of W1
for B2 being linearly-independent Subset of W2 holds B1 \/ B2 is linearly-independent Subset of (W1 + W2)
proofend;

theorem Th3: :: MATRLIN2:3
for K being Field
for V being VectSp of K
for W1, W2 being Subspace of V st W1 /\ W2 = (0). V holds
for B1 being Basis of W1
for B2 being Basis of W2 holds B1 \/ B2 is Basis of W1 + W2
proofend;

theorem :: MATRLIN2:4
for K being Field
for V being finite-dimensional VectSp of K
for B being OrdBasis of (Omega). V holds B is OrdBasis of V
proofend;

theorem :: MATRLIN2:5
for K being Field
for V1 being VectSp of K
for A being finite Subset of V1 st dim (Lin A) = card A holds
A is linearly-independent
proofend;

theorem :: MATRLIN2:6
for K being Field
for V being VectSp of K
for A being finite Subset of V holds dim (Lin A) <= card A
proofend;

begin

Lm1:  for K being Field
for V1 being finite-dimensional VectSp of K
for R being FinSequence of V1
for p being FinSequence of K holds dom (lmlt (p,R)) = (dom p) /\ (dom R)
proofend;

Lm2:  for K being Field
for p1, p2 being FinSequence of K holds dom (p1 + p2) = (dom p1) /\ (dom p2)
proofend;

Lm3:  for K being Field
for V1 being finite-dimensional VectSp of K
for R1, R2 being FinSequence of V1 holds dom (R1 + R2) = (dom R1) /\ (dom R2)
proofend;

theorem Th7: :: MATRLIN2:7
for K being Field
for V1 being finite-dimensional VectSp of K
for R being FinSequence of V1
for p1, p2 being FinSequence of K holds lmlt ((p1 + p2),R) = (lmlt (p1,R)) + (lmlt (p2,R))
proofend;

theorem :: MATRLIN2:8
for K being Field
for V1 being finite-dimensional VectSp of K
for R1, R2 being FinSequence of V1
for p being FinSequence of K holds lmlt (p,(R1 + R2)) = (lmlt (p,R1)) + (lmlt (p,R2))
proofend;

theorem Th9: :: MATRLIN2:9
for K being Field
for V1 being finite-dimensional VectSp of K
for R1, R2 being FinSequence of V1
for p1, p2 being FinSequence of K st len p1 = len R1 &amp; len p2 = len R2 holds
lmlt ((p1 ^ p2),(R1 ^ R2)) = (lmlt (p1,R1)) ^ (lmlt (p2,R2))
proofend;

theorem :: MATRLIN2:10
for K being Field
for V1 being finite-dimensional VectSp of K
for R1, R2 being FinSequence of V1 st len R1 = len R2 holds
Sum (R1 + R2) = (Sum R1) + (Sum R2)
proofend;

theorem :: MATRLIN2:11
for K being Field
for a being Element of K
for V1 being finite-dimensional VectSp of K
for R being FinSequence of V1 holds Sum (lmlt (((len R) |-> a),R)) = a * (Sum R)
proofend;

theorem :: MATRLIN2:12
for K being Field
for V1 being finite-dimensional VectSp of K
for v1 being Element of V1
for p being FinSequence of K holds Sum (lmlt (p,((len p) |-> v1))) = (Sum p) * v1
proofend;

theorem :: MATRLIN2:13
for K being Field
for a being Element of K
for V1 being finite-dimensional VectSp of K
for R being FinSequence of V1
for p being FinSequence of K holds Sum (lmlt ((a * p),R)) = a * (Sum (lmlt (p,R)))
proofend;

theorem :: MATRLIN2:14
for K being Field
for V1 being finite-dimensional VectSp of K
for p being FinSequence of K
for B1 being FinSequence of V1
for W1 being Subspace of V1
for B2 being FinSequence of W1 st B1 = B2 holds
lmlt (p,B1) = lmlt (p,B2)
proofend;

theorem :: MATRLIN2:15
for K being Field
for V1 being finite-dimensional VectSp of K
for B1 being FinSequence of V1
for W1 being Subspace of V1
for B2 being FinSequence of W1 st B1 = B2 holds
Sum B1 = Sum B2
proofend;

theorem :: MATRLIN2:16
for i being Nat
for K being Field
for V1 being finite-dimensional VectSp of K
for R being FinSequence of V1 st i in dom R holds
Sum (lmlt ((Line ((1. (K,(len R))),i)),R)) = R /. i
proofend;

begin

theorem Th17: :: MATRLIN2:17
for K being Field
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for v1, w1 being Element of V1 holds (v1 + w1) |-- b1 = (v1 |-- b1) + (w1 |-- b1)
proofend;

theorem Th18: :: MATRLIN2:18
for K being Field
for a being Element of K
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for v1 being Element of V1 holds (a * v1) |-- b1 = a * (v1 |-- b1)
proofend;

theorem Th19: :: MATRLIN2:19
for i being Nat
for K being Field
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1 st i in dom b1 holds
(b1 /. i) |-- b1 = Line ((1. (K,(len b1))),i)
proofend;

theorem Th20: :: MATRLIN2:20
for K being Field
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1 holds (0. V1) |-- b1 = (len b1) |-> (0. K)
proofend;

theorem Th21: :: MATRLIN2:21
for K being Field
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1 holds len b1 = dim V1
proofend;

Lm4:  for K being Field
for V being VectSp of K
for W1 being Subspace of V
for L1 being Linear_Combination of W1 ex K1 being Linear_Combination of V st
( Carrier K1 = Carrier L1 &amp; Sum K1 = Sum L1 &amp; K1 | the carrier of W1 = L1 )
proofend;

theorem :: MATRLIN2:22
for m being Nat
for K being Field
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1 holds
( rng (b1 | m) is linearly-independent Subset of V1 &amp; ( for A being Subset of V1 st A = rng (b1 | m) holds
b1 | m is OrdBasis of Lin A ) )
proofend;

theorem :: MATRLIN2:23
for m being Nat
for K being Field
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1 holds
( rng (b1 /^ m) is linearly-independent Subset of V1 &amp; ( for A being Subset of V1 st A = rng (b1 /^ m) holds
b1 /^ m is OrdBasis of Lin A ) )
proofend;

theorem Th24: :: MATRLIN2:24
for K being Field
for V1 being finite-dimensional VectSp of K
for W1, W2 being Subspace of V1 st W1 /\ W2 = (0). V1 holds
for b1 being OrdBasis of W1
for b2 being OrdBasis of W2
for b being OrdBasis of W1 + W2 st b = b1 ^ b2 holds
for v, v1, v2 being Vector of (W1 + W2)
for w1 being Vector of W1
for w2 being Vector of W2 st v = v1 + v2 &amp; v1 = w1 &amp; v2 = w2 holds
v |-- b = (w1 |-- b1) ^ (w2 |-- b2)
proofend;

theorem Th25: :: MATRLIN2:25
for K being Field
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for W1 being Subspace of V1 st W1 = (Omega). V1 holds
for w being Vector of W1
for v being Vector of V1
for w1 being OrdBasis of W1 st v = w &amp; b1 = w1 holds
v |-- b1 = w |-- w1
proofend;

theorem Th26: :: MATRLIN2:26
for K being Field
for V1 being finite-dimensional VectSp of K
for W1, W2 being Subspace of V1 st W1 /\ W2 = (0). V1 holds
for w1 being OrdBasis of W1
for w2 being OrdBasis of W2 holds w1 ^ w2 is OrdBasis of W1 + W2
proofend;

begin

definition
let K be Field;
let V1, V2 be finite-dimensional VectSp of K;
let f be Function of V1,V2;
let B1 be FinSequence of V1;
let b2 be OrdBasis of V2;
:: original:AutMt
redefine func AutMt (f,B1,b2) ->  Matrix of len B1, len b2,K;
coherence
 AutMt (f,B1,b2) is Matrix of len B1, len b2,K
proofend;
end;

definition
let S be 1-sorted ;
let R be Relation;
funcR | S ->  set  equals :: MATRLIN2:def 1
R | the carrier of S;
coherence
 R | the carrier of S is set ;
end;

:: deftheorem  defines | MATRLIN2:def_1_:_
 for S being 1-sorted
for R being Relation holds R | S = R | the carrier of S;

theorem :: MATRLIN2:27
for K being Field
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for f being linear-transformation of V1,V2
for W1, W2 being Subspace of V1
for U1, U2 being Subspace of V2 st ( dim W1 = 0 implies dim U1 = 0 ) &amp; ( dim W2 = 0 implies dim U2 = 0 ) &amp; V2 is_the_direct_sum_of U1,U2 holds
for fW1 being linear-transformation of W1,U1
for fW2 being linear-transformation of W2,U2 st fW1 = f | W1 &amp; fW2 = f | W2 holds
for w1 being OrdBasis of W1
for w2 being OrdBasis of W2
for u1 being OrdBasis of U1
for u2 being OrdBasis of U2 st w1 ^ w2 = b1 &amp; u1 ^ u2 = b2 holds
AutMt (f,b1,b2) = block_diagonal (<*(AutMt (fW1,w1,u1)),(AutMt (fW2,w2,u2))*>,(0. K))
proofend;

definition
let K be Field;
let V1, V2 be finite-dimensional VectSp of K;
let f be Function of V1,V2;
let B1 be FinSequence of V1;
let b2 be OrdBasis of V2;
assume A1: len B1 = len b2 ;
func AutEqMt (f,B1,b2) ->  Matrix of len B1, len B1,K equals :Def2: :: MATRLIN2:def 2
 AutMt (f,B1,b2);
coherence
 AutMt (f,B1,b2) is Matrix of len B1, len B1,K by A1;
end;

:: deftheorem Def2 defines AutEqMt MATRLIN2:def_2_:_
 for K being Field
for V1, V2 being finite-dimensional VectSp of K
for f being Function of V1,V2
for B1 being FinSequence of V1
for b2 being OrdBasis of V2 st len B1 = len b2 holds
AutEqMt (f,B1,b2) = AutMt (f,B1,b2);

theorem Th28: :: MATRLIN2:28
for K being Field
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1 holds AutMt ((id V1),b1,b1) = 1. (K,(len b1))
proofend;

theorem :: MATRLIN2:29
for K being Field
for V1 being finite-dimensional VectSp of K
for b1, b19 being OrdBasis of V1 holds
( AutEqMt ((id V1),b1,b19) is invertible &amp; AutEqMt ((id V1),b19,b1) = (AutEqMt ((id V1),b1,b19)) ~ )
proofend;

theorem Th30: :: MATRLIN2:30
for j being Nat
for K being Field
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B1 being FinSequence of V1
for p1, p2 being FinSequence of K st len p1 = len p2 &amp; len p1 = len B1 &amp; len p1 > 0 &amp; j in dom b1 &amp; ( for i being Nat st i in dom p2 holds
p2 . i = ((B1 /. i) |-- b1) . j ) holds
p1 "*" p2 = ((Sum (lmlt (p1,B1))) |-- b1) . j
proofend;

theorem Th31: :: MATRLIN2:31
for K being Field
for V2, V1 being finite-dimensional VectSp of K
for f being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for v1 being Element of V1 st len b1 > 0 &amp; f is additive &amp; f is homogeneous holds
(LineVec2Mx (v1 |-- b1)) * (AutMt (f,b1,b2)) = LineVec2Mx ((f . v1) |-- b2)
proofend;

begin

definition
let K be Field;
let V1, V2 be finite-dimensional VectSp of K;
let b1 be OrdBasis of V1;
let B2 be FinSequence of V2;
let M be Matrix of len b1, len B2,K;
func Mx2Tran (M,b1,B2) ->  Function of V1,V2 means :Def3: :: MATRLIN2:def 3
 for v being Vector of V1 holds it . v = Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * M),1)),B2));
existence
 ex b1 being Function of V1,V2 st
for v being Vector of V1 holds b1 . v = Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * M),1)),B2))
proofend;
uniqueness
 for b1, b2 being Function of V1,V2 st ( for v being Vector of V1 holds b1 . v = Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * M),1)),B2)) ) &amp; ( for v being Vector of V1 holds b2 . v = Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * M),1)),B2)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines Mx2Tran MATRLIN2:def_3_:_
 for K being Field
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for M being Matrix of len b1, len B2,K
for b7 being Function of V1,V2 holds
( b7 = Mx2Tran (M,b1,B2) iff for v being Vector of V1 holds b7 . v = Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * M),1)),B2)) );

theorem Th32: :: MATRLIN2:32
for K being Field
for V2, V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for v1 being Element of V1
for M being Matrix of len b1, len b2,K st len b1 > 0 holds
LineVec2Mx (((Mx2Tran (M,b1,b2)) . v1) |-- b2) = (LineVec2Mx (v1 |-- b1)) * M
proofend;

theorem Th33: :: MATRLIN2:33
for K being Field
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for v1 being Element of V1
for M being Matrix of len b1, len B2,K st len b1 = 0 holds
(Mx2Tran (M,b1,B2)) . v1 = 0. V2
proofend;

Lm5:  for K being Field
for A, B being Matrix of K st width A = width B holds
for i being Nat st 1 <= i &amp; i <= len A holds
Line ((A + B),i) = (Line (A,i)) + (Line (B,i))
proofend;

registration
let K be Field;
let V1, V2 be finite-dimensional VectSp of K;
let b1 be OrdBasis of V1;
let B2 be FinSequence of V2;
let M be Matrix of len b1, len B2,K;
cluster Mx2Tran (M,b1,B2) ->  additive homogeneous ;
coherence
 ( Mx2Tran (M,b1,B2) is homogeneous &amp; Mx2Tran (M,b1,B2) is additive )
proofend;
end;

theorem Th34: :: MATRLIN2:34
for K being Field
for V1, V2 being finite-dimensional VectSp of K
for f being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2 st f is additive &amp; f is homogeneous holds
Mx2Tran ((AutMt (f,b1,b2)),b1,b2) = f
proofend;

theorem Th35: :: MATRLIN2:35
for i being Nat
for K being Field
for A, B being Matrix of K st i in dom A &amp; width A = len B holds
(LineVec2Mx (Line (A,i))) * B = LineVec2Mx (Line ((A * B),i))
proofend;

theorem Th36: :: MATRLIN2:36
for K being Field
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for M being Matrix of len b1, len b2,K holds AutMt ((Mx2Tran (M,b1,b2)),b1,b2) = M
proofend;

definition
let n, m be Nat;
let K be Field;
let A be Matrix of n,m,K;
let B be Matrix of K;
:: original:+
redefine funcA + B ->  Matrix of n,m,K;
coherence
 A + B is Matrix of n,m,K
proofend;
end;

theorem :: MATRLIN2:37
for K being Field
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for A, B being Matrix of len b1, len B2,K holds Mx2Tran ((A + B),b1,B2) = (Mx2Tran (A,b1,B2)) + (Mx2Tran (B,b1,B2))
proofend;

theorem :: MATRLIN2:38
for K being Field
for a being Element of K
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for A being Matrix of len b1, len B2,K holds a * (Mx2Tran (A,b1,B2)) = Mx2Tran ((a * A),b1,B2)
proofend;

theorem :: MATRLIN2:39
for K being Field
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for A, B being Matrix of len b1, len b2,K st Mx2Tran (A,b1,b2) = Mx2Tran (B,b1,b2) holds
A = B
proofend;

theorem :: MATRLIN2:40
for K being Field
for V1, V2, V3 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for B3 being FinSequence of V3
for A being Matrix of len b1, len b2,K
for B being Matrix of len b2, len B3,K st width A = len B holds
for AB being Matrix of len b1, len B3,K st AB = A * B holds
Mx2Tran (AB,b1,B3) = (Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2))
proofend;

theorem Th41: :: MATRLIN2:41
for K being Field
for V2, V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for v1 being Element of V1
for A being Matrix of len b1, len b2,K st len b1 > 0 &amp; len b2 > 0 holds
( v1 in ker (Mx2Tran (A,b1,b2)) iff v1 |-- b1 in Space_of_Solutions_of (A @) )
proofend;

theorem Th42: :: MATRLIN2:42
for K being Field
for V1 being finite-dimensional VectSp of K holds
( V1 is trivial iff dim V1 = 0 )
proofend;

theorem Th43: :: MATRLIN2:43
for K being Field
for V1, V2 being VectSp of K
for f being linear-transformation of V1,V2 holds
( f is one-to-one iff ker f = (0). V1 )
proofend;

registration
let K be Field;
let V1, V2 be VectSp of K;
let f, g be linear-transformation of V1,V2;
clusterf + g ->  additive homogeneous ;
coherence
 ( f + g is homogeneous &amp; f + g is additive )
proofend;
end;

registration
let K be Field;
let V1, V2 be VectSp of K;
let f be linear-transformation of V1,V2;
let a be Element of K;
clustera * f ->  additive homogeneous ;
coherence
 ( a * f is homogeneous &amp; a * f is additive )
proofend;
end;

definition
let K be Field;
let V1, V2, V3 be VectSp of K;
let f1 be linear-transformation of V1,V2;
let f2 be linear-transformation of V2,V3;
:: original:(#)
redefine funcf2 * f1 ->  linear-transformation of V1,V3;
coherence
 f1 (#) f2 is linear-transformation of V1,V3 by MOD_2:2;
end;

theorem Th44: :: MATRLIN2:44
for K being Field
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for A being Matrix of len b1, len b2,K st the_rank_of A = len b1 holds
Mx2Tran (A,b1,b2) is one-to-one
proofend;

Lm6:  for n being Nat
for K being Field holds the_rank_of (1. (K,n)) = n
proofend;

theorem Th45: :: MATRLIN2:45
for n being Nat
for K being Field holds MX2FinS (1. (K,n)) is OrdBasis of n -VectSp_over K
proofend;

theorem Th46: :: MATRLIN2:46
for K being Field
for V2 being finite-dimensional VectSp of K
for b2 being OrdBasis of V2
for M being OrdBasis of (len b2) -VectSp_over K st M = MX2FinS (1. (K,(len b2))) holds
for v1 being Vector of ((len b2) -VectSp_over K) holds v1 |-- M = v1
proofend;

theorem Th47: :: MATRLIN2:47
for K being Field
for V2, V1 being finite-dimensional VectSp of K
for f being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for v1 being Element of V1
for M being OrdBasis of (len b2) -VectSp_over K st M = MX2FinS (1. (K,(len b2))) holds
for A being Matrix of len b1, len M,K st A = AutMt (f,b1,b2) &amp; f is additive &amp; f is homogeneous holds
(Mx2Tran (A,b1,M)) . v1 = (f . v1) |-- b2
proofend;

definition
let K be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let V1, V2 be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K;
let W be Subspace of V1;
let f be Function of V1,V2;
:: original:|
redefine funcf | W ->  Function of W,V2;
coherence
 f | W is Function of W,V2
proofend;
end;

definition
let K be Field;
let V1, V2 be VectSp of K;
let W be Subspace of V1;
let f be linear-transformation of V1,V2;
:: original:|
redefine funcf | W ->  linear-transformation of W,V2;
coherence
 f | W is linear-transformation of W,V2
proofend;
end;

Lm7:  for K being Field
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for A being Matrix of len b1, len b2,K st len b1 > 0 &amp; len b2 > 0 holds
nullity (Mx2Tran (A,b1,b2)) = (len b1) - (the_rank_of A)
proofend;

begin

theorem Th48: :: MATRLIN2:48
for K being Field
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for f being linear-transformation of V1,V2 holds rank f = the_rank_of (AutMt (f,b1,b2))
proofend;

theorem :: MATRLIN2:49
for K being Field
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for M being Matrix of len b1, len b2,K holds rank (Mx2Tran (M,b1,b2)) = the_rank_of M
proofend;

theorem :: MATRLIN2:50
for K being Field
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for f being linear-transformation of V1,V2 st dim V1 = dim V2 holds
( not ker f is trivial iff Det (AutEqMt (f,b1,b2)) = 0. K )
proofend;

Lm8:  for K being Field
for V1, V2, V3 being finite-dimensional VectSp of K
for f being linear-transformation of V1,V2
for g being Function of V2,V3 holds g * f = (g | (im f)) * f
proofend;

theorem :: MATRLIN2:51
for K being Field
for V1, V2, V3 being finite-dimensional VectSp of K
for f being linear-transformation of V1,V2
for g being linear-transformation of V2,V3 st g | (im f) is one-to-one holds
( rank (g * f) = rank f &amp; nullity (g * f) = nullity f )
proofend;