:: Some Properties Of Some Special Matrices, Part {II}
:: by Xiaopeng Yue , Dahai Hu , Xiquan Liang and Zhongpin Sun
::
:: Received January 4, 2006
:: Copyright (c) 2006-2011 Association of Mizar Users

begin

definition

let n be Nat;
let K be Field;
let M1 be Matrix of n,K;
attr M1 is Idempotent means :Def1: :: MATRIX_8:def 1
M1 * M1 = M1;
attr M1 is Nilpotent means :Def2: :: MATRIX_8:def 2
M1 * M1 = 0. (K,n);
attr M1 is Involutory means :Def3: :: MATRIX_8:def 3
M1 * M1 = 1. (K,n);
attr M1 is Self_Reversible means :Def4: :: MATRIX_8:def 4
( M1 is invertible & M1 ~ = M1 );

end;

:: deftheorem Def1 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 );

:: deftheorem Def2 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) );

:: deftheorem Def3 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) );

:: deftheorem Def4 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 ) );

theorem Th1: :: MATRIX_8:1

for n being Nat
for K being Field holds
( 1. (K,n) is Idempotent & 1. (K,n) is Involutory )

proof end;

theorem Th2: :: MATRIX_8:2

for n being Nat
for K being Field holds
( 0. (K,n) is Idempotent & 0. (K,n) is Nilpotent )

proof end;

registration

let n be Nat;
let K be Field;
cluster 1. (K,n) -> Idempotent Involutory ;
coherence
( 1. (K,n) is Idempotent & 1. (K,n) is Involutory ) by Th1;
cluster 0. (K,n) -> Idempotent Nilpotent ;
coherence
( 0. (K,n) is Idempotent & 0. (K,n) is Nilpotent ) by Th2;

end;

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 )

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

proof end;

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

proof end;

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

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

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

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

proof end;

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)

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

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

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

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

proof end;

theorem :: MATRIX_8:15

for n being Nat
for K being Field
for M2, M1 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)

proof end;

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

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

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

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

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)

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)

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

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

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

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

proof end;

theorem :: MATRIX_8:27

for n being Nat
for K being Field
for M1 being Matrix of n,K st M1 is Nilpotent & M1 is Idempotent holds
M1 = 0. (K,n)

proof end;

theorem Th28: :: MATRIX_8:28

for n being Nat
for K being Field st n > 0 holds
0. (K,n) <> 1. (K,n)

proof end;

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

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

proof end;

theorem :: MATRIX_8:31

for n being Nat
for K being Field holds 1. (K,n) is Self_Reversible

proof end;

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)

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

proof end;

definition

let n be Nat;
let K be Field;
let M1, M2 be Matrix of n,K;
pred M1 is_similar_to M2 means :Def5: :: MATRIX_8:def 5
ex M being Matrix of n,K st
( M is invertible & M1 = ((M ~) * M2) * M );
reflexivity
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;

end;

:: deftheorem Def5 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 ) );

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

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

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

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

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))

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

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

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

proof end;

theorem :: MATRIX_8:42

for n being Nat
for K being Field
for M2, M1 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 M2, M1 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;
pred M1 is_congruent_Matrix_of M2 means :Def6: :: MATRIX_8:def 6
ex M being Matrix of n,K st
( M is invertible & M1 = ((M @) * M2) * M );
reflexivity
for M1 being Matrix of n,K ex M being Matrix of n,K st
( M is invertible & M1 = ((M @) * M1) * M )

proof end;

end;

:: deftheorem Def6 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 ) );

theorem :: MATRIX_8:44

canceled;

theorem :: MATRIX_8:45

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

proof end;

theorem :: MATRIX_8:46

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

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 is_congruent_Matrix_of 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_congruent_Matrix_of M2 & n > 0 holds
(M1 + M1) + M1 is_congruent_Matrix_of (M2 + M2) + M2

proof end;

theorem :: MATRIX_8:49

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

proof end;

theorem :: MATRIX_8:50

for n being Nat
for K being Field
for M2, M1 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:51

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 @

proof end;

theorem :: MATRIX_8:52

for n being Nat
for K being Field
for M4, M2 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;
func Trace M -> Element of K equals :: MATRIX_8:def 7
Sum (diagonal_of_Matrix M);
coherence
Sum (diagonal_of_Matrix M) is Element of K ;

end;

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

theorem :: MATRIX_8:53

for n being Nat
for K being Field
for M1 being Matrix of n,K holds Trace M1 = Trace (M1 @)

proof end;

theorem Th54: :: MATRIX_8:54

for n being Nat
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:55

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)

proof end;

theorem Th56: :: MATRIX_8:56

for n being Nat
for K being Field holds Trace (0. (K,n)) = 0. K

proof end;

theorem Th57: :: MATRIX_8:57

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

proof end;

theorem :: MATRIX_8:58

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

proof end;

theorem :: MATRIX_8:59

for n being Nat
for K being Field
for M1 being Matrix of n,K holds Trace (M1 + (- M1)) = 0. K

proof end;

theorem Th60: :: MATRIX_8:60

for n being Nat
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: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)

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)

proof end;

theorem :: MATRIX_8:63

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)

proof end;