:: Some Properties Of Some Special Matrices
:: by Xiaopeng Yue , Xiquan Liang and Zhongpin Sun
::
:: Received December 7, 2005
:: Copyright (c) 2005-2012 Association of Mizar Users


begin

definition
let n be Nat;
let K be Field;
let M1, M2 be Matrix of n,K;
predM1 commutes_with M2 means :Def1: :: MATRIX_6:def 1
M1 * M2 = M2 * M1;
reflexivity
 for M1 being Matrix of n,K holds M1 * M1 = M1 * M1 ;
symmetry
 for M1, M2 being Matrix of n,K st M1 * M2 = M2 * M1 holds
M2 * M1 = M1 * M2 ;
end;

:: deftheorem Def1 defines commutes_with MATRIX_6:def_1_:_
 for n being Nat
for K being Field
for M1, M2 being Matrix of n,K holds
( M1 commutes_with M2 iff M1 * M2 = M2 * M1 );

definition
let n be Nat;
let K be Field;
let M1, M2 be Matrix of n,K;
predM1 is_reverse_of M2 means :Def2: :: MATRIX_6:def 2
( M1 * M2 = M2 * M1 & M1 * M2 = 1. (K,n) );
symmetry
 for M1, M2 being Matrix of n,K st M1 * M2 = M2 * M1 & M1 * M2 = 1. (K,n) holds
( M2 * M1 = M1 * M2 & M2 * M1 = 1. (K,n) ) ;
end;

:: deftheorem Def2 defines is_reverse_of MATRIX_6:def_2_:_
 for n being Nat
for K being Field
for M1, M2 being Matrix of n,K holds
( M1 is_reverse_of M2 iff ( M1 * M2 = M2 * M1 & M1 * M2 = 1. (K,n) ) );

definition
let n be Nat;
let K be Field;
let M1 be Matrix of n,K;
attrM1 is invertible  means :Def3: :: MATRIX_6:def 3
 ex M2 being Matrix of n,K st M1 is_reverse_of M2;
end;

:: deftheorem Def3 defines invertible MATRIX_6:def_3_:_
 for n being Nat
for K being Field
for M1 being Matrix of n,K holds
( M1 is invertible iff ex M2 being Matrix of n,K st M1 is_reverse_of M2 );

definition
let n be Nat;
let K be Field;
let M1 be Matrix of n,K;
:: original:-
redefine func - M1 ->  Matrix of n,K;
coherence
 - M1 is Matrix of n,K
proofend;
end;

definition
let n be Nat;
let K be Field;
let M1, M2 be Matrix of n,K;
:: original:+
redefine funcM1 + M2 ->  Matrix of n,K;
coherence
 M1 + M2 is Matrix of n,K
proofend;
end;

definition
let n be Nat;
let K be Field;
let M1, M2 be Matrix of n,K;
:: original:-
redefine funcM1 - M2 ->  Matrix of n,K;
coherence
 M1 - M2 is Matrix of n,K
proofend;
:: original:*
redefine funcM1 * M2 ->  Matrix of n,K;
coherence
 M1 * M2 is Matrix of n,K
proofend;
end;

theorem Th1: :: MATRIX_6:1
for K being Field
for A being Matrix of K holds (0. (K,(len A),(len A))) * A = 0. (K,(len A),(width A))
proofend;

theorem Th2: :: MATRIX_6:2
for K being Field
for A being Matrix of K st width A > 0 holds
A * (0. (K,(width A),(width A))) = 0. (K,(len A),(width A))
proofend;

theorem Th3: :: MATRIX_6:3
for n being Nat
for K being Field
for M1 being Matrix of n,K holds M1 commutes_with 0. (K,n,n)
proofend;

theorem :: MATRIX_6:4
for n being Nat
for K being Field
for M1, M2, M3 being Matrix of n,K st M1 commutes_with M2 & M2 commutes_with M3 & M1 commutes_with M3 holds
M1 commutes_with M2 * M3
proofend;

theorem :: MATRIX_6:5
for n being Nat
for K being Field
for M1, M2, M3 being Matrix of n,K st M1 commutes_with M2 & M1 commutes_with M3 & n > 0 holds
M1 commutes_with M2 + M3
proofend;

