:: by Xiaopeng Yue , Dahai Hu , Xiquan Liang and Zhongpin Sun

::

:: Received January 4, 2006

:: Copyright (c) 2006-2018 Association of Mizar Users

:: deftheorem defines Idempotent MATRIX_8:def 1 :

for n being Nat

for K being Field

for M1 being Matrix of n,K holds

( M1 is Idempotent iff M1 * M1 = M1 );

for n being Nat

for K being Field

for M1 being Matrix of n,K holds

( M1 is Idempotent iff M1 * M1 = M1 );

:: deftheorem defines Nilpotent MATRIX_8:def 2 :

for n being Nat

for K being Field

for M1 being Matrix of n,K holds

( M1 is Nilpotent iff M1 * M1 = 0. (K,n) );

for n being Nat

for K being Field

for M1 being Matrix of n,K holds

( M1 is Nilpotent iff M1 * M1 = 0. (K,n) );

:: deftheorem defines Involutory MATRIX_8:def 3 :

for n being Nat

for K being Field

for M1 being Matrix of n,K holds

( M1 is Involutory iff M1 * M1 = 1. (K,n) );

for n being Nat

for K being Field

for M1 being Matrix of n,K holds

( M1 is Involutory iff M1 * M1 = 1. (K,n) );

:: deftheorem defines Self_Reversible MATRIX_8:def 4 :

for n being Nat

for K being Field

for M1 being Matrix of n,K holds

( M1 is Self_Reversible iff ( M1 is invertible & M1 ~ = M1 ) );

for n being Nat

for K being Field

for M1 being Matrix of n,K holds

( M1 is Self_Reversible iff ( M1 is invertible & M1 ~ = M1 ) );

theorem Th1: :: MATRIX_8:1

for n being Nat

for K being Field holds

( 1. (K,n) is Idempotent & 1. (K,n) is Involutory ) by MATRIX_3:18;

for K being Field holds

( 1. (K,n) is Idempotent & 1. (K,n) is Involutory ) by MATRIX_3:18;

registration

let n be Nat;

let K be Field;

coherence

( 1. (K,n) is Idempotent & 1. (K,n) is Involutory ) by Th1;

coherence

( 0. (K,n) is Idempotent & 0. (K,n) is Nilpotent ) by Th2;

end;
let K be Field;

coherence

( 1. (K,n) is Idempotent & 1. (K,n) is Involutory ) by Th1;

coherence

( 0. (K,n) is Idempotent & 0. (K,n) is Nilpotent ) by Th2;

theorem :: MATRIX_8:3

for n being Nat

for K being Field

for M1 being Matrix of n,K st n > 0 holds

( M1 is Idempotent iff M1 @ is Idempotent )

for K being Field

for M1 being Matrix of n,K st n > 0 holds

( M1 is Idempotent iff M1 @ is Idempotent )

proof end;

theorem :: MATRIX_8:4

for n being Nat

for K being Field

for M1 being Matrix of n,K st M1 is Involutory holds

M1 is invertible by MATRIX_6:def 2, MATRIX_6:def 3;

for K being Field

for M1 being Matrix of n,K st M1 is Involutory holds

M1 is invertible by MATRIX_6:def 2, MATRIX_6:def 3;

theorem :: MATRIX_8:5

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 holds

M1 * M1 commutes_with M2 * M2 ;

for K being Field

for M1, M2 being Matrix of n,K st M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 holds

M1 * M1 commutes_with M2 * M2 ;

theorem :: MATRIX_8:6

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st n > 0 & M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 & M1 * M2 = 0. (K,n) holds

M1 + M2 is Idempotent

for K being Field

for M1, M2 being Matrix of n,K st n > 0 & M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 & M1 * M2 = 0. (K,n) holds

M1 + M2 is Idempotent

proof end;

theorem :: MATRIX_8:7

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st M1 is Idempotent & M2 is Idempotent & M1 * M2 = - (M2 * M1) holds

M1 + M2 is Idempotent

for K being Field

for M1, M2 being Matrix of n,K st M1 is Idempotent & M2 is Idempotent & M1 * M2 = - (M2 * M1) holds

M1 + M2 is Idempotent

proof end;

theorem :: MATRIX_8:8

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st M1 is Idempotent & M2 is invertible holds

((M2 ~) * M1) * M2 is Idempotent

for K being Field

for M1, M2 being Matrix of n,K st M1 is Idempotent & M2 is invertible holds

((M2 ~) * M1) * M2 is Idempotent

proof end;

theorem :: MATRIX_8:9

for n being Nat

