let n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( M is Upper_Triangular_Matrix of n,K & diagonal_of_Matrix M = mlt (diagonal_of_Matrix M1),(diagonal_of_Matrix M2) )
set KK = the carrier of K;
set SS = [:(Seg n),(Seg n):];
A2: ( width M1 = n & len M1 = n & width M2 = n & len M2 = n ) by MATRIX_1:25;
thus M is Upper_Triangular_Matrix of n,K :: thesis: diagonal_of_Matrix M = mlt (diagonal_of_Matrix M1),(diagonal_of_Matrix M2)

proof

now

let i, j be Nat; :: thesis: ( [i,j] in Indices M & i > j implies 0. K = M * i,j )
assume A3: ( [i,j] in Indices M & i > j ) ; :: thesis: 0. K = M * i,j
set L = Line M1,i;
set C = Col M2,j;
reconsider L' = Line M1,i, C' = Col M2,j as Element of N -tuples_on the carrier of K by MATRIX_1:25;
set m = mlt L',C';
set n0 = n |-> (0. K);
A4: ( len (mlt L',C') = n & len (n |-> (0. K)) = n ) by FINSEQ_1:def 18;

now

let k be Nat; :: thesis: ( 1 <= k & k <= n implies (mlt L',C') . b₁ = (n |-> (0. K)) . b₁ )
assume A5: ( 1 <= k & k <= n ) ; :: thesis: (mlt L',C') . b₁ = (n |-> (0. K)) . b₁
A6: k in NAT by ORDINAL1:def 13;
Indices M = [:(Seg n),(Seg n):] by MATRIX_1:25;
then ( i in Seg n & j in Seg n & k in Seg n & dom M2 = Seg n & Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by A2, A3, A5, A6, FINSEQ_1:def 3, ZFMISC_1:106;
then A7: ( (Line M1,i) . k = M1 * i,k & (Col M2,j) . k = M2 * k,j & [i,k] in Indices M1 & [k,j] in Indices M2 & (n |-> (0. K)) . k = 0. K ) by A2, FINSEQ_2:71, MATRIX_1:def 8, MATRIX_1:def 9, ZFMISC_1:106;
A8: ( dom (mlt L',C') = Seg n & k in Seg n ) by A4, A5, A6, FINSEQ_1:def 3;

per cases ( k <= j or k > j ) ;

suppose k <= j ; :: thesis: (mlt L',C') . b₁ = (n |-> (0. K)) . b₁

then k < i by A3, XXREAL_0:2;
then ( M1 * i,k = 0. K & (mlt L',C') . k = (M1 * i,k) * (M2 * k,j) ) by A7, A8, FVSUM_1:73, MATRIX_2:def 3;
hence (mlt L',C') . k = (n |-> (0. K)) . k by A7, VECTSP_1:44; :: thesis: verum

end;

suppose k > j ; :: thesis: (mlt L',C') . b₁ = (n |-> (0. K)) . b₁

then ( M2 * k,j = 0. K & (mlt L',C') . k = (M1 * i,k) * (M2 * k,j) ) by A7, A8, FVSUM_1:73, MATRIX_2:def 3;
hence (mlt L',C') . k = (n |-> (0. K)) . k by A7, VECTSP_1:44; :: thesis: verum

end;

end;

end;

then mlt L',C' = n |-> (0. K) by A4, FINSEQ_1:18;
hence 0. K = (Line M1,i) "*" (Col M2,j) by MATRIX_3:13
.= M * i,j by A1, A2, A3, MATRIX_3:def 4 ;
:: thesis: verum

end;

hence M is Upper_Triangular_Matrix of n,K by MATRIX_2:def 3; :: thesis: verum

end;

set DM = diagonal_of_Matrix M;
set D1 = diagonal_of_Matrix M1;
set D2 = diagonal_of_Matrix M2;
( len (diagonal_of_Matrix M1) = n & len (diagonal_of_Matrix M2) = n ) by MATRIX_3:def 10;
then reconsider D1' = diagonal_of_Matrix M1, D2' = diagonal_of_Matrix M2 as Element of N -tuples_on the carrier of K by FINSEQ_2:110;
set m = mlt D1',D2';
A9: ( len (mlt D1',D2') = n & len (diagonal_of_Matrix M) = n ) by FINSEQ_1:def 18, MATRIX_3:def 10;

now

let i be Nat; :: thesis: ( 1 <= i & i <= n implies (mlt D1',D2') . i = (diagonal_of_Matrix M) . i )
assume A10: ( 1 <= i & i <= n ) ; :: thesis: (mlt D1',D2') . i = (diagonal_of_Matrix M) . i
set L = Line M1,i;
set C = Col M2,i;
reconsider L' = Line M1,i, C' = Col M2,i as Element of N -tuples_on the carrier of K by MATRIX_1:25;
set mLC = mlt L',C';
i in NAT by ORDINAL1:def 13;
then ( i in Seg n & dom (mlt D1',D2') = Seg n & Indices M = [:(Seg n),(Seg n):] ) by A9, A10, FINSEQ_1:def 3, MATRIX_1:25;
then ( (diagonal_of_Matrix M1) . i = M1 * i,i & (diagonal_of_Matrix M2) . i = M2 * i,i & (diagonal_of_Matrix M) . i = M * i,i & i in dom (mlt D1',D2') & [i,i] in Indices M ) by MATRIX_3:def 10, ZFMISC_1:106;
then A11: ( (mlt D1',D2') . i = (M1 * i,i) * (M2 * i,i) & (diagonal_of_Matrix M) . i = (Line M1,i) "*" (Col M2,i) & (Line M1,i) "*" (Col M2,i) = Sum (mlt L',C') ) by A1, A2, FVSUM_1:73, MATRIX_3:def 4;
A12: for j being Nat st j in Seg n holds
( ( j <> i implies (mlt L',C') . j = 0. K ) & ( j = i implies (mlt L',C') . j = (mlt D1',D2') . i ) )

proof

let j be Nat; :: thesis: ( j in Seg n implies ( ( j <> i implies (mlt L',C') . j = 0. K ) & ( j = i implies (mlt L',C') . j = (mlt D1',D2') . i ) ) )
assume A13: j in Seg n ; :: thesis: ( ( j <> i implies (mlt L',C') . j = 0. K ) & ( j = i implies (mlt L',C') . j = (mlt D1',D2') . i ) )
i in NAT by ORDINAL1:def 13;
then ( dom M2 = Seg n & Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] & i in Seg n ) by A2, A10, FINSEQ_1:def 3;
then A14: ( (Line M1,i) . j = M1 * i,j & (Col M2,i) . j = M2 * j,i & [i,j] in Indices M1 & [j,i] in Indices M2 ) by A2, A13, MATRIX_1:def 8, MATRIX_1:def 9, ZFMISC_1:106;