theorem Th6: :: MATRIX_6:6
for n being Nat
for K being Field
for M1 being Matrix of n,K holds M1 commutes_with 1. (K,n)
proofend;

theorem Th7: :: MATRIX_6:7
for n being Nat
for K being Field
for M2, M3, M1 being Matrix of n,K st M2 is_reverse_of M3 & M1 is_reverse_of M3 holds
M1 = M2
proofend;

definition
let n be Nat;
let K be Field;
let M1 be Matrix of n,K;
assume A1: M1 is invertible ;
funcM1 ~  ->  Matrix of n,K means :Def4: :: MATRIX_6:def 4
it is_reverse_of M1;
existence
 ex b1 being Matrix of n,K st b1 is_reverse_of M1 by A1, Def3;
uniqueness
 for b1, b2 being Matrix of n,K st b1 is_reverse_of M1 & b2 is_reverse_of M1 holds
b1 = b2 by Th7;
end;

:: deftheorem Def4 defines ~ MATRIX_6:def_4_:_
 for n being Nat
for K being Field
for M1 being Matrix of n,K st M1 is invertible holds
for b4 being Matrix of n,K holds
( b4 = M1 ~ iff b4 is_reverse_of M1 );

theorem Th8: :: MATRIX_6:8
for n being Nat
for K being Field holds
( (1. (K,n)) ~ = 1. (K,n) & 1. (K,n) is invertible )
proofend;

theorem :: MATRIX_6:9
for n being Nat
for K being Field holds ((1. (K,n)) ~) ~ = 1. (K,n)
proofend;

theorem Th10: :: MATRIX_6:10
for n being Nat
for K being Field holds (1. (K,n)) @ = 1. (K,n)
proofend;

theorem :: MATRIX_6:11
for K being Field
for n being Nat holds ((1. (K,n)) @) ~ = 1. (K,n)
proofend;

theorem :: MATRIX_6:12
for n being Nat
for K being Field
for M3, M1 being Matrix of n,K st M3 is_reverse_of M1 & n > 0 holds
M1 @ is_reverse_of M3 @
proofend;

theorem :: MATRIX_6:13
for n being Nat
for K being Field
for M being Matrix of n,K st M is invertible & n > 0 holds
(M @) ~ = (M ~) @
proofend;

theorem :: MATRIX_6:14
for K being Field
for n being Nat
for M1, M2, M3, M4 being Matrix of n,K st M3 is_reverse_of M1 & M4 is_reverse_of M2 holds
M3 * M4 is_reverse_of M2 * M1
proofend;

theorem :: MATRIX_6:15
for K being Field
for n being Nat
for M1, M2 being Matrix of n,K st M2 is_reverse_of M1 holds
M1 commutes_with M2
proofend;

theorem Th16: :: MATRIX_6:16
for n being Nat
for K being Field
for M being Matrix of n,K st M is invertible holds
( M ~ is invertible & (M ~) ~ = M )
proofend;

theorem :: MATRIX_6:17
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st n > 0 & M1 * M2 = 0. (K,n,n) & M1 is invertible holds
M1 commutes_with M2
proofend;

theorem :: MATRIX_6:18
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 = M1 * M2 & M1 is invertible holds
M1 commutes_with M2
proofend;

theorem :: MATRIX_6:19
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 = M2 * M1 & M1 is invertible holds
M1 commutes_with M2
proofend;

definition
let n be Nat;
let K be Field;
let M1 be Matrix of n,K;
attrM1 is symmetric  means :Def5: :: MATRIX_6:def 5
M1 @ = M1;
end;

:: deftheorem Def5 defines symmetric MATRIX_6:def_5_:_
 for n being Nat
for K being Field
for M1 being Matrix of n,K holds
( M1 is symmetric iff M1 @ = M1 );

registration
let n be Nat;
let K be Field;
cluster 1. (K,n) ->  symmetric ;
coherence
 1. (K,n) is symmetric
proofend;
end;

theorem Th20: :: MATRIX_6:20
for n being Nat
for K being Field
for a being Element of K holds ((n,n) --> a) @ = (n,n) --> a
proofend;

