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

definition

let n be Nat;
let R be Ring;
let M1, M2 be Matrix of n,R;

pred M1 commutes_with M2 means :: MATRIX_6:def 1
M1 * M2 = M2 * M1;

reflexivity
for M1 being Matrix of n,R holds M1 * M1 = M1 * M1 ;
symmetry
for M1, M2 being Matrix of n,R st M1 * M2 = M2 * M1 holds
M2 * M1 = M1 * M2 ;

end;

:: deftheorem defines commutes_with MATRIX_6:def 1 :
for n being Nat
for R being Ring
for M1, M2 being Matrix of n,R holds
( M1 commutes_with M2 iff M1 * M2 = M2 * M1 );

definition

let n be Nat;
let R be Ring;
let M1, M2 be Matrix of n,R;

pred M1 is_reverse_of M2 means :: MATRIX_6:def 2
( M1 * M2 = M2 * M1 & M1 * M2 = 1. (R,n) );

symmetry
for M1, M2 being Matrix of n,R st M1 * M2 = M2 * M1 & M1 * M2 = 1. (R,n) holds
( M2 * M1 = M1 * M2 & M2 * M1 = 1. (R,n) ) ;

end;

:: deftheorem defines is_reverse_of MATRIX_6:def 2 :
for n being Nat
for R being Ring
for M1, M2 being Matrix of n,R holds
( M1 is_reverse_of M2 iff ( M1 * M2 = M2 * M1 & M1 * M2 = 1. (R,n) ) );

definition

let n be Nat;
let R be Ring;
let M1 be Matrix of n,R;

attr M1 is invertible means :: MATRIX_6:def 3
ex M2 being Matrix of n,R st M1 is_reverse_of M2;

end;

:: deftheorem defines invertible MATRIX_6:def 3 :
for n being Nat
for R being Ring
for M1 being Matrix of n,R holds
( M1 is invertible iff ex M2 being Matrix of n,R 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 Ring
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 Ring
for A being Matrix of K 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 Ring
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 R being Ring
for M1, M2, M3 being Matrix of n,R 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 R being Ring
for M1, M2, M3 being Matrix of n,R st M1 commutes_with M2 & M1 commutes_with M3 holds
M1 commutes_with M2 + M3

proof end;

theorem Th7: :: MATRIX_6:6

for n being Nat
for R being Ring
for M1 being Matrix of n,R holds M1 commutes_with 1. (R,n)

proof end;

theorem Th8: :: MATRIX_6:7

for n being Nat
for R being Ring
for M1, M2, M3 being Matrix of n,R st M2 is_reverse_of M3 & M1 is_reverse_of M3 holds
M1 = M2

proof end;

definition

let n be Nat;
let R be Ring;
let M1 be Matrix of n,R;
assume A1: M1 is invertible ;

func M1 ~ -> Matrix of n,R means :Def4: :: MATRIX_6:def 4
it is_reverse_of M1;

existence
ex b₁ being Matrix of n,R st b₁ is_reverse_of M1 by A1;
uniqueness
for b₁, b₂ being Matrix of n,R st b₁ is_reverse_of M1 & b₂ is_reverse_of M1 holds
b₁ = b₂ by Th8;

end;

:: deftheorem Def4 defines ~ MATRIX_6:def 4 :
for n being Nat
for R being Ring
for M1 being Matrix of n,R st M1 is invertible holds
for b₄ being Matrix of n,R holds
( b₄ = M1 ~ iff b₄ is_reverse_of M1 );

registration

let R be Ring;
let n be Nat;

cluster 1. (R,n) -> invertible ;

coherence
1. (R,n) is invertible

proof end;

end;

theorem Th9: :: MATRIX_6:8

for n being Nat
for R being Ring holds
( (1. (R,n)) ~ = 1. (R,n) & 1. (R,n) is invertible )

proof end;

registration

let R be Ring;
let n be Nat;

cluster Relation-like -defined -valued) Function-like finite FinSequence-like FinSubsequence-like Function-yielding tabular n,n -size invertible for FinSequence of K165( the U1 of R);

existence
ex b₁ being Matrix of n,R st b₁ is invertible

proof end;

end;

theorem :: MATRIX_6:9

for n being Nat
for R being Ring holds ((1. (R,n)) ~) ~ = 1. (R,n)

proof end;

theorem Th11: :: MATRIX_6:10

for n being Nat
for R being Ring holds (1. (R,n)) @ = 1. (R,n)

proof end;

theorem :: MATRIX_6:11

for R being Ring
for n being Nat holds ((1. (R,n)) @) ~ = 1. (R,n)

proof end;

theorem :: MATRIX_6:12

for n being Nat
for R being commutative Ring
for M1, M3 being Matrix of n,R st M3 is_reverse_of M1 & n > 0 holds
M1 @ is_reverse_of M3 @

proof end;

theorem Th14: :: MATRIX_6:13

for n being Nat
for R being commutative Ring
for M being Matrix of n,R 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 Th14;

end;

theorem :: MATRIX_6:14

for K being Ring
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 Th17: :: MATRIX_6:16

for R being Ring
for n being Nat
for M being Matrix of n,R st M is invertible holds
( M ~ is invertible & (M ~) ~ = M )

proof end;

registration

let K be Ring;
let n be Nat;
let M be invertible Matrix of n,K;

cluster M ~ -> invertible ;

coherence
M ~ is invertible by Th17;

end;

theorem :: MATRIX_6:17

