:: by Robert Milewski

::

:: Received June 30, 1995

:: Copyright (c) 1995-2012 Association of Mizar Users

begin

definition

let D be non empty set ;

let k be Nat;

let M be Matrix of D;

:: original: Del

redefine func Del (M,k) -> Matrix of D;

coherence

Del (M,k) is Matrix of D

end;
let k be Nat;

let M be Matrix of D;

:: original: Del

redefine func Del (M,k) -> Matrix of D;

coherence

Del (M,k) is Matrix of D

proof end;

theorem Th2: :: MATRLIN:2

for n, m being Nat

for D being non empty set

for M being Matrix of n + 1,m,D

for M1 being Matrix of D holds

( ( n > 0 implies width M = width (Del (M,(n + 1))) ) & ( M1 = <*(M . (n + 1))*> implies width M = width M1 ) )

for D being non empty set

for M being Matrix of n + 1,m,D

for M1 being Matrix of D holds

( ( n > 0 implies width M = width (Del (M,(n + 1))) ) & ( M1 = <*(M . (n + 1))*> implies width M = width M1 ) )

proof end;

theorem Th3: :: MATRLIN:3

for n, m being Nat

for D being non empty set

for M being Matrix of n + 1,m,D holds Del (M,(n + 1)) is Matrix of n,m,D

for D being non empty set

for M being Matrix of n + 1,m,D holds Del (M,(n + 1)) is Matrix of n,m,D

proof end;

definition

let D be non empty set ;

let P be FinSequence of D;

:: original: <*

redefine func <*P*> -> Matrix of 1, len P,D;

coherence

<*P*> is Matrix of 1, len P,D by MATRIX_1:11;

end;
let P be FinSequence of D;

:: original: <*

redefine func <*P*> -> Matrix of 1, len P,D;

coherence

<*P*> is Matrix of 1, len P,D by MATRIX_1:11;

begin

begin

theorem Th5: :: MATRLIN:5

for K being Field

for V being VectSp of K

for KL1, KL2 being Linear_Combination of V

for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 holds

KL1 = KL2

for V being VectSp of K

for KL1, KL2 being Linear_Combination of V

for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 holds

KL1 = KL2

proof end;

theorem Th6: :: MATRLIN:6

for K being Field

for V being VectSp of K

for KL1, KL2, KL3 being Linear_Combination of V

for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Carrier KL3 c= X & Sum KL1 = (Sum KL2) + (Sum KL3) holds

KL1 = KL2 + KL3

for V being VectSp of K

for KL1, KL2, KL3 being Linear_Combination of V

for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Carrier KL3 c= X & Sum KL1 = (Sum KL2) + (Sum KL3) holds

KL1 = KL2 + KL3

proof end;

theorem Th7: :: MATRLIN:7

for K being Field

for V being VectSp of K

for a being Element of K

for KL1, KL2 being Linear_Combination of V

for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & a <> 0. K & Sum KL1 = a * (Sum KL2) holds

KL1 = a * KL2

for V being VectSp of K

for a being Element of K

for KL1, KL2 being Linear_Combination of V

for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & a <> 0. K & Sum KL1 = a * (Sum KL2) holds

KL1 = a * KL2

proof end;

theorem Th8: :: MATRLIN:8

for K being Field

for V being VectSp of K

for W being Element of V

for b2 being Basis of V ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= b2 )

for V being VectSp of K

for W being Element of V

for b2 being Basis of V ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= b2 )

proof end;

definition

let K be Field;

let V be VectSp of K;

end;
let V be VectSp of K;

attr V is finite-dimensional means :Def1: :: MATRLIN:def 1

ex A being finite Subset of V st A is Basis of V;

ex A being finite Subset of V st A is Basis of V;

:: deftheorem Def1 defines finite-dimensional MATRLIN:def 1 :

for K being Field

for V being VectSp of K holds

( V is finite-dimensional iff ex A being finite Subset of V st A is Basis of V );

for K being Field

for V being VectSp of K holds

