let K be Field; :: thesis: 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)
defpred S1[ Nat] means for V1 being finite-dimensional VectSp of K
for F being nilpotent linear-transformation of V1,V1 st deg F = $1 holds
ex J being 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 i being Nat st i in dom J holds
(Len J) . i <> 0 ) );
A1:
S1[ 0 ]
proof
let V1 be
finite-dimensional VectSp of
K;
:: thesis: for F being nilpotent linear-transformation of V1,V1 st deg F = 0 holds
ex J being 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 i being Nat st i in dom J holds
(Len J) . i <> 0 ) )let F be
nilpotent linear-transformation of
V1,
V1;
:: thesis: ( deg F = 0 implies ex J being 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 i being Nat st i in dom J holds
(Len J) . i <> 0 ) ) )
assume A2:
deg F = 0
;
:: thesis: ex J being 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 i being Nat st i in dom J holds
(Len J) . i <> 0 ) )
reconsider J =
{} as
FinSequence_of_Jordan_block of
0. K,
K by Th10;
consider b1 being
OrdBasis of
V1;
take
J
;
:: thesis: ex b1 being OrdBasis of V1 st
( AutMt F,b1,b1 = block_diagonal J,(0. K) & ( for i being Nat st i in dom J holds
(Len J) . i <> 0 ) )
take
b1
;
:: thesis: ( AutMt F,b1,b1 = block_diagonal J,(0. K) & ( for i being Nat st i in dom J holds
(Len J) . i <> 0 ) )
[#] V1 =
{(0. V1)}
by A2, Th15
.=
the
carrier of
((0). V1)
by VECTSP_4:def 3
;
then
(0). V1 = (Omega). V1
by VECTSP_4:37;
then 0 =
dim V1
by VECTSP_9:33
.=
len b1
by MATRLIN2:21
.=
len (AutMt F,b1,b1)
by MATRIX_1:def 3
;
hence AutMt F,
b1,
b1 =
{}
.=
block_diagonal J,
(0. K)
by MATRIXJ1:22
;
:: thesis: for i being Nat st i in dom J holds
(Len J) . i <> 0
thus
for
i being
Nat st
i in dom J holds
(Len J) . i <> 0
;
:: thesis: verum
end;
A3:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
:: thesis: ( S1[n] implies S1[n + 1] )
assume A4:
S1[
n]
;
:: thesis: S1[n + 1]
set n1 =
n + 1;
let V1 be
finite-dimensional VectSp of
K;
:: thesis: for F being nilpotent linear-transformation of V1,V1 st deg F = n + 1 holds
ex J being 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 i being Nat st i in dom J holds
(Len J) . i <> 0 ) )let F be
nilpotent linear-transformation of
V1,
V1;
:: thesis: ( deg F = n + 1 implies ex J being 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 i being Nat st i in dom J holds
(Len J) . i <> 0 ) ) )
assume A5:
deg F = n + 1
;
:: thesis: ex J being 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 i being Nat st i in dom J holds
(Len J) . i <> 0 ) )
set IM =
im (F |^ 1);
reconsider FI =
F | (im (F |^ 1)) as
linear-transformation of
(im (F |^ 1)),
(im (F |^ 1)) by VECTSP11:32;
reconsider FI =
FI as
nilpotent linear-transformation of
(im (F |^ 1)),
(im (F |^ 1)) by Th17;
(deg FI) + 1
= n + 1
by A5, Th18, NAT_1:11;
then consider J being
FinSequence_of_Jordan_block of
0. K,
K,
b1 being
OrdBasis of
im (F |^ 1) such that A6:
AutMt FI,
b1,
b1 = block_diagonal J,
(0. K)
and A7:
for
i being
Nat st
i in dom J holds
(Len J) . i <> 0
by A4;
A8:
FI = Mx2Tran (AutMt FI,b1,b1),
b1,
b1
by MATRLIN2:34;
A9:
len b1 =
len (AutMt FI,b1,b1)
by MATRIX_1:def 3
.=
Sum (Len J)
by A6, MATRIXJ1:def 5
;
then A10:
dom b1 = Seg (Sum (Len J))
by FINSEQ_1:def 3;
set LJ =
Len J;
set S =
Sum (Len J);
set L =
len J;
defpred S2[
Nat,
Nat]
means ( $2
in dom (Len J) & $2
<= $1 &
Sum ((Len J) | ($2 -' 1)) <= $1
-' $2 );
defpred S3[
set ,
set ]
means for
i,
k being
Nat st
i = $1 &
k = $2 holds
(
S2[
i,
k] &
i -' k <= Sum ((Len J) | k) & ( for
n being
Nat st
S2[
i,
n] holds
n <= k ) );
A11:
for
x being
set st
x in Seg ((Sum (Len J)) + (len J)) holds
ex
y being
set st
(
y in NAT &
S3[
x,
y] )
proof
let x be
set ;
:: thesis: ( x in Seg ((Sum (Len J)) + (len J)) implies ex y being set st
( y in NAT & S3[x,y] ) )
assume A12:
x in Seg ((Sum (Len J)) + (len J))
;
:: thesis: ex y being set st
( y in NAT & S3[x,y] )
reconsider i =
x as
Nat by A12;
defpred S4[
Nat]
means ( $1
in dom (Len J) & $1
<= i &
Sum ((Len J) | ($1 -' 1)) <= i -' $1 );
A13:
for
k being
Nat st
S4[
k] holds
k <= len J
( 1
-' 1
= 0 &
0 <= len (Len J) )
by XREAL_1:234;
then A14:
(
Sum ((Len J) | (1 -' 1)) = 0 &
0 <= i -' 1 )
by RVSUM_1:102;
len J <> 0
then
( 1
<= len J &
len (Len J) = len J )
by FINSEQ_1:def 18, NAT_1:14;
then
( 1
in dom (Len J) & 1
<= i )
by A12, FINSEQ_1:3, FINSEQ_3:27;
then A16:
ex
k being
Nat st
S4[
k]
by A14;
consider k being
Nat such that A17:
S4[
k]
and A18:
for
n being
Nat st
S4[
n] holds
n <= k
from NAT_1:sch 6(A13, A16);
take
k
;
:: thesis: ( k in NAT & S3[x,k] )
thus
k in NAT
by ORDINAL1:def 13;
:: thesis: S3[x,k]
let i',
k' be
Nat;
:: thesis: ( i' = x & k' = k implies ( S2[i',k'] & i' -' k' <= Sum ((Len J) | k') & ( for n being Nat st S2[i',n] holds
n <= k' ) ) )
assume A19:
(
i' = x &
k' = k )
;
:: thesis: ( S2[i',k'] & i' -' k' <= Sum ((Len J) | k') & ( for n being Nat st S2[i',n] holds
n <= k' ) )
i -' k <= Sum ((Len J) | k)
hence
(
S2[
i',
k'] &
i' -' k' <= Sum ((Len J) | k') & ( for
n being
Nat st
S2[
i',
n] holds
n <= k' ) )
by A17, A18, A19;
:: thesis: verum
end;
consider r being
Function of
(Seg ((Sum (Len J)) + (len J))),
NAT such that A27:
for
x being
set st
x in Seg ((Sum (Len J)) + (len J)) holds
S3[
x,
r . x]
from FUNCT_2:sch 1(A11);
A28:
dom r = Seg ((Sum (Len J)) + (len J))
by FUNCT_2:def 1;
defpred S4[
set ,
set ]
means for
i,
k being
Nat st
i = $1 &
k = r . i holds
( (
i -' k = Sum ((Len J) | (k -' 1)) implies (
F . $2
= b1 . ((i -' k) + 1) &
(i -' k) + 1
in dom b1 ) ) & (
i -' k <> Sum ((Len J) | (k -' 1)) implies ( $2
= b1 . (i -' k) &
i -' k in dom b1 &
min (Len J),
(i -' k) = k & (
i -' k < Sum ((Len J) | k) implies (
F . $2
= b1 . ((i -' k) + 1) &
(i -' k) + 1
in dom b1 ) ) & (
i -' k = Sum ((Len J) | k) implies
F . $2
= 0. V1 ) ) ) );
A29:
for
x being
set st
x in Seg ((Sum (Len J)) + (len J)) holds
ex
y being
set st
(
y in the
carrier of
V1 &
S4[
x,
y] )
proof
let x be
set ;
:: thesis: ( x in Seg ((Sum (Len J)) + (len J)) implies ex y being set st
( y in the carrier of V1 & S4[x,y] ) )
assume A30:
x in Seg ((Sum (Len J)) + (len J))
;
:: thesis: ex y being set st
( y in the carrier of V1 & S4[x,y] )
reconsider i =
x as
Nat by A30;
r . i = r /. i
by A30, A28, PARTFUN1:def 8;
then reconsider k =
r . i as
Element of
NAT ;
A31:
(
S2[
i,
k] &
i -' k <= Sum ((Len J) | k) )
by A30, A27;
k <= len (Len J)
by A31, FINSEQ_3:27;
then A32:
(
Sum ((Len J) | k) <= Sum ((Len J) | (len (Len J))) &
(Len J) | (len (Len J)) = Len J )
by FINSEQ_1:79, POLYNOM3:18;
dom (Len J) = dom J
by MATRIXJ1:def 3;
then A33:
(
(Len J) . k = len (J . k) &
(Len J) . k <> 0 )
by A7, A31, MATRIXJ1:def 3;
1
<= k
by A31, FINSEQ_3:27;
then A34:
k -' 1
= k - 1
by XREAL_1:235;
then
k = (k -' 1) + 1
;
then
(Len J) | k = ((Len J) | (k -' 1)) ^ <*((Len J) . k)*>
by A31, FINSEQ_5:11;
then A35:
Sum ((Len J) | k) = (Sum ((Len J) | (k -' 1))) + (len (J . k))
by A33, RVSUM_1:104;
per cases
( i -' k = Sum ((Len J) | (k -' 1)) or i -' k <> Sum ((Len J) | (k -' 1)) )
;
suppose A36:
i -' k = Sum ((Len J) | (k -' 1))
;
:: thesis: ex y being set st
( y in the carrier of V1 & S4[x,y] )then
i -' k <> Sum ((Len J) | k)
by A33, A35;
then
i -' k < Sum ((Len J) | k)
by A31, XXREAL_0:1;
then
(i -' k) + 1
<= Sum ((Len J) | k)
by NAT_1:13;
then A37:
( 1
<= (i -' k) + 1 &
(i -' k) + 1
<= Sum (Len J) )
by A32, NAT_1:11, XXREAL_0:2;
then
(i -' k) + 1
in dom b1
by A10;
then A38:
b1 /. ((i -' k) + 1) = b1 . ((i -' k) + 1)
by PARTFUN1:def 8;
(
b1 /. ((i -' k) + 1) in im (F |^ 1) &
b1 /. ((i -' k) + 1) is
Element of
V1 )
by STRUCT_0:def 5, VECTSP_4:18;
then consider y being
Element of
V1 such that A39:
(F |^ 1) . y = b1 /. ((i -' k) + 1)
by RANKNULL:13;
take
y
;
:: thesis: ( y in the carrier of V1 & S4[x,y] )thus
y in the
carrier of
V1
;
:: thesis: S4[x,y]thus
S4[
x,
y]
by A10, A36, A37, A38, A39, VECTSP11:19;
:: thesis: verum end; suppose A40:
i -' k <> Sum ((Len J) | (k -' 1))
;
:: thesis: ex y being set st
( y in the carrier of V1 & S4[x,y] )then
i -' k > Sum ((Len J) | (k -' 1))
by A31, XXREAL_0:1;
then
( 1
<= i -' k &
i -' k <= Sum (Len J) )
by A31, A32, NAT_1:14, XXREAL_0:2;
then A41:
i -' k in dom b1
by A10;
take y =
b1 /. (i -' k);
:: thesis: ( y in the carrier of V1 & S4[x,y] )
y in im (F |^ 1)
by STRUCT_0:def 5;
then
y in V1
by VECTSP_4:17;
hence
y in the
carrier of
V1
by STRUCT_0:def 5;
:: thesis: S4[x,y]let i',
k' be
Nat;
:: thesis: ( i' = x & k' = r . i' implies ( ( i' -' k' = Sum ((Len J) | (k' -' 1)) implies ( F . y = b1 . ((i' -' k') + 1) & (i' -' k') + 1 in dom b1 ) ) & ( i' -' k' <> Sum ((Len J) | (k' -' 1)) implies ( y = b1 . (i' -' k') & i' -' k' in dom b1 & min (Len J),(i' -' k') = k' & ( i' -' k' < Sum ((Len J) | k') implies ( F . y = b1 . ((i' -' k') + 1) & (i' -' k') + 1 in dom b1 ) ) & ( i' -' k' = Sum ((Len J) | k') implies F . y = 0. V1 ) ) ) ) )assume A42:
(
x = i' &
k' = r . i' )
;
:: thesis: ( ( i' -' k' = Sum ((Len J) | (k' -' 1)) implies ( F . y = b1 . ((i' -' k') + 1) & (i' -' k') + 1 in dom b1 ) ) & ( i' -' k' <> Sum ((Len J) | (k' -' 1)) implies ( y = b1 . (i' -' k') & i' -' k' in dom b1 & min (Len J),(i' -' k') = k' & ( i' -' k' < Sum ((Len J) | k') implies ( F . y = b1 . ((i' -' k') + 1) & (i' -' k') + 1 in dom b1 ) ) & ( i' -' k' = Sum ((Len J) | k') implies F . y = 0. V1 ) ) ) )
i -' k <= Sum ((Len J) | k)
by A30, A27;
then A43:
min (Len J),
(i -' k) <= k
by A41, A10, MATRIXJ1:def 1;
A44:
min (Len J),
(i -' k) = k
proof
assume
min (Len J),
(i -' k) <> k
;
:: thesis: contradiction
then
min (Len J),
(i -' k) < (k -' 1) + 1
by A34, A43, XXREAL_0:1;
then
min (Len J),
(i -' k) <= k -' 1
by NAT_1:13;
then
(
i -' k <= Sum ((Len J) | (min (Len J),(i -' k))) &
Sum ((Len J) | (min (Len J),(i -' k))) <= Sum ((Len J) | (k -' 1)) )
by A41, A10, MATRIXJ1:def 1, POLYNOM3:18;
then
i -' k <= Sum ((Len J) | (k -' 1))
by XXREAL_0:2;
hence
contradiction
by A31, A40, XXREAL_0:1;
:: thesis: verum
end; A45:
Len (J | k) = (Len J) | k
by MATRIXJ1:17;
A46:
now assume A47:
i -' k < Sum ((Len J) | k)
;
:: thesis: ( F . y = b1 . ((i -' k) + 1) & (i -' k) + 1 in dom b1 )then
(i -' k) + 1
<= Sum ((Len J) | k)
by NAT_1:13;
then A48:
( 1
<= (i -' k) + 1 &
(i -' k) + 1
<= Sum (Len J) )
by A32, NAT_1:11, XXREAL_0:2;
then A49:
(i -' k) + 1
in dom b1
by A10;
F . (b1 /. (i -' k)) =
FI . (b1 /. (i -' k))
by FUNCT_1:72
.=
((0. K) * (b1 /. (i -' k))) + (b1 /. ((i -' k) + 1))
by A8, A6, A41, A44, A45, Th24, A47
.=
(0. (im (F |^ 1))) + (b1 /. ((i -' k) + 1))
by VECTSP_1:59
.=
b1 /. ((i -' k) + 1)
by RLVECT_1:def 7
.=
b1 . ((i -' k) + 1)
by A49, PARTFUN1:def 8
;
hence
(
F . y = b1 . ((i -' k) + 1) &
(i -' k) + 1
in dom b1 )
by A48, A10;
:: thesis: verum end; hence
( (
i' -' k' = Sum ((Len J) | (k' -' 1)) implies (
F . y = b1 . ((i' -' k') + 1) &
(i' -' k') + 1
in dom b1 ) ) & (
i' -' k' <> Sum ((Len J) | (k' -' 1)) implies (
y = b1 . (i' -' k') &
i' -' k' in dom b1 &
min (Len J),
(i' -' k') = k' & (
i' -' k' < Sum ((Len J) | k') implies (
F . y = b1 . ((i' -' k') + 1) &
(i' -' k') + 1
in dom b1 ) ) & (
i' -' k' = Sum ((Len J) | k') implies
F . y = 0. V1 ) ) ) )
by A40, A41, A42, A46, A44, PARTFUN1:def 8;
:: thesis: verum end;
end;
consider B being
Function of
(Seg ((Sum (Len J)) + (len J))),the
carrier of
V1 such that A51:
for
x being
set st
x in Seg ((Sum (Len J)) + (len J)) holds
S4[
x,
B . x]
from FUNCT_2:sch 1(A29);
A52:
(
rng B c= the
carrier of
V1 &
dom B = Seg ((Sum (Len J)) + (len J)) )
by FUNCT_2:def 1, RELAT_1:def 19;
then reconsider B =
B as
FinSequence by FINSEQ_1:def 2;
reconsider B =
B as
FinSequence of
V1 by A52, FINSEQ_1:def 4;
reconsider RNG =
rng B as
Subset of
V1 by FINSEQ_1:def 4;
now let l be
Linear_Combination of
RNG;
:: thesis: ( Sum l = 0. V1 implies Carrier l = {} )assume A53:
Sum l = 0. V1
;
:: thesis: Carrier l = {} set RA =
{ v1 where v1 is Vector of V1 : ex i, k being Nat st
( i in Seg ((len J) + (Sum (Len J))) & k = r . i & v1 = B . i & i -' k < Sum ((Len J) | k) ) } ;
set RB =
{ v1 where v1 is Vector of V1 : ex i, k being Nat st
( i in Seg ((len J) + (Sum (Len J))) & k = r . i & v1 = B . i & i -' k <> Sum ((Len J) | (k -' 1)) & i -' k = Sum ((Len J) | k) ) } ;
A54:
{ v1 where v1 is Vector of V1 : ex i, k being Nat st
( i in Seg ((len J) + (Sum (Len J))) & k = r . i & v1 = B . i & i -' k < Sum ((Len J) | k) ) } c= the
carrier of
V1
{ v1 where v1 is Vector of V1 : ex i, k being Nat st
( i in Seg ((len J) + (Sum (Len J))) & k = r . i & v1 = B . i & i -' k <> Sum ((Len J) | (k -' 1)) & i -' k = Sum ((Len J) | k) ) } c= the
carrier of
V1
then reconsider RA =
{ v1 where v1 is Vector of V1 : ex i, k being Nat st
( i in Seg ((len J) + (Sum (Len J))) & k = r . i & v1 = B . i & i -' k < Sum ((Len J) | k) ) } ,
RB =
{ v1 where v1 is Vector of V1 : ex i, k being Nat st
( i in Seg ((len J) + (Sum (Len J))) & k = r . i & v1 = B . i & i -' k <> Sum ((Len J) | (k -' 1)) & i -' k = Sum ((Len J) | k) ) } as
Subset of
V1 by A54;
A55:
Carrier l c= RB \/ RA
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in Carrier l or x in RB \/ RA )
assume A56:
x in Carrier l
;
:: thesis: x in RB \/ RA
reconsider v1 =
x as
Vector of
V1 by A56;
Carrier l c= RNG
by VECTSP_6:def 7;
then consider i being
set such that A57:
(
i in dom B &
B . i = v1 )
by A56, FUNCT_1:def 5;
reconsider i =
i as
Nat by A57;
r . i = r /. i
by A57, A52, A28, PARTFUN1:def 8;
then reconsider k =
r . i as
Element of
NAT ;
A58:
i -' k <= Sum ((Len J) | k)
by A27, A57, A52;
per cases
( i -' k = Sum ((Len J) | k) or i -' k < Sum ((Len J) | k) )
by A58, XXREAL_0:1;
suppose A59:
i -' k = Sum ((Len J) | k)
;
:: thesis: x in RB \/ RAA60:
S2[
i,
k]
by A57, A52, A27;
then
1
<= k
by FINSEQ_3:27;
then
k -' 1
= k - 1
by XREAL_1:235;
then
(k -' 1) + 1
= k
;
then
(
(Len J) | k = ((Len J) | (k -' 1)) ^ <*((Len J) . k)*> &
dom (Len J) = dom J )
by A60, FINSEQ_5:11, MATRIXJ1:def 3;
then
(
i -' k = (Sum ((Len J) | (k -' 1))) + ((Len J) . k) &
(Len J) . k <> 0 )
by A7, A59, A60, RVSUM_1:104;
then
i -' k <> Sum ((Len J) | (k -' 1))
;
then
(
v1 in RB or
v1 in RA )
by A57, A59, A52;
hence
x in RB \/ RA
by XBOOLE_0:def 3;
:: thesis: verum end;
end; A61:
F | RA is
one-to-one
proof
let x1,
x2 be
set ;
:: according to FUNCT_1:def 8 :: thesis: ( not x1 in dom (F | RA) or not x2 in dom (F | RA) or not (F | RA) . x1 = (F | RA) . x2 or x1 = x2 )
assume A62:
(
x1 in dom (F | RA) &
x2 in dom (F | RA) &
(F | RA) . x1 = (F | RA) . x2 )
;
:: thesis: x1 = x2
dom (F | RA) = (dom F) /\ RA
by RELAT_1:90;
then A63:
(
x1 in RA &
x2 in RA &
(F | RA) . x1 = F . x1 &
(F | RA) . x2 = F . x2 )
by A62, FUNCT_1:70, XBOOLE_0:def 4;
then consider v1 being
Vector of
V1 such that A64:
x1 = v1
and A65:
ex
i1,
k1 being
Nat st
(
i1 in Seg ((len J) + (Sum (Len J))) &
k1 = r . i1 &
v1 = B . i1 &
i1 -' k1 < Sum ((Len J) | k1) )
;
consider i1,
k1 being
Nat such that A66:
(
i1 in Seg ((len J) + (Sum (Len J))) &
k1 = r . i1 &
v1 = B . i1 &
i1 -' k1 < Sum ((Len J) | k1) )
by A65;
consider v2 being
Vector of
V1 such that A67:
x2 = v2
and A68:
ex
i2,
k2 being
Nat st
(
i2 in Seg ((len J) + (Sum (Len J))) &
k2 = r . i2 &
v2 = B . i2 &
i2 -' k2 < Sum ((Len J) | k2) )
by A63;
consider i2,
k2 being
Nat such that A69:
(
i2 in Seg ((len J) + (Sum (Len J))) &
k2 = r . i2 &
v2 = B . i2 &
i2 -' k2 < Sum ((Len J) | k2) )
by A68;
A70:
b1 is
one-to-one
by MATRLIN:def 4;
A71:
(
k1 <= i1 &
k2 <= i2 &
k1 in dom (Len J) &
k2 in dom (Len J) )
by A66, A69, A27;
then A72:
(
i1 -' k1 = i1 - k1 &
i2 -' k2 = i2 - k2 & 1
<= k1 & 1
<= k2 )
by FINSEQ_3:27, XREAL_1:235;
then A73:
(
k1 -' 1
= k1 - 1 &
k2 -' 1
= k2 - 1 )
by XREAL_1:235;
then
(
(k1 -' 1) + 1
<= len (Len J) &
(k2 -' 1) + 1
<= len (Len J) )
by A71, FINSEQ_3:27;
then A75:
(
k1 -' 1
<= len (Len J) &
k2 -' 1
<= len (Len J) )
by NAT_1:13;
A76:
dom (Len J) = dom J
by MATRIXJ1:def 3;
A77:
(
k1 -' 1
in dom (Len J) implies
(Len J) . (k1 -' 1) <> 0 )
by A7, A76;
A78:
(
k2 -' 1
in dom (Len J) implies
(Len J) . (k2 -' 1) <> 0 )
by A7, A76;
per cases
( ( i1 -' k1 = Sum ((Len J) | (k1 -' 1)) & i2 -' k2 = Sum ((Len J) | (k2 -' 1)) ) or ( i1 -' k1 = Sum ((Len J) | (k1 -' 1)) & i2 -' k2 <> Sum ((Len J) | (k2 -' 1)) ) or ( i1 -' k1 <> Sum ((Len J) | (k1 -' 1)) & i2 -' k2 = Sum ((Len J) | (k2 -' 1)) ) or ( i1 -' k1 <> Sum ((Len J) | (k1 -' 1)) & i2 -' k2 <> Sum ((Len J) | (k2 -' 1)) ) )
;
suppose A81:
(
i1 -' k1 = Sum ((Len J) | (k1 -' 1)) &
i2 -' k2 = Sum ((Len J) | (k2 -' 1)) )
;
:: thesis: x1 = x2then
(
F . v1 = b1 . ((i1 -' k1) + 1) &
(i1 -' k1) + 1
in dom b1 &
F . v2 = b1 . ((i2 -' k2) + 1) &
(i2 -' k2) + 1
in dom b1 )
by A66, A69, A51;
then
(i1 -' k1) + 1
= (i2 -' k2) + 1
by A62, A63, A64, A67, A70, FUNCT_1:def 8;
then
k1 -' 1
= k2 -' 1
by A75, A81, A77, A78, MATRIXJ1:11;
then
i1 - k1 = i2 - k1
by A72, A73, A81;
hence
x1 = x2
by A64, A66, A67, A69;
:: thesis: verum end; suppose A82:
(
i1 -' k1 = Sum ((Len J) | (k1 -' 1)) &
i2 -' k2 <> Sum ((Len J) | (k2 -' 1)) )
;
:: thesis: x1 = x2then A83:
(
F . v1 = b1 . ((i1 -' k1) + 1) &
(i1 -' k1) + 1
in dom b1 &
F . v2 = b1 . ((i2 -' k2) + 1) &
(i2 -' k2) + 1
in dom b1 &
min (Len J),
(i2 -' k2) = k2 )
by A66, A69, A51;
then A84:
(i1 -' k1) + 1
= (i2 -' k2) + 1
by A62, A63, A64, A67, A70, FUNCT_1:def 8;
k1 -' 1
<> 0
then
k1 -' 1
>= 1
by NAT_1:14;
then A85:
k1 -' 1
in dom (Len J)
by A75, FINSEQ_3:27;
then
(Len J) . (k1 -' 1) <> 0
by A76, A7;
hence
x1 = x2
by A69, A82, A84, A83, A85, MATRIXJ1:6;
:: thesis: verum end; suppose A86:
(
i1 -' k1 <> Sum ((Len J) | (k1 -' 1)) &
i2 -' k2 = Sum ((Len J) | (k2 -' 1)) )
;
:: thesis: x1 = x2then A87:
(
F . v1 = b1 . ((i1 -' k1) + 1) &
(i1 -' k1) + 1
in dom b1 &
F . v2 = b1 . ((i2 -' k2) + 1) &
(i2 -' k2) + 1
in dom b1 &
min (Len J),
(i1 -' k1) = k1 )
by A66, A69, A51;
then A88:
(i1 -' k1) + 1
= (i2 -' k2) + 1
by A62, A63, A64, A67, A70, FUNCT_1:def 8;
k2 -' 1
<> 0
then
k2 -' 1
>= 1
by NAT_1:14;
then A89:
k2 -' 1
in dom (Len J)
by A75, FINSEQ_3:27;
then
(Len J) . (k2 -' 1) <> 0
by A76, A7;
hence
x1 = x2
by A66, A86, A88, A87, A89, MATRIXJ1:6;
:: thesis: verum end; suppose
(
i1 -' k1 <> Sum ((Len J) | (k1 -' 1)) &
i2 -' k2 <> Sum ((Len J) | (k2 -' 1)) )
;
:: thesis: x1 = x2then A90:
(
F . v1 = b1 . ((i1 -' k1) + 1) &
(i1 -' k1) + 1
in dom b1 &
min (Len J),
(i2 -' k2) = k2 &
F . v2 = b1 . ((i2 -' k2) + 1) &
(i2 -' k2) + 1
in dom b1 &
min (Len J),
(i1 -' k1) = k1 )
by A66, A69, A51;
then
(i1 -' k1) + 1
= (i2 -' k2) + 1
by A62, A63, A64, A67, A70, FUNCT_1:def 8;
then
i1 - k1 = i2 - k1
by A90, A72;
hence
x1 = x2
by A64, A66, A67, A69;
:: thesis: verum end;
end;
rng b1 is
Basis of
im (F |^ 1)
by MATRLIN:def 4;
then
rng b1 is
linearly-independent Subset of
(im (F |^ 1))
by VECTSP_7:def 3;
then reconsider rngb1 =
rng b1 as
linearly-independent Subset of
V1 by VECTSP_9:15;
F .: RA c= rngb1
then A95:
F .: RA is
linearly-independent Subset of
V1
by VECTSP_7:2;
A96:
F .: RB c= {(0. V1)}
A100:
Carrier l c= RB
by A53, A55, A61, A95, A96, VECTSP11:44;
RB c= rngb1
then
Carrier l c= rngb1
by A100, XBOOLE_1:1;
then
l is
Linear_Combination of
rngb1
by VECTSP_6:def 7;
hence
Carrier l = {}
by A53, VECTSP_7:def 1;
:: thesis: verum end;
then A104:
RNG is
linearly-independent Subset of
V1
by VECTSP_7:def 1;
consider BAS being
Basis of
V1;
A105:
(
BAS is
linearly-independent &
Lin BAS = VectSpStr(# the
carrier of
V1,the
addF of
V1,the
U2 of
V1,the
lmult of
V1 #) )
by VECTSP_7:def 3;
then reconsider BAS =
BAS,
RNG =
RNG as
finite Subset of
V1 by VECTSP_9:25;
A106:
(Omega). (Lin BAS) = (Omega). V1
by VECTSP_7:def 3;
consider C being
finite Subset of
V1 such that A107:
(
C c= BAS &
card C = (card BAS) - (card RNG) )
and A108:
VectSpStr(# the
carrier of
V1,the
addF of
V1,the
U2 of
V1,the
lmult of
V1 #)
= Lin (RNG \/ C)
by A104, A105, VECTSP_9:23;
A109:
(
dim V1 = dim (Lin (RNG \/ C)) &
dim V1 = dim (Lin BAS) &
dim (Lin BAS) = card BAS )
by A105, A108, A106, VECTSP_9:30, VECTSP_9:32;
then A110:
card (RNG \/ C) >= card BAS
by MATRLIN2:6;
A111:
card (RNG \/ C) =
((card RNG) + (card C)) - (card (RNG /\ C))
by CARD_2:64
.=
(card BAS) - (card (RNG /\ C))
by A107
;
then
(card (RNG \/ C)) + (card (RNG /\ C)) = card BAS
;
then
card (RNG \/ C) <= card BAS
by NAT_1:11;
then A112:
(
card (RNG \/ C) = card BAS &
RNG \/ C is
linearly-independent )
by A109, A110, MATRLIN2:5, XXREAL_0:1;
defpred S5[
Nat]
means ( $1
<= card C implies ex
f being
FinSequence of
V1 st
(
f is
one-to-one &
len f = card C &
RNG misses rng f &
RNG \/ (rng f) is
Basis of
V1 & ( for
i being
Nat st
i in dom f &
i <= $1 holds
F . (f . i) = 0. V1 ) ) );
A113:
S5[
0 ]
A115:
for
n being
Nat st
S5[
n] holds
S5[
n + 1]
proof
let n be
Nat;
:: thesis: ( S5[n] implies S5[n + 1] )
assume A116:
S5[
n]
;
:: thesis: S5[n + 1]
set n1 =
n + 1;
assume A117:
n + 1
<= card C
;
:: thesis: ex f being FinSequence of V1 st
( f is one-to-one & len f = card C & RNG misses rng f & RNG \/ (rng f) is Basis of V1 & ( for i being Nat st i in dom f & i <= n + 1 holds
F . (f . i) = 0. V1 ) )
then consider f being
FinSequence of
V1 such that A118:
f is
one-to-one
and A119:
len f = card C
and A120:
(
RNG misses rng f &
RNG \/ (rng f) is
Basis of
V1 )
and A121:
for
i being
Nat st
i in dom f &
i <= n holds
F . (f . i) = 0. V1
by A116, NAT_1:13;
per cases
( F . (f . (n + 1)) = 0. V1 or F . (f . (n + 1)) <> 0. V1 )
;
suppose A122:
F . (f . (n + 1)) <> 0. V1
;
:: thesis: ex f being FinSequence of V1 st
( f is one-to-one & len f = card C & RNG misses rng f & RNG \/ (rng f) is Basis of V1 & ( for i being Nat st i in dom f & i <= n + 1 holds
F . (f . i) = 0. V1 ) )A123:
rng b1 c= F .: RNG
proof
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in rng b1 or y in F .: RNG )
assume A124:
y in rng b1
;
:: thesis: y in F .: RNG
consider x being
set such that A125:
(
x in dom b1 &
b1 . x = y )
by A124, FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A125;
set m =
min (Len J),
x;
set x1 =
x -' 1;
set mx =
(min (Len J),x) + (x -' 1);
A126:
min (Len J),
x in dom (Len J)
by A125, A10, MATRIXJ1:def 1;
then
( 1
<= min (Len J),
x &
min (Len J),
x <= len (Len J) &
len (Len J) = len J & 1
<= x &
x <= Sum (Len J) )
by A125, A9, FINSEQ_1:def 18, FINSEQ_3:27;
then A127:
( 1
+ 1
<= (min (Len J),x) + x &
(min (Len J),x) + x <= (len J) + (Sum (Len J)) &
x -' 1
= x - 1 )
by XREAL_1:9, XREAL_1:235;
then
( 2
- 1
<= ((min (Len J),x) + x) - 1 &
((min (Len J),x) + x) - 1
<= ((len J) + (Sum (Len J))) - 1 &
((len J) + (Sum (Len J))) - 1
<= ((len J) + (Sum (Len J))) - 0 )
by XREAL_1:11, XREAL_1:12;
then
( 1
<= (min (Len J),x) + (x -' 1) &
(min (Len J),x) + (x -' 1) <= (len J) + (Sum (Len J)) )
by A127, XXREAL_0:2;
then A128:
(min (Len J),x) + (x -' 1) in Seg ((Sum (Len J)) + (len J))
;
then
r . ((min (Len J),x) + (x -' 1)) = r /. ((min (Len J),x) + (x -' 1))
by A28, PARTFUN1:def 8;
then reconsider k =
r . ((min (Len J),x) + (x -' 1)) as
Element of
NAT ;
A129:
S2[
(min (Len J),x) + (x -' 1),
k]
by A27, A128;
A130:
min (Len J),
x <= (min (Len J),x) + (x -' 1)
by NAT_1:11;
then A131:
(
((min (Len J),x) + (x -' 1)) -' (min (Len J),x) = ((min (Len J),x) + (x -' 1)) - (min (Len J),x) &
((min (Len J),x) + (x -' 1)) -' k = ((min (Len J),x) + (x -' 1)) - k &
Sum ((Len J) | ((min (Len J),x) -' 1)) < (x -' 1) + 1 &
x <= Sum ((Len J) | (min (Len J),x)) )
by A10, A125, A127, A129, MATRIXJ1:7, MATRIXJ1:def 1, XREAL_1:235;
then
Sum ((Len J) | ((min (Len J),x) -' 1)) <= ((min (Len J),x) + (x -' 1)) -' (min (Len J),x)
by NAT_1:13;
then A132:
min (Len J),
x <= k
by A126, A27, A128, A130;
A133:
min (Len J),
x = k
proof
assume A134:
min (Len J),
x <> k
;
:: thesis: contradiction
then A135:
min (Len J),
x < k
by A132, XXREAL_0:1;
then reconsider k1 =
k - 1 as
Element of
NAT by NAT_1:20;
k = k1 + 1
;
then
(
k -' 1
= k1 &
min (Len J),
x <= k1 )
by A135, NAT_1:13, NAT_D:34;
then
(
Sum ((Len J) | (min (Len J),x)) <= Sum ((Len J) | k1) &
Sum ((Len J) | k1) <= ((min (Len J),x) + (x -' 1)) -' k &
((min (Len J),x) + (x -' 1)) -' k <= ((min (Len J),x) + (x -' 1)) -' (min (Len J),x) &
((min (Len J),x) + (x -' 1)) -' k <> ((min (Len J),x) + (x -' 1)) -' (min (Len J),x) )
by A128, A131, A27, A134, A132, NAT_D:41, POLYNOM3:18;
then
(
Sum ((Len J) | (min (Len J),x)) <= ((min (Len J),x) + (x -' 1)) -' k &
((min (Len J),x) + (x -' 1)) -' k < ((min (Len J),x) + (x -' 1)) -' (min (Len J),x) )
by XXREAL_0:1, XXREAL_0:2;
then
Sum ((Len J) | (min (Len J),x)) <= x -' 1
by A131, XXREAL_0:2;
hence
contradiction
by A127, A131, NAT_1:13;
:: thesis: verum
end;
(
((min (Len J),x) + (x -' 1)) -' (min (Len J),x) < Sum ((Len J) | (min (Len J),x)) & (
((min (Len J),x) + (x -' 1)) -' (min (Len J),x) = Sum ((Len J) | ((min (Len J),x) -' 1)) or
((min (Len J),x) + (x -' 1)) -' (min (Len J),x) <> Sum ((Len J) | ((min (Len J),x) -' 1)) ) )
by A131, A127, NAT_1:13;
then
(
F . (B . ((min (Len J),x) + (x -' 1))) = b1 . ((((min (Len J),x) + (x -' 1)) -' (min (Len J),x)) + 1) &
(((min (Len J),x) + (x -' 1)) -' (min (Len J),x)) + 1
= x &
B . ((min (Len J),x) + (x -' 1)) in RNG &
dom F = [#] V1 )
by A51, A52, A127, A128, A131, A133, FUNCT_1:def 5, FUNCT_2:def 1;
hence
y in F .: RNG
by A125, FUNCT_1:def 12;
:: thesis: verum
end; reconsider rngB1 =
rng b1 as
Basis of
im (F |^ 1) by MATRLIN:def 4;
1
<= n + 1
by NAT_1:14;
then A136:
n + 1
in dom f
by A117, A119, FINSEQ_3:27;
then A137:
(
f /. (n + 1) = f . (n + 1) &
f . (n + 1) in rng f )
by FUNCT_1:def 5, PARTFUN1:def 8;
(
F . (f /. (n + 1)) in im F &
F |^ 1
= F )
by RANKNULL:13, VECTSP11:19;
then
F . (f /. (n + 1)) in Lin rngB1
by VECTSP_7:def 3;
then consider L being
Linear_Combination of
rngB1 such that A138:
F . (f /. (n + 1)) = Sum L
by VECTSP_7:12;
consider K being
Linear_Combination of
V1 such that A139:
(
Carrier L = Carrier K &
Sum L = Sum K )
by VECTSP_9:12;
Carrier L c= rngB1
by VECTSP_6:def 7;
then consider M being
Linear_Combination of
RNG such that A140:
F . (Sum M) = Sum K
by A139, A123, VECTSP11:41, XBOOLE_1:1;
reconsider Rf =
RNG \/ (rng f) as
finite Subset of
V1 by A120;
A141:
Rf is
linearly-independent
by A120, VECTSP_7:def 3;
set fn =
f /. (n + 1);
A142:
f /. (n + 1) in Rf
by A137, XBOOLE_0:def 3;
(
RNG c= Rf & not
f /. (n + 1) in RNG )
by A137, A120, XBOOLE_0:3, XBOOLE_1:7;
then
(
Carrier M c= RNG &
Carrier M = Carrier (- M) &
RNG c= Rf \ {(f /. (n + 1))} )
by VECTSP_6:69, VECTSP_6:def 7, ZFMISC_1:40;
then
Carrier (- M) c= Rf \ {(f /. (n + 1))}
by XBOOLE_1:1;
then reconsider M' =
- M as
Linear_Combination of
Rf \ {(f /. (n + 1))} by VECTSP_6:def 7;
set fnM =
(f /. (n + 1)) + (Sum M');
set fnS =
(n + 1) .--> ((f /. (n + 1)) + (Sum M'));
take ff =
f +* (n + 1),
((f /. (n + 1)) + (Sum M'));
:: thesis: ( ff is one-to-one & len ff = card C & RNG misses rng ff & RNG \/ (rng ff) is Basis of V1 & ( for i being Nat st i in dom ff & i <= n + 1 holds
F . (ff . i) = 0. V1 ) )A143:
not
(f /. (n + 1)) + (Sum M') in Rf \ {(f /. (n + 1))}
A145:
(f /. (n + 1)) + (Sum M') <> f /. (n + 1)
not
(f /. (n + 1)) + (Sum M') in rng f
then
(
rng f misses {((f /. (n + 1)) + (Sum M'))} &
rng ((n + 1) .--> ((f /. (n + 1)) + (Sum M'))) = {((f /. (n + 1)) + (Sum M'))} )
by FUNCOP_1:14, ZFMISC_1:56;
then
f +* ((n + 1) .--> ((f /. (n + 1)) + (Sum M'))) is
one-to-one
by A118, FUNCT_4:98;
hence
ff is
one-to-one
by A136, FUNCT_7:def 3;
:: thesis: ( len ff = card C & RNG misses rng ff & RNG \/ (rng ff) is Basis of V1 & ( for i being Nat st i in dom ff & i <= n + 1 holds
F . (ff . i) = 0. V1 ) )A146:
dom ff = dom f
by FUNCT_7:32;
hence
len ff = card C
by A119, FINSEQ_3:31;
:: thesis: ( RNG misses rng ff & RNG \/ (rng ff) is Basis of V1 & ( for i being Nat st i in dom ff & i <= n + 1 holds
F . (ff . i) = 0. V1 ) )A147:
rng ff = ((rng f) \ {(f /. (n + 1))}) \/ {((f /. (n + 1)) + (Sum M'))}
by Lm1, A118, A136, A137;
thus
RNG misses rng ff
:: thesis: ( RNG \/ (rng ff) is Basis of V1 & ( for i being Nat st i in dom ff & i <= n + 1 holds
F . (ff . i) = 0. V1 ) )A149:
not
f /. (n + 1) in RNG
by A120, A137, XBOOLE_0:3;
A150:
(Rf \ {(f /. (n + 1))}) \/ {((f /. (n + 1)) + (Sum M'))} =
((RNG \ {(f /. (n + 1))}) \/ ((rng f) \ {(f /. (n + 1))})) \/ {((f /. (n + 1)) + (Sum M'))}
by XBOOLE_1:42
.=
(RNG \/ ((rng f) \ {(f /. (n + 1))})) \/ {((f /. (n + 1)) + (Sum M'))}
by A149, ZFMISC_1:65
.=
RNG \/ (rng ff)
by A147, XBOOLE_1:4
;
then reconsider Rff =
RNG \/ (rng ff) as
finite Subset of
V1 ;
A151:
(Rf \ {(f /. (n + 1))}) \/ {((f /. (n + 1)) + (Sum M'))} is
linearly-independent
by A141, A142, VECTSP11:40;
dim V1 =
card Rf
by A120, VECTSP_9:def 2
.=
card (RNG \/ (rng ff))
by A141, A142, A150, VECTSP11:40
;
then
dim (Lin Rff) = dim V1
by A150, A141, A142, VECTSP11:40, VECTSP_9:30;
then
(Omega). V1 = (Omega). (Lin Rff)
by VECTSP_9:32;
hence
RNG \/ (rng ff) is
Basis of
V1
by A150, A151, VECTSP_7:def 3;
:: thesis: for i being Nat st i in dom ff & i <= n + 1 holds
F . (ff . i) = 0. V1let i be
Nat;
:: thesis: ( i in dom ff & i <= n + 1 implies F . (ff . i) = 0. V1 )assume A152:
(
i in dom ff &
i <= n + 1 )
;
:: thesis: F . (ff . i) = 0. V1 end;
end;
for
n being
Nat holds
S5[
n]
from NAT_1:sch 2(A113, A115);
then consider f being
FinSequence of
V1 such that A153:
f is
one-to-one
and A154:
len f = card C
and A155:
(
RNG misses rng f &
RNG \/ (rng f) is
Basis of
V1 )
and A156:
for
i being
Nat st
i in dom f &
i <= card C holds
F . (f . i) = 0. V1
;
now let x1,
x2 be
set ;
:: thesis: ( x1 in dom B & x2 in dom B & B . x1 = B . x2 implies x1 = x2 )assume A157:
(
x1 in dom B &
x2 in dom B &
B . x1 = B . x2 )
;
:: thesis: x1 = x2reconsider i1 =
x1,
i2 =
x2 as
Nat by A157;
(
r /. i1 = r . i1 &
r /. i2 = r . i2 )
by A28, A52, A157, PARTFUN1:def 8;
then reconsider k1 =
r . i1,
k2 =
r . i2 as
Element of
NAT ;
A158:
(
S2[
i1,
k1] &
i1 -' k1 <= Sum ((Len J) | k1) )
by A27, A52, A157;
A159:
(
S2[
i2,
k2] &
i2 -' k2 <= Sum ((Len J) | k2) )
by A27, A52, A157;
A160:
(
i1 -' k1 = Sum ((Len J) | (k1 -' 1)) implies (
F . (B . x1) = b1 . ((i1 -' k1) + 1) &
(i1 -' k1) + 1
in dom b1 ) )
by A51, A52, A157;
A161:
(
i1 -' k1 <> Sum ((Len J) | (k1 -' 1)) implies (
B . x1 = b1 . (i1 -' k1) &
i1 -' k1 in dom b1 &
min (Len J),
(i1 -' k1) = k1 & (
i1 -' k1 < Sum ((Len J) | k1) implies (
F . (B . x1) = b1 . ((i1 -' k1) + 1) &
(i1 -' k1) + 1
in dom b1 ) ) & (
i1 -' k1 = Sum ((Len J) | k1) implies
F . (B . x1) = 0. V1 ) ) )
by A51, A52, A157;
A162:
(
i2 -' k2 = Sum ((Len J) | (k2 -' 1)) implies (
F . (B . x2) = b1 . ((i2 -' k2) + 1) &
(i2 -' k2) + 1
in dom b1 ) )
by A51, A52, A157;
A163:
(
i2 -' k2 <> Sum ((Len J) | (k2 -' 1)) implies (
B . x2 = b1 . (i2 -' k2) &
i2 -' k2 in dom b1 &
min (Len J),
(i2 -' k2) = k2 & (
i2 -' k2 < Sum ((Len J) | k2) implies (
F . (B . x2) = b1 . ((i2 -' k2) + 1) &
(i2 -' k2) + 1
in dom b1 ) ) & (
i2 -' k2 = Sum ((Len J) | k2) implies
F . (B . x2) = 0. V1 ) ) )
by A51, A52, A157;
A164:
(
b1 is
one-to-one &
rng b1 is
Basis of
im (F |^ 1) )
by MATRLIN:def 4;
then A165:
rng b1 is
linearly-independent Subset of
(im (F |^ 1))
by VECTSP_7:def 3;
( 1
<= k1 &
k1 <= len (Len J) & 1
<= k2 &
k2 <= len (Len J) &
k1 -' 1
<= k1 &
k2 -' 1
<= k2 )
by A158, A159, FINSEQ_3:27, NAT_D:35;
then A166:
(
k1 -' 1
= k1 - 1 &
k2 -' 1
= k2 - 1 &
i1 -' k1 = i1 - k1 &
i2 -' k2 = i2 - k2 &
k1 -' 1
<= len (Len J) &
k2 -' 1
<= len (Len J) )
by A158, A159, XREAL_1:235, XXREAL_0:2;
A167:
(
dom (Len J) = dom J &
0 <= len (Len J) )
by MATRIXJ1:def 3;
now per cases
( ( i1 -' k1 = Sum ((Len J) | (k1 -' 1)) & i2 -' k2 = Sum ((Len J) | (k2 -' 1)) ) or ( i1 -' k1 = Sum ((Len J) | (k1 -' 1)) & i2 -' k2 <> Sum ((Len J) | (k2 -' 1)) & i2 -' k2 < Sum ((Len J) | k2) ) or ( i1 -' k1 = Sum ((Len J) | (k1 -' 1)) & i2 -' k2 <> Sum ((Len J) | (k2 -' 1)) & i2 -' k2 = Sum ((Len J) | k2) ) or ( i2 -' k2 = Sum ((Len J) | (k2 -' 1)) & i1 -' k1 <> Sum ((Len J) | (k1 -' 1)) & i1 -' k1 < Sum ((Len J) | k1) ) or ( i2 -' k2 = Sum ((Len J) | (k2 -' 1)) & i1 -' k1 <> Sum ((Len J) | (k1 -' 1)) & i1 -' k1 = Sum ((Len J) | k1) ) or ( i1 -' k1 <> Sum ((Len J) | (k1 -' 1)) & i2 -' k2 <> Sum ((Len J) | (k2 -' 1)) ) )
by A158, A159, XXREAL_0:1;
suppose A170:
(
i1 -' k1 = Sum ((Len J) | (k1 -' 1)) &
i2 -' k2 <> Sum ((Len J) | (k2 -' 1)) &
i2 -' k2 < Sum ((Len J) | k2) )
;
:: thesis: i1 = i2then A171:
(
F . (B . x1) = b1 . ((i1 -' k1) + 1) &
(i1 -' k1) + 1
in dom b1 &
F . (B . x2) = b1 . ((i2 -' k2) + 1) &
(i2 -' k2) + 1
in dom b1 &
min (Len J),
(i2 -' k2) = k2 )
by A51, A52, A157;
then A172:
(i1 -' k1) + 1
= (i2 -' k2) + 1
by A164, A157, FUNCT_1:def 8;
k1 -' 1
<> 0
then
k1 -' 1
>= 1
by NAT_1:14;
then A173:
k1 -' 1
in dom (Len J)
by A166, FINSEQ_3:27;
then
(Len J) . (k1 -' 1) <> 0
by A167, A7;
hence
i1 = i2
by A170, A172, A171, A173, MATRIXJ1:6;
:: thesis: verum end; suppose A174:
(
i2 -' k2 = Sum ((Len J) | (k2 -' 1)) &
i1 -' k1 <> Sum ((Len J) | (k1 -' 1)) &
i1 -' k1 < Sum ((Len J) | k1) )
;
:: thesis: i1 = i2then A175:
(
F . (B . x2) = b1 . ((i2 -' k2) + 1) &
(i2 -' k2) + 1
in dom b1 &
F . (B . x1) = b1 . ((i1 -' k1) + 1) &
(i1 -' k1) + 1
in dom b1 &
min (Len J),
(i1 -' k1) = k1 )
by A51, A52, A157;
A176:
(i2 -' k2) + 1
= (i1 -' k1) + 1
by A175, A164, A157, FUNCT_1:def 8;
k2 -' 1
<> 0
then
k2 -' 1
>= 1
by NAT_1:14;
then A177:
k2 -' 1
in dom (Len J)
by A166, FINSEQ_3:27;
then
(Len J) . (k2 -' 1) <> 0
by A167, A7;
hence
i1 = i2
by A174, A176, A175, A177, MATRIXJ1:6;
:: thesis: verum end; hence
x1 = x2
;
:: thesis: verum end;
then
B is
one-to-one
by FUNCT_1:def 8;
then
(
B ^ f is
one-to-one &
rng (B ^ f) = (rng B) \/ (rng f) )
by A153, A155, FINSEQ_1:44, FINSEQ_3:98;
then reconsider Bf =
B ^ f as
OrdBasis of
V1 by A155, MATRLIN:def 4;
for
i being
Nat holds
( not
i in dom Bf or
F . (Bf /. i) = (0. K) * (Bf /. i) or (
i + 1
in dom Bf &
F . (Bf /. i) = ((0. K) * (Bf /. i)) + (Bf /. (i + 1)) ) )
proof
let i be
Nat;
:: thesis: ( not i in dom Bf or F . (Bf /. i) = (0. K) * (Bf /. i) or ( i + 1 in dom Bf & F . (Bf /. i) = ((0. K) * (Bf /. i)) + (Bf /. (i + 1)) ) )
assume A179:
i in dom Bf
;
:: thesis: ( F . (Bf /. i) = (0. K) * (Bf /. i) or ( i + 1 in dom Bf & F . (Bf /. i) = ((0. K) * (Bf /. i)) + (Bf /. (i + 1)) ) )
A180:
Bf /. i = Bf . i
by A179, PARTFUN1:def 8;
per cases
( i in dom B or ex j being Nat st
( j in dom f & i = (len B) + j ) )
by A179, FINSEQ_1:38;
suppose A181:
i in dom B
;
:: thesis: ( F . (Bf /. i) = (0. K) * (Bf /. i) or ( i + 1 in dom Bf & F . (Bf /. i) = ((0. K) * (Bf /. i)) + (Bf /. (i + 1)) ) )
r /. i = r . i
by A28, A52, A181, PARTFUN1:def 8;
then reconsider k =
r . i as
Element of
NAT ;
A182:
(
S2[
i,
k] &
i -' k <= Sum ((Len J) | k) )
by A27, A52, A181;
1
<= k
by A182, FINSEQ_3:27;
then
k -' 1
= k - 1
by XREAL_1:235;
then
(k -' 1) + 1
= k
;
then
(
(Len J) | k = ((Len J) | (k -' 1)) ^ <*((Len J) . k)*> &
dom (Len J) = dom J )
by A182, FINSEQ_5:11, MATRIXJ1:def 3;
then A183:
(
Sum ((Len J) | k) = (Sum ((Len J) | (k -' 1))) + ((Len J) . k) &
(Len J) . k <> 0 )
by A7, A182, RVSUM_1:104;
per cases
( i -' k = Sum ((Len J) | k) or i -' k < Sum ((Len J) | k) )
by A182, XXREAL_0:1;
suppose A186:
i -' k < Sum ((Len J) | k)
;
:: thesis: ( F . (Bf /. i) = (0. K) * (Bf /. i) or ( i + 1 in dom Bf & F . (Bf /. i) = ((0. K) * (Bf /. i)) + (Bf /. (i + 1)) ) )then A187:
(
(i -' k) + 1
<= Sum ((Len J) | k) &
Sum ((Len J) | (k -' 1)) < (i -' k) + 1 )
by A182, NAT_1:13;
(
i -' k = Sum ((Len J) | (k -' 1)) or
i -' k <> Sum ((Len J) | (k -' 1)) )
;
then A188:
(
F . (B . i) = b1 . ((i -' k) + 1) &
(i -' k) + 1
in dom b1 &
dom J = dom (Len J) )
by A51, A52, A181, A186, MATRIXJ1:def 3;
then A189:
( 1
<= (i -' k) + 1 &
(i -' k) + 1
<= Sum (Len J) &
k <= len J &
i -' k = i - k )
by A9, A182, FINSEQ_3:27, XREAL_1:235;
then
( 1
+ 0 <= ((i - k) + 1) + k &
((i - k) + 1) + k <= (Sum (Len J)) + (len J) & 1
+ k <= ((i - k) + 1) + k )
by XREAL_1:9;
then A190:
(
i + 1
in Seg ((Sum (Len J)) + (len J)) &
k <= i + 1 )
by NAT_1:13;
then
r /. (i + 1) = r . (i + 1)
by A28, PARTFUN1:def 8;
then reconsider k1 =
r . (i + 1) as
Element of
NAT ;
set i1 =
i + 1;
A191:
S2[
i + 1,
k1]
by A27, A190;
A192:
(i + 1) -' k = (i + 1) - k
by A190, XREAL_1:235;
then
(
Sum ((Len J) | (k -' 1)) <= (i -' k) + 1 &
(i + 1) -' k = (i -' k) + 1 )
by A182, A189, NAT_1:12;
then A193:
k <= k1
by A182, A27, A190;
k = k1
proof
assume A194:
k <> k1
;
:: thesis: contradiction
then A195:
k < k1
by A193, XXREAL_0:1;
then reconsider K1 =
k1 - 1 as
Element of
NAT by NAT_1:20;
k1 = K1 + 1
;
then
(
k1 -' 1
= K1 &
k <= K1 &
(i + 1) - k1 = (i + 1) -' k1 )
by A191, A195, NAT_1:13, NAT_D:34, XREAL_1:235;
then
(
Sum ((Len J) | k) <= Sum ((Len J) | K1) &
Sum ((Len J) | K1) <= (i + 1) -' k1 &
(i + 1) -' k1 <= (i + 1) -' k &
(i + 1) -' k1 <> (i + 1) -' k )
by A194, A192, A27, A190, A193, NAT_D:41, POLYNOM3:18;
then
(
Sum ((Len J) | k) <= (i + 1) -' k1 &
(i + 1) -' k1 < (i + 1) -' k )
by XXREAL_0:1, XXREAL_0:2;
hence
contradiction
by A192, A187, A189, XXREAL_0:2;
:: thesis: verum
end; then A196:
(
B . (i + 1) = b1 . ((i -' k) + 1) &
dom B c= dom Bf )
by A187, A189, A190, A192, A51, FINSEQ_1:39;
then
(
Bf . (i + 1) = b1 . ((i -' k) + 1) &
i + 1
in dom Bf )
by A190, A52, FINSEQ_1:def 7;
then
Bf /. (i + 1) = b1 . ((i -' k) + 1)
by PARTFUN1:def 8;
then F . (Bf /. i) =
Bf /. (i + 1)
by A181, A180, A188, FINSEQ_1:def 7
.=
(0. V1) + (Bf /. (i + 1))
by RLVECT_1:def 7
.=
((0. K) * (Bf /. i)) + (Bf /. (i + 1))
by VECTSP_1:59
;
hence
(
F . (Bf /. i) = (0. K) * (Bf /. i) or (
i + 1
in dom Bf &
F . (Bf /. i) = ((0. K) * (Bf /. i)) + (Bf /. (i + 1)) ) )
by A196, A190, A52;
:: thesis: verum end; end;
end;
then consider J being
non-empty FinSequence_of_Jordan_block of
0. K,
K such that A199:
AutMt F,
Bf,
Bf = block_diagonal J,
(0. K)
by Th28;
hence
ex
J being
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
i being
Nat st
i in dom J holds
(Len J) . i <> 0 ) )
by A199;
:: thesis: verum
end;
A201:
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A3);
let V1 be finite-dimensional VectSp of K; :: thesis: 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)
let F be nilpotent linear-transformation of V1,V1; :: thesis: 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)
S1[ deg F]
by A201;
then consider J being FinSequence_of_Jordan_block of 0. K,K, b1 being OrdBasis of V1 such that
A202:
AutMt F,b1,b1 = block_diagonal J,(0. K)
and
A203:
for i being Nat st i in dom J holds
(Len J) . i <> 0
;
then
J is non-empty
by FUNCT_1:def 15;
hence
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)
by A202; :: thesis: verum