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