let n be Nat; :: thesis: for K being algebraic-closed Field
for M being Matrix of n,K ex J being non-empty FinSequence_of_Jordan_block of K ex P being Matrix of n,K st
( Sum (Len J) = n & P is invertible & M = (P * (block_diagonal J,(0. K))) * (P ~ ) )
let K be algebraic-closed Field; :: thesis: for M being Matrix of n,K ex J being non-empty FinSequence_of_Jordan_block of K ex P being Matrix of n,K st
( Sum (Len J) = n & P is invertible & M = (P * (block_diagonal J,(0. K))) * (P ~ ) )
let M be Matrix of n,K; :: thesis: ex J being non-empty FinSequence_of_Jordan_block of K ex P being Matrix of n,K st
( Sum (Len J) = n & P is invertible & M = (P * (block_diagonal J,(0. K))) * (P ~ ) )
per cases
( n = 0 or n > 0 )
;
suppose A1:
n = 0
;
:: thesis: ex J being non-empty FinSequence_of_Jordan_block of K ex P being Matrix of n,K st
( Sum (Len J) = n & P is invertible & M = (P * (block_diagonal J,(0. K))) * (P ~ ) )reconsider J =
{} as
FinSequence_of_Jordan_block of
K by Lm2;
for
x being
set st
x in dom J holds
not
J . x is
empty
;
then reconsider J =
J as
non-empty FinSequence_of_Jordan_block of
K by FUNCT_1:def 15;
reconsider P =
{} as
Matrix of
n,
K by A1, MATRIX_1:13;
take
J
;
:: thesis: ex P being Matrix of n,K st
( Sum (Len J) = n & P is invertible & M = (P * (block_diagonal J,(0. K))) * (P ~ ) )take
P
;
:: thesis: ( Sum (Len J) = n & P is invertible & M = (P * (block_diagonal J,(0. K))) * (P ~ ) )A2:
Len J =
<*> NAT
by CARD_1:47, FINSEQ_2:113
.=
<*> REAL
;
hence
Sum (Len J) = n
by A1, RVSUM_1:102;
:: thesis: ( P is invertible & M = (P * (block_diagonal J,(0. K))) * (P ~ ) )reconsider B =
block_diagonal J,
(0. K) as
Matrix of
n,
K by A2, A1, RVSUM_1:102;
(
Det P = 1_ K &
1_ K <> 0. K )
by A1, MATRIXR2:41;
hence
P is
invertible
by LAPLACE:34;
:: thesis: M = (P * (block_diagonal J,(0. K))) * (P ~ )
M = (P * B) * (P ~ )
by A1, MATRIX_1:36;
hence
M = (P * (block_diagonal J,(0. K))) * (P ~ )
;
:: thesis: verum end; suppose A3:
n > 0
;
:: thesis: ex J being non-empty FinSequence_of_Jordan_block of K ex P being Matrix of n,K st
( Sum (Len J) = n & P is invertible & M = (P * (block_diagonal J,(0. K))) * (P ~ ) )set V =
n -VectSp_over K;
consider B being
OrdBasis of
n -VectSp_over K;
A4:
len B =
dim (n -VectSp_over K)
by MATRLIN2:21
.=
n
by MATRIX13:112
;
then reconsider M' =
M as
Matrix of
len B,
K ;
set T =
Mx2Tran M',
B,
B;
dim (n -VectSp_over K) = n
by MATRIX13:112;
then
not
n -VectSp_over K is
trivial
by A3, MATRLIN2:42;
then consider J being
non-empty FinSequence_of_Jordan_block of
K,
b1 being
OrdBasis of
n -VectSp_over K such that A5:
AutMt (Mx2Tran M',B,B),
b1,
b1 = block_diagonal J,
(0. K)
and
for
L being
Scalar of
K holds
(
L is
eigenvalue of
Mx2Tran M',
B,
B iff ex
i being
Nat st
(
i in dom J &
J . i = Jordan_block L,
(len (J . i)) ) )
by Th31;
A6:
len b1 =
dim (n -VectSp_over K)
by MATRLIN2:21
.=
n
by MATRIX13:112
;
reconsider P =
AutEqMt (id (n -VectSp_over K)),
B,
b1 as
Matrix of
n,
K by A4;
take
J
;
:: thesis: ex P being Matrix of n,K st
( Sum (Len J) = n & P is invertible & M = (P * (block_diagonal J,(0. K))) * (P ~ ) )take
P
;
:: thesis: ( Sum (Len J) = n & P is invertible & M = (P * (block_diagonal J,(0. K))) * (P ~ ) )thus Sum (Len J) =
len (AutMt (Mx2Tran M',B,B),b1,b1)
by A5, MATRIXJ1:def 5
.=
n
by A6, MATRIX_1:def 3
;
:: thesis: ( P is invertible & M = (P * (block_diagonal J,(0. K))) * (P ~ ) )thus
P is
invertible
by A4, MATRLIN2:29;
:: thesis: M = (P * (block_diagonal J,(0. K))) * (P ~ )A7:
(
width P = n &
len (P ~ ) = n &
len (AutMt (Mx2Tran M',B,B),b1,b1) = n &
width (AutMt (Mx2Tran M',B,B),b1,b1) = n )
by A3, A6, MATRIX_1:24;
A8:
(
dom (Mx2Tran M',B,B) = [#] (n -VectSp_over K) &
rng (Mx2Tran M',B,B) c= [#] (n -VectSp_over K) )
by FUNCT_2:def 1, RELAT_1:def 19;
thus M =
AutMt (Mx2Tran M',B,B),
B,
B
by MATRLIN2:36
.=
AutMt ((Mx2Tran M',B,B) * (id (n -VectSp_over K))),
B,
B
by A8, RELAT_1:78
.=
(AutMt (id (n -VectSp_over K)),B,b1) * (AutMt (Mx2Tran M',B,B),b1,B)
by A3, A4, A6, MATRLIN:46
.=
P * (AutMt (Mx2Tran M',B,B),b1,B)
by A6, A4, MATRLIN2:def 2
.=
P * (AutMt ((id (n -VectSp_over K)) * (Mx2Tran M',B,B)),b1,B)
by A8, RELAT_1:79
.=
P * ((AutMt (Mx2Tran M',B,B),b1,b1) * (AutMt (id (n -VectSp_over K)),b1,B))
by A3, A6, A4, MATRLIN:46
.=
P * ((AutMt (Mx2Tran M',B,B),b1,b1) * (AutEqMt (id (n -VectSp_over K)),b1,B))
by A6, A4, MATRLIN2:def 2
.=
P * ((AutMt (Mx2Tran M',B,B),b1,b1) * (P ~ ))
by A4, MATRLIN2:29
.=
(P * (block_diagonal J,(0. K))) * (P ~ )
by A5, A7, MATRIX_3:35
;
:: thesis: verum end;