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


definition
let n be Nat;
let K be Field;
let M1, M2 be Matrix of n,K;
pred M1 commutes_with M2 means :: 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 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;
pred M1 is_reverse_of M2 means :: 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 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;
attr M1 is invertible means :: MATRIX_6:def 3
 ex M2 being Matrix of n,K st M1 is_reverse_of M2;
end;

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

registration
let n be Nat;
let K be Ring;
let M1 be Matrix of n,K;
cluster - M1 -> n,n -size ;
coherence
- M1 is n,n -size
proof end;
end;

registration
let n be Nat;
let K be Ring;
let M1, M2 be Matrix of n,K;
cluster M1 + M2 -> n,n -size ;
coherence
M1 + M2 is n,n -size
proof end;
end;

registration
let n be Nat;
let K be Field;
let M1, M2 be Matrix of n,K;
cluster M1 - M2 -> n,n -size ;
coherence
M1 - M2 is n,n -size ;
end;

registration
let n be Nat;
let K be Ring;
let M1, M2 be Matrix of n,K;
cluster M1 * M2 -> n,n -size ;
coherence
M1 * M2 is n,n -size
proof end;
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))
proof end;

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))
proof end;

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)
proof end;

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
proof end;

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
proof end;

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)
proof end;

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

definition
let n be Nat;
let K be Field;
let M1 be Matrix of n,K;
assume A1: M1 is invertible ;
func M1 ~ -> 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;
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 )
proof end;

registration
let K be Field;
let n be Nat;
cluster 1. (K,n) -> invertible ;
coherence
1. (K,n) is invertible by Th8;
end;

registration
let K be Field;
let n be Nat;
cluster V4() V7(K93()) V8(K144( the U1 of K)) V9() FinSequence-like V109() tabular n,n -size invertible for FinSequence of K144( the U1 of K);
existence
ex b1 being Matrix of n,K st b1 is invertible
proof end;
end;

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

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

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

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

theorem Th13: :: MATRIX_6:13
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 ~) @ )
proof end;

registration
let K be Field;
let n be Nat;
let M be invertible Matrix of n,K;
cluster M @ -> invertible ;
coherence
M @ is invertible by Th13;
end;

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
proof end;

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 ;

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 )
proof end;

registration
let K be Field;
let n be Nat;
let M be invertible Matrix of n,K;
cluster M ~ -> invertible ;
coherence
M ~ is invertible by Th16;
end;

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
proof end;

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
proof end;

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
proof end;

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

:: deftheorem 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 by Th10;
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
proof end;

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

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 )
proof end;

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 @)
proof end;

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 by Th23;

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
proof end;

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

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 by Th26;

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
proof end;

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

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

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
proof end;

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
proof end;

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 by Th26;

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
proof end;

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
proof end;

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) )
proof end;

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 ~) )
proof end;

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 ~) )
proof end;

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
proof end;

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

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
proof end;

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

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

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 )
proof end;

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 @)
proof end;

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 by Th40;

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 ~) )
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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 @
proof end;

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 ~) )
proof end;

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
proof end;

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

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
proof end;