:: 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 b₁ being Matrix of n,K st b₁ is_reverse_of M1 by A1;
uniqueness
for b₁, b₂ being Matrix of n,K st b₁ is_reverse_of M1 & b₂ is_reverse_of M1 holds
b₁ = b₂ 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 b₄ being Matrix of n,K holds
( b₄ = M1 ~ iff b₄ 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 b₁ being Matrix of n,K st b₁ 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;