:: by Karol P\c{a}k

::

:: Received July 11, 2008

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

Lm1: for x, y being set

for f being Function st f is one-to-one & x in dom f holds

rng (f +* (x,y)) = ((rng f) \ {(f . x)}) \/ {y}

proof end;

definition

let K be Field;

let L be Element of K;

let n be Nat;

ex b_{1} being Matrix of K st

( len b_{1} = n & width b_{1} = n & ( for i, j being Nat st [i,j] in Indices b_{1} holds

( ( i = j implies b_{1} * (i,j) = L ) & ( i + 1 = j implies b_{1} * (i,j) = 1_ K ) & ( i <> j & i + 1 <> j implies b_{1} * (i,j) = 0. K ) ) ) )

for b_{1}, b_{2} being Matrix of K st len b_{1} = n & width b_{1} = n & ( for i, j being Nat st [i,j] in Indices b_{1} holds

( ( i = j implies b_{1} * (i,j) = L ) & ( i + 1 = j implies b_{1} * (i,j) = 1_ K ) & ( i <> j & i + 1 <> j implies b_{1} * (i,j) = 0. K ) ) ) & len b_{2} = n & width b_{2} = n & ( for i, j being Nat st [i,j] in Indices b_{2} holds

( ( i = j implies b_{2} * (i,j) = L ) & ( i + 1 = j implies b_{2} * (i,j) = 1_ K ) & ( i <> j & i + 1 <> j implies b_{2} * (i,j) = 0. K ) ) ) holds

b_{1} = b_{2}

end;
let L be Element of K;

let n be Nat;

func Jordan_block (L,n) -> Matrix of K means :Def1: :: MATRIXJ2:def 1

( len it = n & width it = n & ( for i, j being Nat st [i,j] in Indices it holds

( ( i = j implies it * (i,j) = L ) & ( i + 1 = j implies it * (i,j) = 1_ K ) & ( i <> j & i + 1 <> j implies it * (i,j) = 0. K ) ) ) );

existence ( len it = n & width it = n & ( for i, j being Nat st [i,j] in Indices it holds

( ( i = j implies it * (i,j) = L ) & ( i + 1 = j implies it * (i,j) = 1_ K ) & ( i <> j & i + 1 <> j implies it * (i,j) = 0. K ) ) ) );

ex b

