begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem
theorem
theorem
begin
Lm1:
for K being Field
for V1 being finite-dimensional VectSp of finite-dimensional
for R being FinSequence of
for p being FinSequence of holds dom (lmlt p,R) = (dom p) /\ (dom R)
Lm2:
for K being Field
for p1, p2 being FinSequence of holds dom (p1 + p2) = (dom p1) /\ (dom p2)
Lm3:
for K being Field
for V1 being finite-dimensional VectSp of finite-dimensional
for R1, R2 being FinSequence of holds dom (R1 + R2) = (dom R1) /\ (dom R2)
theorem Th7:
theorem
theorem Th9:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
Lm4:
for K being Field
for V being VectSp of
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 )
theorem
theorem
theorem Th24:
theorem Th25:
theorem Th26:
begin
definition
let K be
Field;
let V1,
V2 be
finite-dimensional VectSp of
finite-dimensional ;
let f be
Function of
V1,
V2;
let B1 be
FinSequence of ;
let b2 be
OrdBasis of
V2;
AutMtredefine func AutMt f,
B1,
b2 -> Matrix of the
carrier of
K,
len B1,;
coherence
AutMt f,B1,b2 is Matrix of the carrier of K, len B1,
end;
:: deftheorem defines | MATRLIN2:def 1 :
theorem
for
K being
Field for
V1,
V2 being
finite-dimensional VectSp of
finite-dimensional 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)
definition
let K be
Field;
let V1,
V2 be
finite-dimensional VectSp of
finite-dimensional ;
let f be
Function of
V1,
V2;
let B1 be
FinSequence of ;
let b2 be
OrdBasis of
V2;
assume A1:
len B1 = len b2
;
func AutEqMt f,
B1,
b2 -> Matrix of the
carrier of
K,
len B1,
equals :
Def2:
AutMt f,
B1,
b2;
coherence
AutMt f,B1,b2 is Matrix of the carrier of K, len B1,
by A1;
end;
:: deftheorem Def2 defines AutEqMt MATRLIN2:def 2 :
theorem Th28:
theorem
theorem Th30:
theorem Th31:
begin
definition
let K be
Field;
let V1,
V2 be
finite-dimensional VectSp of
finite-dimensional ;
let b1 be
OrdBasis of
V1;
let B2 be
FinSequence of ;
let M be
Matrix of the
carrier of
K,
len b1,;
func Mx2Tran M,
b1,
B2 -> Function of
V1,
V2 means :
Def3:
for
v being
Vector of 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 holds b1 . v = Sum (lmlt (Line ((LineVec2Mx (v |-- b1)) * M),1),B2)
uniqueness
for b1, b2 being Function of V1,V2 st ( for v being Vector of holds b1 . v = Sum (lmlt (Line ((LineVec2Mx (v |-- b1)) * M),1),B2) ) & ( for v being Vector of holds b2 . v = Sum (lmlt (Line ((LineVec2Mx (v |-- b1)) * M),1),B2) ) holds
b1 = b2
end;
:: deftheorem Def3 defines Mx2Tran MATRLIN2:def 3 :
theorem Th32:
theorem Th33:
Lm5:
for K being Field
for A, B being Matrix of 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)
theorem Th34:
theorem Th35:
theorem Th36:
theorem
for
K being
Field for
V1,
V2 being
finite-dimensional VectSp of
finite-dimensional for
b1 being
OrdBasis of
V1 for
B2 being
FinSequence of
for
A,
B being
Matrix of the
carrier of
K,
len b1, holds
Mx2Tran (A + B),
b1,
B2 = (Mx2Tran A,b1,B2) + (Mx2Tran B,b1,B2)
theorem
theorem
theorem
for
K being
Field for
V1,
V2,
V3 being
finite-dimensional VectSp of
finite-dimensional for
b1 being
OrdBasis of
V1 for
b2 being
OrdBasis of
V2 for
B3 being
FinSequence of
for
A being
Matrix of the
carrier of
K,
len b1,
for
B being
Matrix of the
carrier of
K,
len b2, st
width A = len B holds
for
AB being
Matrix of the
carrier of
K,
len b1, st
AB = A * B holds
Mx2Tran AB,
b1,
B3 = (Mx2Tran B,b2,B3) * (Mx2Tran A,b1,b2)
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
Lm6:
for n being Nat
for K being Field holds the_rank_of (1. K,n) = n
theorem Th45:
theorem Th46:
theorem Th47:
Lm7:
for K being Field
for V1, V2 being finite-dimensional VectSp of finite-dimensional
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for A being Matrix of the carrier of K, len b1, st len b1 > 0 & len b2 > 0 holds
nullity (Mx2Tran A,b1,b2) = (len b1) - (the_rank_of A)
begin
theorem Th48:
theorem
theorem
Lm8:
for K being Field
for V1, V2, V3 being finite-dimensional VectSp of finite-dimensional
for f being linear-transformation of V1,V2
for g being Function of V2,V3 holds g * f = (g | (im f)) * f
theorem