for K being Field

for M1 being Matrix of n,K st M1 is invertible & M1 is Idempotent holds

M1 ~ is Idempotent by MATRIX_6:36;

for K being Field

for M1 being Matrix of n,K st M1 is invertible & M1 is Idempotent holds

M1 ~ is Idempotent by MATRIX_6:36;

theorem Th10: :: MATRIX_8:10

for n being Nat

for K being Field

for M1 being Matrix of n,K st M1 is invertible & M1 is Idempotent holds

M1 = 1. (K,n)

for K being Field

for M1 being Matrix of n,K st M1 is invertible & M1 is Idempotent holds

M1 = 1. (K,n)

proof end;

theorem :: MATRIX_8:11

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 holds

M1 * M2 is Idempotent

for K being Field

for M1, M2 being Matrix of n,K st M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 holds

M1 * M2 is Idempotent

proof end;

theorem :: MATRIX_8:12

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 holds

(M1 @) * (M2 @) is Idempotent

for K being Field

for M1, M2 being Matrix of n,K st M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 holds

(M1 @) * (M2 @) is Idempotent

proof end;

theorem :: MATRIX_8:13

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st M1 is Idempotent & M2 is Idempotent & M1 is invertible holds

M1 * M2 is Idempotent

for K being Field

for M1, M2 being Matrix of n,K st M1 is Idempotent & M2 is Idempotent & M1 is invertible holds

M1 * M2 is Idempotent

proof end;

theorem :: MATRIX_8:14

for n being Nat

for K being Field

for M1 being Matrix of n,K st M1 is Idempotent & M1 is Orthogonal holds

M1 is symmetric

for K being Field

for M1 being Matrix of n,K st M1 is Idempotent & M1 is Orthogonal holds

M1 is symmetric

proof end;

theorem :: MATRIX_8:15

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st M2 * M1 = 1. (K,n) holds

M1 * M2 is Idempotent

for K being Field

for M1, M2 being Matrix of n,K st M2 * M1 = 1. (K,n) holds

M1 * M2 is Idempotent

proof end;

theorem :: MATRIX_8:16

for n being Nat

for K being Field

for M1 being Matrix of n,K st M1 is Idempotent & M1 is Orthogonal holds

M1 = 1. (K,n) by Th10, MATRIX_6:def 7;

for K being Field

for M1 being Matrix of n,K st M1 is Idempotent & M1 is Orthogonal holds

M1 = 1. (K,n) by Th10, MATRIX_6:def 7;

theorem :: MATRIX_8:17

for n being Nat

for K being Field

for M1 being Matrix of n,K st M1 is symmetric holds

M1 * (M1 @) is symmetric

for K being Field

for M1 being Matrix of n,K st M1 is symmetric holds

M1 * (M1 @) is symmetric

proof end;

theorem :: MATRIX_8:18

for n being Nat

for K being Field

for M1 being Matrix of n,K st M1 is symmetric holds

(M1 @) * M1 is symmetric

for K being Field

for M1 being Matrix of n,K st M1 is symmetric holds

(M1 @) * M1 is symmetric

proof end;

theorem :: MATRIX_8:19

for n being Nat

for K being Field

for M1, M2, M3 being Matrix of n,K st M1 is invertible & M1 * M2 = M1 * M3 holds

M2 = M3

for K being Field

for M1, M2, M3 being Matrix of n,K st M1 is invertible & M1 * M2 = M1 * M3 holds

M2 = M3

proof end;

theorem :: MATRIX_8:20

for n being Nat

for K being Field

for M1, M2, M3 being Matrix of n,K st M1 is invertible & M2 * M1 = M3 * M1 holds

M2 = M3

for K being Field

for M1, M2, M3 being Matrix of n,K st M1 is invertible & M2 * M1 = M3 * M1 holds

M2 = M3

proof end;

theorem :: MATRIX_8:21

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st M1 is invertible & M2 * M1 = 0. (K,n) holds

M2 = 0. (K,n)

for K being Field

for M1, M2 being Matrix of n,K st M1 is invertible & M2 * M1 = 0. (K,n) holds

M2 = 0. (K,n)

proof end;

theorem :: MATRIX_8:22

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st M1 is invertible & M2 * M1 = 0. (K,n) holds

M2 = 0. (K,n)

for K being Field

for M1, M2 being Matrix of n,K st M1 is invertible & M2 * M1 = 0. (K,n) holds

M2 = 0. (K,n)

proof end;

theorem :: MATRIX_8:23

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st M1 is Nilpotent & M1 commutes_with M2 & n > 0 holds

