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:1;

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

.= (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

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:1;

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

then Trace (M1 + M2) =
Sum ((diagonal_of_Matrix M1) + (diagonal_of_Matrix M2))
by A2, A3, A5, FINSEQ_1:13
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_0:24;

then A8: [i,i] in Indices M1 by A6, ZFMISC_1:87;

( (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:22

.= (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;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_0:24;

then A8: [i,i] in Indices M1 by A6, ZFMISC_1:87;

( (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:22

.= (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

.= (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