per cases ( i <> j or i = j ) ;

suppose A15: i <> j ; :: thesis: ( ( j <> i implies (mlt L',C') . j = 0. K ) & ( j = i implies (mlt L',C') . j = (mlt D1',D2') . i ) )

then ( i < j or j < i ) by XXREAL_0:1;
then ( ( M1 * i,j = 0. K or M2 * j,i = 0. K ) & (mlt L',C') . j = (M1 * i,j) * (M2 * j,i) ) by A13, A14, FVSUM_1:74, MATRIX_2:def 3;
hence ( ( j <> i implies (mlt L',C') . j = 0. K ) & ( j = i implies (mlt L',C') . j = (mlt D1',D2') . i ) ) by A15, VECTSP_1:44; :: thesis: verum

end;

suppose i = j ; :: thesis: ( ( j <> i implies (mlt L',C') . j = 0. K ) & ( j = i implies (mlt L',C') . j = (mlt D1',D2') . i ) )

hence ( ( j <> i implies (mlt L',C') . j = 0. K ) & ( j = i implies (mlt L',C') . j = (mlt D1',D2') . i ) ) by A11, A13, A14, FVSUM_1:74; :: thesis: verum

end;

end;

end;

set aa = the addF of K;
( the addF of K is having_a_unity & len (mlt L',C') = n & n <> 0 ) by A10, FINSEQ_1:def 18, FVSUM_1:10;
then consider f being Function of NAT ,the carrier of K such that
A16: f . 1 = (mlt L',C') . 1 and
A17: for k being Element of NAT st 0 <> k & k < n holds
f . (k + 1) = the addF of K . (f . k),((mlt L',C') . (k + 1)) and
A18: (diagonal_of_Matrix M) . i = f . n by A11, FINSOP_1:def 1;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= n implies ( ( $1 < i implies f . $1 = 0. K ) & ( $1 >= i implies f . $1 = (mlt D1',D2') . i ) ) );
A19: S₁[ 0 ] ;
A20: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A21: S₁[k] ; :: thesis: S₁[k + 1]
set k1 = k + 1;
assume A22: ( 1 <= k + 1 & k + 1 <= n ) ; :: thesis: ( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt D1',D2') . i ) )
then A23: k + 1 in Seg n ;

