let n be Nat; 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; 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; 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
;
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 ~) )then reconsider P =
{} as
Matrix of
n,
K by MATRIX_0:13;
reconsider J =
{} as
FinSequence_of_Jordan_block of
K by Lm2;
reconsider J =
J as
non-empty FinSequence_of_Jordan_block of
K ;
take
J
;
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
;
( Sum (Len J) = n & P is invertible & M = (P * (block_diagonal (J,(0. K)))) * (P ~) )A2:
Len J =
<*> NAT
.=
<*> REAL
;
thus
Sum (Len J) = n
by A1, RVSUM_1:72;
( P is invertible & M = (P * (block_diagonal (J,(0. K)))) * (P ~) )A3:
1_ K <> 0. K
;
Det P = 1_ K
by A1, MATRIXR2:41;
hence
P is
invertible
by A3, LAPLACE:34;
M = (P * (block_diagonal (J,(0. K)))) * (P ~)reconsider B =
block_diagonal (
J,
(0. K)) as
Matrix of
n,
K by A1, A2, RVSUM_1:72;
M = (P * B) * (P ~)
by A1, MATRIX_0:45;
hence
M = (P * (block_diagonal (J,(0. K)))) * (P ~)
;
verum end; suppose A4:
n > 0
;
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;
set B = the
OrdBasis of
n -VectSp_over K;
A5:
len the
OrdBasis of
n -VectSp_over K =
dim (n -VectSp_over K)
by MATRLIN2:21
.=
n
by MATRIX13:112
;
then reconsider M9 =
M as
Matrix of
len the
OrdBasis of
n -VectSp_over K,
K ;
set T =
Mx2Tran (
M9, the
OrdBasis of
n -VectSp_over K, the
OrdBasis of
n -VectSp_over K);
dim (n -VectSp_over K) = n
by MATRIX13:112;
then
not
n -VectSp_over K is
trivial
by A4, MATRLIN2:42;
then consider J being
non-empty FinSequence_of_Jordan_block of
K,
b1 being
OrdBasis of
n -VectSp_over K such that A6:
AutMt (
(Mx2Tran (M9, the OrdBasis of n -VectSp_over K, the OrdBasis of n -VectSp_over K)),
b1,
b1)
= block_diagonal (
J,
(0. K))
and
for
L being
Scalar of
K holds
(
L is
eigenvalue of
Mx2Tran (
M9, the
OrdBasis of
n -VectSp_over K, the
OrdBasis of
n -VectSp_over K) iff ex
i being
Nat st
(
i in dom J &
J . i = Jordan_block (
L,
(len (J . i))) ) )
by Th31;
A7:
dom (Mx2Tran (M9, the OrdBasis of n -VectSp_over K, the OrdBasis of n -VectSp_over K)) = [#] (n -VectSp_over K)
by FUNCT_2:def 1;
reconsider P =
AutEqMt (
(id (n -VectSp_over K)), the
OrdBasis of
n -VectSp_over K,
b1) as
Matrix of
n,
K by A5;
take
J
;
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
;
( Sum (Len J) = n & P is invertible & M = (P * (block_diagonal (J,(0. K)))) * (P ~) )A8:
(
width P = n &
len (P ~) = n )
by A4, MATRIX_0:23;
A9:
rng (Mx2Tran (M9, the OrdBasis of n -VectSp_over K, the OrdBasis of n -VectSp_over K)) c= [#] (n -VectSp_over K)
by RELAT_1:def 19;
A10:
len b1 =
dim (n -VectSp_over K)
by MATRLIN2:21
.=
n
by MATRIX13:112
;
then A11:
(
len (AutMt ((Mx2Tran (M9, the OrdBasis of n -VectSp_over K, the OrdBasis of n -VectSp_over K)),b1,b1)) = n &
width (AutMt ((Mx2Tran (M9, the OrdBasis of n -VectSp_over K, the OrdBasis of n -VectSp_over K)),b1,b1)) = n )
by A4, MATRIX_0:23;
thus Sum (Len J) =
len (AutMt ((Mx2Tran (M9, the OrdBasis of n -VectSp_over K, the OrdBasis of n -VectSp_over K)),b1,b1))
by A6, MATRIXJ1:def 5
.=
n
by A10, MATRIX_0:def 2
;
( P is invertible & M = (P * (block_diagonal (J,(0. K)))) * (P ~) )thus
P is
invertible
by A5, MATRLIN2:29;
M = (P * (block_diagonal (J,(0. K)))) * (P ~)thus M =
AutMt (
(Mx2Tran (M9, the OrdBasis of n -VectSp_over K, the OrdBasis of n -VectSp_over K)), the
OrdBasis of
n -VectSp_over K, the
OrdBasis of
n -VectSp_over K)
by MATRLIN2:36
.=
AutMt (
((Mx2Tran (M9, the OrdBasis of n -VectSp_over K, the OrdBasis of n -VectSp_over K)) * (id (n -VectSp_over K))), the
OrdBasis of
n -VectSp_over K, the
OrdBasis of
n -VectSp_over K)
by A7, RELAT_1:52
.=
(AutMt ((id (n -VectSp_over K)), the OrdBasis of n -VectSp_over K,b1)) * (AutMt ((Mx2Tran (M9, the OrdBasis of n -VectSp_over K, the OrdBasis of n -VectSp_over K)),b1, the OrdBasis of n -VectSp_over K))
by A4, A5, A10, MATRLIN:41
.=
P * (AutMt ((Mx2Tran (M9, the OrdBasis of n -VectSp_over K, the OrdBasis of n -VectSp_over K)),b1, the OrdBasis of n -VectSp_over K))
by A5, A10, MATRLIN2:def 2
.=
P * (AutMt (((id (n -VectSp_over K)) * (Mx2Tran (M9, the OrdBasis of n -VectSp_over K, the OrdBasis of n -VectSp_over K))),b1, the OrdBasis of n -VectSp_over K))
by A9, RELAT_1:53
.=
P * ((AutMt ((Mx2Tran (M9, the OrdBasis of n -VectSp_over K, the OrdBasis of n -VectSp_over K)),b1,b1)) * (AutMt ((id (n -VectSp_over K)),b1, the OrdBasis of n -VectSp_over K)))
by A4, A10, MATRLIN:41
.=
P * ((AutMt ((Mx2Tran (M9, the OrdBasis of n -VectSp_over K, the OrdBasis of n -VectSp_over K)),b1,b1)) * (AutEqMt ((id (n -VectSp_over K)),b1, the OrdBasis of n -VectSp_over K)))
by A5, A10, MATRLIN2:def 2
.=
P * ((AutMt ((Mx2Tran (M9, the OrdBasis of n -VectSp_over K, the OrdBasis of n -VectSp_over K)),b1,b1)) * (P ~))
by A5, MATRLIN2:29
.=
(P * (block_diagonal (J,(0. K)))) * (P ~)
by A6, A8, A11, MATRIX_3:33
;
verum end;