for n being Nat
for R being Ring
for M1, M2 being Matrix of n,R st M1 * M2 = 0. (R,n,n) & M1 is invertible holds
M1 commutes_with M2

proof end;

theorem :: MATRIX_6:18

for n being Nat
for R being Ring
for M1, M2 being Matrix of n,R st M1 = M1 * M2 & M1 is invertible holds
M1 commutes_with M2

proof end;

theorem :: MATRIX_6:19

for n being Nat
for R being Ring
for M1, M2 being Matrix of n,R st M1 = M2 * M1 & M1 is invertible holds
M1 commutes_with M2

proof end;

definition

let n be Nat;
let K be Ring;
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 Ring
for M1 being Matrix of n,K holds
( M1 is symmetric iff M1 @ = M1 );

registration

let n be Nat;
let K be Ring;

cluster 1. (K,n) -> symmetric ;

coherence
1. (K,n) is symmetric by Th11;

end;

theorem Th21: :: MATRIX_6:20

for n being Nat
for R being Ring
for a being Element of R holds ((n,n) --> a) @ = (n,n) --> a

proof end;

theorem :: MATRIX_6:21

for n being Nat
for R being Ring
for a being Element of R holds (n,n) --> a is symmetric by Th21;

theorem :: MATRIX_6:22

for n being Nat
for R being commutative Ring
for M1, M2 being Matrix of n,R st n > 0 & M1 is symmetric & M2 is symmetric holds
( M1 commutes_with M2 iff M1 * M2 is symmetric )

proof end;

theorem Th24: :: MATRIX_6:23

for n being Nat
for R being Ring
for M1, M2 being Matrix of n,R holds (M1 + M2) @ = (M1 @) + (M2 @)

proof end;

theorem :: MATRIX_6:24

for n being Nat
for R being Ring
for M1, M2 being Matrix of n,R st M1 is symmetric & M2 is symmetric holds
M1 + M2 is symmetric by Th24;

theorem :: MATRIX_6:25

for n being Nat
for R being Ring
for M1, M2 being Matrix of n,R st M1 is upper_triangular Matrix of n,R & M1 is lower_triangular Matrix of n,R holds
M1 is symmetric

proof end;

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

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

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 holds
( M1 commutes_with M2 iff (M1 + M2) * (M1 + M2) = (((M1 * M1) + (M1 * M2)) + (M1 * M2)) + (M2 * M2) )

proof end;

theorem Th37: :: MATRIX_6:36

for n being Nat
for R being Ring
for M1, M2 being Matrix of n,R 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 Ring
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 Ring
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 Th41: :: MATRIX_6:40

for n being Nat
for K being Ring
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 Ring;
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 Ring
for M1 being Matrix of n,K holds
( M1 is Orthogonal iff ( M1 is invertible & M1 @ = M1 ~ ) );

theorem Th42: :: MATRIX_6:41

for n being Nat
for K being Ring
for M1 being Matrix of n,K holds
( ( M1 * (M1 @) = 1. (K,n) & M1 is invertible ) iff M1 is Orthogonal )

proof end;

theorem Th43: :: MATRIX_6:42

for n being Nat
for K being Ring
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 Ring
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 Ring
for M1, M2 being Matrix of n,K st M1 is Orthogonal & M1 commutes_with M2 holds
M1 @ commutes_with M2 by Th41;

theorem Th46: :: MATRIX_6:45

for n being Nat
for K being Ring
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 commutative Ring
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 Ring
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 R being Ring
for M1, M2 being Matrix of n,R st M1 commutes_with M2 holds
M1 + M1 commutes_with M2

proof end;

theorem :: MATRIX_6:49

for n being Nat
for R being Ring
for M1, M2 being Matrix of n,R st M1 commutes_with M2 holds
M1 + M2 commutes_with M2

proof end;

theorem :: MATRIX_6:50

for n being Nat
for R being Ring
for M1, M2 being Matrix of n,R st M1 commutes_with M2 holds
M1 + M1 commutes_with M2 + M2

proof end;

theorem :: MATRIX_6:51

for n being Nat
for R being Ring
for M1, M2 being Matrix of n,R st M1 commutes_with M2 holds
M1 + M2 commutes_with M2 + M2

proof end;

theorem :: MATRIX_6:52

for n being Nat
for R being Ring
for M1, M2 being Matrix of n,R st M1 commutes_with M2 holds
M1 * M2 commutes_with M2

proof end;

theorem :: MATRIX_6:53

for n being Nat
for R being Ring
for M1, M2 being Matrix of n,R st M1 commutes_with M2 holds
M1 * M1 commutes_with M2

proof end;

theorem :: MATRIX_6:54

for n being Nat
for R being Ring
for M1, M2 being Matrix of n,R st M1 commutes_with M2 holds
M1 * M1 commutes_with M2 * M2

proof end;

theorem :: MATRIX_6:55

for n being Nat
for R being commutative Ring
for M1, M2 being Matrix of n,R st n > 0 & M1 commutes_with M2 holds
M1 @ commutes_with M2 @

proof end;

theorem Th57: :: MATRIX_6:56

for n being Nat
for R being Ring
for M1, M2, M3 being Matrix of n,R 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 R being commutative Ring
for M1, M2, M3 being Matrix of n,R 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 Ring holds 1. (K,n) is Orthogonal

proof end;

theorem :: MATRIX_6:59

for n being Nat
for R being commutative Ring
for M1, M2 being Matrix of n,R st n > 0 & M1 is Orthogonal & M2 is Orthogonal holds
(M1 ~) * M2 is Orthogonal

proof end;