per cases ( k = 0 or k > 0 ) ;

suppose k = 0 ; :: thesis: ( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt D1',D2') . i ) )

then ( ( f . (k + 1) = 0. K & k + 1 < i ) or ( f . (k + 1) = (mlt L',C') . (k + 1) & k + 1 = i ) ) by A10, A12, A16, A23, XXREAL_0:1;
hence ( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt D1',D2') . i ) ) by A12, A23; :: thesis: verum

end;

suppose A24: k > 0 ; :: thesis: ( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt D1',D2') . i ) )

then ( 1 <= k & k < n & k in NAT ) by A22, NAT_1:13, NAT_1:14, ORDINAL1:def 13;
then A25: f . (k + 1) = the addF of K . (f . k),((mlt L',C') . (k + 1)) by A17;

per cases ( k + 1 < i or k + 1 = i or k + 1 > i ) by XXREAL_0:1;

suppose A26: k + 1 < i ; :: thesis: ( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt D1',D2') . i ) )

then f . (k + 1) = (0. K) + (0. K) by A12, A21, A22, A23, A24, A25, NAT_1:13, NAT_1:14;
hence ( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt D1',D2') . i ) ) by A26, RLVECT_1:def 7; :: thesis: verum

end;

suppose A27: k + 1 = i ; :: thesis: ( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt D1',D2') . i ) )

then f . (k + 1) = (0. K) + ((M1 * i,i) * (M2 * i,i)) by A11, A12, A21, A22, A23, A24, A25, NAT_1:13, NAT_1:14;
hence ( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt D1',D2') . i ) ) by A11, A27, RLVECT_1:def 7; :: thesis: verum

end;

suppose A28: k + 1 > i ; :: thesis: ( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt D1',D2') . i ) )

then f . (k + 1) = ((M1 * i,i) * (M2 * i,i)) + (0. K) by A11, A12, A21, A22, A23, A24, A25, NAT_1:13, NAT_1:14;
hence ( ( k + 1 < i implies f . (k + 1) = 0. K ) & ( k + 1 >= i implies f . (k + 1) = (mlt D1',D2') . i ) ) by A11, A28, RLVECT_1:def 7; :: thesis: verum

end;

end;

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A19, A20);
then for n' being Nat holds
( S₁[n'] & 1 <= n ) by A10, NAT_1:14;
hence (mlt D1',D2') . i = (diagonal_of_Matrix M) . i by A10, A18; :: thesis: verum

end;

hence diagonal_of_Matrix M = mlt (diagonal_of_Matrix M1),(diagonal_of_Matrix M2) by A9, FINSEQ_1:18; :: thesis: verum