let n be Nat; for K being Field
for M being Matrix of n,K
for M1, M2 being Upper_Triangular_Matrix of n,K st M = M1 * M2 holds
( M is Upper_Triangular_Matrix of n,K & diagonal_of_Matrix M = mlt (diagonal_of_Matrix M1),(diagonal_of_Matrix M2) )
let K be Field; for M being Matrix of n,K
for M1, M2 being Upper_Triangular_Matrix of n,K st M = M1 * M2 holds
( M is Upper_Triangular_Matrix of n,K & diagonal_of_Matrix M = mlt (diagonal_of_Matrix M1),(diagonal_of_Matrix M2) )
let M be Matrix of n,K; for M1, M2 being Upper_Triangular_Matrix of n,K st M = M1 * M2 holds
( M is Upper_Triangular_Matrix of n,K & diagonal_of_Matrix M = mlt (diagonal_of_Matrix M1),(diagonal_of_Matrix M2) )
reconsider N = n as Element of NAT by ORDINAL1:def 13;
let M1, M2 be Upper_Triangular_Matrix of n,K; ( M = M1 * M2 implies ( M is Upper_Triangular_Matrix of n,K & diagonal_of_Matrix M = mlt (diagonal_of_Matrix M1),(diagonal_of_Matrix M2) ) )
assume A1:
M = M1 * M2
; ( M is Upper_Triangular_Matrix of n,K & diagonal_of_Matrix M = mlt (diagonal_of_Matrix M1),(diagonal_of_Matrix M2) )
set SS = [:(Seg n),(Seg n):];
set KK = the carrier of K;
A2:
len M2 = n
by MATRIX_1:25;
A3:
width M1 = n
by MATRIX_1:25;
now set n0 =
n |-> (0. K);
let i,
j be
Nat;
( [i,j] in Indices M & i > j implies 0. K = M * i,j )assume that A4:
[i,j] in Indices M
and A5:
i > j
;
0. K = M * i,jset C =
Col M2,
j;
set L =
Line M1,
i;
reconsider L9 =
Line M1,
i,
C9 =
Col M2,
j as
Element of
N -tuples_on the
carrier of
K by MATRIX_1:25;
set m =
mlt L9,
C9;
A6:
len (mlt L9,C9) = n
by FINSEQ_1:def 18;
A7:
now let k be
Nat;
( 1 <= k & k <= n implies (mlt L9,C9) . b1 = (n |-> (0. K)) . b1 )assume that A8:
1
<= k
and A9:
k <= n
;
(mlt L9,C9) . b1 = (n |-> (0. K)) . b1A10:
k in NAT
by ORDINAL1:def 13;
then A11:
k in Seg n
by A8, A9;
then A12:
(n |-> (0. K)) . k = 0. K
by FINSEQ_2:71;
A13:
Indices M2 = [:(Seg n),(Seg n):]
by MATRIX_1:25;
A14:
Indices M1 = [:(Seg n),(Seg n):]
by MATRIX_1:25;
A15:
(Line M1,i) . k = M1 * i,
k
by A3, A11, MATRIX_1:def 8;
A16:
Indices M = [:(Seg n),(Seg n):]
by MATRIX_1:25;
then
i in Seg n
by A4, ZFMISC_1:106;
then A17:
[i,k] in Indices M1
by A11, A14, ZFMISC_1:106;
j in Seg n
by A4, A16, ZFMISC_1:106;
then A18:
[k,j] in Indices M2
by A11, A13, ZFMISC_1:106;
A19:
dom (mlt L9,C9) = Seg n
by A6, FINSEQ_1:def 3;
A20:
k in Seg n
by A8, A9, A10;
dom M2 = Seg n
by A2, FINSEQ_1:def 3;
then A21:
(Col M2,j) . k = M2 * k,
j
by A11, MATRIX_1:def 9;
per cases
( k <= j or k > j )
;
suppose
k <= j
;
(mlt L9,C9) . b1 = (n |-> (0. K)) . b1then
k < i
by A5, XXREAL_0:2;
then A22:
M1 * i,
k = 0. K
by A17, MATRIX_2:def 3;
(mlt L9,C9) . k = (M1 * i,k) * (M2 * k,j)
by A15, A21, A19, A20, FVSUM_1:73;
hence
(mlt L9,C9) . k = (n |-> (0. K)) . k
by A12, A22, VECTSP_1:44;
verum end; suppose
k > j
;
(mlt L9,C9) . b1 = (n |-> (0. K)) . b1then A23:
M2 * k,
j = 0. K
by A18, MATRIX_2:def 3;
(mlt L9,C9) . k = (M1 * i,k) * (M2 * k,j)
by A15, A21, A19, A20, FVSUM_1:73;
hence
(mlt L9,C9) . k = (n |-> (0. K)) . k
by A12, A23, VECTSP_1:44;
verum end; end;
len (n |-> (0. K)) = n
by FINSEQ_1:def 18;
then
mlt L9,
C9 = n |-> (0. K)
by A6, A7, FINSEQ_1:18;
hence 0. K =
(Line M1,i) "*" (Col M2,j)
by MATRIX_3:13
.=
M * i,
j
by A1, A3, A2, A4, MATRIX_3:def 4
;
verum end;
hence
M is Upper_Triangular_Matrix of n,K
by MATRIX_2:def 3; diagonal_of_Matrix M = mlt (diagonal_of_Matrix M1),(diagonal_of_Matrix M2)
set D2 = diagonal_of_Matrix M2;
set D1 = diagonal_of_Matrix M1;
set DM = diagonal_of_Matrix M;
A24:
len (diagonal_of_Matrix M2) = n
by MATRIX_3:def 10;
len (diagonal_of_Matrix M1) = n
by MATRIX_3:def 10;
then reconsider D19 = diagonal_of_Matrix M1, D29 = diagonal_of_Matrix M2 as Element of N -tuples_on the carrier of K by A24, FINSEQ_2:110;
set m = mlt D19,D29;
A25:
len (mlt D19,D29) = n
by FINSEQ_1:def 18;
A26:
now set aa = the
addF of
K;
let i be
Nat;
( 1 <= i & i <= n implies (mlt D19,D29) . i = (diagonal_of_Matrix M) . i )assume that A27:
1
<= i
and A28:
i <= n
;
(mlt D19,D29) . i = (diagonal_of_Matrix M) . i
i in NAT
by ORDINAL1:def 13;
then A29:
i in Seg n
by A27, A28;
then A30:
(diagonal_of_Matrix M) . i = M * i,
i
by MATRIX_3:def 10;
set C =
Col M2,
i;
set L =
Line M1,
i;
reconsider L9 =
Line M1,
i,
C9 =
Col M2,
i as
Element of
N -tuples_on the
carrier of
K by MATRIX_1:25;
set mLC =
mlt L9,
C9;
A31:
the
addF of
K is
having_a_unity
by FVSUM_1:10;
Indices M = [:(Seg n),(Seg n):]
by MATRIX_1:25;
then
[i,i] in Indices M
by A29, ZFMISC_1:106;
then A32:
(diagonal_of_Matrix M) . i = (Line M1,i) "*" (Col M2,i)
by A1, A3, A2, A30, MATRIX_3:def 4;
A33:
(diagonal_of_Matrix M2) . i = M2 * i,
i
by A29, MATRIX_3:def 10;
A34:
(diagonal_of_Matrix M1) . i = M1 * i,
i
by A29, MATRIX_3:def 10;
len (mlt L9,C9) = n
by FINSEQ_1:def 18;
then consider f being
Function of
NAT ,the
carrier of
K such that A35:
f . 1
= (mlt L9,C9) . 1
and A36:
for
k being
Element of
NAT st
0 <> k &
k < n holds
f . (k + 1) = the
addF of
K . (f . k),
((mlt L9,C9) . (k + 1))
and A37:
(diagonal_of_Matrix M) . i = f . n
by A27, A28, A32, A31, FINSOP_1:def 1;
defpred S1[
Nat]
means ( 1
<= $1 & $1
<= n implies ( ( $1
< i implies
f . $1
= 0. K ) & ( $1
>= i implies
f . $1
= (mlt D19,D29) . i ) ) );
i in dom (mlt D19,D29)
by A25, A29, FINSEQ_1:def 3;
then A38:
(mlt D19,D29) . i = (M1 * i,i) * (M2 * i,i)
by A34, A33, FVSUM_1:73;
A39:
for
j being
Nat st
j in Seg n holds
( (
j <> i implies
(mlt L9,C9) . j = 0. K ) & (
j = i implies
(mlt L9,C9) . j = (mlt D19,D29) . i ) )
proof
i in NAT
by ORDINAL1:def 13;
then A40:
i in Seg n
by A27, A28;
let j be
Nat;
( j in Seg n implies ( ( j <> i implies (mlt L9,C9) . j = 0. K ) & ( j = i implies (mlt L9,C9) . j = (mlt D19,D29) . i ) ) )
assume A41:
j in Seg n
;
( ( j <> i implies (mlt L9,C9) . j = 0. K ) & ( j = i implies (mlt L9,C9) . j = (mlt D19,D29) . i ) )
A42:
(Line M1,i) . j = M1 * i,
j
by A3, A41, MATRIX_1:def 8;
Indices M1 = [:(Seg n),(Seg n):]
by MATRIX_1:25;
then A43:
[i,j] in Indices M1
by A41, A40, ZFMISC_1:106;
dom M2 = Seg n
by A2, FINSEQ_1:def 3;
then A44:
(Col M2,i) . j = M2 * j,
i
by A41, MATRIX_1:def 9;
Indices M2 = [:(Seg n),(Seg n):]
by MATRIX_1:25;
then A45:
[j,i] in Indices M2
by A41, A40, ZFMISC_1:106;
per cases
( i <> j or i = j )
;
suppose A46:
i <> j
;
( ( j <> i implies (mlt L9,C9) . j = 0. K ) & ( j = i implies (mlt L9,C9) . j = (mlt D19,D29) . i ) )then
(
i < j or
j < i )
by XXREAL_0:1;
then A47:
(
M1 * i,
j = 0. K or
M2 * j,
i = 0. K )
by A43, A45, MATRIX_2:def 3;
(mlt L9,C9) . j = (M1 * i,j) * (M2 * j,i)
by A41, A42, A44, FVSUM_1:74;
hence
( (
j <> i implies
(mlt L9,C9) . j = 0. K ) & (
j = i implies
(mlt L9,C9) . j = (mlt D19,D29) . i ) )
by A46, A47, VECTSP_1:44;
verum end;
end; A48:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A49:
S1[
k]
;
S1[k + 1]
set k1 =
k + 1;
assume that A50:
1
<= k + 1
and A51:
k + 1
<= n
;
( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt D19,D29) . i ) )
A52:
k + 1
in Seg n
by A50, A51;
per cases
( k = 0 or k > 0 )
;
suppose A53:
k > 0
;
( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt D19,D29) . i ) )A54:
k in NAT
by ORDINAL1:def 13;
k < n
by A51, NAT_1:13;
then A55:
f . (k + 1) = the
addF of
K . (f . k),
((mlt L9,C9) . (k + 1))
by A36, A53, A54;
per cases
( k + 1 < i or k + 1 = i or k + 1 > i )
by XXREAL_0:1;
suppose A56:
k + 1
< i
;
( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt D19,D29) . i ) )end; suppose A57:
k + 1
= i
;
( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt D19,D29) . i ) )then
f . (k + 1) = (0. K) + ((M1 * i,i) * (M2 * i,i))
by A38, A39, A49, A51, A52, A53, A55, NAT_1:13, NAT_1:14;
hence
( (
k + 1
< i implies
f . (k + 1) = 0. K ) & (
k + 1
>= i implies
f . (k + 1) = (mlt D19,D29) . i ) )
by A38, A57, RLVECT_1:def 7;
verum end; suppose A58:
k + 1
> i
;
( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt D19,D29) . i ) )then
f . (k + 1) = ((M1 * i,i) * (M2 * i,i)) + (0. K)
by A38, A39, A49, A51, A52, A53, A55, NAT_1:13, NAT_1:14;
hence
( (
k + 1
< i implies
f . (k + 1) = 0. K ) & (
k + 1
>= i implies
f . (k + 1) = (mlt D19,D29) . i ) )
by A38, A58, RLVECT_1:def 7;
verum end; end;
end; A59:
1
<= n
by A27, A28, NAT_1:14;
A60:
S1[
0 ]
;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A60, A48);
hence
(mlt D19,D29) . i = (diagonal_of_Matrix M) . i
by A28, A37, A59;
verum end;
len (diagonal_of_Matrix M) = n
by MATRIX_3:def 10;
hence
diagonal_of_Matrix M = mlt (diagonal_of_Matrix M1),(diagonal_of_Matrix M2)
by A25, A26, FINSEQ_1:18; verum