let n be Nat; :: thesis: for K being Field
for M1, M2 being Matrix of n,K holds Trace (M1 + M2) = (Trace M1) + (Trace M2)
let K be Field; :: thesis: for M1, M2 being Matrix of n,K holds Trace (M1 + M2) = (Trace M1) + (Trace M2)
let M1, M2 be Matrix of n,K; :: thesis: Trace (M1 + M2) = (Trace M1) + (Trace M2)
A1: len (diagonal_of_Matrix M1) = n by MATRIX_3:def 10;
then A2: dom (diagonal_of_Matrix M1) = Seg n by FINSEQ_1:def 3;
len (diagonal_of_Matrix (M1 + M2)) = n by MATRIX_3:def 10;
then A3: dom (diagonal_of_Matrix (M1 + M2)) = Seg n by FINSEQ_1:def 3;
A4: len (diagonal_of_Matrix M2) = n by MATRIX_3:def 10;
then dom (diagonal_of_Matrix M2) = Seg n by FINSEQ_1:def 3;
then A5: dom ((diagonal_of_Matrix M1) + (diagonal_of_Matrix M2)) = Seg n by A2, POLYNOM1:5;
for i being Nat st i in dom (diagonal_of_Matrix M1) holds
((diagonal_of_Matrix M1) + (diagonal_of_Matrix M2)) . i = (diagonal_of_Matrix (M1 + M2)) . i

proof

let i be Nat; :: thesis: ( i in dom (diagonal_of_Matrix M1) implies ((diagonal_of_Matrix M1) + (diagonal_of_Matrix M2)) . i = (diagonal_of_Matrix (M1 + M2)) . i )
assume i in dom (diagonal_of_Matrix M1) ; :: thesis: ((diagonal_of_Matrix M1) + (diagonal_of_Matrix M2)) . i = (diagonal_of_Matrix (M1 + M2)) . i
then A6: i in Seg n by A1, FINSEQ_1:def 3;
then A7: (diagonal_of_Matrix (M1 + M2)) . i = (M1 + M2) * i,i by MATRIX_3:def 10;
Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:25;
then A8: [i,i] in Indices M1 by A6, ZFMISC_1:106;
( (diagonal_of_Matrix M1) . i = M1 * i,i & (diagonal_of_Matrix M2) . i = M2 * i,i ) by A6, MATRIX_3:def 10;
then ((diagonal_of_Matrix M1) + (diagonal_of_Matrix M2)) . i = (M1 * i,i) + (M2 * i,i) by A5, A6, FUNCOP_1:28
.= (diagonal_of_Matrix (M1 + M2)) . i by A8, A7, MATRIX_3:def 3 ;
hence ((diagonal_of_Matrix M1) + (diagonal_of_Matrix M2)) . i = (diagonal_of_Matrix (M1 + M2)) . i ; :: thesis: verum

end;

then Trace (M1 + M2) = Sum ((diagonal_of_Matrix M1) + (diagonal_of_Matrix M2)) by A2, A3, A5, FINSEQ_1:17
.= (Sum (diagonal_of_Matrix M1)) + (Sum (diagonal_of_Matrix M2)) by A1, A4, MATRIX_4:61 ;
hence Trace (M1 + M2) = (Trace M1) + (Trace M2) ; :: thesis: verum