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

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 )

proof end;

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)

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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)

proof end;

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

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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 & len p2 = len R2 holds
lmlt (p1 ^ p2),(R1 ^ R2) = (lmlt p1,R1) ^ (lmlt p2,R2)

proof end;

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)

proof end;

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)

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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)

proof end;

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)

proof end;

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

proof end;

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)

proof end;

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

proof end;

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 & Sum K1 = Sum L1 & K1 | the carrier of W1 = L1 )

proof end;

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 & ( for A being Subset of V1 st A = rng (b1 | m) holds
b1 | m is OrdBasis of Lin A ) )

proof end;

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 & ( for A being Subset of V1 st A = rng (b1 /^ m) holds
b1 /^ m is OrdBasis of Lin A ) )

proof end;

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 & v1 = w1 & v2 = w2 holds
v |-- b = (w1 |-- b1) ^ (w2 |-- b2)

proof end;

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 & b1 = w1 holds
v |-- b1 = w |-- w1

proof end;

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

proof end;

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

proof end;

end;

definition

let S be 1-sorted ;
let R be Relation;
func R | 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 ) & ( dim W2 = 0 implies dim U2 = 0 ) & 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 & 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 & u1 ^ u2 = b2 holds
AutMt f,b1,b2 = block_diagonal <*(AutMt fW1,w1,u1),(AutMt fW2,w2,u2)*>,(0. K)

proof end;

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)

proof end;

theorem :: MATRLIN2:29

for K being Field
for V1 being finite-dimensional VectSp of K
for b1, b1' being OrdBasis of V1 holds
( AutEqMt (id V1),b1,b1' is invertible & AutEqMt (id V1),b1',b1 = (AutEqMt (id V1),b1,b1') ~ )

proof end;

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 & len p1 = len B1 & len p1 > 0 & j in dom b1 & ( 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

proof end;

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 & f is linear holds
(LineVec2Mx (v1 |-- b1)) * (AutMt f,b1,b2) = LineVec2Mx ((f . v1) |-- b2)

proof end;

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 b₁ being Function of V1,V2 st
for v being Vector of V1 holds b₁ . v = Sum (lmlt (Line ((LineVec2Mx (v |-- b1)) * M),1),B2)

proof end;

uniqueness
for b₁, b₂ being Function of V1,V2 st ( for v being Vector of V1 holds b₁ . v = Sum (lmlt (Line ((LineVec2Mx (v |-- b1)) * M),1),B2) ) & ( for v being Vector of V1 holds b₂ . v = Sum (lmlt (Line ((LineVec2Mx (v |-- b1)) * M),1),B2) ) holds
b₁ = b₂

proof end;

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 b₇ being Function of V1,V2 holds
( b₇ = Mx2Tran M,b1,B2 iff for v being Vector of V1 holds b₇ . 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

proof end;

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

proof end;

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

proof end;

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;
:: original: Mx2Tran
redefine func Mx2Tran M,b1,B2 -> linear-transformation of V1,V2;
coherence
Mx2Tran M,b1,B2 is linear-transformation of V1,V2

proof end;

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 linear holds
Mx2Tran (AutMt f,b1,b2),b1,b2 = f

proof end;

theorem Th35: :: MATRLIN2:35

for i being Nat
for K being Field
for A, B being Matrix of K st i in dom A & width A = len B holds
(LineVec2Mx (Line A,i)) * B = LineVec2Mx (Line (A * B),i)

proof end;

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

proof end;

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 func A + B -> Matrix of n,m,K;
coherence
A + B is Matrix of n,m,K

proof end;

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)

proof end;

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

proof end;

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

proof end;

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)

proof end;

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 & len b2 > 0 holds
( v1 in ker (Mx2Tran A,b1,b2) iff v1 |-- b1 in Space_of_Solutions_of (A @ ) )

proof end;

theorem Th42: :: MATRLIN2:42

for K being Field
for V1 being finite-dimensional VectSp of K holds
( V1 is trivial iff dim V1 = 0 )

proof end;

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 )

proof end;

definition

let K be Field;
let V1 be VectSp of K;
:: original: id
redefine func id V1 -> linear-transformation of V1,V1;
coherence
id V1 is linear-transformation of V1,V1 by MOD_2:13;

end;

definition

let K be Field;
let V1, V2 be VectSp of K;
let f, g be linear-transformation of V1,V2;
:: original: +
redefine func f + g -> linear-transformation of V1,V2;
coherence
f + g is linear-transformation of V1,V2

proof end;

end;

definition

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;
:: original: *
redefine func a * f -> linear-transformation of V1,V2;
coherence
a * f is linear-transformation of V1,V2

proof end;

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 func f2 * f1 -> linear-transformation of V1,V3;
coherence
f1 * f2 is linear-transformation of V1,V3 by MOD_2:6;

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

proof end;

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

proof end;

theorem Th45: :: MATRLIN2:45

for n being Nat
for K being Field holds MX2FinS (1. K,n) is OrdBasis of n -VectSp_over K

proof end;

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

proof end;

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 & f is linear holds
(Mx2Tran A,b1,M) . v1 = (f . v1) |-- b2

proof end;

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 VectSp-like Abelian add-associative right_zeroed VectSpStr of K;
let W be Subspace of V1;
let f be Function of V1,V2;
:: original: |
redefine func f | W -> Function of W,V2;
coherence
f | W is Function of W,V2

proof end;

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 func f | W -> linear-transformation of W,V2;
coherence
f | W is linear-transformation of W,V2

proof end;

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 & len b2 > 0 holds
nullity (Mx2Tran A,b1,b2) = (len b1) - (the_rank_of A)

proof end;

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)

proof end;

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

proof end;

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 )

proof end;

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

proof end;

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 & nullity (g * f) = nullity f )

proof end;