M1 * M2 is Nilpotent

for K being Field

for M1, M2 being Matrix of n,K st M1 is Nilpotent & M1 commutes_with M2 & n > 0 holds

M1 * M2 is Nilpotent

proof end;

theorem :: MATRIX_8:24

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st n > 0 & M1 is Nilpotent & M2 is Nilpotent & M1 commutes_with M2 & M1 * M2 = 0. (K,n) holds

M1 + M2 is Nilpotent

for K being Field

for M1, M2 being Matrix of n,K st n > 0 & M1 is Nilpotent & M2 is Nilpotent & M1 commutes_with M2 & M1 * M2 = 0. (K,n) holds

M1 + M2 is Nilpotent

proof end;

theorem :: MATRIX_8:25

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st M1 is Nilpotent & M2 is Nilpotent & M1 * M2 = - (M2 * M1) & n > 0 holds

M1 + M2 is Nilpotent

for K being Field

for M1, M2 being Matrix of n,K st M1 is Nilpotent & M2 is Nilpotent & M1 * M2 = - (M2 * M1) & n > 0 holds

M1 + M2 is Nilpotent

proof end;

theorem :: MATRIX_8:26

for n being Nat

for K being Field

for M1 being Matrix of n,K st M1 is Nilpotent & n > 0 holds

M1 @ is Nilpotent

for K being Field

for M1 being Matrix of n,K st M1 is Nilpotent & n > 0 holds

M1 @ is Nilpotent

proof end;

theorem :: MATRIX_8:27

theorem :: MATRIX_8:29

for n being Nat

for K being Field

for M1 being Matrix of n,K st n > 0 & M1 is Nilpotent holds

not M1 is invertible

for K being Field

for M1 being Matrix of n,K st n > 0 & M1 is Nilpotent holds

not M1 is invertible

proof end;

theorem :: MATRIX_8:30

for n being Nat

for K being Field

for M1 being Matrix of n,K st M1 is Self_Reversible holds

M1 is Involutory

for K being Field

for M1 being Matrix of n,K st M1 is Self_Reversible holds

M1 is Involutory

proof end;

theorem :: MATRIX_8:31

theorem :: MATRIX_8:32

for n being Nat

for K being Field

for M1 being Matrix of n,K st M1 is Self_Reversible & M1 is Idempotent holds

M1 = 1. (K,n)

for K being Field

for M1 being Matrix of n,K st M1 is Self_Reversible & M1 is Idempotent holds

M1 = 1. (K,n)

proof end;

theorem :: MATRIX_8:33

for n being Nat

for K being Field

for M1 being Matrix of n,K st M1 is Self_Reversible & M1 is symmetric holds

M1 is Orthogonal

for K being Field

for M1 being Matrix of n,K st M1 is Self_Reversible & M1 is symmetric holds

M1 is Orthogonal

proof end;

definition

let n be Nat;

let K be Field;

let M1, M2 be Matrix of n,K;

for M1 being Matrix of n,K ex M being Matrix of n,K st

( M is invertible & M1 = ((M ~) * M1) * M )

for M1, M2 being Matrix of n,K st ex M being Matrix of n,K st

( M is invertible & M1 = ((M ~) * M2) * M ) holds

ex M being Matrix of n,K st

( M is invertible & M2 = ((M ~) * M1) * M )

end;
let K be Field;

let M1, M2 be Matrix of n,K;

pred M1 is_similar_to M2 means :: MATRIX_8:def 5

ex M being Matrix of n,K st

( M is invertible & M1 = ((M ~) * M2) * M );

reflexivity ex M being Matrix of n,K st

( M is invertible & M1 = ((M ~) * M2) * M );

for M1 being Matrix of n,K ex M being Matrix of n,K st

( M is invertible & M1 = ((M ~) * M1) * M )

proof end;

symmetry for M1, M2 being Matrix of n,K st ex M being Matrix of n,K st

( M is invertible & M1 = ((M ~) * M2) * M ) holds

ex M being Matrix of n,K st

( M is invertible & M2 = ((M ~) * M1) * M )

proof end;

:: deftheorem defines is_similar_to MATRIX_8:def 5 :

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K holds

( M1 is_similar_to M2 iff ex M being Matrix of n,K st

( M is invertible & M1 = ((M ~) * M2) * M ) );

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K holds

( M1 is_similar_to M2 iff ex M being Matrix of n,K st

( M is invertible & M1 = ((M ~) * M2) * M ) );

theorem :: MATRIX_8:34

for n being Nat

for K being Field

