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 12;
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_0:24;
A3:
width M1 = n
by MATRIX_0:24;
now for i, j being Nat st [i,j] in Indices M & i > j holds
0. K = M * (i,j)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,j)set 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_0:24;
set m =
mlt (
L9,
C9);
A6:
len (mlt (L9,C9)) = n
by CARD_1:def 7;
A7:
now for k being Nat st 1 <= k & k <= n holds
(mlt (L9,C9)) . k = (n |-> (0. K)) . klet 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 Seg n
by A8, A9;
then A11:
(n |-> (0. K)) . k = 0. K
by FINSEQ_2:57;
A12:
Indices M2 = [:(Seg n),(Seg n):]
by MATRIX_0:24;
A13:
Indices M1 = [:(Seg n),(Seg n):]
by MATRIX_0:24;
A14:
(Line (M1,i)) . k = M1 * (
i,
k)
by A3, A10, MATRIX_0:def 7;
A15:
Indices M = [:(Seg n),(Seg n):]
by MATRIX_0:24;
then
i in Seg n
by A4, ZFMISC_1:87;
then A16:
[i,k] in Indices M1
by A10, A13, ZFMISC_1:87;
j in Seg n
by A4, A15, ZFMISC_1:87;
then A17:
[k,j] in Indices M2
by A10, A12, ZFMISC_1:87;
A18:
dom (mlt (L9,C9)) = Seg n
by A6, FINSEQ_1:def 3;
A19:
k in Seg n
by A8, A9;
dom M2 = Seg n
by A2, FINSEQ_1:def 3;
then A20:
(Col (M2,j)) . k = M2 * (
k,
j)
by A10, MATRIX_0:def 8;
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 A21:
M1 * (
i,
k)
= 0. K
by A16, MATRIX_1:def 8;
(mlt (L9,C9)) . k = (M1 * (i,k)) * (M2 * (k,j))
by A14, A20, A18, A19, FVSUM_1:60;
hence
(mlt (L9,C9)) . k = (n |-> (0. K)) . k
by A11, A21;
verum end; suppose
k > j
;
(mlt (L9,C9)) . b1 = (n |-> (0. K)) . b1then A22:
M2 * (
k,
j)
= 0. K
by A17, MATRIX_1:def 8;
(mlt (L9,C9)) . k = (M1 * (i,k)) * (M2 * (k,j))
by A14, A20, A18, A19, FVSUM_1:60;
hence
(mlt (L9,C9)) . k = (n |-> (0. K)) . k
by A11, A22;
verum end; end; end;
len (n |-> (0. K)) = n
by CARD_1:def 7;
then
mlt (
L9,
C9)
= n |-> (0. K)
by A6, A7;
hence 0. K =
(Line (M1,i)) "*" (Col (M2,j))
by MATRIX_3:11
.=
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_1:def 8; 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;
A23:
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 A23, FINSEQ_2:92;
set m = mlt (D19,D29);
A24:
len (mlt (D19,D29)) = n
by CARD_1:def 7;
A25:
now for i being Nat st 1 <= i & i <= n holds
(mlt (D19,D29)) . i = (diagonal_of_Matrix M) . iset 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 A26:
1
<= i
and A27:
i <= n
;
(mlt (D19,D29)) . i = (diagonal_of_Matrix M) . iA28:
i in Seg n
by A26, A27;
then A29:
(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_0:24;
set mLC =
mlt (
L9,
C9);
A30:
the
addF of
K is
having_a_unity
by FVSUM_1:8;
Indices M = [:(Seg n),(Seg n):]
by MATRIX_0:24;
then
[i,i] in Indices M
by A28, ZFMISC_1:87;
then A31:
(diagonal_of_Matrix M) . i = (Line (M1,i)) "*" (Col (M2,i))
by A1, A3, A2, A29, MATRIX_3:def 4;
A32:
(diagonal_of_Matrix M2) . i = M2 * (
i,
i)
by A28, MATRIX_3:def 10;
A33:
(diagonal_of_Matrix M1) . i = M1 * (
i,
i)
by A28, MATRIX_3:def 10;
len (mlt (L9,C9)) = n
by CARD_1:def 7;
then consider f being
sequence of the
carrier of
K such that A34:
f . 1
= (mlt (L9,C9)) . 1
and A35:
for
k being
Nat st
0 <> k &
k < n holds
f . (k + 1) = the
addF of
K . (
(f . k),
((mlt (L9,C9)) . (k + 1)))
and A36:
(diagonal_of_Matrix M) . i = f . n
by A26, A27, A31, A30, 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 A24, A28, FINSEQ_1:def 3;
then A37:
(mlt (D19,D29)) . i = (M1 * (i,i)) * (M2 * (i,i))
by A33, A32, FVSUM_1:60;
A38:
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
A39:
i in Seg n
by A26, A27;
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 A40:
j in Seg n
;
( ( j <> i implies (mlt (L9,C9)) . j = 0. K ) & ( j = i implies (mlt (L9,C9)) . j = (mlt (D19,D29)) . i ) )
A41:
(Line (M1,i)) . j = M1 * (
i,
j)
by A3, A40, MATRIX_0:def 7;
Indices M1 = [:(Seg n),(Seg n):]
by MATRIX_0:24;
then A42:
[i,j] in Indices M1
by A40, A39, ZFMISC_1:87;
dom M2 = Seg n
by A2, FINSEQ_1:def 3;
then A43:
(Col (M2,i)) . j = M2 * (
j,
i)
by A40, MATRIX_0:def 8;
Indices M2 = [:(Seg n),(Seg n):]
by MATRIX_0:24;
then A44:
[j,i] in Indices M2
by A40, A39, ZFMISC_1:87;
per cases
( i <> j or i = j )
;
suppose A45:
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 A46:
(
M1 * (
i,
j)
= 0. K or
M2 * (
j,
i)
= 0. K )
by A42, A44, MATRIX_1:def 8;
(mlt (L9,C9)) . j = (M1 * (i,j)) * (M2 * (j,i))
by A40, A41, A43, FVSUM_1:61;
hence
( (
j <> i implies
(mlt (L9,C9)) . j = 0. K ) & (
j = i implies
(mlt (L9,C9)) . j = (mlt (D19,D29)) . i ) )
by A45, A46;
verum end; end;
end; A47:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A48:
S1[
k]
;
S1[k + 1]
set k1 =
k + 1;
assume that A49:
1
<= k + 1
and A50:
k + 1
<= n
;
( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt (D19,D29)) . i ) )
A51:
k + 1
in Seg n
by A49, A50;
per cases
( k = 0 or k > 0 )
;
suppose A52:
k > 0
;
( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt (D19,D29)) . i ) )
k < n
by A50, NAT_1:13;
then A53:
f . (k + 1) = the
addF of
K . (
(f . k),
((mlt (L9,C9)) . (k + 1)))
by A35, A52;
per cases
( k + 1 < i or k + 1 = i or k + 1 > i )
by XXREAL_0:1;
suppose A54:
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 A55:
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 A37, A38, A48, A50, A51, A52, A53, 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 A37, A55, RLVECT_1:def 4;
verum end; 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 ) )then
f . (k + 1) = ((M1 * (i,i)) * (M2 * (i,i))) + (0. K)
by A37, A38, A48, A50, A51, A52, A53, 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 A37, A56, RLVECT_1:def 4;
verum end; end; end; end;
end; A57:
1
<= n
by A26, A27, NAT_1:14;
A58:
S1[
0 ]
;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A58, A47);
hence
(mlt (D19,D29)) . i = (diagonal_of_Matrix M) . i
by A27, A36, A57;
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 A24, A25; verum