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

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;
let K be Field;

let M1, M2 be Matrix of n,K;

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 ;

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

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;

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;
let K be Field;

let M1, M2 be Matrix of n,K;

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

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

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

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

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

registration
end;

registration
end;

registration
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))

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))

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

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

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

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 ;

existence

ex b_{1} being Matrix of n,K st b_{1} is_reverse_of M1
by A1;

uniqueness

for b_{1}, b_{2} being Matrix of n,K st b_{1} is_reverse_of M1 & b_{2} is_reverse_of M1 holds

b_{1} = b_{2}
by Th7;

end;
let K be Field;

let M1 be Matrix of n,K;

assume A1: M1 is invertible ;

existence

ex b

uniqueness

for b

b

:: 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_{4} being Matrix of n,K holds

( b_{4} = M1 ~ iff b_{4} is_reverse_of M1 );

for n being Nat

for K being Field

for M1 being Matrix of n,K st M1 is invertible holds

for b

( b

registration

let K be Field;

let n be Nat;

ex b_{1} being Matrix of n,K st b_{1} is invertible

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

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 @

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 ~) @ )

for K being Field

for M being Matrix of n,K st M is invertible holds

( M @ is invertible & (M @) ~ = (M ~) @ )

proof end;

registration
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

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 ;

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 )

for K being Field

for M being Matrix of n,K st M is invertible holds

( M ~ is invertible & (M ~) ~ = M )

proof end;

registration
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

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

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

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;

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

for n being Nat

for K being Field

for M1 being Matrix of n,K holds

( M1 is symmetric iff M1 @ = M1 );

theorem :: MATRIX_6:21

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 )

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 @)

for K being Field

for M1, M2 being Matrix of n,K holds (M1 + M2) @ = (M1 @) + (M2 @)

proof end;

theorem :: MATRIX_6:24

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

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 :: MATRIX_6:27

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

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;

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

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)

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

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

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;

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

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

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) )

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 ~) )

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 ~) )

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

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

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

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;

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

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 )

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 )

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 @)

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;

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 ~) )

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

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

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

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

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

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

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

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

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

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 @

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 ~) )

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

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

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;