theorem :: MATRIX_6:21
for n being Nat
for K being Field
for a being Element of K holds (n,n) --> a is symmetric
proofend;

theorem :: MATRIX_6:22
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st n > 0 & M1 is symmetric & M2 is symmetric holds
( M1 commutes_with M2 iff M1 * M2 is symmetric )
proofend;

theorem Th23: :: MATRIX_6:23
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K holds (M1 + M2) @ = (M1 @) + (M2 @)
proofend;

theorem :: MATRIX_6:24
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is symmetric & M2 is symmetric holds
M1 + M2 is symmetric
proofend;

theorem :: MATRIX_6:25
for n being Nat
for K being Field
for M1 being Matrix of n,K st M1 is Upper_Triangular_Matrix of n,K & M1 is Lower_Triangular_Matrix of n,K holds
M1 is symmetric
proofend;

theorem Th26: :: MATRIX_6:26
for K being Field
for n being Nat
for M1 being Matrix of n,K holds (- M1) @ = - (M1 @)
proofend;

theorem :: MATRIX_6:27
for K being Field
for n being Nat
for M1 being Matrix of n,K st M1 is symmetric holds
- M1 is symmetric
proofend;

theorem :: MATRIX_6:28
for K being Field
for n being Nat
for M1, M2 being Matrix of n,K st M1 is symmetric & M2 is symmetric holds
M1 - M2 is symmetric
proofend;

definition
let n be Nat;
let K be Field;
let M1 be Matrix of n,K;
attrM1 is antisymmetric  means :Def6: :: MATRIX_6:def 6
M1 @ = - M1;
end;

:: deftheorem Def6 defines antisymmetric MATRIX_6:def_6_:_
 for n being Nat
for K being Field
for M1 being Matrix of n,K holds
( M1 is antisymmetric iff M1 @ = - M1 );

theorem :: MATRIX_6:29
for K being Fanoian Field
for n being Nat
for M1 being Matrix of n,K st M1 is symmetric & M1 is antisymmetric holds
M1 = 0. (K,n,n)
proofend;

theorem :: MATRIX_6:30
for K being Fanoian Field
for n, i being Nat
for M1 being Matrix of n,K st M1 is antisymmetric & i in Seg n holds
M1 * (i,i) = 0. K
proofend;

theorem :: MATRIX_6:31
for K being Field
for n being Nat
for M1, M2 being Matrix of n,K st M1 is antisymmetric & M2 is antisymmetric holds
M1 + M2 is antisymmetric
proofend;

theorem :: MATRIX_6:32
for K being Field
for n being Nat
for M1 being Matrix of n,K st M1 is antisymmetric holds
- M1 is antisymmetric
proofend;

theorem :: MATRIX_6:33
for K being Field
for n being Nat
for M1, M2 being Matrix of n,K st M1 is antisymmetric & M2 is antisymmetric holds
M1 - M2 is antisymmetric
proofend;

theorem :: MATRIX_6:34
for n being Nat
for K being Field
for M1 being Matrix of n,K st n > 0 holds
M1 - (M1 @) is antisymmetric
proofend;

theorem :: MATRIX_6:35
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st n > 0 holds
( M1 commutes_with M2 iff (M1 + M2) * (M1 + M2) = (((M1 * M1) + (M1 * M2)) + (M1 * M2)) + (M2 * M2) )
proofend;

theorem Th36: :: MATRIX_6:36
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is invertible & M2 is invertible holds
( M1 * M2 is invertible & (M1 * M2) ~ = (M2 ~) * (M1 ~) )
proofend;

theorem :: MATRIX_6:37
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is invertible & M2 is invertible & M1 commutes_with M2 holds
( M1 * M2 is invertible & (M1 * M2) ~ = (M1 ~) * (M2 ~) )
proofend;

theorem :: MATRIX_6:38
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is invertible & M1 * M2 = 1. (K,n) holds
M1 is_reverse_of M2
proofend;

theorem :: MATRIX_6:39
for n being Nat
for K being Field
for M2, M1 being Matrix of n,K st M2 is invertible & M2 * M1 = 1. (K,n) holds
M1 is_reverse_of M2
proofend;

