:: by Karol P\c{a}k

::

:: Received May 13, 2008

:: Copyright (c) 2008-2017 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 )

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)

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)

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

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

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

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

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

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

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)

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)

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

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

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)

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

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

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)

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)

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)

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)

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

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

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

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)

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

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

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

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

:: deftheorem defines | MATRLIN2:def 1 :

for S being 1-sorted

for R being Relation holds R | S = R | the carrier of S;

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

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 ;

AutMt (f,B1,b2) is Matrix of len B1, len B1,K by A1;

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

AutMt (f,B1,b2) is Matrix of len B1, len B1,K by A1;

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

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

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, b19 being OrdBasis of V1 holds

( AutEqMt ((id V1),b1,b19) is invertible & AutEqMt ((id V1),b19,b1) = (AutEqMt ((id V1),b1,b19)) ~ )

for V1 being finite-dimensional VectSp of K

for b1, b19 being OrdBasis of V1 holds

( AutEqMt ((id V1),b1,b19) is invertible & AutEqMt ((id V1),b19,b1) = (AutEqMt ((id V1),b1,b19)) ~ )

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

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

for v1 being Element of V1 st len b1 > 0 & f is additive & f is homogeneous holds

(LineVec2Mx (v1 |-- b1)) * (AutMt (f,b1,b2)) = LineVec2Mx ((f . v1) |-- b2)

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

for v1 being Element of V1 st len b1 > 0 & f is additive & f is homogeneous 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;

ex b_{1} being Function of V1,V2 st

for v being Vector of V1 holds b_{1} . v = Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * M),1)),B2))

for b_{1}, b_{2} being Function of V1,V2 st ( for v being Vector of V1 holds b_{1} . v = Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * M),1)),B2)) ) & ( for v being Vector of V1 holds b_{2} . v = Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * M),1)),B2)) ) holds

b_{1} = b_{2}

end;
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 for v being Vector of V1 holds it . v = Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * M),1)),B2));

ex b

for v being Vector of V1 holds b

proof end;

uniqueness for b

b

proof 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_{7} being Function of V1,V2 holds

( b_{7} = Mx2Tran (M,b1,B2) iff for v being Vector of V1 holds b_{7} . v = Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * M),1)),B2)) );

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

( b

theorem Th32: :: MATRLIN2:32

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

for V1, V2 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

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

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;

coherence

( Mx2Tran (M,b1,B2) is homogeneous & Mx2Tran (M,b1,B2) is additive )

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

coherence

( Mx2Tran (M,b1,B2) is homogeneous & Mx2Tran (M,b1,B2) is additive )

proof 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 & f is homogeneous holds

Mx2Tran ((AutMt (f,b1,b2)),b1,b2) = f

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 & f is homogeneous 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))

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

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

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

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

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)

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

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

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 V1, V2 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 @) )

for V1, V2 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 )

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 )

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;

registration

let K be Field;

let V1, V2 be VectSp of K;

let f, g be linear-transformation of V1,V2;

coherence

( f + g is homogeneous & f + g is additive )

end;
let V1, V2 be VectSp of K;

let f, g be linear-transformation of V1,V2;

coherence

( f + g is homogeneous & f + g is additive )

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

coherence

( a * f is homogeneous & a * f is additive )

end;
let V1, V2 be VectSp of K;

let f be linear-transformation of V1,V2;

let a be Element of K;

coherence

( a * f is homogeneous & a * f is additive )

proof 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:2;

end;
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:2;

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

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

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

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 additive & f is homogeneous holds

(Mx2Tran (A,b1,M)) . v1 = (f . v1) |-- b2

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

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 additive & f is homogeneous holds

(Mx2Tran (A,b1,M)) . v1 = (f . v1) |-- b2

proof end;

definition

let K be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

let V1, V2 be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over 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

end;
let V1, V2 be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over 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;

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

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

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

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

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 )

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 )

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;