begin
theorem
canceled;
theorem
canceled;
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
begin
theorem
canceled;
theorem
canceled;
begin
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
:: deftheorem MATRLIN:def 1 :
canceled;
:: deftheorem MATRLIN:def 2 :
canceled;
:: deftheorem Def3 defines finite-dimensional MATRLIN:def 3 :
:: deftheorem Def4 defines OrdBasis MATRLIN:def 4 :
:: deftheorem Def5 defines + MATRLIN:def 5 :
:: deftheorem Def6 defines * MATRLIN:def 6 :
theorem Th13:
theorem Th14:
theorem Th15:
:: deftheorem defines lmlt MATRLIN:def 7 :
theorem Th16:
:: deftheorem Def8 defines Sum MATRLIN:def 8 :
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
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;
^redefine func M1 ^ M2 -> Matrix of
n + m,
k,
D;
coherence
M1 ^ M2 is Matrix of n + m,k,D
end;
theorem
theorem Th28:
theorem
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
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem
canceled;
theorem Th37:
theorem Th38:
for
n,
m being
Nat for
K being
Field for
V1 being
finite-dimensional VectSp of
finite-dimensional for
M being
Matrix of
n,
m,the
carrier of
K st
n > 0 &
m > 0 holds
for
p,
d being
FinSequence of 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 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)
begin
:: deftheorem Def9 defines |-- MATRLIN:def 9 :
Lm1:
for K being Field
for V being finite-dimensional VectSp of finite-dimensional
for b being OrdBasis of V
for W being Element of holds dom (W |-- b) = dom b
theorem Th39:
theorem Th40:
theorem Th41:
Lm2:
for p being FinSequence
for k being set st k in dom p holds
len p > 0
theorem Th42:
begin
:: deftheorem Def10 defines AutMt MATRLIN:def 10 :
Lm3:
for K being Field
for V1, V2 being finite-dimensional VectSp of finite-dimensional
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
theorem Th43:
theorem Th44:
theorem
theorem
for
K being
Field for
V1,
V2,
V3 being
finite-dimensional VectSp of
finite-dimensional 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
linear &
len b1 > 0 &
len b2 > 0 holds
AutMt (g * f),
b1,
b3 = (AutMt f,b1,b2) * (AutMt g,b2,b3)
theorem
theorem