( len b

( ( i = j implies b

proof end;

uniqueness for b

( ( i = j implies b

( ( i = j implies b

b

proof end;

:: deftheorem Def1 defines Jordan_block MATRIXJ2:def 1 :

for K being Field

for L being Element of K

for n being Nat

for b_{4} being Matrix of K holds

( b_{4} = Jordan_block (L,n) iff ( len b_{4} = n & width b_{4} = n & ( for i, j being Nat st [i,j] in Indices b_{4} holds

( ( i = j implies b_{4} * (i,j) = L ) & ( i + 1 = j implies b_{4} * (i,j) = 1_ K ) & ( i <> j & i + 1 <> j implies b_{4} * (i,j) = 0. K ) ) ) ) );

for K being Field

for L being Element of K

for n being Nat

for b

( b

( ( i = j implies b

definition

let K be Field;

let L be Element of K;

let n be Nat;

:: original: Jordan_block

redefine func Jordan_block (L,n) -> upper_triangular Matrix of n,K;

coherence

Jordan_block (L,n) is upper_triangular Matrix of n,K

end;
let L be Element of K;

let n be Nat;

:: original: Jordan_block

redefine func Jordan_block (L,n) -> upper_triangular Matrix of n,K;

coherence

Jordan_block (L,n) is upper_triangular Matrix of n,K

proof end;

theorem Th1: :: MATRIXJ2:1

for n being Nat

for K being Field

for L being Element of K holds diagonal_of_Matrix (Jordan_block (L,n)) = n |-> L

for K being Field

for L being Element of K holds diagonal_of_Matrix (Jordan_block (L,n)) = n |-> L

proof end;

theorem Th2: :: MATRIXJ2:2

for n being Nat

for K being Field

for L being Element of K holds Det (Jordan_block (L,n)) = (power K) . (L,n)

for K being Field

for L being Element of K holds Det (Jordan_block (L,n)) = (power K) . (L,n)

proof end;

theorem Th3: :: MATRIXJ2:3

for n being Nat

for K being Field

for L being Element of K holds

( Jordan_block (L,n) is invertible iff ( n = 0 or L <> 0. K ) )

for K being Field

for L being Element of K holds

( Jordan_block (L,n) is invertible iff ( n = 0 or L <> 0. K ) )

proof end;

theorem Th4: :: MATRIXJ2:4

for i, n being Nat

for K being Field

for L being Element of K st i in Seg n & i <> n holds

Line ((Jordan_block (L,n)),i) = (L * (Line ((1. (K,n)),i))) + (Line ((1. (K,n)),(i + 1)))

for K being Field

for L being Element of K st i in Seg n & i <> n holds

Line ((Jordan_block (L,n)),i) = (L * (Line ((1. (K,n)),i))) + (Line ((1. (K,n)),(i + 1)))

proof end;

theorem Th5: :: MATRIXJ2:5

for n being Nat

for K being Field

for L being Element of K holds Line ((Jordan_block (L,n)),n) = L * (Line ((1. (K,n)),n))

for K being Field

for L being Element of K holds Line ((Jordan_block (L,n)),n) = L * (Line ((1. (K,n)),n))

proof end;

theorem Th6: :: MATRIXJ2:6

for i, n being Nat

for K being Field

for L being Element of K

for F being Element of n -tuples_on the carrier of K st i in Seg n holds

( ( i <> n implies (Line ((Jordan_block (L,n)),i)) "*" F = (L * (F /. i)) + (F /. (i + 1)) ) & ( i = n implies (Line ((Jordan_block (L,n)),i)) "*" F = L * (F /. i) ) )

for K being Field

for L being Element of K

for F being Element of n -tuples_on the carrier of K st i in Seg n holds

( ( i <> n implies (Line ((Jordan_block (L,n)),i)) "*" F = (L * (F /. i)) + (F /. (i + 1)) ) & ( i = n implies (Line ((Jordan_block (L,n)),i)) "*" F = L * (F /. i) ) )

proof end;

theorem Th7: :: MATRIXJ2:7

for i, n being Nat

for K being Field

for L being Element of K

for F being Element of n -tuples_on the carrier of K st i in Seg n holds

( ( i = 1 implies (Col ((Jordan_block (L,n)),i)) "*" F = L * (F /. i) ) & ( i <> 1 implies (Col ((Jordan_block (L,n)),i)) "*" F = (L * (F /. i)) + (F /. (i - 1)) ) )

for K being Field

for L being Element of K

for F being Element of n -tuples_on the carrier of K st i in Seg n holds

( ( i = 1 implies (Col ((Jordan_block (L,n)),i)) "*" F = L * (F /. i) ) & ( i <> 1 implies (Col ((Jordan_block (L,n)),i)) "*" F = (L * (F /. i)) + (F /. (i - 1)) ) )

proof end;

theorem :: MATRIXJ2:8

for n being Nat

for K being Field

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

ex M being Matrix of n,K st

( (Jordan_block (L,n)) ~ = M & ( for i, j being Nat st [i,j] in Indices M holds

( ( i > j implies M * (i,j) = 0. K ) & ( i <= j implies M * (i,j) = - ((power K) . ((- (L ")),((j -' i) + 1))) ) ) ) )

for K being Field

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

ex M being Matrix of n,K st

( (Jordan_block (L,n)) ~ = M & ( for i, j being Nat st [i,j] in Indices M holds

( ( i > j implies M * (i,j) = 0. K ) & ( i <= j implies M * (i,j) = - ((power K) . ((- (L ")),((j -' i) + 1))) ) ) ) )

proof end;

theorem Th9: :: MATRIXJ2:9

for n being Nat

for K being Field

for a, L being Element of K holds (Jordan_block (L,n)) + (a * (1. (K,n))) = Jordan_block ((L + a),n)

for K being Field

for a, L being Element of K holds (Jordan_block (L,n)) + (a * (1. (K,n))) = Jordan_block ((L + a),n)

proof end;

definition

let K be Field;

let G be FinSequence of ( the carrier of K *) * ;

end;
let G be FinSequence of ( the carrier of K *) * ;

attr G is Jordan-block-yielding means :Def2: :: MATRIXJ2:def 2

for i being Nat st i in dom G holds

ex L being Element of K ex n being Nat st G . i = Jordan_block (L,n);

for i being Nat st i in dom G holds

ex L being Element of K ex n being Nat st G . i = Jordan_block (L,n);

:: deftheorem Def2 defines Jordan-block-yielding MATRIXJ2:def 2 :

for K being Field

for G being FinSequence of ( the carrier of K *) * holds

( G is Jordan-block-yielding iff for i being Nat st i in dom G holds

ex L being Element of K ex n being Nat st G . i = Jordan_block (L,n) );

for K being Field

for G being FinSequence of ( the carrier of K *) * holds

( G is Jordan-block-yielding iff for i being Nat st i in dom G holds

ex L being Element of K ex n being Nat st G . i = Jordan_block (L,n) );

registration

let K be Field;

ex b_{1} being FinSequence of ( the carrier of K *) * st b_{1} is Jordan-block-yielding

end;
cluster Relation-like NAT -defined ( the carrier of K *) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V186() Jordan-block-yielding for FinSequence of ( the carrier of K *) * ;

existence ex b

proof end;

registration

let K be Field;

for b_{1} being FinSequence of ( the carrier of K *) * st b_{1} is Jordan-block-yielding holds

b_{1} is Square-Matrix-yielding

end;
cluster Jordan-block-yielding -> Square-Matrix-yielding for FinSequence of ( the carrier of K *) * ;

coherence for b

b

proof end;

definition

let K be Field;

mode FinSequence_of_Jordan_block of K is Jordan-block-yielding FinSequence of ( the carrier of K *) * ;

end;
mode FinSequence_of_Jordan_block of K is Jordan-block-yielding FinSequence of ( the carrier of K *) * ;

Lm2: for K being Field holds {} is FinSequence_of_Jordan_block of K

proof end;

definition

let K be Field;

let L be Element of K;

ex b_{1} being FinSequence_of_Jordan_block of K st

for i being Nat st i in dom b_{1} holds

ex n being Nat st b_{1} . i = Jordan_block (L,n)

end;
let L be Element of K;

mode FinSequence_of_Jordan_block of L,K -> FinSequence_of_Jordan_block of K means :Def3: :: MATRIXJ2:def 3

for i being Nat st i in dom it holds

ex n being Nat st it . i = Jordan_block (L,n);

existence for i being Nat st i in dom it holds

ex n being Nat st it . i = Jordan_block (L,n);

ex b

for i being Nat st i in dom b

ex n being Nat st b

proof end;

:: deftheorem Def3 defines FinSequence_of_Jordan_block MATRIXJ2:def 3 :

for K being Field

for L being Element of K

for b_{3} being FinSequence_of_Jordan_block of K holds

( b_{3} is FinSequence_of_Jordan_block of L,K iff for i being Nat st i in dom b_{3} holds

ex n being Nat st b_{3} . i = Jordan_block (L,n) );

for K being Field

for L being Element of K

for b

( b

ex n being Nat st b

theorem Th11: :: MATRIXJ2:11

for n being Nat

for K being Field

for L being Element of K holds <*(Jordan_block (L,n))*> is FinSequence_of_Jordan_block of L,K

for K being Field

for L being Element of K holds <*(Jordan_block (L,n))*> is FinSequence_of_Jordan_block of L,K

proof end;

registration

let K be Field;

let L be Element of K;

ex b_{1} being FinSequence_of_Jordan_block of L,K st b_{1} is non-empty

end;
let L be Element of K;

cluster Relation-like non-empty NAT -defined ( the carrier of K *) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V186() Matrix-yielding Square-Matrix-yielding Jordan-block-yielding for FinSequence_of_Jordan_block of L,K;

existence ex b

proof end;

registration

let K be Field;

ex b_{1} being FinSequence_of_Jordan_block of K st b_{1} is non-empty

end;
cluster Relation-like non-empty NAT -defined ( the carrier of K *) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V186() Matrix-yielding Square-Matrix-yielding Jordan-block-yielding for FinSequence of ( the carrier of K *) * ;

existence ex b

proof end;

theorem Th12: :: MATRIXJ2:12

for K being Field

for a, L being Element of K

for J being FinSequence_of_Jordan_block of L,K holds J (+) (mlt (((len J) |-> a),(1. (K,(Len J))))) is FinSequence_of_Jordan_block of L + a,K

for a, L being Element of K

for J being FinSequence_of_Jordan_block of L,K holds J (+) (mlt (((len J) |-> a),(1. (K,(Len J))))) is FinSequence_of_Jordan_block of L + a,K

proof end;

definition

let K be Field;

let J1, J2 be FinSequence_of_Jordan_block of K;

:: original: ^

redefine func J1 ^ J2 -> FinSequence_of_Jordan_block of K;

coherence

J1 ^ J2 is FinSequence_of_Jordan_block of K

end;
let J1, J2 be FinSequence_of_Jordan_block of K;

:: original: ^

redefine func J1 ^ J2 -> FinSequence_of_Jordan_block of K;

coherence

J1 ^ J2 is FinSequence_of_Jordan_block of K

proof end;

definition

let K be Field;

let n be Nat;

let J be FinSequence_of_Jordan_block of K;

:: original: |

redefine func J | n -> FinSequence_of_Jordan_block of K;

coherence

J | n is FinSequence_of_Jordan_block of K

redefine func J /^ n -> FinSequence_of_Jordan_block of K;

coherence

J /^ n is FinSequence_of_Jordan_block of K

end;
let n be Nat;

let J be FinSequence_of_Jordan_block of K;

:: original: |

redefine func J | n -> FinSequence_of_Jordan_block of K;

coherence

J | n is FinSequence_of_Jordan_block of K

proof end;

:: original: /^redefine func J /^ n -> FinSequence_of_Jordan_block of K;

coherence

J /^ n is FinSequence_of_Jordan_block of K

proof end;

definition

let K be Field;

let L be Element of K;

let J1, J2 be FinSequence_of_Jordan_block of L,K;

:: original: ^

redefine func J1 ^ J2 -> FinSequence_of_Jordan_block of L,K;

coherence

J1 ^ J2 is FinSequence_of_Jordan_block of L,K

end;
let L be Element of K;

let J1, J2 be FinSequence_of_Jordan_block of L,K;

:: original: ^

redefine func J1 ^ J2 -> FinSequence_of_Jordan_block of L,K;

coherence

J1 ^ J2 is FinSequence_of_Jordan_block of L,K

proof end;

definition

let K be Field;

let L be Element of K;

let n be Nat;

let J be FinSequence_of_Jordan_block of L,K;

:: original: |

redefine func J | n -> FinSequence_of_Jordan_block of L,K;

coherence

J | n is FinSequence_of_Jordan_block of L,K

redefine func J /^ n -> FinSequence_of_Jordan_block of L,K;

coherence

J /^ n is FinSequence_of_Jordan_block of L,K

end;
let L be Element of K;

let n be Nat;

let J be FinSequence_of_Jordan_block of L,K;

:: original: |

redefine func J | n -> FinSequence_of_Jordan_block of L,K;

coherence

J | n is FinSequence_of_Jordan_block of L,K

proof end;

:: original: /^redefine func J /^ n -> FinSequence_of_Jordan_block of L,K;

coherence

J /^ n is FinSequence_of_Jordan_block of L,K

proof end;

definition
end;

:: deftheorem Def4 defines nilpotent MATRIXJ2:def 4 :

for K being doubleLoopStr

for V being non empty ModuleStr over K

for f being Function of V,V holds

( f is nilpotent iff ex n being Nat st

for v being Vector of V holds (f |^ n) . v = 0. V );

for K being doubleLoopStr

for V being non empty ModuleStr over K

for f being Function of V,V holds

( f is nilpotent iff ex n being Nat st

for v being Vector of V holds (f |^ n) . v = 0. V );

theorem Th13: :: MATRIXJ2:13

for K being doubleLoopStr

for V being non empty ModuleStr over K

for f being Function of V,V holds

( f is nilpotent iff ex n being Nat st f |^ n = ZeroMap (V,V) )

for V being non empty ModuleStr over K

for f being Function of V,V holds

( f is nilpotent iff ex n being Nat st f |^ n = ZeroMap (V,V) )

proof end;

registration

let K be doubleLoopStr ;

let V be non empty ModuleStr over K;

ex b_{1} being Function of V,V st b_{1} is nilpotent

end;
let V be non empty ModuleStr over K;

cluster Relation-like the carrier of V -defined the carrier of V -valued Function-like non empty total V18( the carrier of V, the carrier of V) nilpotent for Element of bool [: the carrier of V, the carrier of V:];

existence ex b

proof end;

registration

let R be Ring;

let V be LeftMod of R;

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

( b_{1} is nilpotent & b_{1} is additive & b_{1} is homogeneous )

end;
let V be LeftMod of R;

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

existence ex b

( b

proof end;

theorem Th14: :: MATRIXJ2:14

for n being Nat

for K being Field

for V being VectSp of K

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

for K being Field

for V being VectSp of K

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

proof end;

definition

let K be doubleLoopStr ;

let V be non empty ModuleStr over K;

let f be nilpotent Function of V,V;

ex b_{1} being Nat st

( f |^ b_{1} = ZeroMap (V,V) & ( for k being Nat st f |^ k = ZeroMap (V,V) holds

b_{1} <= k ) )

for b_{1}, b_{2} being Nat st f |^ b_{1} = ZeroMap (V,V) & ( for k being Nat st f |^ k = ZeroMap (V,V) holds

b_{1} <= k ) & f |^ b_{2} = ZeroMap (V,V) & ( for k being Nat st f |^ k = ZeroMap (V,V) holds

b_{2} <= k ) holds

b_{1} = b_{2}

end;
let V be non empty ModuleStr over K;

let f be nilpotent Function of V,V;

func degree_of_nilpotent f -> Nat means :Def5: :: MATRIXJ2:def 5

( f |^ it = ZeroMap (V,V) & ( for k being Nat st f |^ k = ZeroMap (V,V) holds

it <= k ) );

existence ( f |^ it = ZeroMap (V,V) & ( for k being Nat st f |^ k = ZeroMap (V,V) holds

it <= k ) );

ex b

( f |^ b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def5 defines degree_of_nilpotent MATRIXJ2:def 5 :

for K being doubleLoopStr

for V being non empty ModuleStr over K

for f being nilpotent Function of V,V

for b_{4} being Nat holds

( b_{4} = degree_of_nilpotent f iff ( f |^ b_{4} = ZeroMap (V,V) & ( for k being Nat st f |^ k = ZeroMap (V,V) holds

b_{4} <= k ) ) );

for K being doubleLoopStr

for V being non empty ModuleStr over K

for f being nilpotent Function of V,V

for b

( b

b

notation

let K be doubleLoopStr ;

let V be non empty ModuleStr over K;

let f be nilpotent Function of V,V;

synonym deg f for degree_of_nilpotent f;

end;
let V be non empty ModuleStr over K;

let f be nilpotent Function of V,V;

synonym deg f for degree_of_nilpotent f;

theorem Th15: :: MATRIXJ2:15

for K being doubleLoopStr

for V being non empty ModuleStr over K

for f being nilpotent Function of V,V holds

( deg f = 0 iff [#] V = {(0. V)} )

for V being non empty ModuleStr over K

for f being nilpotent Function of V,V holds

( deg f = 0 iff [#] V = {(0. V)} )

proof end;

theorem Th16: :: MATRIXJ2:16

for K being doubleLoopStr

for V being non empty ModuleStr over K

for f being nilpotent Function of V,V ex v being Vector of V st

for i being Nat st i < deg f holds

(f |^ i) . v <> 0. V

for V being non empty ModuleStr over K

for f being nilpotent Function of V,V ex v being Vector of V st

for i being Nat st i < deg f holds

(f |^ i) . v <> 0. V

proof end;

theorem Th17: :: MATRIXJ2:17

for K being Field

for V being VectSp of K

for W being Subspace of V

for f being nilpotent Function of V,V st f | W is Function of W,W holds

f | W is nilpotent Function of W,W

for V being VectSp of K

for W being Subspace of V

for f being nilpotent Function of V,V st f | W is Function of W,W holds

f | W is nilpotent Function of W,W

proof end;

theorem Th18: :: MATRIXJ2:18

for n being Nat

for K being Field

for V being VectSp of K

for W being Subspace of V

for f being nilpotent linear-transformation of V,V

for fI being nilpotent Function of (im (f |^ n)),(im (f |^ n)) st fI = f | (im (f |^ n)) & n <= deg f holds

(deg fI) + n = deg f

for K being Field

for V being VectSp of K

for W being Subspace of V

for f being nilpotent linear-transformation of V,V

for fI being nilpotent Function of (im (f |^ n)),(im (f |^ n)) st fI = f | (im (f |^ n)) & n <= deg f holds

(deg fI) + n = deg f

proof end;

theorem Th19: :: MATRIXJ2:19

for i being Nat

for K being Field

for V1, V2 being finite-dimensional VectSp of K

for W1, W2 being Subspace of V1

for U1, U2 being Subspace of V2

for b1 being OrdBasis of V1

for B2 being FinSequence of V2

for bw1 being OrdBasis of W1

for bw2 being OrdBasis of W2

for Bu1 being FinSequence of U1

for Bu2 being FinSequence of U2

for M being Matrix of len b1, len B2,K

for M1 being Matrix of len bw1, len Bu1,K

for M2 being Matrix of len bw2, len Bu2,K st b1 = bw1 ^ bw2 & B2 = Bu1 ^ Bu2 & M = block_diagonal (<*M1,M2*>,(0. K)) & width M1 = len Bu1 & width M2 = len Bu2 holds

( ( i in dom bw1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (Mx2Tran (M1,bw1,Bu1)) . (bw1 /. i) ) & ( i in dom bw2 implies (Mx2Tran (M,b1,B2)) . (b1 /. (i + (len bw1))) = (Mx2Tran (M2,bw2,Bu2)) . (bw2 /. i) ) )

for K being Field

for V1, V2 being finite-dimensional VectSp of K

for W1, W2 being Subspace of V1

for U1, U2 being Subspace of V2

for b1 being OrdBasis of V1

for B2 being FinSequence of V2

for bw1 being OrdBasis of W1

for bw2 being OrdBasis of W2

for Bu1 being FinSequence of U1

for Bu2 being FinSequence of U2

for M being Matrix of len b1, len B2,K

for M1 being Matrix of len bw1, len Bu1,K

for M2 being Matrix of len bw2, len Bu2,K st b1 = bw1 ^ bw2 & B2 = Bu1 ^ Bu2 & M = block_diagonal (<*M1,M2*>,(0. K)) & width M1 = len Bu1 & width M2 = len Bu2 holds

( ( i in dom bw1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (Mx2Tran (M1,bw1,Bu1)) . (bw1 /. i) ) & ( i in dom bw2 implies (Mx2Tran (M,b1,B2)) . (b1 /. (i + (len bw1))) = (Mx2Tran (M2,bw2,Bu2)) . (bw2 /. i) ) )

proof end;

theorem Th20: :: MATRIXJ2:20

for K being Field

for V1, V2 being finite-dimensional VectSp of K

for b1 being OrdBasis of V1

for B2 being FinSequence of V2

for M being Matrix of len b1, len B2,K

for F being FinSequence_of_Matrix of K st M = block_diagonal (F,(0. K)) holds

for i, m being Nat st i in dom b1 & m = min ((Len F),i) holds

( (Mx2Tran (M,b1,B2)) . (b1 /. i) = Sum (lmlt ((Line ((F . m),(i -' (Sum (Len (F | (m -' 1))))))),((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))))) & len ((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))) = width (F . m) )

for V1, V2 being finite-dimensional VectSp of K

for b1 being OrdBasis of V1

for B2 being FinSequence of V2

for M being Matrix of len b1, len B2,K

for F being FinSequence_of_Matrix of K st M = block_diagonal (F,(0. K)) holds

for i, m being Nat st i in dom b1 & m = min ((Len F),i) holds

( (Mx2Tran (M,b1,B2)) . (b1 /. i) = Sum (lmlt ((Line ((F . m),(i -' (Sum (Len (F | (m -' 1))))))),((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))))) & len ((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))) = width (F . m) )

proof end;

theorem Th21: :: MATRIXJ2:21

for K being Field

for L being Element of K

for V1 being finite-dimensional VectSp of K

for B1 being FinSequence of V1 st len B1 in dom B1 holds

Sum (lmlt ((Line ((Jordan_block (L,(len B1))),(len B1))),B1)) = L * (B1 /. (len B1))

for L being Element of K

for V1 being finite-dimensional VectSp of K

for B1 being FinSequence of V1 st len B1 in dom B1 holds

Sum (lmlt ((Line ((Jordan_block (L,(len B1))),(len B1))),B1)) = L * (B1 /. (len B1))

proof end;

theorem Th22: :: MATRIXJ2:22

for i being Nat

for K being Field

for L being Element of K

for V1 being finite-dimensional VectSp of K

for B1 being FinSequence of V1 st i in dom B1 & i <> len B1 holds

Sum (lmlt ((Line ((Jordan_block (L,(len B1))),i)),B1)) = (L * (B1 /. i)) + (B1 /. (i + 1))

for K being Field

for L being Element of K

for V1 being finite-dimensional VectSp of K

for B1 being FinSequence of V1 st i in dom B1 & i <> len B1 holds

Sum (lmlt ((Line ((Jordan_block (L,(len B1))),i)),B1)) = (L * (B1 /. i)) + (B1 /. (i + 1))

proof end;

theorem Th23: :: MATRIXJ2:23

for n being Nat

for K being Field

for L being Element of K

for V1, V2 being finite-dimensional VectSp of K

for b1 being OrdBasis of V1

for B2 being FinSequence of V2

for M being Matrix of len b1, len B2,K st M = Jordan_block (L,n) holds

for i being Nat st i in dom b1 holds

( ( i = len b1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = L * (B2 /. i) ) & ( i <> len b1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) )

for K being Field

for L being Element of K

for V1, V2 being finite-dimensional VectSp of K

for b1 being OrdBasis of V1

for B2 being FinSequence of V2

for M being Matrix of len b1, len B2,K st M = Jordan_block (L,n) holds

for i being Nat st i in dom b1 holds

( ( i = len b1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = L * (B2 /. i) ) & ( i <> len b1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) )

proof end;

theorem Th24: :: MATRIXJ2:24

for K being Field

for L being Element of K

for V1, V2 being finite-dimensional VectSp of K

for b1 being OrdBasis of V1

for B2 being FinSequence of V2

for J being FinSequence_of_Jordan_block of L,K

for M being Matrix of len b1, len B2,K st M = block_diagonal (J,(0. K)) holds

for i, m being Nat st i in dom b1 & m = min ((Len J),i) holds

( ( i = Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = L * (B2 /. i) ) & ( i <> Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) )

for L being Element of K

for V1, V2 being finite-dimensional VectSp of K

for b1 being OrdBasis of V1

for B2 being FinSequence of V2

for J being FinSequence_of_Jordan_block of L,K

for M being Matrix of len b1, len B2,K st M = block_diagonal (J,(0. K)) holds

for i, m being Nat st i in dom b1 & m = min ((Len J),i) holds

( ( i = Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = L * (B2 /. i) ) & ( i <> Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) )

proof end;

theorem Th25: :: MATRIXJ2:25

for K being Field

for V1 being finite-dimensional VectSp of K

for b1 being OrdBasis of V1

for J being FinSequence_of_Jordan_block of 0. K,K

for M being Matrix of len b1, len b1,K st M = block_diagonal (J,(0. K)) holds

for m being Nat st ( for i being Nat st i in dom J holds

len (J . i) <= m ) holds

(Mx2Tran (M,b1,b1)) |^ m = ZeroMap (V1,V1)

for V1 being finite-dimensional VectSp of K

for b1 being OrdBasis of V1

for J being FinSequence_of_Jordan_block of 0. K,K

for M being Matrix of len b1, len b1,K st M = block_diagonal (J,(0. K)) holds

for m being Nat st ( for i being Nat st i in dom J holds

len (J . i) <= m ) holds

(Mx2Tran (M,b1,b1)) |^ m = ZeroMap (V1,V1)

proof end;

Lm3: for n being Nat

for K being Field

for L being Element of K

for V1 being finite-dimensional VectSp of K

for b1 being OrdBasis of V1

for J being FinSequence_of_Jordan_block of L,K

for M being Matrix of len b1, len b1,K st M = block_diagonal (J,(0. K)) & len b1 <> 0 holds

( ((Mx2Tran (M,b1,b1)) |^ n) . (b1 /. (Sum (Len (J | (min ((Len J),(len b1))))))) = ((power K) . (L,n)) * (b1 /. (Sum (Len (J | (min ((Len J),(len b1))))))) & Sum (Len (J | (min ((Len J),(len b1))))) in dom b1 )

proof end;

theorem :: MATRIXJ2:26

for K being Field

for L being Element of K

for V1 being finite-dimensional VectSp of K

for b1 being OrdBasis of V1

for J being FinSequence_of_Jordan_block of L,K

for M being Matrix of len b1, len b1,K st M = block_diagonal (J,(0. K)) holds

( Mx2Tran (M,b1,b1) is nilpotent iff ( len b1 = 0 or L = 0. K ) )

for L being Element of K

for V1 being finite-dimensional VectSp of K

for b1 being OrdBasis of V1

for J being FinSequence_of_Jordan_block of L,K

for M being Matrix of len b1, len b1,K st M = block_diagonal (J,(0. K)) holds

( Mx2Tran (M,b1,b1) is nilpotent iff ( len b1 = 0 or L = 0. K ) )

proof end;

theorem :: MATRIXJ2:27

for K being Field

for V1 being finite-dimensional VectSp of K

for b1 being OrdBasis of V1

for J being FinSequence_of_Jordan_block of 0. K,K

for M being Matrix of len b1, len b1,K st M = block_diagonal (J,(0. K)) & len b1 > 0 holds

for F being nilpotent Function of V1,V1 st F = Mx2Tran (M,b1,b1) holds

( ex i being Nat st

( i in dom J & len (J . i) = deg F ) & ( for i being Nat st i in dom J holds

len (J . i) <= deg F ) )

for V1 being finite-dimensional VectSp of K

for b1 being OrdBasis of V1

for J being FinSequence_of_Jordan_block of 0. K,K

for M being Matrix of len b1, len b1,K st M = block_diagonal (J,(0. K)) & len b1 > 0 holds

for F being nilpotent Function of V1,V1 st F = Mx2Tran (M,b1,b1) holds

( ex i being Nat st

( i in dom J & len (J . i) = deg F ) & ( for i being Nat st i in dom J holds

len (J . i) <= deg F ) )

proof end;

Lm4: 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;

theorem Th28: :: MATRIXJ2:28

for K being Field

for V1, V2 being finite-dimensional VectSp of K

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2

for L being Element of K st len b1 = len b2 holds

for F being linear-transformation of V1,V2 st ( for i being Nat holds

( not i in dom b1 or F . (b1 /. i) = L * (b2 /. i) or ( i + 1 in dom b1 & F . (b1 /. i) = (L * (b2 /. i)) + (b2 /. (i + 1)) ) ) ) holds

ex J being non-empty FinSequence_of_Jordan_block of L,K st AutMt (F,b1,b2) = block_diagonal (J,(0. K))

for V1, V2 being finite-dimensional VectSp of K

for b1 being OrdBasis of V1

for b2 being OrdBasis of V2

for L being Element of K st len b1 = len b2 holds

for F being linear-transformation of V1,V2 st ( for i being Nat holds

( not i in dom b1 or F . (b1 /. i) = L * (b2 /. i) or ( i + 1 in dom b1 & F . (b1 /. i) = (L * (b2 /. i)) + (b2 /. (i + 1)) ) ) ) holds

ex J being non-empty FinSequence_of_Jordan_block of L,K st AutMt (F,b1,b2) = block_diagonal (J,(0. K))

proof end;

theorem Th29: :: MATRIXJ2:29

for K being Field

for V1 being finite-dimensional VectSp of K

for F being nilpotent linear-transformation of V1,V1 ex J being non-empty FinSequence_of_Jordan_block of 0. K,K ex b1 being OrdBasis of V1 st AutMt (F,b1,b1) = block_diagonal (J,(0. K))

for V1 being finite-dimensional VectSp of K

for F being nilpotent linear-transformation of V1,V1 ex J being non-empty FinSequence_of_Jordan_block of 0. K,K ex b1 being OrdBasis of V1 st AutMt (F,b1,b1) = block_diagonal (J,(0. K))

proof end;

theorem Th30: :: MATRIXJ2:30

for n being Nat

for K being Field

for L being Element of K

for V being VectSp of K

for F being linear-transformation of V,V

for V1 being finite-dimensional Subspace of V

for F1 being linear-transformation of V1,V1 st V1 = ker ((F + ((- L) * (id V))) |^ n) & F | V1 = F1 holds

ex J being non-empty FinSequence_of_Jordan_block of L,K ex b1 being OrdBasis of V1 st AutMt (F1,b1,b1) = block_diagonal (J,(0. K))

for K being Field

for L being Element of K

for V being VectSp of K

for F being linear-transformation of V,V

for V1 being finite-dimensional Subspace of V

for F1 being linear-transformation of V1,V1 st V1 = ker ((F + ((- L) * (id V))) |^ n) & F | V1 = F1 holds

ex J being non-empty FinSequence_of_Jordan_block of L,K ex b1 being OrdBasis of V1 st AutMt (F1,b1,b1) = block_diagonal (J,(0. K))

proof end;

theorem Th31: :: MATRIXJ2:31

for K being 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))) ) ) ) )

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))) ) ) ) )

proof end;

:: Jordan Matrix Decomposition Theorem

theorem :: MATRIXJ2:32

for n being 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 ~) )

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 ~) )

proof end;