:: Some Properties Of Some Special Matrices
:: by Xiaopeng Yue , Xiquan Liang and Zhongpin Sun
::
:: Received December 7, 2005
:: Copyright (c) 2005-2019 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NAT_1, VECTSP_1, SUBSET_1, MATRIX_1, REWRITE1, RELAT_1, MESFUNC1,
ALGSTR_0, ARYTM_1, FINSEQ_1, TREES_1, ARYTM_3, SUPINF_2, XXREAL_0,
CARD_1, QC_LANG1, ZFMISC_1, RELAT_2, FUNCOP_1, GROUP_1, MATRIX_6,
FUNCSDOM, MATRIX_0;
notations TARSKI, ZFMISC_1, ORDINAL1, NUMBERS, FINSEQ_1, RLVECT_1, GROUP_1,
VECTSP_1, MATRIX_0, STRUCT_0, MATRIX_1, MATRIX_3, MATRIX_4, XXREAL_0;
constructors XXREAL_0, FVSUM_1, MATRIX_3, MATRIX_4, MATRIX_1;
registrations RELSET_1, XREAL_0, STRUCT_0, VECTSP_1, ORDINAL1, MATRIX_0,
MATRIX_1;
equalities MATRIX_4;
theorems ZFMISC_1, RLVECT_1, MATRIX_0, MATRIX_4, MATRIX_3, VECTSP_1, NAT_1,
CARD_2, XXREAL_0, MATRIX_1;
begin
reserve i,j,n for Nat,
K for Field,
a for Element of K,
M,M1,M2,M3,M4 for Matrix of n,K;
reserve A for Matrix of K;
definition
let n be Nat, K be Field, M1,M2 be Matrix of n,K;
pred M1 commutes_with M2 means
M1 * M2 = M2 * M1;
reflexivity;
symmetry;
end;
definition
let n be Nat,K be Field,M1,M2 be Matrix of n,K;
pred M1 is_reverse_of M2 means
M1*M2 = M2*M1 & M1*M2 = 1.(K,n);
symmetry;
end;
definition
let n be Nat, K be Field;
let M1 be Matrix of n,K;
attr M1 is invertible means
ex M2 be Matrix of n,K st M1 is_reverse_of M2;
end;
registration
let n;
let K be Ring;
let M1 be Matrix of n,K;
cluster -M1 -> (n,n)-size;
coherence
proof
len M1=n by MATRIX_0:24;
then
A1: len (-M1)=n by MATRIX_3:def 2;
width M1=n by MATRIX_0:24;
then width (-M1)=n by MATRIX_3:def 2;
hence thesis by A1,MATRIX_0:51;
end;
end;
registration
let n;
let K be Ring;
let M1,M2 be Matrix of n,K;
cluster M1+M2 -> (n,n)-size;
coherence
proof
A1: width M2=n by MATRIX_0:24;
width M1=n by MATRIX_0:24;
then len (M1+M2)=len M1 & width (M1+M2)=width M2 by A1,MATRIX_3:def 3;
hence thesis by A1,MATRIX_0:24,51;
end;
end;
registration
let n;
let K be Field;
let M1,M2 be Matrix of n,K;
cluster M1-M2 -> (n,n)-size;
coherence;
end;
registration
let n;
let K be Ring;
let M1,M2 be Matrix of n,K;
cluster M1*M2 -> (n,n)-size;
coherence
proof
width M1=n & len M2=n by MATRIX_0:24;
then
A1: len (M1*M2)=len M1 & width (M1*M2)=width M2 by MATRIX_3:def 4;
width M2=n by MATRIX_0:24;
hence thesis by A1,MATRIX_0:24,51;
end;
end;
theorem Th1:
for K being Field, A being Matrix of K holds
(0.(K,len A,len A))*A = 0.(K,len A,width A)
proof
let K, A;
per cases by NAT_1:3;
suppose
A1: len A>0;
set B = (0.(K,len A,len A))*A;
A2: width -((0.(K,len A,len A))*A)=width ((0.(K,len A,len A))*A) by
MATRIX_3:def 2;
A3: len (0.(K,len A,len A))=len A by MATRIX_0:def 2;
then
A4: width (0.(K,len A,len A))=len A by A1,MATRIX_0:20;
then
A5: len ((0.(K,len A,len A))*A)=len A by A3,MATRIX_3:def 4;
A6: width ((0.(K,len A,len A))*A)=width A by A4,MATRIX_3:def 4;
(0.(K,len A,len A))*A =(0.(K,len A,len A)+0.(K,len A,len A))*A by
MATRIX_3:4
.=(0.(K,len A,len A))*A+(0.(K,len A,len A))*A by A1,A3,A4,MATRIX_4:63;
then
len -((0.(K,len A,len A))*A)=len ((0.(K,len A,len A))*A) & 0.(K,len A,
width A)=B+B+(-B) by A5,A6,MATRIX_3:def 2,MATRIX_4:2;
then 0.(K,len A,width A) =B+(B-B) by A2,MATRIX_3:3
.=(0.(K,len A,len A))*A by A5,A2,MATRIX_4:20;
hence thesis;
end;
suppose
A7: len A = 0;
then len (0.(K,len A,len A)) = 0 by MATRIX_0:def 2;
then width (0.(K,len A,len A)) = len A by A7,MATRIX_0:def 3;
then
A8: len ((0.(K,len A,len A))*A) = len ((0.(K,len A,len A))) by MATRIX_3:def 4;
len ((0.(K,len A,len A))) = len A & len (0.(K,len A,width A)) = len A
by MATRIX_0:def 2;
hence thesis by A7,A8,CARD_2:64;
end;
end;
theorem Th2:
for K being Field,A being Matrix of K st width A>0 holds
A*(0.(K,width A,width A))=0.(K,len A,width A)
proof
let K,A;
A1: width -(A*(0.(K,width A,width A)))=width (A*(0.(K,width A,width A))) by
MATRIX_3:def 2;
set B= A*(0.(K,width A,width A));
assume
A2: width A > 0;
then
A3: len A>0 by MATRIX_0:def 3;
A4: len (0.(K,width A,width A))=width A by MATRIX_0:def 2;
then
A5: len (A*(0.(K,width A,width A)))=len A by MATRIX_3:def 4;
A6: width (0.(K,width A,width A))=width A by A2,A4,MATRIX_0:20;
then
A7: width (A*(0.(K,width A,width A)))=width A by A4,MATRIX_3:def 4;
A*(0.(K,width A,width A)) =A*(0.(K,width A,width A)+0.(K,width A,width A
)) by MATRIX_3:4
.= A*(0.(K,width A,width A))+A*(0.(K,width A,width A)) by A2,A3,A4,A6,
MATRIX_4:62;
then
len -(A*(0.(K,width A,width A)))=len (A*(0.(K,width A,width A))) & 0.(K,
len A,width A)=B+B+(-B) by A5,A7,MATRIX_3:def 2,MATRIX_4:2;
then 0.(K,len A,width A)=B+(B-B) by A1,MATRIX_3:3
.=A*(0.(K,width A,width A)) by A5,A1,MATRIX_4:20;
hence thesis;
end;
theorem Th3:
M1 commutes_with 0.(K,n,n)
proof
per cases by NAT_1:3;
suppose
A1: n>0;
A2: len M1 = n & width M1=n by MATRIX_0:24;
then
A3: (0.(K,n,n))*M1=0.(K,n,n) by Th1;
M1*(0.(K,n,n))=0.(K,n,n) by A1,A2,Th2;
hence thesis by A3;
end;
suppose
n = 0;
then len M1 = 0 & len (0.(K,n,n)) = 0 by MATRIX_0:def 2;
hence thesis by CARD_2:64;
end;
end;
theorem
M1 commutes_with M2 & M2 commutes_with M3 & M1 commutes_with M3
implies M1 commutes_with M2*M3
proof
A1: width M1=n by MATRIX_0:24;
A2: width M2=n by MATRIX_0:24;
A3: len M1=n by MATRIX_0:24;
A4: len M3=n by MATRIX_0:24;
A5: width M3=n & len M2=n by MATRIX_0:24;
assume that
A6: M1 commutes_with M2 and
A7: M2 commutes_with M3 and
A8: M1 commutes_with M3;
(M2*M3)*M1=(M3*M2)*M1 by A7
.=M3*(M2*M1) by A2,A3,A5,MATRIX_3:33
.=M3*(M1*M2) by A6
.=(M3*M1)*M2 by A1,A3,A5,MATRIX_3:33
.=(M1*M3)*M2 by A8
.=M1*(M3*M2) by A1,A5,A4,MATRIX_3:33
.=M1*(M2*M3) by A7;
hence thesis;
end;
theorem
M1 commutes_with M2 & M1 commutes_with M3 & n>0 implies
M1 commutes_with M2+M3
proof
A1: width M1=n by MATRIX_0:24;
A2: len M1=n & len M2=n by MATRIX_0:24;
A3: len M3=n by MATRIX_0:24;
assume that
A4: M1 commutes_with M2 and
A5: M1 commutes_with M3 and
A6: n>0;
A7: width M2=n & width M3=n by MATRIX_0:24;
then (M2+M3)*M1=M2*M1+M3*M1 by A2,A3,A6,MATRIX_4:63
.=M1*M2+M3*M1 by A4
.=M1*M2+M1*M3 by A5
.=M1*(M2+M3) by A1,A7,A2,A3,A6,MATRIX_4:62;
hence thesis;
end;
theorem Th6:
M1 commutes_with 1.(K,n)
proof
M1=M1*(1.(K,n)) & M1=1.(K,n)*M1 by MATRIX_3:18,19;
hence thesis;
end;
theorem Th7:
M2 is_reverse_of M3 & M1 is_reverse_of M3 implies M1=M2
proof
A1: width M1=n & width M3=n by MATRIX_0:24;
A2: len M2=n & len M3=n by MATRIX_0:24;
assume that
A3: M2 is_reverse_of M3 and
A4: M1 is_reverse_of M3;
M1=M1*(1.(K,n)) by MATRIX_3:19
.=M1*(M3*M2) by A3
.=(M1*M3)*M2 by A1,A2,MATRIX_3:33
.=(1.(K,n))*M2 by A4
.=M2 by MATRIX_3:18;
hence thesis;
end;
definition
let n be Nat, K be Field, M1 be Matrix of n,K;
assume
A1: M1 is invertible;
func M1~ -> Matrix of n,K means :Def4:
it is_reverse_of M1;
existence by A1;
uniqueness by Th7;
end;
theorem Th8:
(1.(K,n))~ = 1.(K,n) & 1.(K,n) is invertible
proof
(1.(K,n))*(1.(K,n))=1.(K,n) by MATRIX_3:18;
then
A1: 1.(K,n) is_reverse_of 1.(K,n);
then 1.(K,n) is invertible;
hence thesis by A1,Def4;
end;
registration let K be Field, n be Nat;
cluster 1.(K,n) -> invertible;
coherence by Th8;
end;
registration let K be Field, n be Nat;
cluster invertible for Matrix of n, K;
existence
proof
take 1.(K,n);
thus thesis;
end;
end;
theorem
((1.(K,n))~)~ = 1.(K,n)
proof
(1.(K,n))~ = 1.(K,n) by Th8;
hence thesis;
end;
theorem Th10:
(1.(K,n))@ = 1.(K,n)
proof
per cases by NAT_1:3;
suppose
A1: n>0;
A2: len (1.(K,n))=n by MATRIX_0:24;
A3: Indices (1.(K,n)) = [:Seg n, Seg n:] by MATRIX_0:24;
A4: for i,j st [i,j] in Indices (1.(K,n)) holds (1.(K,n))*(i,j)=((1.(K,n))
@)*(i,j)
proof
let i,j;
assume
A5: [i,j] in Indices (1.(K,n));
then i in Seg n & j in Seg n by A3,ZFMISC_1:87;
then
A6: [j,i] in Indices (1.(K,n)) by A3,ZFMISC_1:87;
per cases;
suppose
i=j;
hence thesis by A5,MATRIX_0:def 6;
end;
suppose
i<>j;
then (1.(K,n))*(i,j)=0.K & (1.(K,n))*(j,i)=0.K by A5,A6,MATRIX_1:def 3;
hence thesis by A6,MATRIX_0:def 6;
end;
end;
A7: width (1.(K,n))=n by MATRIX_0:24;
then len ((1.(K,n))@)=width (1.(K,n)) & width ((1.(K,n))@)=len (1.(K,n) )
by A1,MATRIX_0:54;
hence thesis by A7,A2,A4,MATRIX_0:21;
end;
suppose
n=0;
hence thesis by MATRIX_0:45;
end;
end;
theorem
for K being Field, n being Nat holds ((1.(K,n))@)~ = 1.(K,n)
proof
let K,n;
(1.(K,n))@=1.(K,n) by Th10;
hence thesis by Th8;
end;
theorem
M3 is_reverse_of M1 & n>0 implies M1@ is_reverse_of M3@
proof
A1: width M1=n & width M3=n by MATRIX_0:24;
assume that
A2: M3 is_reverse_of M1 and
A3: n>0;
len M1=n & M3*M1=M1*M3 by A2,MATRIX_0:24;
then
A4: (M1*M3)@=(M1@)*(M3@) by A1,A3,MATRIX_3:22; then
A5: (M1@)*(M3@)=1.(K,n) by Th10,A2;
len M3=n by MATRIX_0:24;
then (M3@)*(M1@)=(M1@)*(M3@) by A1,A3,A4,MATRIX_3:22;
hence thesis by A5;
end;
theorem Th13:
M is invertible implies M@ is invertible & M@~= M~@
proof
assume
A1: M is invertible;
set M1=M@, M2=M~@;
per cases by NAT_1:3;
suppose
A2: n > 0;
A3: width M=n & width (M~)=n by MATRIX_0:24;
len M=n by MATRIX_0:24; then
A4: ((M~)*M)@=(M@)*(M~@) by A2,A3,MATRIX_3:22;
A5: M~ is_reverse_of M by A1,Def4; then
A6: M1*M2=1.(K,n) by A4,Th10;
len (M~)=n by MATRIX_0:24;
then (M*(M~))@=(M~@)*(M@) by A2,A3,MATRIX_3:22;
then M1*M2=M2*M1 by A5,A4;
then
A7: M1 is_reverse_of M2 by A6;
then M1 is invertible;
hence thesis by A7,Def4;
end;
suppose n = 0; then
B1: M = 1.(K,n) by MATRIX_0:45; then
B2: M1 = 1.(K,n) by Th10; then
M@~ = 1.(K,n) by Th8;
hence thesis by B1,B2;
end;
end;
registration let K, n;
let M be invertible Matrix of n, K;
cluster M@ -> invertible;
coherence by Th13;
end;
theorem
for K being Field, n being Nat, 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
let K,n,M1,M2,M3,M4;
A1: width M1=n by MATRIX_0:24;
A2: width M2=n & len M1=n by MATRIX_0:24;
A3: len M3=n by MATRIX_0:24;
A4: width M3=n & len M4=n by MATRIX_0:24;
assume that
A5: M3 is_reverse_of M1 and
A6: M4 is_reverse_of M2;
width (M2*M1)=n by MATRIX_0:24;
then
A7: (M2*M1)*(M3*M4)=((M2*M1)*M3)*M4 by A3,A4,MATRIX_3:33
.=(M2*(M1*M3))*M4 by A1,A2,A3,MATRIX_3:33
.=(M2*(1.(K,n)))*M4 by A5
.=M2*M4 by MATRIX_3:19
.=1.(K,n) by A6;
A8: width M4=n by MATRIX_0:24;
A9: len M2=n by MATRIX_0:24;
width (M3*M4)=n by MATRIX_0:24;
then (M3*M4)*(M2*M1)=((M3*M4)*M2)*M1 by A2,A9,MATRIX_3:33
.=(M3*(M4*M2))*M1 by A9,A8,A4,MATRIX_3:33
.=(M3*(1.(K,n)))*M1 by A6
.=M3*M1 by MATRIX_3:19
.=1.(K,n) by A5;
hence thesis by A7;
end;
theorem
for K being Field, n being Nat, M1,M2 being Matrix of n,K st
M2 is_reverse_of M1 holds M1 commutes_with M2;
theorem Th16:
M is invertible implies M~ is invertible & (M~)~= M
proof
assume M is invertible; then
A1: M~ is_reverse_of M by Def4;
then M~ is invertible;
hence thesis by A1,Def4;
end;
registration let K, n;
let M be invertible Matrix of n, K;
cluster M~ -> invertible;
coherence by Th16;
end;
theorem
n > 0 & M1*M2=0.(K,n,n) & M1 is invertible implies M1 commutes_with M2
proof
assume that
A1: n > 0 and
A2: M1*M2=0.(K,n,n) and
A3: M1 is invertible;
A4: M1~ is_reverse_of M1 by A3,Def4;
A5: len M2 = n by MATRIX_0:24;
A6: len M1=n & width M1=n by MATRIX_0:24;
A7: len (M1~) =n by MATRIX_0:24;
A8: width (M1~) = n by MATRIX_0:24;
M2=(1.(K,n))*M2 by MATRIX_3:18
.=(M1~*M1)*M2 by A4
.=M1~*(0.(K,n,n)) by A2,A6,A5,A8,MATRIX_3:33
.=0.(K,n,n) by A1,A7,A8,Th2;
hence thesis by Th3;
end;
theorem
M1=M1*M2 & M1 is invertible implies M1 commutes_with M2
proof
assume that
A1: M1=M1*M2 and
A2: M1 is invertible;
A3: M1~ is_reverse_of M1 by A2,Def4;
A4: len M2=n & width (M1~) = n by MATRIX_0:24;
A5: len M1=n & width M1=n by MATRIX_0:24;
M2=(1.(K,n))*M2 by MATRIX_3:18
.=(M1~*M1)*M2 by A3
.=M1~*M1 by A1,A5,A4,MATRIX_3:33
.=1.(K,n) by A3;
hence thesis by Th6;
end;
theorem
M1=M2*M1 & M1 is invertible implies M1 commutes_with M2
proof
assume that
A1: M1=M2*M1 and
A2: M1 is invertible;
A3: M1~ is_reverse_of M1 by A2,Def4;
A4: width M2=n & len (M1~)=n by MATRIX_0:24;
A5: len M1=n & width M1=n by MATRIX_0:24;
M2=M2*(1.(K,n)) by MATRIX_3:19
.=M2*(M1*M1~) by A3
.=M1*M1~ by A1,A5,A4,MATRIX_3:33
.=1.(K,n) by A3;
hence thesis by Th6;
end;
definition
let n be Nat, K be Field;
let M1 be Matrix of n,K;
attr M1 is symmetric means
M1@=M1;
end;
registration
let n be Nat, K be Field;
cluster 1.(K,n) -> symmetric;
coherence
by Th10;
end;
theorem Th20:
((n,n)-->a)@ = (n,n)-->a
proof
len ((n,n)-->a)=n by MATRIX_0:24;
then
A1: len(((n,n)-->a)@)=len ((n,n)-->a) by MATRIX_0:24;
A2: Indices ((n,n)-->a)=[:Seg n, Seg n:] by MATRIX_0:24;
A3: for i,j st [i,j] in Indices (((n,n)-->a)@) holds (((n,n)-->a)@)*(i,j)=
((n,n)-->a)*(i,j)
proof
let i,j;
assume [i,j] in Indices (((n,n)-->a)@);
then
A4: [i,j] in Indices (((n,n)-->a)) by MATRIX_0:26;
then i in Seg n & j in Seg n by A2,ZFMISC_1:87;
then [j,i] in Indices ((n,n)-->a) by A2,ZFMISC_1:87;
then (((n,n)-->a)@)*(i,j)=((n,n)-->a)*(j,i) & ((n,n)-->a)*(j,i)=a by
MATRIX_0:46,def 6;
hence thesis by A4,MATRIX_0:46;
end;
width ((n,n)-->a)=n by MATRIX_0:24;
then width (((n,n)-->a)@) = width ((n,n)-->a) by MATRIX_0:24;
hence thesis by A1,A3,MATRIX_0:21;
end;
theorem
(n,n)-->a is symmetric by Th20;
theorem
n > 0 & M1 is symmetric & M2 is symmetric implies (M1 commutes_with M2
iff M1*M2 is symmetric)
proof
assume that
A1: n > 0 and
A2: M1 is symmetric & M2 is symmetric;
A3: width M1=n & len M2=n by MATRIX_0:24;
A4: width M2=n by MATRIX_0:24;
A5: M1@=M1 & M2@=M2 by A2;
thus M1 commutes_with M2 implies M1*M2 is symmetric
by A1,A5,A3,A4,MATRIX_3:22;
assume
A6: M1*M2 is symmetric;
M2*M1=(M1*M2)@ by A1,A5,A3,A4,MATRIX_3:22
.=M1*M2 by A6;
hence thesis;
end;
theorem Th23:
(M1+M2)@=M1@+M2@
proof
for i,j st [i,j] in Indices ((M1+M2)@) holds ((M1+M2)@)*(i,j)=(M1@+M2@)*
(i,j)
proof
let i,j;
assume [i,j] in Indices ((M1+M2)@);
then
A1: [i,j] in [:Seg n, Seg n:] by MATRIX_0:24;
then
A2: [i,j] in Indices (M1@) by MATRIX_0:24;
i in Seg n & j in Seg n by A1,ZFMISC_1:87;
then
A3: [j,i] in [:Seg n, Seg n:] by ZFMISC_1:87;
then
A4: [j,i] in Indices M1 by MATRIX_0:24;
A5: [j,i] in Indices M2 by A3,MATRIX_0:24;
[j,i] in Indices (M1+M2) by A3,MATRIX_0:24;
then ((M1+M2)@)*(i,j)=(M1+M2)*(j,i) by MATRIX_0:def 6
.=M1*(j,i)+M2*(j,i) by A4,MATRIX_3:def 3
.=(M1@)*(i,j)+M2*(j,i) by A4,MATRIX_0:def 6
.=(M1@)*(i,j)+(M2@)*(i,j) by A5,MATRIX_0:def 6
.=(M1@+M2@)*(i,j) by A2,MATRIX_3:def 3;
hence thesis;
end;
hence thesis by MATRIX_0:27;
end;
theorem
M1 is symmetric & M2 is symmetric implies M1+M2 is symmetric by Th23;
theorem ::: should be a cluster
M1 is upper_triangular Matrix of n,K & M1 is lower_triangular Matrix
of n,K implies M1 is symmetric
proof
assume
A1: M1 is upper_triangular Matrix of n,K & M1 is lower_triangular Matrix
of n,K;
A2: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
for i,j st [i,j] in Indices M1 holds M1@*(i,j)=M1*(i,j)
proof
let i,j;
assume
A3: [i,j] in Indices M1;
then [i,j] in [:Seg n, Seg n:] by MATRIX_0:24;
then i in Seg n & j in Seg n by ZFMISC_1:87;
then
A4: [j,i] in Indices M1 by A2,ZFMISC_1:87;
per cases;
suppose
i=j;
hence thesis by A4,MATRIX_0:def 6;
end;
suppose
A5: i<>j;
per cases by A5,XXREAL_0:1;
suppose
ij;
then M1*(i,j)=0.K & M1*(j,i)=0.K by A1,A3,A4,MATRIX_1:def 8,def 9;
hence thesis by A4,MATRIX_0:def 6;
end;
end;
end;
hence thesis by MATRIX_0:27;
end;
theorem Th26:
for K being Field,n being Nat,M1 being Matrix of n,K holds (-M1) @=-(M1@)
proof
let K,n,M1;
for i,j st [i,j] in Indices ((-M1)@) holds ((-M1)@)*(i,j)=(-(M1@))*(i,j)
proof
let i,j;
assume
A1: [i,j] in Indices ((-M1)@);
then
A2: [i,j] in Indices M1@ by MATRIX_0:26;
[i,j] in [:Seg n, Seg n:] by A1,MATRIX_0:24;
then i in Seg n & j in Seg n by ZFMISC_1:87;
then
A3: [j,i] in [:Seg n, Seg n:] by ZFMISC_1:87;
then
A4: [j,i] in Indices M1 by MATRIX_0:24;
[j,i] in Indices (-M1) by A3,MATRIX_0:24;
then ((-M1)@)*(i,j)=(-M1)*(j,i) by MATRIX_0:def 6
.=-(M1*(j,i)) by A4,MATRIX_3:def 2
.=-(M1@*(i,j)) by A4,MATRIX_0:def 6
.=(-(M1@))*(i,j) by A2,MATRIX_3:def 2;
hence thesis;
end;
hence thesis by MATRIX_0:27;
end;
theorem
for K being Field, n being Nat, M1 being Matrix of n,K st M1 is
symmetric holds -M1 is symmetric
by Th26;
theorem
for K being Field,n being Nat,M1,M2 being Matrix of n,K st M1 is
symmetric & M2 is symmetric holds M1-M2 is symmetric
proof
let K,n,M1,M2;
assume that
A1: M1 is symmetric and
A2: M2 is symmetric;
(M1-M2)@=M1@+(-M2)@ by Th23
.=M1+(-M2)@ by A1
.=M1+-(M2@) by Th26
.=M1-M2 by A2;
hence thesis;
end;
definition
let n be Nat,K be Field;
let M1 be Matrix of n,K;
attr M1 is antisymmetric means
M1@=-M1;
end;
theorem
for K being Fanoian Field,n being Nat,M1 being Matrix of n,K st M1 is
symmetric antisymmetric holds M1=0.(K,n,n)
proof
let K be Fanoian Field;
let n;
let M1 be Matrix of n,K;
assume M1 is symmetric antisymmetric;
then
A1: M1@=M1 & M1@=-M1;
for i,j st [i,j] in Indices M1 holds M1*(i,j)=(0.(K,n,n))*(i,j)
proof
let i,j;
assume
A2: [i,j] in Indices M1;
then M1*(i,j)=-M1*(i,j) by A1,MATRIX_3:def 2;
then M1*(i,j)+M1*(i,j)=0.K by RLVECT_1:5;
then (1_K)*(M1*(i,j))+(1_K)*(M1*(i,j))=0.K;
then 1_K+1_K<>0.K & (1_K+1_K)*(M1*(i,j))=0.K by VECTSP_1:def 7,def 19;
then
A3: M1*(i,j)=0.K by VECTSP_1:12;
[i,j] in Indices (0.(K,n,n)) by A2,MATRIX_0:26;
hence thesis by A3,MATRIX_3:1;
end;
hence thesis by MATRIX_0:27;
end;
theorem
for K being Fanoian Field,n,i being Nat,M1 being Matrix of n,K st M1
is antisymmetric & i in Seg n holds M1*(i,i) =0.K
proof
let K be Fanoian Field;
let n,i;
let M1 be Matrix of n,K;
assume that
A1: M1 is antisymmetric and
A2: i in Seg n;
A3: M1@=-M1 by A1;
Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
then
A4: [i,i] in Indices M1 by A2,ZFMISC_1:87;
then M1@*(i,i)=M1*(i,i) by MATRIX_0:def 6;
then M1*(i,i)=-M1*(i,i) by A4,A3,MATRIX_3:def 2;
then M1*(i,i)+M1*(i,i)=0.K by RLVECT_1:5;
then (1_K)*(M1*(i,i))+(1_K)*(M1*(i,i))=0.K;
then 1_K+1_K<>0.K & (1_K+1_K)*(M1*(i,i))=0.K by VECTSP_1:def 7,def 19;
hence thesis by VECTSP_1:12;
end;
theorem
for K being Field,n being Nat,M1,M2 being Matrix of n,K st M1 is
antisymmetric & M2 is antisymmetric holds M1+M2 is antisymmetric
proof
let K,n,M1,M2;
assume that
A1: M1 is antisymmetric and
A2: M2 is antisymmetric;
A3: len M1=n & width M1=n by MATRIX_0:24;
A4: len M2=n & width M2=n by MATRIX_0:24;
(M1+M2)@=M1@+M2@ by Th23
.=-M1+M2@ by A1
.=-M1+-M2 by A2
.=-(M1+M2) by A3,A4,MATRIX_4:12;
hence thesis;
end;
theorem
for K being Field,n being Nat,M1 being Matrix of n,K st M1 is
antisymmetric holds -M1 is antisymmetric
by Th26;
theorem
for K being Field,n being Nat,M1,M2 being Matrix of n,K st M1 is
antisymmetric & M2 is antisymmetric holds M1-M2 is antisymmetric
proof
let K,n,M1,M2;
assume that
A1: M1 is antisymmetric and
A2: M2 is antisymmetric;
A3: len (-M2)=n & width (-M2)=n by MATRIX_0:24;
A4: len M1=n & width M1=n by MATRIX_0:24;
(M1-M2)@=M1@+(-M2)@ by Th23
.=-M1+(-M2)@ by A1
.=-M1+-(M2@) by Th26
.=-M1+-(-M2) by A2
.=-(M1-M2) by A3,A4,MATRIX_4:12;
hence thesis;
end;
theorem
n>0 implies M1-M1@ is antisymmetric
proof
assume
A1: n>0;
set M2=M1-(M1@);
A2: len M1 = n & width M1=n by MATRIX_0:24;
A3: len (M1@)=n & width (M1@)=n by MATRIX_0:24;
M2@=M1@+(-(M1@))@ by Th23
.=M1@+-((M1@)@) by Th26
.=M1@-M1 by A1,A2,MATRIX_0:57
.=-(M1-M1@) by A2,A3,MATRIX_4:43;
hence thesis;
end;
theorem
n>0 implies (M1 commutes_with M2 iff (M1+M2)*(M1+M2)=M1*M1+M1*M2+M1*M2
+M2*M2)
proof
assume
A1: n>0;
A2: len (M1*M2)=n & width (M1*M2)=n by MATRIX_0:24;
A3: len (M1*M1+M1*M2)=n & width (M1*M1+M1*M2)=n by MATRIX_0:24;
A4: len (M1*M2+M2*M2)=n & width (M1*M2+M2*M2)=n by MATRIX_0:24;
A5: len (M1*M1)=n & width (M1*M1)=n by MATRIX_0:24;
A6: len M1 =n & width M1=n by MATRIX_0:24;
A7: len (M1*M1+M2*M1)=n & width (M1*M1+M2*M1)=n by MATRIX_0:24;
A8: len M2=n & width M2=n by MATRIX_0:24;
A9: len (M1+M2)=n & width (M1+M2)=n by MATRIX_0:24;
thus M1 commutes_with M2 implies (M1+M2)*(M1+M2)=M1*M1+M1*M2+M1*M2+M2*M2
proof
assume
A10: M1 commutes_with M2;
(M1+M2)*(M1+M2)=(M1+M2)*M1+(M1+M2)*M2 by A1,A6,A8,A9,MATRIX_4:62
.=M1*M1+M2*M1+(M1+M2)*M2 by A1,A6,A8,MATRIX_4:63
.=M1*M1+M2*M1+(M1*M2+M2*M2) by A1,A6,A8,MATRIX_4:63
.=M1*M1+M2*M1+M1*M2+M2*M2 by A2,A7,MATRIX_3:3;
hence thesis by A10;
end;
assume
A11: (M1+M2)*(M1+M2)=M1*M1+M1*M2+M1*M2+M2*M2;
A12: len (M2*M1)=n & width (M2*M1)=n by MATRIX_0:24;
(M1+M2)*(M1+M2)=(M1+M2)*M1+(M1+M2)*M2 by A1,A6,A8,A9,MATRIX_4:62
.=M1*M1+M2*M1+(M1+M2)*M2 by A1,A6,A8,MATRIX_4:63
.=M1*M1+M2*M1+(M1*M2+M2*M2) by A1,A6,A8,MATRIX_4:63
.=M1*M1+M2*M1+M1*M2+M2*M2 by A2,A7,MATRIX_3:3;
then M1*M1+M2*M1+(M1*M2+M2*M2)=M1*M1+M1*M2+M1*M2+M2*M2 by A2,A7,A11,
MATRIX_3:3;
then M1*M1+M2*M1+(M1*M2+M2*M2)=M1*M1+M1*M2+(M1*M2+M2*M2) by A2,A3,MATRIX_3:3;
then M1*M1+M2*M1=M1*M1+M1*M2 by A7,A4,A3,MATRIX_4:4;
then M2*M1+M1*M1=M1*M1+M1*M2 by A5,A12,MATRIX_3:2;
then M2*M1+M1*M1=M1*M2+M1*M1 by A5,A2,MATRIX_3:2;
hence thesis by A5,A2,A12,MATRIX_4:4;
end;
theorem Th36:
M1 is invertible & M2 is invertible implies M1*M2 is invertible
& (M1*M2)~=(M2~)*(M1~)
proof
assume that
A1: M1 is invertible and
A2: M2 is invertible;
A3: M2~ is_reverse_of M2 by A2,Def4;
A4: M1~ is_reverse_of M1 by A1,Def4;
A5: len (M2~)=n by MATRIX_0:24;
A6: width (M1~)=n by MATRIX_0:24;
A7: len M1=n by MATRIX_0:24;
A8: width M2=n by MATRIX_0:24;
A9: width M1=n & len M2=n by MATRIX_0:24;
A10: width (M2~)=n & len (M1~)=n by MATRIX_0:24;
width (M1*M2)=n by MATRIX_0:24;
then
A11: (M1*M2)*(M2~*M1~)=((M1*M2)*M2~)*M1~ by A5,A10,MATRIX_3:33
.=(M1*(M2*M2~))*M1~ by A9,A8,A5,MATRIX_3:33
.=(M1*(1.(K,n)))*M1~ by A3
.=M1*M1~ by MATRIX_3:19
.=1.(K,n) by A4;
width (M2~*M1~)=n by MATRIX_0:24;
then (M2~*M1~)*(M1*M2)=(M2~*M1~)*M1*M2 by A9,A7,MATRIX_3:33
.=(M2~*(M1~*M1))*M2 by A7,A6,A10,MATRIX_3:33
.=(M2~*(1.(K,n)))*M2 by A4
.=M2~*M2 by MATRIX_3:19
.=1.(K,n) by A3;
then
A12: (M2~)*(M1~) is_reverse_of M1*M2 by A11;
then M1*M2 is invertible;
hence thesis by A12,Def4;
end;
theorem
M1 is invertible & M2 is invertible & M1 commutes_with M2 implies M1*
M2 is invertible & (M1*M2)~ = (M1~)*(M2~)
proof
assume that
A1: M1 is invertible and
A2: M2 is invertible and
A3: M1 commutes_with M2;
A4: M2~ is_reverse_of M2 by A2,Def4;
A5: width (M1~*M2~)=n by MATRIX_0:24;
A6: width (M2~)=n by MATRIX_0:24;
A7: len M2=n by MATRIX_0:24;
A8: width M1=n by MATRIX_0:24;
A9: width M2=n & len M1=n by MATRIX_0:24;
A10: M1~ is_reverse_of M1 by A1,Def4;
A11: width (M1~)=n & len (M2~)=n by MATRIX_0:24;
A12: len (M1~)=n by MATRIX_0:24;
width (M1*M2)=n by MATRIX_0:24;
then
A13: (M1*M2)*(M1~*M2~)=((M1*M2)*M1~)*M2~ by A11,A12,MATRIX_3:33
.=((M2*M1)*M1~)*M2~ by A3
.=(M2*(M1*M1~))*M2~ by A8,A9,A12,MATRIX_3:33
.=(M2*(1.(K,n)))*M2~ by A10
.=M2*M2~ by MATRIX_3:19
.=1.(K,n) by A4;
(M1~)*(M2~)*(M1*M2)=(M1~)*(M2~)*(M2*M1) by A3
.=(M1~)*(M2~)*M2*M1 by A7,A9,A5,MATRIX_3:33
.=((M1~)*((M2~)*M2))*M1 by A7,A11,A6,MATRIX_3:33
.=((M1~)*(1.(K,n)))*M1 by A4
.=(M1~)*M1 by MATRIX_3:19
.=1.(K,n) by A10;
then
A14: (M1~)*(M2~) is_reverse_of M1*M2 by A13;
then M1*M2 is invertible;
hence thesis by A14,Def4;
end;
theorem
M1 is invertible & M1*M2=1.(K,n) implies M1 is_reverse_of M2
proof
A1: width M1=n & len M1=n by MATRIX_0:24;
A2: len M2=n & width (M1~)=n by MATRIX_0:24;
assume that
A3: M1 is invertible and
A4: M1*M2=1.(K,n);
A5: M1~ is_reverse_of M1 by A3,Def4;
M1~*(M1*M2)=M1~ by A4,MATRIX_3:19;
then (M1~*M1)*M2=M1~ by A1,A2,MATRIX_3:33;
then (1.(K,n))*M2=M1~ by A5;
then M2=M1~ by MATRIX_3:18;
hence thesis by A3,Def4;
end;
theorem
M2 is invertible & M2*M1=1.(K,n) implies M1 is_reverse_of M2
proof
A1: len M1=n & width M2=n by MATRIX_0:24;
A2: len M2=n & width (M2~)=n by MATRIX_0:24;
assume that
A3: M2 is invertible and
A4: M2*M1=1.(K,n);
A5: M2~ is_reverse_of M2 by A3,Def4;
(M2~)*(M2*M1)=M2~ by A4,MATRIX_3:19;
then (M2~*M2)*M1=M2~ by A1,A2,MATRIX_3:33;
then (1.(K,n))*M1=M2~ by A5;
then M1=M2~ by MATRIX_3:18;
hence thesis by A3,Def4;
end;
theorem Th40:
M1 is invertible & M1 commutes_with M2 implies M1~ commutes_with M2
proof
assume that
A1: M1 is invertible and
A2: M1 commutes_with M2;
A3: M1~ is_reverse_of M1 by A1,Def4;
A4: width M2=n by MATRIX_0:24;
A5: width M1=n & len M1=n by MATRIX_0:24;
A6: len (M2*M1)=n & width (M2*M1)=n by MATRIX_0:24;
A7: len (M1~)=n by MATRIX_0:24;
A8: len M2=n by MATRIX_0:24;
A9: width (M1~)=n by MATRIX_0:24;
M2=(1.(K,n))*M2 by MATRIX_3:18
.=(M1~*M1)*M2 by A3
.=M1~*(M1*M2) by A5,A8,A9,MATRIX_3:33
.=M1~*(M2*M1) by A2;
then M2*M1~=M1~*((M2*M1)*M1~) by A9,A7,A6,MATRIX_3:33
.=M1~*(M2*(M1*M1~)) by A5,A4,A7,MATRIX_3:33
.=M1~*(M2*(1.(K,n))) by A3
.=M1~*M2 by MATRIX_3:19;
hence thesis;
end;
definition
let n be Nat, K be Field;
let M1 be Matrix of n,K;
attr M1 is Orthogonal means
M1 is invertible & M1@ = M1~;
end;
theorem Th41:
M1*(M1@)=1.(K,n) & M1 is invertible iff M1 is Orthogonal
proof
A1: width M1=n & len M1=n by MATRIX_0:24;
A2: len (M1@)=n by MATRIX_0:24;
A3: width (M1~)=n by MATRIX_0:24;
A4: len (M1~)=n by MATRIX_0:24;
thus M1*(M1@)=1.(K,n) & M1 is invertible implies M1 is Orthogonal
proof
assume that
A5: M1*(M1@)=1.(K,n) and
A6: M1 is invertible;
A7: M1~ is_reverse_of M1 by A6,Def4;
then M1~*(M1*M1~)=M1~*(M1*(M1@)) by A5;
then (M1~*M1)*M1~=M1~*(M1*(M1@)) by A1,A3,A4,MATRIX_3:33;
then (M1~*M1)*M1~=(M1~*M1)*(M1@) by A1,A3,A2,MATRIX_3:33;
then (1.(K,n))*M1~=(M1~*M1)*(M1@) by A7;
then (1.(K,n))*M1~=(1.(K,n))*(M1@) by A7;
then M1~=(1.(K,n))*(M1@) by MATRIX_3:18;
then M1~=M1@ by MATRIX_3:18;
hence thesis by A6;
end;
assume
A8: M1 is Orthogonal;
then
A9: M1~ is_reverse_of M1 by Def4;
M1*(M1@)=M1*M1~ by A8;
hence thesis by A9;
end;
theorem Th42:
M1 is invertible & (M1@)*M1=1.(K,n) iff M1 is Orthogonal
proof
A1: width M1=n & len M1=n by MATRIX_0:24;
A2: width (M1@)=n by MATRIX_0:24;
A3: len (M1~)=n by MATRIX_0:24;
A4: width (M1~)=n by MATRIX_0:24;
thus M1 is invertible & (M1@)*M1=1.(K,n) implies M1 is Orthogonal
proof
assume that
A5: M1 is invertible and
A6: (M1@)*M1=1.(K,n);
A7: M1~ is_reverse_of M1 by A5,Def4;
then (M1~*M1)*M1~=((M1@)*M1)*M1~ by A6;
then M1~*(M1*M1~)=((M1@)*M1)*M1~ by A1,A4,A3,MATRIX_3:33;
then M1~*(M1*M1~)=(M1@)*(M1*M1~) by A1,A3,A2,MATRIX_3:33;
then M1~*(1.(K,n))=(M1@)*(M1*M1~) by A7;
then M1~*(1.(K,n))=(M1@)*(1.(K,n)) by A7;
then M1~=(M1@)*(1.(K,n)) by MATRIX_3:19;
then M1~=M1@ by MATRIX_3:19;
hence thesis by A5;
end;
assume
A8: M1 is Orthogonal;
then
A9: M1~ is_reverse_of M1 by Def4;
(M1@)*M1=M1~*M1 by A8;
hence thesis by A9;
end;
theorem
M1 is Orthogonal implies (M1@)*M1=M1*(M1@)
proof
assume
A1: M1 is Orthogonal;
then (M1@)*M1=1.(K,n) by Th42;
hence thesis by A1,Th41;
end;
theorem
M1 is Orthogonal & M1 commutes_with M2 implies M1@ commutes_with M2
by Th40;
theorem Th45:
M1 is invertible & M2 is invertible implies M1*M2 is invertible
& (M1*M2)~=M2~*M1~
proof
assume that
A1: M1 is invertible and
A2: M2 is invertible;
A3: M1~ is_reverse_of M1 by A1,Def4;
A4: M2~ is_reverse_of M2 by A2,Def4;
A5: len M1=n by MATRIX_0:24;
A6: width (M1~)=n by MATRIX_0:24;
A7: width M1=n & len M2=n by MATRIX_0:24;
A8: width M2=n by MATRIX_0:24;
A9: len (M2~)=n by MATRIX_0:24;
A10: width (M2~)=n & len (M1~)=n by MATRIX_0:24;
width (M2~*M1~)=n by MATRIX_0:24;
then
A11: (M2~*M1~)*(M1*M2)=(((M2~)*(M1~))*M1)*M2 by A7,A5,MATRIX_3:33
.=((M2~)*((M1~)*M1))*M2 by A5,A6,A10,MATRIX_3:33
.=((M2~)*(1.(K,n)))*M2 by A3
.=(M2~)*M2 by MATRIX_3:19
.=1.(K,n) by A4;
width (M1*M2)=n by MATRIX_0:24;
then (M1*M2)*(M2~*M1~)=((M1*M2)*M2~)*M1~ by A9,A10,MATRIX_3:33
.=(M1*(M2*M2~))*M1~ by A7,A8,A9,MATRIX_3:33
.=(M1*(1.(K,n)))*M1~ by A4
.=M1*M1~ by MATRIX_3:19
.=1.(K,n) by A3;
then
A12: (M2~*M1~) is_reverse_of M1*M2 by A11;
then M1*M2 is invertible;
hence thesis by A12,Def4;
end;
theorem
n > 0 & M1 is Orthogonal & M2 is Orthogonal implies M1*M2 is Orthogonal
proof
assume that
A1: n > 0 and
A2: M1 is Orthogonal & M2 is Orthogonal;
M1 is invertible & M2 is invertible by A2;
then
A3: M1*M2 is invertible & (M1*M2)~=M2~*M1~ by Th45;
A4: width M2=n by MATRIX_0:24;
A5: width M1=n & len M2=n by MATRIX_0:24;
M1@=M1~ & M2@=M2~ by A2;
then (M1*M2)@ = M2~*M1~ by A1,A5,A4,MATRIX_3:22;
hence thesis by A3;
end;
theorem
M1 is Orthogonal & M1 commutes_with M2 implies M1@ commutes_with M2
proof
set M3=M1@;
assume that
A1: M1 is Orthogonal and
A2: M1 commutes_with M2;
M1 is invertible by A1;
then
A3: M1~ is_reverse_of M1 by Def4;
A4: width M2=n by MATRIX_0:24;
A5: width M1=n by MATRIX_0:24;
A6: len M2=n & width (M1~)=n by MATRIX_0:24;
A7: len (M1~)=n & width (M1~*M2)=n by MATRIX_0:24;
A8: len M1=n by MATRIX_0:24;
M2*M3=((1.(K,n))*M2)*(M1@) by MATRIX_3:18
.=((M1~*M1)*M2)*(M1@) by A3
.=(M1~*(M1*M2))*(M1@) by A5,A8,A6,MATRIX_3:33
.=(M1~*(M2*M1))*(M1@) by A2
.=(M1~*(M2*M1))*(M1~) by A1
.=(M1~*M2)*M1*(M1~) by A4,A8,A6,MATRIX_3:33
.=(M1~*M2)*(M1*(M1~)) by A5,A8,A7,MATRIX_3:33
.=(M1~*M2)*(1.(K,n)) by A3
.=M1~*M2 by MATRIX_3:19
.=M3*M2 by A1;
hence thesis;
end;
theorem
n > 0 & M1 commutes_with M2 implies M1+M1 commutes_with M2
proof
assume that
A1: n >0 and
A2: M1 commutes_with M2;
A3: width M2=n by MATRIX_0:24;
A4: len M1=n by MATRIX_0:24;
A5: width M1=n & len M2=n by MATRIX_0:24;
then (M1+M1)*M2=M1*M2+M1*M2 by A1,A4,MATRIX_4:63
.=M2*M1+M1*M2 by A2
.=M2*M1+M2*M1 by A2
.=M2*(M1+M1) by A1,A5,A3,A4,MATRIX_4:62;
hence thesis;
end;
theorem
n >0 & M1 commutes_with M2 implies M1+M2 commutes_with M2
proof
assume that
A1: n >0 and
A2: M1 commutes_with M2;
A3: width M2=n & len M1=n by MATRIX_0:24;
A4: width M1=n & len M2=n by MATRIX_0:24;
then (M1+M2)*M2=M1*M2+M2*M2 by A1,A3,MATRIX_4:63
.=M2*M1+M2*M2 by A2
.=M2*(M1+M2) by A1,A4,A3,MATRIX_4:62;
hence thesis;
end;
theorem
n >0 & M1 commutes_with M2 implies M1+M1 commutes_with M2+M2
proof
assume that
A1: n >0 and
A2: M1 commutes_with M2;
A3: len M2=n by MATRIX_0:24;
A4: len (M1+M1)=n by MATRIX_0:24;
A5: width M2=n by MATRIX_0:24;
A6: width M1=n & len M1=n by MATRIX_0:24;
width (M1+M1)=n by MATRIX_0:24;
then (M1+M1)*(M2+M2)=(M1+M1)*M2+(M1+M1)*M2 by A1,A3,A5,A4,MATRIX_4:62
.=M1*M2+M1*M2+(M1+M1)*M2 by A1,A3,A6,MATRIX_4:63
.=M1*M2+M1*M2+(M1*M2+M1*M2) by A1,A3,A6,MATRIX_4:63
.=M2*M1+M1*M2+(M1*M2+M1*M2) by A2
.=M2*M1+M2*M1+(M1*M2+M1*M2) by A2
.=M2*M1+M2*M1+(M2*M1+M2*M1) by A2
.=M2*(M1+M1)+(M2*M1+M2*M1) by A1,A3,A5,A6,MATRIX_4:62
.=M2*(M1+M1)+M2*(M1+M1) by A1,A3,A5,A6,MATRIX_4:62
.=(M2+M2)*(M1+M1) by A1,A3,A5,A4,MATRIX_4:63;
hence thesis;
end;
theorem
n >0 & M1 commutes_with M2 implies M1+M2 commutes_with M2+M2
proof
assume that
A1: n >0 and
A2: M1 commutes_with M2;
A3: len M2=n & width M2=n by MATRIX_0:24;
A4: len (M1+M2)=n by MATRIX_0:24;
A5: width M1=n & len M1=n by MATRIX_0:24;
width (M1+M2)=n by MATRIX_0:24;
then (M1+M2)*(M2+M2)=(M1+M2)*M2+(M1+M2)*M2 by A1,A3,A4,MATRIX_4:62
.=M1*M2+M2*M2+(M1+M2)*M2 by A1,A3,A5,MATRIX_4:63
.=M1*M2+M2*M2+(M1*M2+M2*M2) by A1,A3,A5,MATRIX_4:63
.=M2*M1+M2*M2+(M1*M2+M2*M2) by A2
.=M2*M1+M2*M2+(M2*M1+M2*M2) by A2
.=M2*(M1+M2)+(M2*M1+M2*M2) by A1,A3,A5,MATRIX_4:62
.=M2*(M1+M2)+M2*(M1+M2) by A1,A3,A5,MATRIX_4:62
.=(M2+M2)*(M1+M2) by A1,A3,A4,MATRIX_4:63;
hence thesis;
end;
theorem
M1 commutes_with M2 implies M1*M2 commutes_with M2
proof
A1: width M1=n & width M2=n by MATRIX_0:24;
A2: len M1=n & len M2=n by MATRIX_0:24;
assume M1 commutes_with M2;
then (M1*M2)*M2=M2*(M1*M2) by A1,A2,MATRIX_3:33;
hence thesis;
end;
theorem
M1 commutes_with M2 implies M1*M1 commutes_with M2
proof
A1: width M2=n by MATRIX_0:24;
A2: width M1=n & len M1=n by MATRIX_0:24;
assume
A3: M1 commutes_with M2;
A4: len M2=n by MATRIX_0:24;
then (M1*M1)*M2=M1*(M1*M2) by A2,MATRIX_3:33
.=M1*(M2*M1) by A3
.=(M1*M2)*M1 by A1,A2,A4,MATRIX_3:33
.=(M2*M1)*M1 by A3
.=M2*(M1*M1) by A1,A2,MATRIX_3:33;
hence thesis;
end;
theorem
M1 commutes_with M2 implies M1*M1 commutes_with M2*M2
proof
A1: width M2=n by MATRIX_0:24;
A2: len (M1*M1)=n by MATRIX_0:24;
A3: width M1=n & len M1=n by MATRIX_0:24;
assume
A4: M1 commutes_with M2;
A5: len M2=n by MATRIX_0:24;
A6: width (M1*M1)=n by MATRIX_0:24;
then (M1*M1)*(M2*M2)=((M1*M1)*M2)*M2 by A1,A5,MATRIX_3:33
.=(M1*(M1*M2))*M2 by A3,A5,MATRIX_3:33
.=(M1*(M2*M1))*M2 by A4
.=((M1*M2)*M1)*M2 by A1,A3,A5,MATRIX_3:33
.=((M2*M1)*M1)*M2 by A4
.=(M2*(M1*M1))*M2 by A1,A3,MATRIX_3:33
.=M2*((M1*M1)*M2) by A1,A5,A6,A2,MATRIX_3:33
.=M2*(M1*(M1*M2)) by A3,A5,MATRIX_3:33
.=M2*(M1*(M2*M1)) by A4
.=M2*((M1*M2)*M1) by A1,A3,A5,MATRIX_3:33
.=M2*((M2*M1)*M1) by A4
.=M2*(M2*(M1*M1)) by A1,A3,MATRIX_3:33
.=(M2*M2)*(M1*M1) by A1,A5,A2,MATRIX_3:33;
hence thesis;
end;
theorem
n>0 & M1 commutes_with M2 implies M1@ commutes_with M2@
proof
A1: width M1=n & width M2=n by MATRIX_0:24;
set M3=M1@, M4=M2@;
A2: len M2=n by MATRIX_0:24;
assume that
A3: n>0 and
A4: M1 commutes_with M2;
len M1=n by MATRIX_0:24;
then M3*M4=(M2*M1)@ by A1,A3,MATRIX_3:22
.=(M1*M2)@ by A4
.=M4*M3 by A1,A2,A3,MATRIX_3:22;
hence thesis;
end;
theorem Th56:
M1 is invertible & M2 is invertible & M3 is invertible implies
M1*M2*M3 is invertible & (M1*M2*M3)~=M3~*M2~*M1~
proof
assume that
A1: M1 is invertible and
A2: M2 is invertible and
A3: M3 is invertible;
A4: M1~ is_reverse_of M1 by A1,Def4;
A5: M2~ is_reverse_of M2 by A2,Def4;
A6: len M3=n by MATRIX_0:24;
A7: M3~ is_reverse_of M3 by A3,Def4;
A8: width (M2~)=n by MATRIX_0:24;
A9: width M3=n by MATRIX_0:24;
A10: width (M1*M2)=n by MATRIX_0:24;
A11: len (M1~)=n by MATRIX_0:24;
set M5 = M3~*M2~*M1~;
set M4=M1*M2*M3;
A12: width M2=n by MATRIX_0:24;
A13: len (M2*M3)=n & width (M3~*M2~*M1~)=n by MATRIX_0:24;
A14: len M2=n by MATRIX_0:24;
A15: width ((M1*M2)*M3)=n & len (M2~*M1~)=n by MATRIX_0:24;
A16: len (M3~)=n by MATRIX_0:24;
A17: width (M3~*M2~)=n by MATRIX_0:24;
A18: width (M3~)=n by MATRIX_0:24;
A19: width (M1~)=n by MATRIX_0:24;
A20: len M1=n by MATRIX_0:24;
A21: len (M2~)=n by MATRIX_0:24;
A22: width M1=n by MATRIX_0:24;
then
A23: M5*M4=(M3~*M2~*M1~)*(M1*(M2*M3)) by A12,A14,A6,MATRIX_3:33
.=((M3~*M2~*M1~)*M1)*(M2*M3) by A22,A20,A13,MATRIX_3:33
.=((M3~*M2~)*(M1~*M1))*(M2*M3) by A20,A19,A11,A17,MATRIX_3:33
.=((M3~*M2~)*(1.(K,n)))*(M2*M3) by A4
.=(M3~*M2~)*(M2*M3) by MATRIX_3:19
.=((M3~*M2~)*M2)*M3 by A12,A14,A6,A17,MATRIX_3:33
.=(M3~*(M2~*M2))*M3 by A14,A8,A18,A21,MATRIX_3:33
.=(M3~*(1.(K,n)))*M3 by A5
.=M3~*M3 by MATRIX_3:19
.=1.(K,n) by A7;
M4*M5 =((M1*M2)*M3)*(M3~*(M2~*M1~)) by A8,A18,A11,A21,MATRIX_3:33
.=(((M1*M2)*M3)*M3~)*(M2~*M1~) by A18,A16,A15,MATRIX_3:33
.=((M1*M2)*(M3*M3~))*(M2~*M1~) by A9,A6,A10,A16,MATRIX_3:33
.=((M1*M2)*(1.(K,n)))*(M2~*M1~) by A7
.=(M1*M2)*(M2~*M1~) by MATRIX_3:19
.=((M1*M2)*M2~)*M1~ by A10,A8,A11,A21,MATRIX_3:33
.=(M1*(M2*M2~))*M1~ by A22,A12,A14,A21,MATRIX_3:33
.=(M1*(1.(K,n)))*M1~ by A5
.=M1*M1~ by MATRIX_3:19
.=1.(K,n) by A4;
then
A24: M5 is_reverse_of M4 by A23;
then M4 is invertible;
hence thesis by A24,Def4;
end;
theorem
n > 0 & M1 is Orthogonal & M2 is Orthogonal & M3 is Orthogonal implies
M1*M2*M3 is Orthogonal
proof
assume that
A1: n > 0 and
A2: M1 is Orthogonal & M2 is Orthogonal and
A3: M3 is Orthogonal;
A4: M3 is invertible by A3;
set M5=M3~*M2~*M1~;
set M4=M1*M2*M3;
A5: width M1=n & len M2=n by MATRIX_0:24;
M1 is invertible & M2 is invertible by A2;
then
A6: M4~=M5 & M4 is invertible by A4,Th56;
A7: width M2=n & M3@=M3~ by A3,MATRIX_0:24;
A8: width (M2~)=n & width (M3~)=n by MATRIX_0:24;
A9: M1@=M1~ & M2@=M2~ by A2;
A10: width (M1*M2)=n by MATRIX_0:24;
A11: len (M1~)=n & len (M2~)=n by MATRIX_0:24;
len M3=n & width M3=n by MATRIX_0:24;
then (M1*M2*M3)@ = M3@*((M1*M2)@) by A1,A10,MATRIX_3:22
.=M3~*(M2~*M1~) by A1,A5,A9,A7,MATRIX_3:22
.=M5 by A8,A11,MATRIX_3:33;
hence thesis by A6;
end;
theorem
1.(K,n) is Orthogonal
proof
A1: (1.(K,n))@=1.(K,n) by Th10;
(1.(K,n))~=1.(K,n) & 1.(K,n) is invertible by Th8;
hence thesis by A1;
end;
theorem
n > 0 & M1 is Orthogonal & M2 is Orthogonal implies M1~*M2 is Orthogonal
proof
assume that
A1: n > 0 and
A2: M1 is Orthogonal and
A3: M2 is Orthogonal;
A4: M1 is invertible by A2; then
A5: M1~ is invertible;
A6: M2 is invertible by A3;
then
A7: M1~*M2 is invertible by A5,Th36;
(M1~*M2)~=M2~*(M1~)~ by A6,A5,Th36;
then
A8: (M1~*M2)~=M2~*M1 by A4,Th16;
A9: len M2=n by MATRIX_0:24;
A10: width (M1~)=n & width M2=n by MATRIX_0:24;
A11: width M1=n & len M1=n by MATRIX_0:24;
M1@=M1~ & M2@=M2~ by A2,A3;
then (M1~*M2)@=(M2~)*((M1@)@) by A1,A10,A9,MATRIX_3:22
.=(M2~)*M1 by A1,A11,MATRIX_0:57;
hence thesis by A7,A8;
end;