:: by Karol P\c{a}k

::

:: Received July 11, 2008

:: Copyright (c) 2008-2019 Association of Mizar Users

theorem Th1: :: VECTSP11:1

for m, n being Nat

for K being Field

for A, B being Matrix of K

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT st [:(rng nt),(rng mt):] c= Indices A holds

Segm ((A + B),nt,mt) = (Segm (A,nt,mt)) + (Segm (B,nt,mt))

for K being Field

for A, B being Matrix of K

for nt being Element of n -tuples_on NAT

for mt being Element of m -tuples_on NAT st [:(rng nt),(rng mt):] c= Indices A holds

Segm ((A + B),nt,mt) = (Segm (A,nt,mt)) + (Segm (B,nt,mt))

proof end;

theorem Th2: :: VECTSP11:2

for n being Nat

for K being Field

for P being finite without_zero Subset of NAT st P c= Seg n holds

Segm ((1. (K,n)),P,P) = 1. (K,(card P))

for K being Field

for P being finite without_zero Subset of NAT st P c= Seg n holds

Segm ((1. (K,n)),P,P) = 1. (K,(card P))

proof end;

theorem Th3: :: VECTSP11:3

for K being Field

for A, B being Matrix of K

for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices A holds

Segm ((A + B),P,Q) = (Segm (A,P,Q)) + (Segm (B,P,Q))

for A, B being Matrix of K

for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices A holds

Segm ((A + B),P,Q) = (Segm (A,P,Q)) + (Segm (B,P,Q))

proof end;

theorem Th4: :: VECTSP11:4

for i, j, n being Nat

for K being Field

for A, B being Matrix of n,K st i in Seg n & j in Seg n holds

Delete ((A + B),i,j) = (Delete (A,i,j)) + (Delete (B,i,j))

for K being Field

for A, B being Matrix of n,K st i in Seg n & j in Seg n holds

Delete ((A + B),i,j) = (Delete (A,i,j)) + (Delete (B,i,j))

proof end;

theorem Th5: :: VECTSP11:5

for i, j, n being Nat

for K being Field

for a being Element of K

for A being Matrix of n,K st i in Seg n & j in Seg n holds

Delete ((a * A),i,j) = a * (Delete (A,i,j))

for K being Field

for a being Element of K

for A being Matrix of n,K st i in Seg n & j in Seg n holds

Delete ((a * A),i,j) = a * (Delete (A,i,j))

proof end;

theorem Th7: :: VECTSP11:7

for n being Nat

for K being Field

for A, B being Matrix of n,K ex P being Polynomial of K st

( len P <= n + 1 & ( for x being Element of K holds eval (P,x) = Det (A + (x * B)) ) )

for K being Field

for A, B being Matrix of n,K ex P being Polynomial of K st

( len P <= n + 1 & ( for x being Element of K holds eval (P,x) = Det (A + (x * B)) ) )

proof end;

:: The Characteristic Polynomials of Square Matrixs

theorem Th8: :: VECTSP11:8

for n being Nat

for K being Field

for A being Matrix of n,K ex P being Polynomial of K st

( len P = n + 1 & ( for x being Element of K holds eval (P,x) = Det (A + (x * (1. (K,n)))) ) )

for K being Field

for A being Matrix of n,K ex P being Polynomial of K st

( len P = n + 1 & ( for x being Element of K holds eval (P,x) = Det (A + (x * (1. (K,n)))) ) )

proof end;

Lm1: for K being Field

for V1, V2 being VectSp of K

for f being linear-transformation of V1,V2

for W1 being Subspace of V1

for W2 being Subspace of V2

for F being Function of W1,W2 st F = f | W1 holds

F is linear-transformation of W1,W2

proof end;

registration

let K be Field;

ex b_{1} being VectSp of K st

( not b_{1} is trivial & b_{1} is finite-dimensional )

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

existence ex b

