let K be 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))
defpred S1[ Nat] means 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 $1 = card { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } & ( 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));
A1:
S1[ 0 ]
proof
let V1,
V2 be
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 0 = card { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } & ( 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))let b1 be
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 0 = card { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } & ( 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))let b2 be
OrdBasis of
V2;
for L being Element of K st len b1 = len b2 holds
for F being linear-transformation of V1,V2 st 0 = card { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } & ( 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))let L be
Element of
K;
( len b1 = len b2 implies for F being linear-transformation of V1,V2 st 0 = card { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } & ( 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)) )
assume
len b1 = len b2
;
for F being linear-transformation of V1,V2 st 0 = card { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } & ( 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))
set Lb =
len b1;
reconsider J =
{} as
FinSequence_of_Jordan_block of
L,
K by Th10;
let F be
linear-transformation of
V1,
V2;
( 0 = card { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } & ( 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)) ) ) ) implies ex J being non-empty FinSequence_of_Jordan_block of L,K st AutMt (F,b1,b2) = block_diagonal (J,(0. K)) )
assume that A2:
0 = card { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) }
and A3:
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)) ) )
;
ex J being non-empty FinSequence_of_Jordan_block of L,K st AutMt (F,b1,b2) = block_diagonal (J,(0. K))
reconsider J =
J as
non-empty FinSequence_of_Jordan_block of
L,
K ;
take
J
;
AutMt (F,b1,b2) = block_diagonal (J,(0. K))
len b1 = 0
then
len (AutMt (F,b1,b2)) = 0
by MATRIX_0:def 2;
then
AutMt (
F,
b1,
b2)
= {}
;
hence
AutMt (
F,
b1,
b2)
= block_diagonal (
J,
(0. K))
by MATRIXJ1:22;
verum
end;
A6:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A7:
S1[
n]
;
S1[n + 1]
set n1 =
n + 1;
let V1,
V2 be
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 n + 1 = card { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } & ( 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))let b1 be
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 n + 1 = card { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } & ( 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))let b2 be
OrdBasis of
V2;
for L being Element of K st len b1 = len b2 holds
for F being linear-transformation of V1,V2 st n + 1 = card { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } & ( 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))let L be
Element of
K;
( len b1 = len b2 implies for F being linear-transformation of V1,V2 st n + 1 = card { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } & ( 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)) )
assume A8:
len b1 = len b2
;
for F being linear-transformation of V1,V2 st n + 1 = card { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } & ( 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))
A9:
dom b1 = dom b2
by A8, FINSEQ_3:29;
set Lb =
len b1;
let F be
linear-transformation of
V1,
V2;
( n + 1 = card { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } & ( 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)) ) ) ) implies ex J being non-empty FinSequence_of_Jordan_block of L,K st AutMt (F,b1,b2) = block_diagonal (J,(0. K)) )
assume that A10:
n + 1
= card { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) }
and A11:
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)) ) )
;
ex J being non-empty FinSequence_of_Jordan_block of L,K st AutMt (F,b1,b2) = block_diagonal (J,(0. K))
set FF =
{ i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } ;
reconsider FF =
{ i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } as
finite set by A10;
consider x being
object such that A12:
x in FF
by A10, CARD_1:27, XBOOLE_0:def 1;
ex
ii being
Element of
NAT st
(
ii = x &
ii in dom b1 &
F . (b1 /. ii) = L * (b2 /. ii) )
by A12;
then
dom b1 <> {}
;
then
Seg (len b1) <> {}
by FINSEQ_1:def 3;
then A13:
len b1 <> 0
;
A14:
dom b1 = Seg (len b1)
by FINSEQ_1:def 3;
then A15:
not
(len b1) + 1
in dom b1
by FINSEQ_3:8;
A16:
len b1 in dom b1
by A14, A13, FINSEQ_1:3;
then
F . (b1 /. (len b1)) = L * (b2 /. (len b1))
by A11, A15;
then A17:
len b1 in FF
by A16;
per cases
( n = 0 or n <> 0 )
;
suppose A18:
n = 0
;
ex J being non-empty FinSequence_of_Jordan_block of L,K st AutMt (F,b1,b2) = block_diagonal (J,(0. K))set J =
Jordan_block (
L,
(len b1));
reconsider JJ =
<*(Jordan_block (L,(len b1)))*> as
FinSequence_of_Jordan_block of
L,
K by Th11;
then reconsider JJ =
JJ as
non-empty FinSequence_of_Jordan_block of
L,
K by FUNCT_1:def 9;
reconsider F9 =
F as
Function of
V1,
V2 ;
reconsider BB =
block_diagonal (
JJ,
(0. K)) as
Matrix of
len b1,
len b2,
K by A8, MATRIXJ1:34;
set T =
Mx2Tran (
BB,
b1,
b2);
A20:
block_diagonal (
JJ,
(0. K))
= Jordan_block (
L,
(len b1))
by MATRIXJ1:34;
A21:
now for y being object st y in dom b1 holds
(F9 * b1) . y = ((Mx2Tran (BB,b1,b2)) * b1) . ylet y be
object ;
( y in dom b1 implies (F9 * b1) . y = ((Mx2Tran (BB,b1,b2)) * b1) . y )assume A22:
y in dom b1
;
(F9 * b1) . y = ((Mx2Tran (BB,b1,b2)) * b1) . yreconsider j =
y as
Element of
NAT by A22;
A23:
((Mx2Tran (BB,b1,b2)) * b1) . y = (Mx2Tran (BB,b1,b2)) . (b1 . y)
by A22, FUNCT_1:13;
A24:
b1 /. j = b1 . j
by A22, PARTFUN1:def 6;
A25:
(F9 * b1) . y = F . (b1 . y)
by A22, FUNCT_1:13;
now ((Mx2Tran (BB,b1,b2)) * b1) . y = (F9 * b1) . yper cases
( j = len b1 or j <> len b1 )
;
suppose A26:
j = len b1
;
((Mx2Tran (BB,b1,b2)) * b1) . y = (F9 * b1) . yhence ((Mx2Tran (BB,b1,b2)) * b1) . y =
L * (b2 /. (len b1))
by A20, A22, A23, A24, Th23
.=
(F9 * b1) . y
by A11, A16, A15, A25, A24, A26
;
verum end; suppose A27:
j <> len b1
;
((Mx2Tran (BB,b1,b2)) * b1) . y = (F9 * b1) . y
ex
z being
object st
FF = {z}
by A10, A18, CARD_2:42;
then
FF = {(len b1)}
by A17, TARSKI:def 1;
then
not
j in FF
by A27, TARSKI:def 1;
then A28:
F . (b1 /. j) <> L * (b2 /. j)
by A22;
((Mx2Tran (BB,b1,b2)) * b1) . y = (L * (b2 /. j)) + (b2 /. (j + 1))
by A20, A22, A23, A24, A27, Th23;
hence
((Mx2Tran (BB,b1,b2)) * b1) . y = (F9 * b1) . y
by A11, A22, A25, A24, A28;
verum end; end; end; hence
(F9 * b1) . y = ((Mx2Tran (BB,b1,b2)) * b1) . y
;
verum end; take
JJ
;
AutMt (F,b1,b2) = block_diagonal (JJ,(0. K))A29:
rng b1 c= [#] V1
by FINSEQ_1:def 4;
dom (Mx2Tran (BB,b1,b2)) = [#] V1
by FUNCT_2:def 1;
then A30:
dom ((Mx2Tran (BB,b1,b2)) * b1) = dom b1
by A29, RELAT_1:27;
dom F = [#] V1
by FUNCT_2:def 1;
then
dom (F9 * b1) = dom b1
by A29, RELAT_1:27;
then
F = Mx2Tran (
BB,
b1,
b2)
by A13, A30, A21, FUNCT_1:2, MATRLIN:22;
hence
AutMt (
F,
b1,
b2)
= block_diagonal (
JJ,
(0. K))
by MATRLIN2:36;
verum end; suppose A31:
n <> 0
;
ex J being non-empty FinSequence_of_Jordan_block of L,K st AutMt (F,b1,b2) = block_diagonal (J,(0. K))defpred S2[
Nat]
means ( $1
in FF & $1
< len b1 );
A32:
ex
k being
Nat st
S2[
k]
A37:
for
k being
Nat st
S2[
k] holds
k <= len b1
;
consider m being
Nat such that A38:
S2[
m]
and A39:
for
k being
Nat st
S2[
k] holds
k <= m
from NAT_1:sch 6(A37, A32);
set b1m =
b1 | m;
A40:
len (b1 | m) = m
by A38, FINSEQ_1:59;
set JB =
Jordan_block (
L,
((len b1) -' m));
reconsider JJ =
<*(Jordan_block (L,((len b1) -' m)))*> as
FinSequence_of_Jordan_block of
L,
K by Th11;
set b19m =
b1 /^ m;
A41:
len (b1 /^ m) = (len b1) - m
by A38, RFINSEQ:def 1;
set b29m =
b2 /^ m;
A42:
len (b2 /^ m) = (len b1) - m
by A8, A38, RFINSEQ:def 1;
set b2m =
b2 | m;
A43:
len (b2 | m) = m
by A8, A38, FINSEQ_1:59;
reconsider Rb2 =
rng (b2 | m),
Rb29 =
rng (b2 /^ m) as
linearly-independent Subset of
V2 by MATRLIN2:22, MATRLIN2:23;
reconsider Rb1 =
rng (b1 | m),
Rb19 =
rng (b1 /^ m) as
linearly-independent Subset of
V1 by MATRLIN2:22, MATRLIN2:23;
set Lb1 =
Lin Rb1;
set Lb2 =
Lin Rb2;
set Lb19 =
Lin Rb19;
set Lb29 =
Lin Rb29;
set FRb1 =
F .: Rb1;
A44:
rng (F | (Lin Rb1)) = F .: the
carrier of
(Lin Rb1)
by RELAT_1:115;
reconsider b2m =
b2 | m as
OrdBasis of
Lin Rb2 by MATRLIN2:22;
reconsider b1m =
b1 | m as
OrdBasis of
Lin Rb1 by MATRLIN2:22;
A45:
dom b1m = dom b2m
by A40, A43, FINSEQ_3:29;
reconsider b19m =
b1 /^ m as
OrdBasis of
Lin Rb19 by MATRLIN2:23;
reconsider b29m =
b2 /^ m as
OrdBasis of
Lin Rb29 by MATRLIN2:23;
A46:
b2 = b2m ^ b29m
by RFINSEQ:8;
A47:
b1 = b1m ^ b19m
by RFINSEQ:8;
then A48:
dom b1m c= dom b1
by FINSEQ_1:26;
A49:
for
i being
Nat holds
( not
i in dom b1m or
(F | (Lin Rb1)) . (b1m /. i) = L * (b2m /. i) or (
i + 1
in dom b1m &
(F | (Lin Rb1)) . (b1m /. i) = (L * (b2m /. i)) + (b2m /. (i + 1)) ) )
proof
let i be
Nat;
( not i in dom b1m or (F | (Lin Rb1)) . (b1m /. i) = L * (b2m /. i) or ( i + 1 in dom b1m & (F | (Lin Rb1)) . (b1m /. i) = (L * (b2m /. i)) + (b2m /. (i + 1)) ) )
assume A50:
i in dom b1m
;
( (F | (Lin Rb1)) . (b1m /. i) = L * (b2m /. i) or ( i + 1 in dom b1m & (F | (Lin Rb1)) . (b1m /. i) = (L * (b2m /. i)) + (b2m /. (i + 1)) ) )
A51:
b1m . i = b1m /. i
by A50, PARTFUN1:def 6;
set i1 =
i + 1;
A52:
F . (b1m /. i) = (F | (Lin Rb1)) . (b1m /. i)
by FUNCT_1:49;
A53:
(
b2 /. i = b2 . i &
b2 . i = b2m . i )
by A9, A46, A48, A45, A50, FINSEQ_1:def 7, PARTFUN1:def 6;
A54:
(
b1 /. i = b1 . i &
b1 . i = b1m . i )
by A47, A48, A50, FINSEQ_1:def 7, PARTFUN1:def 6;
per cases
( F . (b1 /. i) = L * (b2 /. i) or ( i + 1 in dom b1 & F . (b1 /. i) = (L * (b2 /. i)) + (b2 /. (i + 1)) ) )
by A11, A48, A50;
suppose A55:
(
i + 1
in dom b1 &
F . (b1 /. i) = (L * (b2 /. i)) + (b2 /. (i + 1)) )
;
( (F | (Lin Rb1)) . (b1m /. i) = L * (b2m /. i) or ( i + 1 in dom b1m & (F | (Lin Rb1)) . (b1m /. i) = (L * (b2m /. i)) + (b2m /. (i + 1)) ) )reconsider rngb2 =
rng b2 as
Basis of
V2 by MATRLIN:def 2;
A56:
i + 1
<= m
proof
assume
i + 1
> m
;
contradiction
then A57:
i >= m
by NAT_1:13;
i <= m
by A40, A50, FINSEQ_3:25;
then A58:
i = m
by A57, XXREAL_0:1;
ex
ii being
Element of
NAT st
(
m = ii &
ii in dom b1 &
F . (b1 /. ii) = L * (b2 /. ii) )
by A38;
then
F . (b1 /. i) = (L * (b2 /. i)) + (0. V2)
by A58, RLVECT_1:def 4;
then A59:
b2 /. (i + 1) = 0. V2
by A55, RLVECT_1:8;
A60:
rngb2 is
linearly-independent
by VECTSP_7:def 3;
(
b2 /. (i + 1) = b2 . (i + 1) &
b2 . (i + 1) in rngb2 )
by A9, A55, FUNCT_1:def 3, PARTFUN1:def 6;
hence
contradiction
by A59, A60, VECTSP_7:2;
verum
end; A61:
1
<= i + 1
by NAT_1:11;
then A62:
i + 1
in dom b1m
by A40, A56, FINSEQ_3:25;
then A63:
b2m . (i + 1) = b2m /. (i + 1)
by A45, PARTFUN1:def 6;
A64:
L * (b2 /. i) = L * (b2m /. i)
by A45, A50, A53, PARTFUN1:def 6, VECTSP_4:14;
(
b2 /. (i + 1) = b2 . (i + 1) &
b2 . (i + 1) = b2m . (i + 1) )
by A9, A46, A48, A45, A62, FINSEQ_1:def 7, PARTFUN1:def 6;
hence
(
(F | (Lin Rb1)) . (b1m /. i) = L * (b2m /. i) or (
i + 1
in dom b1m &
(F | (Lin Rb1)) . (b1m /. i) = (L * (b2m /. i)) + (b2m /. (i + 1)) ) )
by A40, A54, A51, A52, A55, A56, A61, A63, A64, FINSEQ_3:25, VECTSP_4:13;
verum end; end;
end;
F .: Rb1 c= the
carrier of
(Lin Rb2)
then
( the
carrier of
(Lin (F .: Rb1)) = F .: the
carrier of
(Lin Rb1) &
Lin (F .: Rb1) is
Subspace of
Lin Rb2 )
by VECTSP11:42, VECTSP_9:16;
then
F .: the
carrier of
(Lin Rb1) c= the
carrier of
(Lin Rb2)
by VECTSP_4:def 2;
then reconsider FL =
F | (Lin Rb1) as
linear-transformation of
(Lin Rb1),
(Lin Rb2) by A44, Lm4, FUNCT_2:6;
A69:
for
i being
Nat holds
( not
i in dom b1m or
FL . (b1m /. i) = L * (b2m /. i) or (
i + 1
in dom b1m &
FL . (b1m /. i) = (L * (b2m /. i)) + (b2m /. (i + 1)) ) )
by A49;
set FF1 =
{ i where i is Element of NAT : ( i in dom b1m & FL . (b1m /. i) = L * (b2m /. i) ) } ;
A70:
FF \ {(len b1)} c= { i where i is Element of NAT : ( i in dom b1m & FL . (b1m /. i) = L * (b2m /. i) ) }
proof
let x be
object ;
TARSKI:def 3 ( not x in FF \ {(len b1)} or x in { i where i is Element of NAT : ( i in dom b1m & FL . (b1m /. i) = L * (b2m /. i) ) } )
assume A71:
x in FF \ {(len b1)}
;
x in { i where i is Element of NAT : ( i in dom b1m & FL . (b1m /. i) = L * (b2m /. i) ) }
A72:
x <> len b1
by A71, ZFMISC_1:56;
x in FF
by A71;
then consider j being
Element of
NAT such that A73:
j = x
and A74:
j in dom b1
and A75:
F . (b1 /. j) = L * (b2 /. j)
;
j <= len b1
by A74, FINSEQ_3:25;
then
j < len b1
by A72, A73, XXREAL_0:1;
then A76:
j <= m
by A39, A71, A73;
1
<= j
by A74, FINSEQ_3:25;
then A77:
j in dom b1m
by A40, A76, FINSEQ_3:25;
then A78:
(
b1m /. j = b1m . j &
b1m . j = b1 . j )
by A47, FINSEQ_1:def 7, PARTFUN1:def 6;
A79:
(
FL . (b1m /. j) = F . (b1m /. j) &
b1 /. j = b1 . j )
by A48, A77, FUNCT_1:49, PARTFUN1:def 6;
(
b2m . j = b2 . j &
b2 /. j = b2 . j )
by A9, A46, A48, A45, A77, FINSEQ_1:def 7, PARTFUN1:def 6;
then
FL . (b1m /. j) = L * (b2m /. j)
by A45, A75, A77, A78, A79, PARTFUN1:def 6, VECTSP_4:14;
hence
x in { i where i is Element of NAT : ( i in dom b1m & FL . (b1m /. i) = L * (b2m /. i) ) }
by A73, A77;
verum
end;
{ i where i is Element of NAT : ( i in dom b1m & FL . (b1m /. i) = L * (b2m /. i) ) } c= FF \ {(len b1)}
proof
let x be
object ;
TARSKI:def 3 ( not x in { i where i is Element of NAT : ( i in dom b1m & FL . (b1m /. i) = L * (b2m /. i) ) } or x in FF \ {(len b1)} )
assume
x in { i where i is Element of NAT : ( i in dom b1m & FL . (b1m /. i) = L * (b2m /. i) ) }
;
x in FF \ {(len b1)}
then consider j being
Element of
NAT such that A80:
x = j
and A81:
j in dom b1m
and A82:
FL . (b1m /. j) = L * (b2m /. j)
;
A83:
(
b1m /. j = b1m . j &
b1m . j = b1 . j )
by A47, A81, FINSEQ_1:def 7, PARTFUN1:def 6;
A84:
(
FL . (b1m /. j) = F . (b1m /. j) &
b1 /. j = b1 . j )
by A48, A81, FUNCT_1:49, PARTFUN1:def 6;
(
b2m . j = b2 . j &
b2 /. j = b2 . j )
by A9, A46, A48, A45, A81, FINSEQ_1:def 7, PARTFUN1:def 6;
then
F . (b1 /. j) = L * (b2 /. j)
by A45, A81, A82, A83, A84, PARTFUN1:def 6, VECTSP_4:14;
then A85:
j in FF
by A48, A81;
j <= m
by A40, A81, FINSEQ_3:25;
hence
x in FF \ {(len b1)}
by A38, A80, A85, ZFMISC_1:56;
verum
end; then
{ i where i is Element of NAT : ( i in dom b1m & FL . (b1m /. i) = L * (b2m /. i) ) } = FF \ {(len b1)}
by A70, XBOOLE_0:def 10;
then
card { i where i is Element of NAT : ( i in dom b1m & FL . (b1m /. i) = L * (b2m /. i) ) } = n
by A10, A17, STIRL2_1:55;
then consider J being
non-empty FinSequence_of_Jordan_block of
L,
K such that A86:
AutMt (
FL,
b1m,
b2m)
= block_diagonal (
J,
(0. K))
by A7, A40, A43, A69;
set JJJ =
J ^ JJ;
A87:
(len b1) - m = (len b1) -' m
by A38, XREAL_1:233;
len b19m = len b29m
by A8, A38, A41, RFINSEQ:def 1;
then reconsider JB =
Jordan_block (
L,
((len b1) -' m)) as
Matrix of
len b19m,
len b29m,
K by A41, A87;
A95:
width JB = len b19m
by A41, A42, MATRIX_0:24;
reconsider JJJ =
J ^ JJ as
non-empty FinSequence_of_Jordan_block of
L,
K by A88, FUNCT_1:def 9;
take
JJJ
;
AutMt (F,b1,b2) = block_diagonal (JJJ,(0. K))reconsider F9 =
F as
Function of
V1,
V2 ;
reconsider B =
block_diagonal (
J,
(0. K)) as
Matrix of
len b1m,
len b2m,
K by A86;
A96:
width B = len b1m
by A40, A43, MATRIX_0:24;
A97:
(
Sum (Len <*B,JB*>) = (len B) + (len JB) &
Sum (Width <*B,JB*>) = (width B) + (width JB) )
by MATRIXJ1:16, MATRIXJ1:20;
set BB =
block_diagonal (
<*B,JB*>,
(0. K));
A98:
len B = len b1m
by A40, A43, MATRIX_0:24;
A99:
Sum (Len <*B,JB*>) = len b1
by A40, A41, A42, A97, A96, A95, A98, MATRIX_0:24;
Sum (Width <*B,JB*>) = len b2
by A8, A40, A41, A97, A96, A95;
then reconsider BB =
block_diagonal (
<*B,JB*>,
(0. K)) as
Matrix of
len b1,
len b2,
K by A99;
set T =
Mx2Tran (
BB,
b1,
b2);
A100:
dom b19m = dom b29m
by A41, A42, FINSEQ_3:29;
A101:
now for x being object st x in dom b1 holds
(F9 * b1) . x = ((Mx2Tran (BB,b1,b2)) * b1) . xlet x be
object ;
( x in dom b1 implies (F9 * b1) . x = ((Mx2Tran (BB,b1,b2)) * b1) . x )assume A102:
x in dom b1
;
(F9 * b1) . x = ((Mx2Tran (BB,b1,b2)) * b1) . xreconsider I =
x as
Element of
NAT by A102;
A103:
((Mx2Tran (BB,b1,b2)) * b1) . x = (Mx2Tran (BB,b1,b2)) . (b1 . I)
by A102, FUNCT_1:13;
A104:
b1 . I = b1 /. I
by A102, PARTFUN1:def 6;
A105:
(F9 * b1) . x = F . (b1 . I)
by A102, FUNCT_1:13;
now ((Mx2Tran (BB,b1,b2)) * b1) . x = (F9 * b1) . xper cases
( I in dom b1m or ex j being Nat st
( j in dom b19m & I = (len b1m) + j ) )
by A47, A102, FINSEQ_1:25;
suppose A106:
I in dom b1m
;
((Mx2Tran (BB,b1,b2)) * b1) . x = (F9 * b1) . xthen A107:
(
b1m /. I = b1m . I &
b1 . I = b1m . I )
by A47, FINSEQ_1:def 7, PARTFUN1:def 6;
A108:
FL . (b1m /. I) = F . (b1m /. I)
by FUNCT_1:49;
thus ((Mx2Tran (BB,b1,b2)) * b1) . x =
(Mx2Tran (B,b1m,b2m)) . (b1m /. I)
by A40, A43, A41, A42, A47, A46, A96, A95, A103, A104, A106, Th19
.=
FL . (b1m /. I)
by A86, MATRLIN2:34
.=
(F9 * b1) . x
by A102, A108, A107, FUNCT_1:13
;
verum end; suppose
ex
j being
Nat st
(
j in dom b19m &
I = (len b1m) + j )
;
(F9 * b1) . x = ((Mx2Tran (BB,b1,b2)) * b1) . xthen consider j being
Nat such that A109:
j in dom b19m
and A110:
I = (len b1m) + j
;
now (F9 * b1) . x = (Mx2Tran (JB,b19m,b29m)) . (b19m /. j)per cases
( j = len b19m or j <> len b19m )
;
suppose A111:
j = len b19m
;
(F9 * b1) . x = (Mx2Tran (JB,b19m,b29m)) . (b19m /. j)A112:
(
b2 . I = b29m . j &
b2 /. I = b2 . I )
by A9, A40, A43, A46, A100, A102, A109, A110, FINSEQ_1:def 7, PARTFUN1:def 6;
thus (F9 * b1) . x =
L * (b2 /. I)
by A11, A16, A15, A40, A41, A105, A104, A110, A111
.=
L * (b29m /. j)
by A100, A109, A112, PARTFUN1:def 6, VECTSP_4:14
.=
(Mx2Tran (JB,b19m,b29m)) . (b19m /. j)
by A109, A111, Th23
;
verum end; suppose A113:
j <> len b19m
;
(F9 * b1) . x = (Mx2Tran (JB,b19m,b29m)) . (b19m /. j)A114:
(F9 * b1) . x = (L * (b2 /. I)) + (b2 /. (I + 1))
proof
assume
(F9 * b1) . x <> (L * (b2 /. I)) + (b2 /. (I + 1))
;
contradiction
then
F . (b1 /. I) = L * (b2 /. I)
by A11, A102, A105, A104;
then A115:
I in FF
by A102;
(
I <> len b1 &
I <= len b1 )
by A40, A41, A102, A110, A113, FINSEQ_3:25;
then
I < len b1
by XXREAL_0:1;
then
(len b1m) + j <= (len b1m) + 0
by A39, A40, A110, A115;
then
j <= 0
by XREAL_1:6;
hence
contradiction
by A109, FINSEQ_3:25;
verum
end;
j <= len b19m
by A109, FINSEQ_3:25;
then
j < len b19m
by A113, XXREAL_0:1;
then
( 1
<= j + 1 &
j + 1
<= len b19m )
by NAT_1:11, NAT_1:13;
then A116:
j + 1
in dom b19m
by FINSEQ_3:25;
then
(
b29m /. (j + 1) = b29m . (j + 1) &
b2 . ((len b1m) + (j + 1)) = b29m . (j + 1) )
by A40, A43, A46, A100, FINSEQ_1:def 7, PARTFUN1:def 6;
then A117:
b29m /. (j + 1) = b2 /. (I + 1)
by A9, A47, A110, A116, FINSEQ_1:28, PARTFUN1:def 6;
(
b2 . I = b29m . j &
b2 /. I = b2 . I )
by A9, A40, A43, A46, A100, A102, A109, A110, FINSEQ_1:def 7, PARTFUN1:def 6;
then
L * (b29m /. j) = L * (b2 /. I)
by A100, A109, PARTFUN1:def 6, VECTSP_4:14;
then (L * (b2 /. I)) + (b2 /. (I + 1)) =
(L * (b29m /. j)) + (b29m /. (j + 1))
by A117, VECTSP_4:13
.=
(Mx2Tran (JB,b19m,b29m)) . (b19m /. j)
by A109, A113, Th23
;
hence
(F9 * b1) . x = (Mx2Tran (JB,b19m,b29m)) . (b19m /. j)
by A114;
verum end; end; end; hence
(F9 * b1) . x = ((Mx2Tran (BB,b1,b2)) * b1) . x
by A40, A43, A41, A42, A47, A46, A96, A95, A103, A104, A109, A110, Th19;
verum end; end; end; hence
(F9 * b1) . x = ((Mx2Tran (BB,b1,b2)) * b1) . x
;
verum end; A118:
rng b1 c= [#] V1
by FINSEQ_1:def 4;
dom (Mx2Tran (BB,b1,b2)) = [#] V1
by FUNCT_2:def 1;
then A119:
dom ((Mx2Tran (BB,b1,b2)) * b1) = dom b1
by A118, RELAT_1:27;
dom F = [#] V1
by FUNCT_2:def 1;
then
dom (F9 * b1) = dom b1
by A118, RELAT_1:27;
then
(
block_diagonal (
JJJ,
(0. K))
= block_diagonal (
<*B,JB*>,
(0. K)) &
F = Mx2Tran (
BB,
b1,
b2) )
by A13, A119, A101, FUNCT_1:2, MATRIXJ1:35, MATRLIN:22;
hence
AutMt (
F,
b1,
b2)
= block_diagonal (
JJJ,
(0. K))
by MATRLIN2:36;
verum end; end;
end;
let V1, V2 be 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))
let b1 be 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))
let b2 be 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))
let L be Element of K; ( len b1 = len b2 implies 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)) )
assume A120:
len b1 = len b2
; 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))
let F be linear-transformation of V1,V2; ( ( 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)) ) ) ) implies ex J being non-empty FinSequence_of_Jordan_block of L,K st AutMt (F,b1,b2) = block_diagonal (J,(0. K)) )
assume A121:
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)) ) )
; ex J being non-empty FinSequence_of_Jordan_block of L,K st AutMt (F,b1,b2) = block_diagonal (J,(0. K))
set FF = { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } ;
{ i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } c= dom b1
then reconsider FF = { i where i is Element of NAT : ( i in dom b1 & F . (b1 /. i) = L * (b2 /. i) ) } as finite set ;
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A6);
then
S1[ card FF]
;
hence
ex J being non-empty FinSequence_of_Jordan_block of L,K st AutMt (F,b1,b2) = block_diagonal (J,(0. K))
by A120, A121; verum