let K be algebraic-closed Field; for V being non trivial finite-dimensional VectSp of K
for F being linear-transformation of V,V ex J being non-empty FinSequence_of_Jordan_block of K ex b1 being OrdBasis of V st
( AutMt (F,b1,b1) = block_diagonal (J,(0. K)) & ( for L being Scalar of K holds
( L is eigenvalue of F iff ex i being Nat st
( i in dom J & J . i = Jordan_block (L,(len (J . i))) ) ) ) )
defpred S1[ Nat] means for V being non trivial finite-dimensional VectSp of K st dim V <= $1 holds
for F being linear-transformation of V,V ex J being non-empty FinSequence_of_Jordan_block of K ex b1 being OrdBasis of V st
( AutMt (F,b1,b1) = block_diagonal (J,(0. K)) & ( for L being Scalar of K holds
( L is eigenvalue of F iff ex i being Nat st
( i in dom J & J . i = Jordan_block (L,(len (J . i))) ) ) ) );
let V be non trivial finite-dimensional VectSp of K; for F being linear-transformation of V,V ex J being non-empty FinSequence_of_Jordan_block of K ex b1 being OrdBasis of V st
( AutMt (F,b1,b1) = block_diagonal (J,(0. K)) & ( for L being Scalar of K holds
( L is eigenvalue of F iff ex i being Nat st
( i in dom J & J . i = Jordan_block (L,(len (J . i))) ) ) ) )
let F be linear-transformation of V,V; ex J being non-empty FinSequence_of_Jordan_block of K ex b1 being OrdBasis of V st
( AutMt (F,b1,b1) = block_diagonal (J,(0. K)) & ( for L being Scalar of K holds
( L is eigenvalue of F iff ex i being Nat st
( i in dom J & J . i = Jordan_block (L,(len (J . i))) ) ) ) )
A1:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A2:
S1[
n]
;
S1[n + 1]
set n1 =
n + 1;
let V be non
trivial finite-dimensional VectSp of
K;
( dim V <= n + 1 implies for F being linear-transformation of V,V ex J being non-empty FinSequence_of_Jordan_block of K ex b1 being OrdBasis of V st
( AutMt (F,b1,b1) = block_diagonal (J,(0. K)) & ( for L being Scalar of K holds
( L is eigenvalue of F iff ex i being Nat st
( i in dom J & J . i = Jordan_block (L,(len (J . i))) ) ) ) ) )
assume A3:
dim V <= n + 1
;
for F being linear-transformation of V,V ex J being non-empty FinSequence_of_Jordan_block of K ex b1 being OrdBasis of V st
( AutMt (F,b1,b1) = block_diagonal (J,(0. K)) & ( for L being Scalar of K holds
( L is eigenvalue of F iff ex i being Nat st
( i in dom J & J . i = Jordan_block (L,(len (J . i))) ) ) ) )
per cases
( dim V <= n or dim V = n + 1 )
by A3, NAT_1:8;
suppose A4:
dim V = n + 1
;
for F being linear-transformation of V,V ex J being non-empty FinSequence_of_Jordan_block of K ex b1 being OrdBasis of V st
( AutMt (F,b1,b1) = block_diagonal (J,(0. K)) & ( for L being Scalar of K holds
( L is eigenvalue of F iff ex i being Nat st
( i in dom J & J . i = Jordan_block (L,(len (J . i))) ) ) ) )let F be
linear-transformation of
V,
V;
ex J being non-empty FinSequence_of_Jordan_block of K ex b1 being OrdBasis of V st
( AutMt (F,b1,b1) = block_diagonal (J,(0. K)) & ( for L being Scalar of K holds
( L is eigenvalue of F iff ex i being Nat st
( i in dom J & J . i = Jordan_block (L,(len (J . i))) ) ) ) )A5:
F is
with_eigenvalues
by VECTSP11:16;
then consider v being
Vector of
V,
L being
Scalar of
K such that A6:
(
v <> 0. V &
F . v = L * v )
by VECTSP11:def 1;
set FL =
F + ((- L) * (id V));
L is
eigenvalue of
F
by A5, A6, VECTSP11:def 2;
then
not
ker (F + ((- L) * (id V))) is
trivial
by A5, VECTSP11:14;
then A7:
dim (ker (F + ((- L) * (id V)))) <> 0
by MATRLIN2:42;
consider m being
Nat such that A8:
UnionKers (F + ((- L) * (id V))) = ker ((F + ((- L) * (id V))) |^ m)
by VECTSP11:27;
set IM =
im ((F + ((- L) * (id V))) |^ m);
set KER =
ker ((F + ((- L) * (id V))) |^ m);
A9:
dim V = (dim (ker ((F + ((- L) * (id V))) |^ m))) + (dim (im ((F + ((- L) * (id V))) |^ m)))
by A8, VECTSP11:35, VECTSP_9:34;
A10:
im ((F + ((- L) * (id V))) |^ m) is
Linear_Compl of
ker ((F + ((- L) * (id V))) |^ m)
by A8, VECTSP11:35, VECTSP_5:37;
reconsider FK =
F | (ker ((F + ((- L) * (id V))) |^ m)) as
linear-transformation of
(ker ((F + ((- L) * (id V))) |^ m)),
(ker ((F + ((- L) * (id V))) |^ m)) by VECTSP11:29;
consider Jk being
non-empty FinSequence_of_Jordan_block of
L,
K,
Bker being
OrdBasis of
ker ((F + ((- L) * (id V))) |^ m) such that A11:
AutMt (
FK,
Bker,
Bker)
= block_diagonal (
Jk,
(0. K))
by Th30;
(F + ((- L) * (id V))) |^ 1
= F + ((- L) * (id V))
by VECTSP11:19;
then A12:
ker (F + ((- L) * (id V))) is
Subspace of
ker ((F + ((- L) * (id V))) |^ m)
by A8, VECTSP11:25;
A13:
len Jk <> 0
reconsider FI =
F | (im ((F + ((- L) * (id V))) |^ m)) as
linear-transformation of
(im ((F + ((- L) * (id V))) |^ m)),
(im ((F + ((- L) * (id V))) |^ m)) by VECTSP11:33;
A14:
(ker ((F + ((- L) * (id V))) |^ m)) /\ (im ((F + ((- L) * (id V))) |^ m)) = (0). V
by A8, VECTSP11:34;
A15:
V is_the_direct_sum_of ker ((F + ((- L) * (id V))) |^ m),
im ((F + ((- L) * (id V))) |^ m)
by A8, VECTSP11:35;
then A16:
(ker ((F + ((- L) * (id V))) |^ m)) + (im ((F + ((- L) * (id V))) |^ m)) = (Omega). V
by VECTSP_5:def 4;
per cases
( im ((F + ((- L) * (id V))) |^ m) is trivial or not im ((F + ((- L) * (id V))) |^ m) is trivial )
;
suppose A17:
im ((F + ((- L) * (id V))) |^ m) is
trivial
;
ex J being non-empty FinSequence_of_Jordan_block of K ex b1 being OrdBasis of V st
( AutMt (F,b1,b1) = block_diagonal (J,(0. K)) & ( for L being Scalar of K holds
( L is eigenvalue of F iff ex i being Nat st
( i in dom J & J . i = Jordan_block (L,(len (J . i))) ) ) ) )set Bim = the
OrdBasis of
im ((F + ((- L) * (id V))) |^ m);
0 =
dim (im ((F + ((- L) * (id V))) |^ m))
by A17, MATRLIN2:42
.=
len the
OrdBasis of
im ((F + ((- L) * (id V))) |^ m)
by MATRLIN2:21
.=
len (AutMt (FI, the OrdBasis of im ((F + ((- L) * (id V))) |^ m), the OrdBasis of im ((F + ((- L) * (id V))) |^ m)))
by MATRIX_0:def 2
;
then A18:
AutMt (
FI, the
OrdBasis of
im ((F + ((- L) * (id V))) |^ m), the
OrdBasis of
im ((F + ((- L) * (id V))) |^ m))
= {}
;
Bker ^ the
OrdBasis of
im ((F + ((- L) * (id V))) |^ m) is
OrdBasis of
(ker ((F + ((- L) * (id V))) |^ m)) + (im ((F + ((- L) * (id V))) |^ m))
by A14, MATRLIN2:26;
then reconsider BB =
Bker ^ the
OrdBasis of
im ((F + ((- L) * (id V))) |^ m) as
OrdBasis of
V by A16, MATRLIN2:4;
take
Jk
;
ex b1 being OrdBasis of V st
( AutMt (F,b1,b1) = block_diagonal (Jk,(0. K)) & ( for L being Scalar of K holds
( L is eigenvalue of F iff ex i being Nat st
( i in dom Jk & Jk . i = Jordan_block (L,(len (Jk . i))) ) ) ) )take
BB
;
( AutMt (F,BB,BB) = block_diagonal (Jk,(0. K)) & ( for L being Scalar of K holds
( L is eigenvalue of F iff ex i being Nat st
( i in dom Jk & Jk . i = Jordan_block (L,(len (Jk . i))) ) ) ) )A19:
(
dim (im ((F + ((- L) * (id V))) |^ m)) = 0 implies
dim (im ((F + ((- L) * (id V))) |^ m)) = 0 )
;
(
dim (ker ((F + ((- L) * (id V))) |^ m)) = 0 implies
dim (ker ((F + ((- L) * (id V))) |^ m)) = 0 )
;
hence AutMt (
F,
BB,
BB) =
block_diagonal (
<*(AutMt (FK,Bker,Bker)),(AutMt (FI, the OrdBasis of im ((F + ((- L) * (id V))) |^ m), the OrdBasis of im ((F + ((- L) * (id V))) |^ m)))*>,
(0. K))
by A15, A19, MATRLIN2:27
.=
block_diagonal (
<*(AutMt (FK,Bker,Bker))*>,
(0. K))
by A18, MATRIXJ1:40
.=
block_diagonal (
Jk,
(0. K))
by A11, MATRIXJ1:34
;
for L being Scalar of K holds
( L is eigenvalue of F iff ex i being Nat st
( i in dom Jk & Jk . i = Jordan_block (L,(len (Jk . i))) ) )let L1 be
Scalar of
K;
( L1 is eigenvalue of F iff ex i being Nat st
( i in dom Jk & Jk . i = Jordan_block (L1,(len (Jk . i))) ) )thus
(
L1 is
eigenvalue of
F implies ex
i being
Nat st
(
i in dom Jk &
Jk . i = Jordan_block (
L1,
(len (Jk . i))) ) )
( ex i being Nat st
( i in dom Jk & Jk . i = Jordan_block (L1,(len (Jk . i))) ) implies L1 is eigenvalue of F )given i being
Nat such that A22:
i in dom Jk
and A23:
Jk . i = Jordan_block (
L1,
(len (Jk . i)))
;
L1 is eigenvalue of F
Jk . i <> {}
by A22, FUNCT_1:def 9;
then
len (Jk . i) in Seg (len (Jk . i))
by FINSEQ_1:3;
then
[(len (Jk . i)),(len (Jk . i))] in [:(Seg (len (Jk . i))),(Seg (len (Jk . i))):]
by ZFMISC_1:87;
then A24:
[(len (Jk . i)),(len (Jk . i))] in Indices (Jk . i)
by MATRIX_0:24;
ex
k being
Nat st
Jk . i = Jordan_block (
L,
k)
by A22, Def3;
then L =
(Jk . i) * (
(len (Jk . i)),
(len (Jk . i)))
by A24, Def1
.=
L1
by A23, A24, Def1
;
hence
L1 is
eigenvalue of
F
by A5, A6, VECTSP11:def 2;
verum end; suppose A25:
not
im ((F + ((- L) * (id V))) |^ m) is
trivial
;
ex J being non-empty FinSequence_of_Jordan_block of K ex b1 being OrdBasis of V st
( AutMt (F,b1,b1) = block_diagonal (J,(0. K)) & ( for L being Scalar of K holds
( L is eigenvalue of F iff ex i being Nat st
( i in dom J & J . i = Jordan_block (L,(len (J . i))) ) ) ) )
(
n + 1
<> dim (im ((F + ((- L) * (id V))) |^ m)) &
dim (im ((F + ((- L) * (id V))) |^ m)) <= n + 1 )
by A4, A12, A7, A9, VECTSP_9:25;
then
dim (im ((F + ((- L) * (id V))) |^ m)) < n + 1
by XXREAL_0:1;
then
dim (im ((F + ((- L) * (id V))) |^ m)) <= n
by NAT_1:13;
then consider Ji being
non-empty FinSequence_of_Jordan_block of
K,
Bim being
OrdBasis of
im ((F + ((- L) * (id V))) |^ m) such that A26:
AutMt (
FI,
Bim,
Bim)
= block_diagonal (
Ji,
(0. K))
and A27:
for
L being
Scalar of
K holds
(
L is
eigenvalue of
FI iff ex
i being
Nat st
(
i in dom Ji &
Ji . i = Jordan_block (
L,
(len (Ji . i))) ) )
by A2, A25;
Bker ^ Bim is
OrdBasis of
(ker ((F + ((- L) * (id V))) |^ m)) + (im ((F + ((- L) * (id V))) |^ m))
by A14, MATRLIN2:26;
then reconsider BB =
Bker ^ Bim as
OrdBasis of
V by A16, MATRLIN2:4;
set JJ =
Jk ^ Ji;
A33:
FI is
with_eigenvalues
by A25, VECTSP11:16;
A34:
(
dim (im ((F + ((- L) * (id V))) |^ m)) = 0 implies
dim (im ((F + ((- L) * (id V))) |^ m)) = 0 )
;
reconsider JJ =
Jk ^ Ji as
non-empty FinSequence_of_Jordan_block of
K by A28, FUNCT_1:def 9;
take
JJ
;
ex b1 being OrdBasis of V st
( AutMt (F,b1,b1) = block_diagonal (JJ,(0. K)) & ( for L being Scalar of K holds
( L is eigenvalue of F iff ex i being Nat st
( i in dom JJ & JJ . i = Jordan_block (L,(len (JJ . i))) ) ) ) )take
BB
;
( AutMt (F,BB,BB) = block_diagonal (JJ,(0. K)) & ( for L being Scalar of K holds
( L is eigenvalue of F iff ex i being Nat st
( i in dom JJ & JJ . i = Jordan_block (L,(len (JJ . i))) ) ) ) )
(
dim (ker ((F + ((- L) * (id V))) |^ m)) = 0 implies
dim (ker ((F + ((- L) * (id V))) |^ m)) = 0 )
;
hence AutMt (
F,
BB,
BB) =
block_diagonal (
<*(block_diagonal (Jk,(0. K))),(block_diagonal (Ji,(0. K)))*>,
(0. K))
by A11, A15, A26, A34, MATRLIN2:27
.=
block_diagonal (
(<*(block_diagonal (Jk,(0. K)))*> ^ Ji),
(0. K))
by MATRIXJ1:36
.=
block_diagonal (
JJ,
(0. K))
by MATRIXJ1:35
;
for L being Scalar of K holds
( L is eigenvalue of F iff ex i being Nat st
( i in dom JJ & JJ . i = Jordan_block (L,(len (JJ . i))) ) )let L1 be
Scalar of
K;
( L1 is eigenvalue of F iff ex i being Nat st
( i in dom JJ & JJ . i = Jordan_block (L1,(len (JJ . i))) ) )thus
(
L1 is
eigenvalue of
F implies ex
i being
Nat st
(
i in dom JJ &
JJ . i = Jordan_block (
L1,
(len (JJ . i))) ) )
( ex i being Nat st
( i in dom JJ & JJ . i = Jordan_block (L1,(len (JJ . i))) ) implies L1 is eigenvalue of F )proof
assume A35:
L1 is
eigenvalue of
F
;
ex i being Nat st
( i in dom JJ & JJ . i = Jordan_block (L1,(len (JJ . i))) )
per cases
( L = L1 or L <> L1 )
;
suppose
L <> L1
;
ex i being Nat st
( i in dom JJ & JJ . i = Jordan_block (L1,(len (JJ . i))) )then
L1 is
eigenvalue of
FI
by A5, A8, A10, A35, VECTSP11:39;
then consider i being
Nat such that A39:
i in dom Ji
and A40:
Ji . i = Jordan_block (
L1,
(len (Ji . i)))
by A27;
take ii =
(len Jk) + i;
( ii in dom JJ & JJ . ii = Jordan_block (L1,(len (JJ . ii))) )
JJ . ii = Ji . i
by A39, FINSEQ_1:def 7;
hence
(
ii in dom JJ &
JJ . ii = Jordan_block (
L1,
(len (JJ . ii))) )
by A39, A40, FINSEQ_1:28;
verum end; end;
end; given i being
Nat such that A41:
i in dom JJ
and A42:
JJ . i = Jordan_block (
L1,
(len (JJ . i)))
;
L1 is eigenvalue of Fper cases
( i in dom Jk or ex j being Nat st
( j in dom Ji & i = (len Jk) + j ) )
by A41, FINSEQ_1:25;
suppose A43:
i in dom Jk
;
L1 is eigenvalue of Fthen
Jk . i <> {}
by FUNCT_1:def 9;
then
len (Jk . i) in Seg (len (Jk . i))
by FINSEQ_1:3;
then
[(len (Jk . i)),(len (Jk . i))] in [:(Seg (len (Jk . i))),(Seg (len (Jk . i))):]
by ZFMISC_1:87;
then A44:
[(len (Jk . i)),(len (Jk . i))] in Indices (Jk . i)
by MATRIX_0:24;
A45:
JJ . i = Jk . i
by A43, FINSEQ_1:def 7;
ex
k being
Nat st
Jk . i = Jordan_block (
L,
k)
by A43, Def3;
then L =
(Jk . i) * (
(len (Jk . i)),
(len (Jk . i)))
by A44, Def1
.=
L1
by A42, A45, A44, Def1
;
hence
L1 is
eigenvalue of
F
by A5, A6, VECTSP11:def 2;
verum end; end; end; end; end; end;
end;
A51:
S1[ 0 ]
proof
let V be non
trivial finite-dimensional VectSp of
K;
( dim V <= 0 implies for F being linear-transformation of V,V ex J being non-empty FinSequence_of_Jordan_block of K ex b1 being OrdBasis of V st
( AutMt (F,b1,b1) = block_diagonal (J,(0. K)) & ( for L being Scalar of K holds
( L is eigenvalue of F iff ex i being Nat st
( i in dom J & J . i = Jordan_block (L,(len (J . i))) ) ) ) ) )
assume
dim V <= 0
;
for F being linear-transformation of V,V ex J being non-empty FinSequence_of_Jordan_block of K ex b1 being OrdBasis of V st
( AutMt (F,b1,b1) = block_diagonal (J,(0. K)) & ( for L being Scalar of K holds
( L is eigenvalue of F iff ex i being Nat st
( i in dom J & J . i = Jordan_block (L,(len (J . i))) ) ) ) )
then
dim V = 0
;
hence
for
F being
linear-transformation of
V,
V ex
J being
non-empty FinSequence_of_Jordan_block of
K ex
b1 being
OrdBasis of
V st
(
AutMt (
F,
b1,
b1)
= block_diagonal (
J,
(0. K)) & ( for
L being
Scalar of
K holds
(
L is
eigenvalue of
F iff ex
i being
Nat st
(
i in dom J &
J . i = Jordan_block (
L,
(len (J . i))) ) ) ) )
by MATRLIN2:42;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A51, A1);
then
S1[ dim V]
;
hence
ex J being non-empty FinSequence_of_Jordan_block of K ex b1 being OrdBasis of V st
( AutMt (F,b1,b1) = block_diagonal (J,(0. K)) & ( for L being Scalar of K holds
( L is eigenvalue of F iff ex i being Nat st
( i in dom J & J . i = Jordan_block (L,(len (J . i))) ) ) ) )
; verum