theorem Th40: :: MATRIX_6:40
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is invertible & M1 commutes_with M2 holds
M1 ~ commutes_with M2
proofend;

definition
let n be Nat;
let K be Field;
let M1 be Matrix of n,K;
attrM1 is Orthogonal  means :Def7: :: MATRIX_6:def 7
( M1 is invertible & M1 @ = M1 ~ );
end;

:: deftheorem Def7 defines Orthogonal MATRIX_6:def_7_:_
 for n being Nat
for K being Field
for M1 being Matrix of n,K holds
( M1 is Orthogonal iff ( M1 is invertible & M1 @ = M1 ~ ) );

theorem Th41: :: MATRIX_6:41
for n being Nat
for K being Field
for M1 being Matrix of n,K holds
( ( M1 * (M1 @) = 1. (K,n) & M1 is invertible ) iff M1 is Orthogonal )
proofend;

theorem Th42: :: MATRIX_6:42
for n being Nat
for K being Field
for M1 being Matrix of n,K holds
( ( M1 is invertible & (M1 @) * M1 = 1. (K,n) ) iff M1 is Orthogonal )
proofend;

theorem :: MATRIX_6:43
for n being Nat
for K being Field
for M1 being Matrix of n,K st M1 is Orthogonal holds
(M1 @) * M1 = M1 * (M1 @)
proofend;

theorem :: MATRIX_6:44
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is Orthogonal & M1 commutes_with M2 holds
M1 @ commutes_with M2
proofend;

theorem Th45: :: MATRIX_6:45
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is invertible & M2 is invertible holds
( M1 * M2 is invertible & (M1 * M2) ~ = (M2 ~) * (M1 ~) )
proofend;

theorem :: MATRIX_6:46
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st n > 0 & M1 is Orthogonal & M2 is Orthogonal holds
M1 * M2 is Orthogonal
proofend;

theorem :: MATRIX_6:47
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is Orthogonal & M1 commutes_with M2 holds
M1 @ commutes_with M2
proofend;

theorem :: MATRIX_6:48
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st n > 0 & M1 commutes_with M2 holds
M1 + M1 commutes_with M2
proofend;

theorem :: MATRIX_6:49
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st n > 0 & M1 commutes_with M2 holds
M1 + M2 commutes_with M2
proofend;

theorem :: MATRIX_6:50
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st n > 0 & M1 commutes_with M2 holds
M1 + M1 commutes_with M2 + M2
proofend;

theorem :: MATRIX_6:51
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st n > 0 & M1 commutes_with M2 holds
M1 + M2 commutes_with M2 + M2
proofend;

theorem :: MATRIX_6:52
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 commutes_with M2 holds
M1 * M2 commutes_with M2
proofend;

theorem :: MATRIX_6:53
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 commutes_with M2 holds
M1 * M1 commutes_with M2
proofend;

theorem :: MATRIX_6:54
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 commutes_with M2 holds
M1 * M1 commutes_with M2 * M2
proofend;

theorem :: MATRIX_6:55
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st n > 0 & M1 commutes_with M2 holds
M1 @ commutes_with M2 @
proofend;

theorem Th56: :: MATRIX_6:56
for n being Nat
for K being Field
for M1, M2, M3 being Matrix of n,K st M1 is invertible & M2 is invertible & M3 is invertible holds
( (M1 * M2) * M3 is invertible & ((M1 * M2) * M3) ~ = ((M3 ~) * (M2 ~)) * (M1 ~) )
proofend;

theorem :: MATRIX_6:57
for n being Nat
for K being Field
for M1, M2, M3 being Matrix of n,K st n > 0 & M1 is Orthogonal & M2 is Orthogonal & M3 is Orthogonal holds
(M1 * M2) * M3 is Orthogonal
proofend;

theorem :: MATRIX_6:58
for n being Nat
for K being Field holds 1. (K,n) is Orthogonal
proofend;

theorem :: MATRIX_6:59
for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st n > 0 & M1 is Orthogonal & M2 is Orthogonal holds
(M1 ~) * M2 is Orthogonal
proofend;