( V is finite-dimensional iff ex A being finite Subset of V st A is Basis of V );

registration

let K be Field;

ex b_{1} being VectSp of K st

( b_{1} is strict & b_{1} is finite-dimensional )

end;
cluster non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed finite-dimensional for VectSpStr over K;

existence ex b

( b

proof end;

definition

let K be Field;

let V be finite-dimensional VectSp of K;

ex b_{1} being FinSequence of V st

( b_{1} is one-to-one & rng b_{1} is Basis of V )

end;
let V be finite-dimensional VectSp of K;

mode OrdBasis of V -> FinSequence of V means :Def2: :: MATRLIN:def 2

( it is one-to-one & rng it is Basis of V );

existence ( it is one-to-one & rng it is Basis of V );

ex b

( b

proof end;

:: deftheorem Def2 defines OrdBasis MATRLIN:def 2 :

for K being Field

for V being finite-dimensional VectSp of K

for b_{3} being FinSequence of V holds

( b_{3} is OrdBasis of V iff ( b_{3} is one-to-one & rng b_{3} is Basis of V ) );

for K being Field

for V being finite-dimensional VectSp of K

for b

( b

definition

let K be non empty doubleLoopStr ;

let V1, V2 be non empty VectSpStr over K;

let f1, f2 be Function of V1,V2;

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

for v being Element of V1 holds b_{1} . v = (f1 . v) + (f2 . v)

for b_{1}, b_{2} being Function of V1,V2 st ( for v being Element of V1 holds b_{1} . v = (f1 . v) + (f2 . v) ) & ( for v being Element of V1 holds b_{2} . v = (f1 . v) + (f2 . v) ) holds

b_{1} = b_{2}

end;
let V1, V2 be non empty VectSpStr over K;

let f1, f2 be Function of V1,V2;

func f1 + f2 -> Function of V1,V2 means :Def3: :: MATRLIN:def 3

for v being Element of V1 holds it . v = (f1 . v) + (f2 . v);

existence for v being Element of V1 holds it . v = (f1 . v) + (f2 . v);

ex b

for v being Element of V1 holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines + MATRLIN:def 3 :

for K being non empty doubleLoopStr

for V1, V2 being non empty VectSpStr over K

for f1, f2, b_{6} being Function of V1,V2 holds

( b_{6} = f1 + f2 iff for v being Element of V1 holds b_{6} . v = (f1 . v) + (f2 . v) );

for K being non empty doubleLoopStr

for V1, V2 being non empty VectSpStr over K

for f1, f2, b

( b

definition

let K be non empty doubleLoopStr ;

let V1, V2 be non empty VectSpStr over K;

let f be Function of V1,V2;

let a be Element of K;

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

for v being Element of V1 holds b_{1} . v = a * (f . v)

for b_{1}, b_{2} being Function of V1,V2 st ( for v being Element of V1 holds b_{1} . v = a * (f . v) ) & ( for v being Element of V1 holds b_{2} . v = a * (f . v) ) holds

b_{1} = b_{2}

end;
let V1, V2 be non empty VectSpStr over K;

let f be Function of V1,V2;

let a be Element of K;

func a * f -> Function of V1,V2 means :Def4: :: MATRLIN:def 4

for v being Element of V1 holds it . v = a * (f . v);

existence for v being Element of V1 holds it . v = a * (f . v);

ex b

for v being Element of V1 holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines * MATRLIN:def 4 :

for K being non empty doubleLoopStr

for V1, V2 being non empty VectSpStr over K

for f being Function of V1,V2

for a being Element of K

for b_{6} being Function of V1,V2 holds

( b_{6} = a * f iff for v being Element of V1 holds b_{6} . v = a * (f . v) );

for K being non empty doubleLoopStr

for V1, V2 being non empty VectSpStr over K

for f being Function of V1,V2

for a being Element of K

for b

( b

theorem Th9: :: MATRLIN:9

for K being Field

for V1 being finite-dimensional VectSp of K

for a being Element of V1

for F being FinSequence of V1

for G being FinSequence of K st len F = len G & ( for k being Nat

for v being Element of K st k in dom F & v = G . k holds

F . k = v * a ) holds

Sum F = (Sum G) * a

for V1 being finite-dimensional VectSp of K

for a being Element of V1

for F being FinSequence of V1

for G being FinSequence of K st len F = len G & ( for k being Nat

for v being Element of K st k in dom F & v = G . k holds

F . k = v * a ) holds

Sum F = (Sum G) * a

proof end;

theorem Th10: :: MATRLIN:10

for K being Field

for V1 being finite-dimensional VectSp of K

for a being Element of V1

for F being FinSequence of K

for G being FinSequence of V1 st len F = len G & ( for k being Nat st k in dom F holds

G . k = (F /. k) * a ) holds

Sum G = (Sum F) * a

for V1 being finite-dimensional VectSp of K

for a being Element of V1

for F being FinSequence of K

for G being FinSequence of V1 st len F = len G & ( for k being Nat st k in dom F holds

G . k = (F /. k) * a ) holds

Sum G = (Sum F) * a

proof end;

theorem Th11: :: MATRLIN:11

for V1 being non empty right_complementable add-associative right_zeroed addLoopStr

for F being FinSequence of V1 st ( for k being Nat st k in dom F holds

F /. k = 0. V1 ) holds

Sum F = 0. V1

for F being FinSequence of V1 st ( for k being Nat st k in dom F holds

F /. k = 0. V1 ) holds

Sum F = 0. V1

proof end;

definition

let K be Field;

let V1 be finite-dimensional VectSp of K;

let p1 be FinSequence of K;

let p2 be FinSequence of V1;

coherence

the lmult of V1 .: (p1,p2) is FinSequence of V1 ;

end;
let V1 be finite-dimensional VectSp of K;

let p1 be FinSequence of K;

let p2 be FinSequence of V1;

coherence

the lmult of V1 .: (p1,p2) is FinSequence of V1 ;

:: deftheorem defines lmlt MATRLIN:def 5 :

for K being Field

for V1 being finite-dimensional VectSp of K

for p1 being FinSequence of K

for p2 being FinSequence of V1 holds lmlt (p1,p2) = the lmult of V1 .: (p1,p2);

for K being Field

for V1 being finite-dimensional VectSp of K

for p1 being FinSequence of K

for p2 being FinSequence of V1 holds lmlt (p1,p2) = the lmult of V1 .: (p1,p2);

theorem Th12: :: MATRLIN:12

for K being Field

for V1 being finite-dimensional VectSp of K

for p2 being FinSequence of V1

for p1 being FinSequence of K st dom p1 = dom p2 holds

dom (lmlt (p1,p2)) = dom p1

for V1 being finite-dimensional VectSp of K

for p2 being FinSequence of V1

for p1 being FinSequence of K st dom p1 = dom p2 holds

dom (lmlt (p1,p2)) = dom p1

proof end;

definition

let V1 be non empty addLoopStr ;

let M be FinSequence of the carrier of V1 * ;

ex b_{1} being FinSequence of V1 st

( len b_{1} = len M & ( for k being Nat st k in dom b_{1} holds

b_{1} /. k = Sum (M /. k) ) )

for b_{1}, b_{2} being FinSequence of V1 st len b_{1} = len M & ( for k being Nat st k in dom b_{1} holds

b_{1} /. k = Sum (M /. k) ) & len b_{2} = len M & ( for k being Nat st k in dom b_{2} holds

b_{2} /. k = Sum (M /. k) ) holds

b_{1} = b_{2}

end;
let M be FinSequence of the carrier of V1 * ;

func Sum M -> FinSequence of V1 means :Def6: :: MATRLIN:def 6

( len it = len M & ( for k being Nat st k in dom it holds

it /. k = Sum (M /. k) ) );

existence ( len it = len M & ( for k being Nat st k in dom it holds

it /. k = Sum (M /. k) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def6 defines Sum MATRLIN:def 6 :

for V1 being non empty addLoopStr

for M being FinSequence of the carrier of V1 *

for b_{3} being FinSequence of V1 holds

( b_{3} = Sum M iff ( len b_{3} = len M & ( for k being Nat st k in dom b_{3} holds

b_{3} /. k = Sum (M /. k) ) ) );

for V1 being non empty addLoopStr

for M being FinSequence of the carrier of V1 *

for b

( b

b

theorem Th13: :: MATRLIN:13

for K being Field

for V1 being finite-dimensional VectSp of K

for M being Matrix of the carrier of V1 st len M = 0 holds

Sum (Sum M) = 0. V1

for V1 being finite-dimensional VectSp of K

for M being Matrix of the carrier of V1 st len M = 0 holds

Sum (Sum M) = 0. V1

proof end;

theorem Th14: :: MATRLIN:14

for m being Nat

for K being Field

for V1 being finite-dimensional VectSp of K

for M being Matrix of m + 1, 0 , the carrier of V1 holds Sum (Sum M) = 0. V1

for K being Field

for V1 being finite-dimensional VectSp of K

for M being Matrix of m + 1, 0 , the carrier of V1 holds Sum (Sum M) = 0. V1

proof end;

theorem Th16: :: MATRLIN:16

for K being Field

for V1, V2 being VectSp of K

for f being Function of V1,V2

for p being FinSequence of V1 st f is additive & f is homogeneous holds

f . (Sum p) = Sum (f * p)

for V1, V2 being VectSp of K

for f being Function of V1,V2

for p being FinSequence of V1 st f is additive & f is homogeneous holds

f . (Sum p) = Sum (f * p)

proof end;

theorem Th17: :: MATRLIN:17

for K being Field

for V2, V1 being finite-dimensional VectSp of K

for f being Function of V1,V2

for a being FinSequence of K

for p being FinSequence of V1 st len p = len a & f is additive & f is homogeneous holds

f * (lmlt (a,p)) = lmlt (a,(f * p))

for V2, V1 being finite-dimensional VectSp of K

for f being Function of V1,V2

for a being FinSequence of K

for p being FinSequence of V1 st len p = len a & f is additive & f is homogeneous holds

f * (lmlt (a,p)) = lmlt (a,(f * p))

proof end;

theorem Th18: :: MATRLIN:18

for K being Field

for V3, V2 being finite-dimensional VectSp of K

for g being Function of V2,V3

for b2 being OrdBasis of V2

for a being FinSequence of K st len a = len b2 & g is additive & g is homogeneous holds

g . (Sum (lmlt (a,b2))) = Sum (lmlt (a,(g * b2)))

for V3, V2 being finite-dimensional VectSp of K

for g being Function of V2,V3

for b2 being OrdBasis of V2

for a being FinSequence of K st len a = len b2 & g is additive & g is homogeneous holds

g . (Sum (lmlt (a,b2))) = Sum (lmlt (a,(g * b2)))

proof end;

theorem Th19: :: MATRLIN:19

for K being Field

for V1 being finite-dimensional VectSp of K

for F, F1 being FinSequence of V1

for KL being Linear_Combination of V1

for p being Permutation of (dom F) st F1 = F * p holds

KL (#) F1 = (KL (#) F) * p

for V1 being finite-dimensional VectSp of K

for F, F1 being FinSequence of V1

for KL being Linear_Combination of V1

for p being Permutation of (dom F) st F1 = F * p holds

KL (#) F1 = (KL (#) F) * p

proof end;

theorem Th20: :: MATRLIN:20

for K being Field

for V1 being finite-dimensional VectSp of K

for F being FinSequence of V1

for KL being Linear_Combination of V1 st F is one-to-one & Carrier KL c= rng F holds

Sum (KL (#) F) = Sum KL

for V1 being finite-dimensional VectSp of K

for F being FinSequence of V1

for KL being Linear_Combination of V1 st F is one-to-one & Carrier KL c= rng F holds

Sum (KL (#) F) = Sum KL

proof end;

theorem Th21: :: MATRLIN:21

for K being Field

for V2, V1 being finite-dimensional VectSp of K

for f1, f2 being Function of V1,V2

for A being set

for p being FinSequence of V1 st rng p c= A & f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & ( for v being Element of V1 st v in A holds

f1 . v = f2 . v ) holds

f1 . (Sum p) = f2 . (Sum p)

for V2, V1 being finite-dimensional VectSp of K

for f1, f2 being Function of V1,V2

for A being set

for p being FinSequence of V1 st rng p c= A & f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & ( for v being Element of V1 st v in A holds

f1 . v = f2 . v ) holds

f1 . (Sum p) = f2 . (Sum p)

proof end;

theorem Th22: :: MATRLIN:22

for K being Field

for V2, V1 being finite-dimensional VectSp of K

for f1, f2 being Function of V1,V2 st f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous holds

for b1 being OrdBasis of V1 st len b1 > 0 & f1 * b1 = f2 * b1 holds

f1 = f2

for V2, V1 being finite-dimensional VectSp of K

for f1, f2 being Function of V1,V2 st f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous holds

for b1 being OrdBasis of V1 st len b1 > 0 & f1 * b1 = f2 * b1 holds

f1 = f2

proof end;

registration

let D be non empty set ;

coherence

for b_{1} being Matrix of D holds b_{1} is FinSequence-yielding
;

end;
coherence

for b

definition

let D be non empty set ;

let F, G be Matrix of D;

:: original: ^^

redefine func F ^^ G -> Matrix of D;

coherence

F ^^ G is Matrix of D

end;
let F, G be Matrix of D;

:: original: ^^

redefine func F ^^ G -> Matrix of D;

coherence

F ^^ G is Matrix of D

proof end;

definition

let D be non empty set ;

let n, m, k be Nat;

let M1 be Matrix of n,k,D;

let M2 be Matrix of m,k,D;

:: original: ^

redefine func M1 ^ M2 -> Matrix of n + m,k,D;

coherence

M1 ^ M2 is Matrix of n + m,k,D

end;
let n, m, k be Nat;

let M1 be Matrix of n,k,D;

let M2 be Matrix of m,k,D;

:: original: ^

redefine func M1 ^ M2 -> Matrix of n + m,k,D;

coherence

M1 ^ M2 is Matrix of n + m,k,D

proof end;

theorem :: MATRLIN:23

for n, k, m, i being Nat

for D being non empty set

for M1 being Matrix of n,k,D

for M2 being Matrix of m,k,D st i in dom M1 holds

Line ((M1 ^ M2),i) = Line (M1,i)

for D being non empty set

for M1 being Matrix of n,k,D

for M2 being Matrix of m,k,D st i in dom M1 holds

Line ((M1 ^ M2),i) = Line (M1,i)

proof end;

theorem Th24: :: MATRLIN:24

for n, k, m being Nat

for D being non empty set

for M1 being Matrix of n,k,D

for M2 being Matrix of m,k,D st width M1 = width M2 holds

width (M1 ^ M2) = width M1

for D being non empty set

for M1 being Matrix of n,k,D

for M2 being Matrix of m,k,D st width M1 = width M2 holds

width (M1 ^ M2) = width M1

proof end;

theorem :: MATRLIN:25

for t, k, m, n, i being Nat

for D being non empty set

for M1 being Matrix of t,k,D

for M2 being Matrix of m,k,D st n in dom M2 & i = (len M1) + n holds

Line ((M1 ^ M2),i) = Line (M2,n)

for D being non empty set

for M1 being Matrix of t,k,D

for M2 being Matrix of m,k,D st n in dom M2 & i = (len M1) + n holds

Line ((M1 ^ M2),i) = Line (M2,n)

proof end;

theorem Th26: :: MATRLIN:26

for n, k, m being Nat

for D being non empty set

for M1 being Matrix of n,k,D

for M2 being Matrix of m,k,D st width M1 = width M2 holds

for i being Nat st i in Seg (width M1) holds

Col ((M1 ^ M2),i) = (Col (M1,i)) ^ (Col (M2,i))

for D being non empty set

for M1 being Matrix of n,k,D

for M2 being Matrix of m,k,D st width M1 = width M2 holds

for i being Nat st i in Seg (width M1) holds

Col ((M1 ^ M2),i) = (Col (M1,i)) ^ (Col (M2,i))

proof end;

theorem Th27: :: MATRLIN:27

for n, k, m being Nat

for K being Field

for V being VectSp of K

for M1 being Matrix of n,k, the carrier of V

for M2 being Matrix of m,k, the carrier of V holds Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2)

for K being Field

for V being VectSp of K

for M1 being Matrix of n,k, the carrier of V

for M2 being Matrix of m,k, the carrier of V holds Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2)

proof end;

theorem Th28: :: MATRLIN:28

for n, k, m being Nat

for D being non empty set

for M1 being Matrix of n,k,D

for M2 being Matrix of m,k,D st width M1 = width M2 holds

(M1 ^ M2) @ = (M1 @) ^^ (M2 @)

for D being non empty set

for M1 being Matrix of n,k,D

for M2 being Matrix of m,k,D st width M1 = width M2 holds

(M1 ^ M2) @ = (M1 @) ^^ (M2 @)

proof end;

theorem Th29: :: MATRLIN:29

for K being Field

for V1 being finite-dimensional VectSp of K

for M1, M2 being Matrix of the carrier of V1 holds (Sum M1) + (Sum M2) = Sum (M1 ^^ M2)

for V1 being finite-dimensional VectSp of K

for M1, M2 being Matrix of the carrier of V1 holds (Sum M1) + (Sum M2) = Sum (M1 ^^ M2)

proof end;

theorem Th30: :: MATRLIN:30

for K being Field

for V1 being finite-dimensional VectSp of K

for P1, P2 being FinSequence of V1 st len P1 = len P2 holds

Sum (P1 + P2) = (Sum P1) + (Sum P2)

for V1 being finite-dimensional VectSp of K

for P1, P2 being FinSequence of V1 st len P1 = len P2 holds

Sum (P1 + P2) = (Sum P1) + (Sum P2)

proof end;

theorem Th31: :: MATRLIN:31

for K being Field

for V1 being finite-dimensional VectSp of K

for M1, M2 being Matrix of the carrier of V1 st len M1 = len M2 holds

(Sum (Sum M1)) + (Sum (Sum M2)) = Sum (Sum (M1 ^^ M2))

for V1 being finite-dimensional VectSp of K

for M1, M2 being Matrix of the carrier of V1 st len M1 = len M2 holds

(Sum (Sum M1)) + (Sum (Sum M2)) = Sum (Sum (M1 ^^ M2))

proof end;

theorem Th32: :: MATRLIN:32

for K being Field

for V1 being finite-dimensional VectSp of K

for M being Matrix of the carrier of V1 holds Sum (Sum M) = Sum (Sum (M @))

for V1 being finite-dimensional VectSp of K

for M being Matrix of the carrier of V1 holds Sum (Sum M) = Sum (Sum (M @))

proof end;

theorem Th33: :: MATRLIN:33

for n, m being Nat

for K being Field

for V1 being finite-dimensional VectSp of K

for M being Matrix of n,m, the carrier of K st n > 0 & m > 0 holds

for p, d being FinSequence of K st len p = n & len d = m & ( for j being Nat st j in dom d holds

d /. j = Sum (mlt (p,(Col (M,j)))) ) holds

for b, c being FinSequence of V1 st len b = m & len c = n & ( for i being Nat st i in dom c holds

c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds

Sum (lmlt (p,c)) = Sum (lmlt (d,b))

for K being Field

for V1 being finite-dimensional VectSp of K

for M being Matrix of n,m, the carrier of K st n > 0 & m > 0 holds

for p, d being FinSequence of K st len p = n & len d = m & ( for j being Nat st j in dom d holds

d /. j = Sum (mlt (p,(Col (M,j)))) ) holds

for b, c being FinSequence of V1 st len b = m & len c = n & ( for i being Nat st i in dom c holds

c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds

Sum (lmlt (p,c)) = Sum (lmlt (d,b))

proof end;

begin

definition

let K be Field;

let V be finite-dimensional VectSp of K;

let b1 be OrdBasis of V;

let W be Element of V;

ex b_{1} being FinSequence of K st

( len b_{1} = len b1 & ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len b_{1} holds

b_{1} /. k = KL . (b1 /. k) ) ) )

for b_{1}, b_{2} being FinSequence of K st len b_{1} = len b1 & ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len b_{1} holds

b_{1} /. k = KL . (b1 /. k) ) ) & len b_{2} = len b1 & ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len b_{2} holds

b_{2} /. k = KL . (b1 /. k) ) ) holds

b_{1} = b_{2}

end;
let V be finite-dimensional VectSp of K;

let b1 be OrdBasis of V;

let W be Element of V;

func W |-- b1 -> FinSequence of K means :Def7: :: MATRLIN:def 7

( len it = len b1 & ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len it holds

it /. k = KL . (b1 /. k) ) ) );

existence ( len it = len b1 & ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len it holds

it /. k = KL . (b1 /. k) ) ) );

ex b

( len b

( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len b

b

proof end;

uniqueness for b

( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len b

b

( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len b

b

b

proof end;

:: deftheorem Def7 defines |-- MATRLIN:def 7 :

for K being Field

for V being finite-dimensional VectSp of K

for b1 being OrdBasis of V

for W being Element of V

for b_{5} being FinSequence of K holds

( b_{5} = W |-- b1 iff ( len b_{5} = len b1 & ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len b_{5} holds

b_{5} /. k = KL . (b1 /. k) ) ) ) );

for K being Field

for V being finite-dimensional VectSp of K

for b1 being OrdBasis of V

for W being Element of V

for b

( b

( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len b

b

Lm1: for K being Field

for V being finite-dimensional VectSp of K

for b being OrdBasis of V

for W being Element of V holds dom (W |-- b) = dom b

proof end;

theorem Th34: :: MATRLIN:34

for K being Field

for V2 being finite-dimensional VectSp of K

for b2 being OrdBasis of V2

for v1, v2 being Vector of V2 st v1 |-- b2 = v2 |-- b2 holds

v1 = v2

for V2 being finite-dimensional VectSp of K

for b2 being OrdBasis of V2

for v1, v2 being Vector of V2 st v1 |-- b2 = v2 |-- b2 holds

v1 = v2

proof end;

theorem Th35: :: MATRLIN:35

for K being Field

for V1 being finite-dimensional VectSp of K

for b1 being OrdBasis of V1

for v being Element of V1 holds v = Sum (lmlt ((v |-- b1),b1))

for V1 being finite-dimensional VectSp of K

for b1 being OrdBasis of V1

for v being Element of V1 holds v = Sum (lmlt ((v |-- b1),b1))

proof end;

theorem Th36: :: MATRLIN:36

for K being Field

for V1 being finite-dimensional VectSp of K

for b1 being OrdBasis of V1

for d being FinSequence of K st len d = len b1 holds

d = (Sum (lmlt (d,b1))) |-- b1

for V1 being finite-dimensional VectSp of K

for b1 being OrdBasis of V1

for d being FinSequence of K st len d = len b1 holds

d = (Sum (lmlt (d,b1))) |-- b1

proof end;

Lm2: for p being FinSequence

for k being set st k in dom p holds

len p > 0

proof end;

theorem Th37: :: MATRLIN:37

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 a, d being FinSequence of K st len a = len b1 holds

for j being Nat st j in dom b2 & len d = len b1 & ( for k being Nat st k in dom b1 holds

d . k = ((f . (b1 /. k)) |-- b2) /. j ) & len b1 > 0 holds

((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d))

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 a, d being FinSequence of K st len a = len b1 holds

for j being Nat st j in dom b2 & len d = len b1 & ( for k being Nat st k in dom b1 holds

d . k = ((f . (b1 /. k)) |-- b2) /. j ) & len b1 > 0 holds

((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d))

proof end;

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;

ex b_{1} being Matrix of K st

( len b_{1} = len b1 & ( for k being Nat st k in dom b1 holds

b_{1} /. k = (f . (b1 /. k)) |-- b2 ) )

for b_{1}, b_{2} being Matrix of K st len b_{1} = len b1 & ( for k being Nat st k in dom b1 holds

b_{1} /. k = (f . (b1 /. k)) |-- b2 ) & len b_{2} = len b1 & ( for k being Nat st k in dom b1 holds

b_{2} /. k = (f . (b1 /. k)) |-- b2 ) holds

b_{1} = b_{2}

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;

func AutMt (f,b1,b2) -> Matrix of K means :Def8: :: MATRLIN:def 8

( len it = len b1 & ( for k being Nat st k in dom b1 holds

it /. k = (f . (b1 /. k)) |-- b2 ) );

existence ( len it = len b1 & ( for k being Nat st k in dom b1 holds

it /. k = (f . (b1 /. k)) |-- b2 ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def8 defines AutMt MATRLIN:def 8 :

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

for b_{7} being Matrix of K holds

( b_{7} = AutMt (f,b1,b2) iff ( len b_{7} = len b1 & ( for k being Nat st k in dom b1 holds

b_{7} /. k = (f . (b1 /. k)) |-- 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

for b

( b

b

Lm3: 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 holds dom (AutMt (f,b1,b2)) = dom b1

proof end;

theorem Th38: :: MATRLIN:38

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 len b1 = 0 holds

AutMt (f,b1,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 st len b1 = 0 holds

AutMt (f,b1,b2) = {}

proof end;

theorem Th39: :: MATRLIN:39

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 len b1 > 0 holds

width (AutMt (f,b1,b2)) = len 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 st len b1 > 0 holds

width (AutMt (f,b1,b2)) = len b2

proof end;

theorem :: MATRLIN:40

for K being Field

for V1, V2 being finite-dimensional VectSp of K

for f1, f2 being Function of V1,V2

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2 st f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & AutMt (f1,b1,b2) = AutMt (f2,b1,b2) & len b1 > 0 holds

f1 = f2

for V1, V2 being finite-dimensional VectSp of K

for f1, f2 being Function of V1,V2

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2 st f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & AutMt (f1,b1,b2) = AutMt (f2,b1,b2) & len b1 > 0 holds

f1 = f2

proof end;

theorem :: MATRLIN:41

for K being Field

for V1, V2, V3 being finite-dimensional VectSp of K

for f being Function of V1,V2

for g being Function of V2,V3

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2

for b3 being OrdBasis of V3 st g is additive & g is homogeneous & len b1 > 0 & len b2 > 0 holds

AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3))

for V1, V2, V3 being finite-dimensional VectSp of K

for f being Function of V1,V2

for g being Function of V2,V3

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2

for b3 being OrdBasis of V3 st g is additive & g is homogeneous & len b1 > 0 & len b2 > 0 holds

AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3))

proof end;

theorem :: MATRLIN:42

for K being Field

for V1, V2 being finite-dimensional VectSp of K

for f1, f2 being Function of V1,V2

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2 holds AutMt ((f1 + f2),b1,b2) = (AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))

for V1, V2 being finite-dimensional VectSp of K

for f1, f2 being Function of V1,V2

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2 holds AutMt ((f1 + f2),b1,b2) = (AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))

proof end;

theorem :: MATRLIN:43

for K being Field

for a being Element of K

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 a <> 0. K holds

AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2))

for a being Element of K

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 a <> 0. K holds

AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2))

proof end;