( not b

proof end;

definition

let R be non empty doubleLoopStr ;

let V be non empty ModuleStr over R;

let IT be Function of V,V;

end;
let V be non empty ModuleStr over R;

let IT be Function of V,V;

attr IT is with_eigenvalues means :: VECTSP11:def 1

ex v being Vector of V ex a being Scalar of R st

( v <> 0. V & IT . v = a * v );

ex v being Vector of V ex a being Scalar of R st

( v <> 0. V & IT . v = a * v );

:: deftheorem defines with_eigenvalues VECTSP11:def 1 :

for R being non empty doubleLoopStr

for V being non empty ModuleStr over R

for IT being Function of V,V holds

( IT is with_eigenvalues iff ex v being Vector of V ex a being Scalar of R st

( v <> 0. V & IT . v = a * v ) );

for R being non empty doubleLoopStr

for V being non empty ModuleStr over R

for IT being Function of V,V holds

( IT is with_eigenvalues iff ex v being Vector of V ex a being Scalar of R st

( v <> 0. V & IT . v = a * v ) );

Lm2: for K being Field

for V being non trivial VectSp of K holds

( id V is with_eigenvalues & ex v being Vector of V st

( v <> 0. V & (id V) . v = (1_ K) * v ) )

proof end;

registration

let K be Field;

let V be non trivial VectSp of K;

ex b_{1} being linear-transformation of V,V st b_{1} is with_eigenvalues

end;
let V be non trivial VectSp of K;

cluster Relation-like the carrier of V -defined the carrier of V -valued Function-like non empty total quasi_total additive homogeneous with_eigenvalues for Element of bool [: the carrier of V, the carrier of V:];

existence ex b

proof end;

definition

let R be non empty doubleLoopStr ;

let V be non empty ModuleStr over R;

let f be Function of V,V;

assume A1: f is with_eigenvalues ;

ex b_{1} being Element of R ex v being Vector of V st

( v <> 0. V & f . v = b_{1} * v )
by A1;

end;
let V be non empty ModuleStr over R;

let f be Function of V,V;

assume A1: f is with_eigenvalues ;

mode eigenvalue of f -> Element of R means :Def2: :: VECTSP11:def 2

ex v being Vector of V st

( v <> 0. V & f . v = it * v );

existence ex v being Vector of V st

( v <> 0. V & f . v = it * v );

ex b

( v <> 0. V & f . v = b

:: deftheorem Def2 defines eigenvalue VECTSP11:def 2 :

for R being non empty doubleLoopStr

for V being non empty ModuleStr over R

for f being Function of V,V st f is with_eigenvalues holds

for b_{4} being Element of R holds

( b_{4} is eigenvalue of f iff ex v being Vector of V st

( v <> 0. V & f . v = b_{4} * v ) );

for R being non empty doubleLoopStr

for V being non empty ModuleStr over R

for f being Function of V,V st f is with_eigenvalues holds

for b

( b

( v <> 0. V & f . v = b

definition

let R be non empty doubleLoopStr ;

let V be non empty ModuleStr over R;

let f be Function of V,V;

let L be Scalar of R;

assume A1: ( f is with_eigenvalues & L is eigenvalue of f ) ;

existence

ex b_{1} being Vector of V st f . b_{1} = L * b_{1}

end;
let V be non empty ModuleStr over R;

let f be Function of V,V;

let L be Scalar of R;

assume A1: ( f is with_eigenvalues & L is eigenvalue of f ) ;

existence

ex b

proof end;

:: deftheorem Def3 defines eigenvector VECTSP11:def 3 :

for R being non empty doubleLoopStr

for V being non empty ModuleStr over R

for f being Function of V,V

for L being Scalar of R st f is with_eigenvalues & L is eigenvalue of f holds

for b_{5} being Vector of V holds

( b_{5} is eigenvector of f,L iff f . b_{5} = L * b_{5} );

for R being non empty doubleLoopStr

for V being non empty ModuleStr over R

for f being Function of V,V

for L being Scalar of R st f is with_eigenvalues & L is eigenvalue of f holds

for b

( b

theorem :: VECTSP11:9

for K being Field

for V being non trivial VectSp of K

for w being Vector of V

for a being Element of K st a <> 0. K holds

for f being with_eigenvalues Function of V,V

for L being eigenvalue of f holds

( a * f is with_eigenvalues & a * L is eigenvalue of a * f & ( w is eigenvector of f,L implies w is eigenvector of a * f,a * L ) & ( w is eigenvector of a * f,a * L implies w is eigenvector of f,L ) )

for V being non trivial VectSp of K

for w being Vector of V

for a being Element of K st a <> 0. K holds

for f being with_eigenvalues Function of V,V

for L being eigenvalue of f holds

( a * f is with_eigenvalues & a * L is eigenvalue of a * f & ( w is eigenvector of f,L implies w is eigenvector of a * f,a * L ) & ( w is eigenvector of a * f,a * L implies w is eigenvector of f,L ) )

proof end;

theorem :: VECTSP11:10

for K being Field

for V being non trivial VectSp of K

for f1, f2 being with_eigenvalues Function of V,V

for L1, L2 being Scalar of K st L1 is eigenvalue of f1 & L2 is eigenvalue of f2 & ex v being Vector of V st

( v is eigenvector of f1,L1 & v is eigenvector of f2,L2 & v <> 0. V ) holds

( f1 + f2 is with_eigenvalues & L1 + L2 is eigenvalue of f1 + f2 & ( for w being Vector of V st w is eigenvector of f1,L1 & w is eigenvector of f2,L2 holds

w is eigenvector of f1 + f2,L1 + L2 ) )

for V being non trivial VectSp of K

for f1, f2 being with_eigenvalues Function of V,V

for L1, L2 being Scalar of K st L1 is eigenvalue of f1 & L2 is eigenvalue of f2 & ex v being Vector of V st

( v is eigenvector of f1,L1 & v is eigenvector of f2,L2 & v <> 0. V ) holds

( f1 + f2 is with_eigenvalues & L1 + L2 is eigenvalue of f1 + f2 & ( for w being Vector of V st w is eigenvector of f1,L1 & w is eigenvector of f2,L2 holds

w is eigenvector of f1 + f2,L1 + L2 ) )

proof end;

theorem Th11: :: VECTSP11:11

for K being Field

for V being non trivial VectSp of K holds

( id V is with_eigenvalues & 1_ K is eigenvalue of id V & ( for v being Vector of V holds v is eigenvector of id V, 1_ K ) )

for V being non trivial VectSp of K holds

( id V is with_eigenvalues & 1_ K is eigenvalue of id V & ( for v being Vector of V holds v is eigenvector of id V, 1_ K ) )

proof end;

theorem :: VECTSP11:13

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1 st not ker f is trivial holds

( f is with_eigenvalues & 0. K is eigenvalue of f )

for V1 being VectSp of K

for f being linear-transformation of V1,V1 st not ker f is trivial holds

( f is with_eigenvalues & 0. K is eigenvalue of f )

proof end;

theorem Th14: :: VECTSP11:14

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1

for L being Scalar of K holds

( ( f is with_eigenvalues & L is eigenvalue of f ) iff not ker (f + ((- L) * (id V1))) is trivial )

for V1 being VectSp of K

for f being linear-transformation of V1,V1

for L being Scalar of K holds

( ( f is with_eigenvalues & L is eigenvalue of f ) iff not ker (f + ((- L) * (id V1))) is trivial )

proof end;

theorem Th15: :: VECTSP11:15

for K being Field

for L being Scalar of K

for V1 being finite-dimensional VectSp of K

for b1, b19 being OrdBasis of V1

for f being linear-transformation of V1,V1 holds

( ( f is with_eigenvalues & L is eigenvalue of f ) iff Det (AutEqMt ((f + ((- L) * (id V1))),b1,b19)) = 0. K )

for L being Scalar of K

for V1 being finite-dimensional VectSp of K

for b1, b19 being OrdBasis of V1

for f being linear-transformation of V1,V1 holds

( ( f is with_eigenvalues & L is eigenvalue of f ) iff Det (AutEqMt ((f + ((- L) * (id V1))),b1,b19)) = 0. K )

proof end;

theorem :: VECTSP11:16

for K being algebraic-closed Field

for V1 being non trivial finite-dimensional VectSp of K

for f being linear-transformation of V1,V1 holds f is with_eigenvalues

for V1 being non trivial finite-dimensional VectSp of K

for f being linear-transformation of V1,V1 holds f is with_eigenvalues

proof end;

theorem Th17: :: VECTSP11:17

for K being Field

for V1 being VectSp of K

for v1 being Vector of V1

for f being linear-transformation of V1,V1

for L being Scalar of K st f is with_eigenvalues & L is eigenvalue of f holds

( v1 is eigenvector of f,L iff v1 in ker (f + ((- L) * (id V1))) )

for V1 being VectSp of K

for v1 being Vector of V1

for f being linear-transformation of V1,V1

for L being Scalar of K st f is with_eigenvalues & L is eigenvalue of f holds

( v1 is eigenvector of f,L iff v1 in ker (f + ((- L) * (id V1))) )

proof end;

definition

let S be 1-sorted ;

let F be Function of S,S;

let n be Nat;

ex b_{1} being Function of S,S st

for F9 being Element of (GFuncs the carrier of S) st F9 = F holds

b_{1} = Product (n |-> F9)

for b_{1}, b_{2} being Function of S,S st ( for F9 being Element of (GFuncs the carrier of S) st F9 = F holds

b_{1} = Product (n |-> F9) ) & ( for F9 being Element of (GFuncs the carrier of S) st F9 = F holds

b_{2} = Product (n |-> F9) ) holds

b_{1} = b_{2}

end;
let F be Function of S,S;

let n be Nat;

func F |^ n -> Function of S,S means :Def4: :: VECTSP11:def 4

for F9 being Element of (GFuncs the carrier of S) st F9 = F holds

it = Product (n |-> F9);

existence for F9 being Element of (GFuncs the carrier of S) st F9 = F holds

it = Product (n |-> F9);

ex b

for F9 being Element of (GFuncs the carrier of S) st F9 = F holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def4 defines |^ VECTSP11:def 4 :

for S being 1-sorted

for F being Function of S,S

for n being Nat

for b_{4} being Function of S,S holds

( b_{4} = F |^ n iff for F9 being Element of (GFuncs the carrier of S) st F9 = F holds

b_{4} = Product (n |-> F9) );

for S being 1-sorted

for F being Function of S,S

for n being Nat

for b

( b

b

theorem Th20: :: VECTSP11:20

for i, j being Nat

for S being 1-sorted

for F being Function of S,S holds F |^ (i + j) = (F |^ j) * (F |^ i)

for S being 1-sorted

for F being Function of S,S holds F |^ (i + j) = (F |^ j) * (F |^ i)

proof end;

theorem :: VECTSP11:21

for i being Nat

for S being 1-sorted

for F being Function of S,S

for s1, s2 being Element of S

for n, m being Nat st (F |^ m) . s1 = s2 & (F |^ n) . s2 = s2 holds

(F |^ (m + (i * n))) . s1 = s2

for S being 1-sorted

for F being Function of S,S

for s1, s2 being Element of S

for n, m being Nat st (F |^ m) . s1 = s2 & (F |^ n) . s2 = s2 holds

(F |^ (m + (i * n))) . s1 = s2

proof end;

theorem :: VECTSP11:22

for n being Nat

for K being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr

for V1 being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over K

for W being Subspace of V1

for f being Function of V1,V1

for fW being Function of W,W st fW = f | W holds

(f |^ n) | W = fW |^ n

for K being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr

for V1 being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over K

for W being Subspace of V1

for f being Function of V1,V1

for fW being Function of W,W st fW = f | W holds

(f |^ n) | W = fW |^ n

proof end;

registration

let K be Field;

let V1 be VectSp of K;

let f be linear-transformation of V1,V1;

let n be Nat;

coherence

( f |^ n is homogeneous & f |^ n is additive )

end;
let V1 be VectSp of K;

let f be linear-transformation of V1,V1;

let n be Nat;

coherence

( f |^ n is homogeneous & f |^ n is additive )

proof end;

theorem Th23: :: VECTSP11:23

for i, j being Nat

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1

for v1 being Vector of V1 st (f |^ i) . v1 = 0. V1 holds

(f |^ (i + j)) . v1 = 0. V1

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1

for v1 being Vector of V1 st (f |^ i) . v1 = 0. V1 holds

(f |^ (i + j)) . v1 = 0. V1

proof end;

definition

let K be Field;

let V1 be VectSp of K;

let f be linear-transformation of V1,V1;

ex b_{1} being strict Subspace of V1 st the carrier of b_{1} = { v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1 }

for b_{1}, b_{2} being strict Subspace of V1 st the carrier of b_{1} = { v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1 } & the carrier of b_{2} = { v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1 } holds

b_{1} = b_{2}
by VECTSP_4:29;

end;
let V1 be VectSp of K;

let f be linear-transformation of V1,V1;

func UnionKers f -> strict Subspace of V1 means :Def5: :: VECTSP11:def 5

the carrier of it = { v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1 } ;

existence the carrier of it = { v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1 } ;

ex b

proof end;

uniqueness for b

b

:: deftheorem Def5 defines UnionKers VECTSP11:def 5 :

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1

for b_{4} being strict Subspace of V1 holds

( b_{4} = UnionKers f iff the carrier of b_{4} = { v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1 } );

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1

for b

( b

theorem Th24: :: VECTSP11:24

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1

for v1 being Vector of V1 holds

( v1 in UnionKers f iff ex n being Nat st (f |^ n) . v1 = 0. V1 )

for V1 being VectSp of K

for f being linear-transformation of V1,V1

for v1 being Vector of V1 holds

( v1 in UnionKers f iff ex n being Nat st (f |^ n) . v1 = 0. V1 )

proof end;

theorem Th25: :: VECTSP11:25

for i being Nat

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1 holds ker (f |^ i) is Subspace of UnionKers f

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1 holds ker (f |^ i) is Subspace of UnionKers f

proof end;

theorem Th26: :: VECTSP11:26

for i, j being Nat

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1 holds ker (f |^ i) is Subspace of ker (f |^ (i + j))

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1 holds ker (f |^ i) is Subspace of ker (f |^ (i + j))

proof end;

theorem :: VECTSP11:27

for K being Field

for V being finite-dimensional VectSp of K

for f being linear-transformation of V,V ex n being Nat st UnionKers f = ker (f |^ n)

for V being finite-dimensional VectSp of K

for f being linear-transformation of V,V ex n being Nat st UnionKers f = ker (f |^ n)

proof end;

theorem Th28: :: VECTSP11:28

for n being Nat

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1 holds f | (ker (f |^ n)) is linear-transformation of (ker (f |^ n)),(ker (f |^ n))

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1 holds f | (ker (f |^ n)) is linear-transformation of (ker (f |^ n)),(ker (f |^ n))

proof end;

theorem :: VECTSP11:29

for n being Nat

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1

for L being Scalar of K holds f | (ker ((f + (L * (id V1))) |^ n)) is linear-transformation of (ker ((f + (L * (id V1))) |^ n)),(ker ((f + (L * (id V1))) |^ n))

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1

for L being Scalar of K holds f | (ker ((f + (L * (id V1))) |^ n)) is linear-transformation of (ker ((f + (L * (id V1))) |^ n)),(ker ((f + (L * (id V1))) |^ n))

proof end;

theorem Th30: :: VECTSP11:30

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1 holds f | (UnionKers f) is linear-transformation of (UnionKers f),(UnionKers f)

for V1 being VectSp of K

for f being linear-transformation of V1,V1 holds f | (UnionKers f) is linear-transformation of (UnionKers f),(UnionKers f)

proof end;

theorem Th31: :: VECTSP11:31

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1

for L being Scalar of K holds f | (UnionKers (f + (L * (id V1)))) is linear-transformation of (UnionKers (f + (L * (id V1)))),(UnionKers (f + (L * (id V1))))

for V1 being VectSp of K

for f being linear-transformation of V1,V1

for L being Scalar of K holds f | (UnionKers (f + (L * (id V1)))) is linear-transformation of (UnionKers (f + (L * (id V1)))),(UnionKers (f + (L * (id V1))))

proof end;

theorem Th32: :: VECTSP11:32

for n being Nat

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1 holds f | (im (f |^ n)) is linear-transformation of (im (f |^ n)),(im (f |^ n))

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1 holds f | (im (f |^ n)) is linear-transformation of (im (f |^ n)),(im (f |^ n))

proof end;

theorem :: VECTSP11:33

for n being Nat

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1

for L being Scalar of K holds f | (im ((f + (L * (id V1))) |^ n)) is linear-transformation of (im ((f + (L * (id V1))) |^ n)),(im ((f + (L * (id V1))) |^ n))

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1

for L being Scalar of K holds f | (im ((f + (L * (id V1))) |^ n)) is linear-transformation of (im ((f + (L * (id V1))) |^ n)),(im ((f + (L * (id V1))) |^ n))

proof end;

theorem Th34: :: VECTSP11:34

for n being Nat

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1 st UnionKers f = ker (f |^ n) holds

(ker (f |^ n)) /\ (im (f |^ n)) = (0). V1

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1 st UnionKers f = ker (f |^ n) holds

(ker (f |^ n)) /\ (im (f |^ n)) = (0). V1

proof end;

theorem :: VECTSP11:35

for K being Field

for V being finite-dimensional VectSp of K

for f being linear-transformation of V,V

for n being Nat st UnionKers f = ker (f |^ n) holds

V is_the_direct_sum_of ker (f |^ n), im (f |^ n)

for V being finite-dimensional VectSp of K

for f being linear-transformation of V,V

for n being Nat st UnionKers f = ker (f |^ n) holds

V is_the_direct_sum_of ker (f |^ n), im (f |^ n)

proof end;

theorem Th36: :: VECTSP11:36

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1

for I being Linear_Compl of UnionKers f holds f | I is one-to-one

for V1 being VectSp of K

for f being linear-transformation of V1,V1

for I being Linear_Compl of UnionKers f holds f | I is one-to-one

proof end;

theorem Th37: :: VECTSP11:37

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1

for L being Scalar of K

for I being Linear_Compl of UnionKers (f + ((- L) * (id V1)))

for fI being linear-transformation of I,I st fI = f | I holds

for v being Vector of I st fI . v = L * v holds

v = 0. V1

for V1 being VectSp of K

for f being linear-transformation of V1,V1

for L being Scalar of K

for I being Linear_Compl of UnionKers (f + ((- L) * (id V1)))

for fI being linear-transformation of I,I st fI = f | I holds

for v being Vector of I st fI . v = L * v holds

v = 0. V1

proof end;

Lm3: for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1

for a, b being Scalar of K holds (a * b) * f = a * (b * f)

proof end;

Lm4: for K being Field

for V1 being VectSp of K

for L being Scalar of K

for f, g being Function of V1,V1 holds L * (f * g) = (L * f) * g

proof end;

Lm5: for K being Field

for V1 being VectSp of K

for L being Scalar of K

for f, g being Function of V1,V1 st f is additive & f is homogeneous holds

L * (f * g) = f * (L * g)

proof end;

Lm6: for K being Field

for V1 being VectSp of K

for f1, f2, g being Function of V1,V1 holds (f1 + f2) * g = (f1 * g) + (f2 * g)

proof end;

Lm7: for K being Field

for V1 being VectSp of K

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

g * (f1 + f2) = (g * f1) + (g * f2)

proof end;

Lm8: for K being Field

for V1 being VectSp of K

for f1, f2, f3 being Function of V1,V1 holds (f1 + f2) + f3 = f1 + (f2 + f3)

proof end;

Lm9: for n being Nat

for K being Field

for V1 being VectSp of K

for L being Scalar of K holds (L * (id V1)) |^ n = ((power K) . (L,n)) * (id V1)

proof end;

Lm10: for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1

for a, b being Scalar of K holds (a + b) * f = (a * f) + (b * f)

proof end;

theorem Th38: :: VECTSP11:38

for n being Nat

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1

for L being Scalar of K st n >= 1 holds

ex h being linear-transformation of V1,V1 st

( (f + (L * (id V1))) |^ n = (f * h) + ((L * (id V1)) |^ n) & ( for i being Nat holds (f |^ i) * h = h * (f |^ i) ) )

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1

for L being Scalar of K st n >= 1 holds

ex h being linear-transformation of V1,V1 st

( (f + (L * (id V1))) |^ n = (f * h) + ((L * (id V1)) |^ n) & ( for i being Nat holds (f |^ i) * h = h * (f |^ i) ) )

proof end;

theorem :: VECTSP11:39

for K being Field

for V1 being VectSp of K

for f being linear-transformation of V1,V1

for L1, L2 being Scalar of K st f is with_eigenvalues & L1 <> L2 & L2 is eigenvalue of f holds

for I being Linear_Compl of UnionKers (f + ((- L1) * (id V1)))

for fI being linear-transformation of I,I st fI = f | I holds

( fI is with_eigenvalues & L1 is not eigenvalue of fI & L2 is eigenvalue of fI & UnionKers (f + ((- L2) * (id V1))) is Subspace of I )

for V1 being VectSp of K

for f being linear-transformation of V1,V1

for L1, L2 being Scalar of K st f is with_eigenvalues & L1 <> L2 & L2 is eigenvalue of f holds

for I being Linear_Compl of UnionKers (f + ((- L1) * (id V1)))

for fI being linear-transformation of I,I st fI = f | I holds

( fI is with_eigenvalues & L1 is not eigenvalue of fI & L2 is eigenvalue of fI & UnionKers (f + ((- L2) * (id V1))) is Subspace of I )

proof end;

:: Main Lemmas for Expansion of Matrices of Nilpotent Linear Transformations

theorem :: VECTSP11:40

for K being Field

for V1 being VectSp of K

for U being finite Subset of V1 st U is linearly-independent holds

for u being Vector of V1 st u in U holds

for L being Linear_Combination of U \ {u} holds

( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )

for V1 being VectSp of K

for U being finite Subset of V1 st U is linearly-independent holds

for u being Vector of V1 st u in U holds

for L being Linear_Combination of U \ {u} holds

( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )

proof end;

theorem Th41: :: VECTSP11:41

for K being Field

for V1, V2 being VectSp of K

for A being Subset of V1

for L being Linear_Combination of V2

for f being linear-transformation of V1,V2 st Carrier L c= f .: A holds

ex M being Linear_Combination of A st f . (Sum M) = Sum L

for V1, V2 being VectSp of K

for A being Subset of V1

for L being Linear_Combination of V2

for f being linear-transformation of V1,V2 st Carrier L c= f .: A holds

ex M being Linear_Combination of A st f . (Sum M) = Sum L

proof end;

theorem :: VECTSP11:42

for K being Field

for V1, V2 being VectSp of K

for f being linear-transformation of V1,V2

for A being Subset of V1

for B being Subset of V2 st f .: A = B holds

f .: the carrier of (Lin A) = the carrier of (Lin B)

for V1, V2 being VectSp of K

for f being linear-transformation of V1,V2

for A being Subset of V1

for B being Subset of V2 st f .: A = B holds

f .: the carrier of (Lin A) = the carrier of (Lin B)

proof end;

theorem Th43: :: VECTSP11:43

for K being Field

for V1, V2 being VectSp of K

for L being Linear_Combination of V1

for F being FinSequence of V1

for f being linear-transformation of V1,V2 st f | ((Carrier L) /\ (rng F)) is one-to-one & rng F c= Carrier L holds

ex Lf being Linear_Combination of V2 st

( Carrier Lf = f .: ((Carrier L) /\ (rng F)) & f * (L (#) F) = Lf (#) (f * F) & ( for v1 being Vector of V1 st v1 in (Carrier L) /\ (rng F) holds

L . v1 = Lf . (f . v1) ) )

for V1, V2 being VectSp of K

for L being Linear_Combination of V1

for F being FinSequence of V1

for f being linear-transformation of V1,V2 st f | ((Carrier L) /\ (rng F)) is one-to-one & rng F c= Carrier L holds

ex Lf being Linear_Combination of V2 st

( Carrier Lf = f .: ((Carrier L) /\ (rng F)) & f * (L (#) F) = Lf (#) (f * F) & ( for v1 being Vector of V1 st v1 in (Carrier L) /\ (rng F) holds

L . v1 = Lf . (f . v1) ) )

proof end;

theorem :: VECTSP11:44

for K being Field

for V1, V2 being VectSp of K

for A, B being Subset of V1

for L being Linear_Combination of V1 st Carrier L c= A \/ B & Sum L = 0. V1 holds

for f being additive homogeneous Function of V1,V2 st f | B is one-to-one & f .: B is linearly-independent Subset of V2 & f .: A c= {(0. V2)} holds

Carrier L c= A

for V1, V2 being VectSp of K

for A, B being Subset of V1

for L being Linear_Combination of V1 st Carrier L c= A \/ B & Sum L = 0. V1 holds

for f being additive homogeneous Function of V1,V2 st f | B is one-to-one & f .: B is linearly-independent Subset of V2 & f .: A c= {(0. V2)} holds

Carrier L c= A

proof end;