for M1, M2, M3 being Matrix of n,K st M1 is_similar_to M2 & M2 is_similar_to M3 holds

M1 is_similar_to M3

for K being Field

for M1, M2, M3 being Matrix of n,K st M1 is_similar_to M2 & M2 is_similar_to M3 holds

M1 is_similar_to M3

proof end;

theorem :: MATRIX_8:35

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & M2 is Idempotent holds

M1 is Idempotent

for K being Field

for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & M2 is Idempotent holds

M1 is Idempotent

proof end;

theorem :: MATRIX_8:36

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & M2 is Nilpotent & n > 0 holds

M1 is Nilpotent

for K being Field

for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & M2 is Nilpotent & n > 0 holds

M1 is Nilpotent

proof end;

theorem :: MATRIX_8:37

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & M2 is Involutory holds

M1 is Involutory

for K being Field

for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & M2 is Involutory holds

M1 is Involutory

proof end;

theorem :: MATRIX_8:38

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & n > 0 holds

M1 + (1. (K,n)) is_similar_to M2 + (1. (K,n))

for K being Field

for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & n > 0 holds

M1 + (1. (K,n)) is_similar_to M2 + (1. (K,n))

proof end;

theorem :: MATRIX_8:39

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & n > 0 holds

M1 + M1 is_similar_to M2 + M2

for K being Field

for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & n > 0 holds

M1 + M1 is_similar_to M2 + M2

proof end;

theorem :: MATRIX_8:40

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & n > 0 holds

(M1 + M1) + M1 is_similar_to (M2 + M2) + M2

for K being Field

for M1, M2 being Matrix of n,K st M1 is_similar_to M2 & n > 0 holds

(M1 + M1) + M1 is_similar_to (M2 + M2) + M2

proof end;

theorem :: MATRIX_8:41

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st M1 is invertible holds

M2 * M1 is_similar_to M1 * M2

for K being Field

for M1, M2 being Matrix of n,K st M1 is invertible holds

M2 * M1 is_similar_to M1 * M2

proof end;

theorem :: MATRIX_8:42

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st M2 is invertible & M1 is_similar_to M2 holds

M1 is invertible

for K being Field

for M1, M2 being Matrix of n,K st M2 is invertible & M1 is_similar_to M2 holds

M1 is invertible

proof end;

theorem :: MATRIX_8:43

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st M2 is invertible & M1 is_similar_to M2 holds

M1 ~ is_similar_to M2 ~

for K being Field

for M1, M2 being Matrix of n,K st M2 is invertible & M1 is_similar_to M2 holds

M1 ~ is_similar_to M2 ~

proof end;

definition

let n be Nat;

let K be Field;

let M1, M2 be Matrix of n,K;

for M1 being Matrix of n,K ex M being Matrix of n,K st

( M is invertible & M1 = ((M @) * M1) * M )

end;
let K be Field;

let M1, M2 be Matrix of n,K;

pred M1 is_congruent_Matrix_of M2 means :: MATRIX_8:def 6

ex M being Matrix of n,K st

( M is invertible & M1 = ((M @) * M2) * M );

reflexivity ex M being Matrix of n,K st

( M is invertible & M1 = ((M @) * M2) * M );

for M1 being Matrix of n,K ex M being Matrix of n,K st

( M is invertible & M1 = ((M @) * M1) * M )

proof end;

:: deftheorem defines is_congruent_Matrix_of MATRIX_8:def 6 :

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K holds

( M1 is_congruent_Matrix_of M2 iff ex M being Matrix of n,K st

( M is invertible & M1 = ((M @) * M2) * M ) );

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K holds

( M1 is_congruent_Matrix_of M2 iff ex M being Matrix of n,K st

( M is invertible & M1 = ((M @) * M2) * M ) );

theorem :: MATRIX_8:44

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & n > 0 holds

M2 is_congruent_Matrix_of M1

for K being Field

for M1, M2 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & n > 0 holds

M2 is_congruent_Matrix_of M1

proof end;

theorem :: MATRIX_8:45

for n being Nat

for K being Field

for M1, M2, M3 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & M2 is_congruent_Matrix_of M3 & n > 0 holds

M1 is_congruent_Matrix_of M3

for K being Field

for M1, M2, M3 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & M2 is_congruent_Matrix_of M3 & n > 0 holds

M1 is_congruent_Matrix_of M3

proof end;

theorem :: MATRIX_8:46

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & n > 0 holds

M1 + M1 is_congruent_Matrix_of M2 + M2

for K being Field

for M1, M2 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & n > 0 holds

