:: 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-2012 Association of Mizar Users


begin

definition
let n be Nat;
let K be Field;
let M1 be Matrix of n,K;
attrM1 is Idempotent  means :Def1: :: MATRIX_8:def 1
M1 * M1 = M1;
attrM1 is Nilpotent  means :Def2: :: MATRIX_8:def 2
M1 * M1 = 0. (K,n);
attrM1 is Involutory  means :Def3: :: MATRIX_8:def 3
M1 * M1 = 1. (K,n);
attrM1 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 )
proofend;

theorem Th2: :: MATRIX_8:2
for n being Nat
for K being Field holds
( 0. (K,n) is Idempotent & 0. (K,n) is Nilpotent )
proofend;

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

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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

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

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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

theorem Th28: :: MATRIX_8:28
for n being Nat
for K being Field st n > 0 holds
0. (K,n) <> 1. (K,n)
proofend;

theorem :: MATRIX_8:29
for n being Nat
for K being Field
for M1 being Matrix of n,K st n > 0 &amp; M1 is Nilpotent holds
not M1 is invertible
proofend;

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
proofend;

theorem :: MATRIX_8:31
for n being Nat
for K being Field holds 1. (K,n) is Self_Reversible
proofend;

theorem :: MATRIX_8:32
for n being Nat
for K being Field
for M1 being Matrix of n,K st M1 is Self_Reversible &amp; M1 is Idempotent holds
M1 = 1. (K,n)
proofend;

theorem :: MATRIX_8:33
for n being Nat
for K being Field
for M1 being Matrix of n,K st M1 is Self_Reversible &amp; M1 is symmetric holds
M1 is Orthogonal
proofend;

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

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 &amp; M2 is Idempotent holds
M1 is Idempotent
proofend;

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 &amp; M2 is Nilpotent &amp; n > 0 holds
M1 is Nilpotent
proofend;

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 &amp; M2 is Involutory holds
M1 is Involutory
proofend;

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 &amp; n > 0 holds
M1 + (1. (K,n)) is_similar_to M2 + (1. (K,n))
proofend;

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 &amp; n > 0 holds
M1 + M1 is_similar_to M2 + M2
proofend;

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 &amp; n > 0 holds
(M1 + M1) + M1 is_similar_to (M2 + M2) + M2
proofend;

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
proofend;

theorem :: MATRIX_8:42
for n being Nat
for K being Field
for M2, M1 being Matrix of n,K st M2 is invertible &amp; M1 is_similar_to M2 holds
M1 is invertible
proofend;

theorem :: MATRIX_8:43
for n being Nat
for K being Field
for M2, M1 being Matrix of n,K st M2 is invertible &amp; M1 is_similar_to M2 holds
M1 ~ is_similar_to M2 ~
proofend;

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

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 &amp; M2 is_congruent_Matrix_of M3 &amp; n > 0 holds
M1 is_congruent_Matrix_of M3
proofend;

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 &amp; n > 0 holds
M1 + M1 is_congruent_Matrix_of M2 + M2
proofend;

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

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
proofend;

theorem :: MATRIX_8:49
for n being Nat
for K being Field
for M2, M1 being Matrix of n,K st M2 is invertible &amp; M1 is_congruent_Matrix_of M2 &amp; n > 0 holds
M1 is invertible
proofend;

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 &amp; n > 0 holds
M1 @ is_congruent_Matrix_of M2 @
proofend;

theorem :: MATRIX_8:51
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
proofend;

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:52
for n being Nat
for K being Field
for M1 being Matrix of n,K holds Trace M1 = Trace (M1 @)
proofend;

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

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

theorem Th55: :: MATRIX_8:55
for n being Nat
for K being Field holds Trace (0. (K,n)) = 0. K
proofend;

theorem Th56: :: MATRIX_8:56
for n being Nat
for K being Field
for M1 being Matrix of n,K holds Trace (- M1) = - (Trace M1)
proofend;

theorem :: MATRIX_8:57
for n being Nat
for K being Field
for M1 being Matrix of n,K holds - (Trace (- M1)) = Trace M1
proofend;

theorem :: MATRIX_8:58
for n being Nat
for K being Field
for M1 being Matrix of n,K holds Trace (M1 + (- M1)) = 0. K
proofend;

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

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

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

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