M1 + M1 is_congruent_Matrix_of M2 + M2

proof end;

theorem :: MATRIX_8:47

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & n > 0 holds

(M1 + M1) + M1 is_congruent_Matrix_of (M2 + M2) + M2

for K being Field

for M1, M2 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & n > 0 holds

(M1 + M1) + M1 is_congruent_Matrix_of (M2 + M2) + M2

proof end;

theorem :: MATRIX_8:48

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st M1 is Orthogonal holds

M2 * M1 is_congruent_Matrix_of M1 * M2

for K being Field

for M1, M2 being Matrix of n,K st M1 is Orthogonal holds

M2 * M1 is_congruent_Matrix_of M1 * M2

proof end;

theorem :: MATRIX_8:49

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st M2 is invertible & M1 is_congruent_Matrix_of M2 & n > 0 holds

M1 is invertible

for K being Field

for M1, M2 being Matrix of n,K st M2 is invertible & M1 is_congruent_Matrix_of M2 & n > 0 holds

M1 is invertible

proof end;

theorem :: MATRIX_8:50

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & n > 0 holds

M1 @ is_congruent_Matrix_of M2 @

for K being Field

for M1, M2 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & n > 0 holds

M1 @ is_congruent_Matrix_of M2 @

proof end;

theorem :: MATRIX_8:51

for n being Nat

for K being Field

for M2, M4 being Matrix of n,K st M4 is Orthogonal holds

((M4 @) * M2) * M4 is_similar_to M2

for K being Field

for M2, M4 being Matrix of n,K st M4 is Orthogonal holds

((M4 @) * M2) * M4 is_similar_to M2

proof end;

definition

let n be Nat;

let K be Field;

let M be Matrix of n,K;

coherence

Sum (diagonal_of_Matrix M) is Element of K ;

end;
let K be Field;

let M be Matrix of n,K;

coherence

Sum (diagonal_of_Matrix M) is Element of K ;

:: deftheorem defines Trace MATRIX_8:def 7 :

for n being Nat

for K being Field

for M being Matrix of n,K holds Trace M = Sum (diagonal_of_Matrix M);

for n being Nat

for K being Field

for M being Matrix of n,K holds Trace M = Sum (diagonal_of_Matrix M);

theorem Th53: :: MATRIX_8:53

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K holds Trace (M1 + M2) = (Trace M1) + (Trace M2)

for K being Field

for M1, M2 being Matrix of n,K holds Trace (M1 + M2) = (Trace M1) + (Trace M2)

proof end;

theorem :: MATRIX_8:54

for n being Nat

for K being Field

for M1, M2, M3 being Matrix of n,K holds Trace ((M1 + M2) + M3) = ((Trace M1) + (Trace M2)) + (Trace M3)

for K being Field

for M1, M2, M3 being Matrix of n,K holds Trace ((M1 + M2) + M3) = ((Trace M1) + (Trace M2)) + (Trace M3)

proof end;

theorem Th59: :: MATRIX_8:59

for n being Nat

for K being Field

for M1, M2 being Matrix of n,K holds Trace (M1 - M2) = (Trace M1) - (Trace M2)

for K being Field

for M1, M2 being Matrix of n,K holds Trace (M1 - M2) = (Trace M1) - (Trace M2)

proof end;

theorem :: MATRIX_8:60

for n being Nat

for K being Field

for M1, M2, M3 being Matrix of n,K holds Trace ((M1 - M2) + M3) = ((Trace M1) - (Trace M2)) + (Trace M3)

for K being Field

for M1, M2, M3 being Matrix of n,K holds Trace ((M1 - M2) + M3) = ((Trace M1) - (Trace M2)) + (Trace M3)

proof end;

theorem :: MATRIX_8:61

for n being Nat

for K being Field

for M1, M2, M3 being Matrix of n,K holds Trace ((M1 + M2) - M3) = ((Trace M1) + (Trace M2)) - (Trace M3)

for K being Field

for M1, M2, M3 being Matrix of n,K holds Trace ((M1 + M2) - M3) = ((Trace M1) + (Trace M2)) - (Trace M3)

proof end;

theorem :: MATRIX_8:62

for n being Nat

for K being Field

for M1, M2, M3 being Matrix of n,K holds Trace ((M1 - M2) - M3) = ((Trace M1) - (Trace M2)) - (Trace M3)

for K being Field

for M1, M2, M3 being Matrix of n,K holds Trace ((M1 - M2) - M3) = ((Trace M1) - (Trace M2)) - (Trace M3)

proof end;