:: Some Properties Of Some Special Matrices
:: by Xiaopeng Yue , Xiquan Liang and Zhongpin Sun
::
:: Received December 7, 2005
:: Copyright (c) 2005-2026 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 ORDINAL1, XCMPLX_0, XBOOLE_0, 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, BINOP_1, FUNCOP_1, GROUP_1, MATRIX_6, FUNCSDOM, MATRIX_0;
notations XCMPLX_0, XBOOLE_0, TARSKI, ZFMISC_1, ORDINAL1, NUMBERS, FINSEQ_1,
RLVECT_1, GROUP_1, VECTSP_1, MATRIX_0, STRUCT_0, MATRIX_1, MATRIX_3,
XXREAL_0;
constructors ORDINAL1, XCMPLX_0, NAT_1, XBOOLE_0, XXREAL_0, FVSUM_1, MATRIX_3,
MATRIX_1;
registrations XCMPLX_0, XBOOLE_0, RELSET_1, XREAL_0, STRUCT_0, FINSEQ_1,
VECTSP_1, NAT_1, ORDINAL1, MATRIX_0, MATRIX_1, MATRIX_4;
requirements NUMERALS, BOOLE, SUBSET;
equalities MATRIX_1;
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, R be Ring, M1,M2 be Matrix of n,R;
pred M1 commutes_with M2 means
M1 * M2 = M2 * M1;
reflexivity;
symmetry;
end;
definition
let n be Nat,R be Ring,M1,M2 be Matrix of n,R;
pred M1 is_reverse_of M2 means
M1*M2 = M2*M1 & M1*M2 = 1.(R,n);
symmetry;
end;
definition
let n be Nat, R be Ring;
let M1 be Matrix of n,R;
attr M1 is invertible means
ex M2 be Matrix of n,R 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;
end;
registration
let n;
let K be Ring;
let M1,M2 be Matrix of n,K;
cluster M1+M2 -> (n,n)-size;
coherence;
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 Ring, A being Matrix of K holds
(0.(K,len A,len A))*A = 0.(K,len A,width A)
proof
let K be Ring, A be Matrix of K;
per cases by NAT_1:3;
suppose
A1: len A>0;
set B = (0.(K,len A,len A))*A;
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 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_1:def 4,MATRIX_4:2;
then 0.(K,len A,width A) =B+(B-B) by MATRIX_3:3
.=(0.(K,len A,len A))*A by 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 Ring,A being Matrix of K holds
A*(0.(K,width A,width A))=0.(K,len A,width A)
proof
let K be Ring,A be Matrix of K;
set B= A*(0.(K,width A,width A));
per cases by NAT_1:3;
suppose
A2: width A > 0;
A3: len (0.(K,width A,width A))=width A by MATRIX_0:def 2;
then
A4: len (A*(0.(K,width A,width A)))=len A by MATRIX_3:def 4;
width (0.(K,width A,width A))=width A by A2,A3,MATRIX_0:20;
then
A6: width (A*(0.(K,width A,width A)))=width A by A3,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 A3,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 A4,A6,MATRIX_1:def 4,MATRIX_4:2;
then 0.(K,len A,width A)=B+(B-B) by MATRIX_3:3
.=A*(0.(K,width A,width A)) by MATRIX_4:20;
hence thesis;
end;
suppose
A7: width A = 0;
set LHS = A*(0.(K,width A,width A));
set RHS = (0.(K,len A,width A));
per cases by NAT_1:3;
suppose
A8: len A = 0;
A9: len (0.(K,width A,width A)) = 0 by A7,MATRIX_0:22;
A10: width (0.(K,width A,width A)) = 0 by A7,MATRIX_0:22;
A11: len LHS = len A & width LHS = width (0.(K,width A,width A))
by A7,A9,MATRIX_3:def 4;
then width LHS = 0 by A10;
then Seg (width LHS) = {};
then {} = [:(dom LHS), Seg (width LHS):] by ZFMISC_1:90
.= Indices LHS by MATRIX_0:def 4;
then
A12: for i,j being Nat st [i,j] in Indices LHS
holds LHS * (i,j) = RHS * (i,j);
len LHS = len RHS & width LHS = width RHS
by A8,A10,A11,MATRIX_0:22;
hence thesis by A12,MATRIX_0:21;
end;
suppose
A13: len A > 0;
A14: width (0.(K,width A,width A)) = 0 by A7,MATRIX_0:22;
len (0.(K, width A, width A)) = width A by A7,MATRIX_0:22;
then
A15: len LHS = len A & width LHS = width (0.(K,width A,width A))
by MATRIX_3:def 4;
Seg (width LHS) = {} by A14,A15;
then {} = [:(dom LHS), Seg (width LHS):] by ZFMISC_1:90
.= Indices LHS by MATRIX_0:def 4;
then
A16: for i,j being Nat st [i,j] in Indices LHS
holds LHS * (i,j) = RHS * (i,j);
len LHS = len RHS & width LHS = width RHS
by A7,A14,A15,A13,MATRIX_0:23;
hence thesis by A16,MATRIX_0:21;
end;
end;
end;
theorem Th3:
for K being Ring, M1 being Matrix of n,K
holds M1 commutes_with 0.(K,n,n)
proof
let K be Ring;
let M1 be Matrix of n,K;
A2: len M1 = n & width M1=n by MATRIX_0:24;
then (0.(K,n,n))*M1=0.(K,n,n) by Th1;
hence thesis by A2,Th2;
end;
theorem
for R being Ring
for M1,M2,M3 being Matrix of n,R
holds M1 commutes_with M2 & M2 commutes_with M3 & M1 commutes_with M3
implies M1 commutes_with M2*M3
proof
let R be Ring;
let M1,M2,M3 be Matrix of n,R;
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
for R being Ring
for M1,M2,M3 being Matrix of n,R
holds
M1 commutes_with M2 & M1 commutes_with M3 implies
M1 commutes_with M2+M3
proof
let R be Ring;
let M1,M2,M3 be Matrix of n,R;
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;
A6: width M2=n & width M3=n by MATRIX_0:24;
then (M2 + M3) * M1 = (M2 * M1) + (M3 * M1) by A2,A3,MATRIX_4:63
.= M1*M2 + M3*M1 by A4
.= M1*M2 + M1*M3 by A5
.= M1*(M2 + M3) by A1,A6,A2,A3,MATRIX_4:62;
hence thesis;
end;
theorem Th7:
for R being Ring
for M1 being Matrix of n,R
holds M1 commutes_with 1.(R,n)
proof
let R be Ring;
let M1 be Matrix of n,R;
M1 = M1 * (1.(R,n)) & M1 = 1.(R,n) * M1 by MATRIX_3:18,19;
hence thesis;
end;
theorem Th8:
for R being Ring
for M1,M2,M3 being Matrix of n,R
holds M2 is_reverse_of M3 & M1 is_reverse_of M3 implies M1=M2
proof
let R be Ring;
let M1,M2,M3 be Matrix of n,R;
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.(R,n)) by MATRIX_3:19
.=M1*(M3*M2) by A3
.=(M1*M3)*M2 by A1,A2,MATRIX_3:33
.=(1.(R,n))*M2 by A4
.=M2 by MATRIX_3:18;
hence thesis;
end;
definition
let n be Nat, R be Ring, M1 be Matrix of n,R;
assume
A1: M1 is invertible;
func M1~ -> Matrix of n,R means :Def4:
it is_reverse_of M1;
existence by A1;
uniqueness by Th8;
end;
registration let R be Ring, n be Nat;
cluster 1.(R,n) -> invertible;
coherence
proof
(1.(R,n))*(1.(R,n))=1.(R,n) by MATRIX_3:18;
then 1.(R,n) is_reverse_of 1.(R,n);
hence 1.(R,n) is invertible;
end;
end;
theorem Th9:
for R being Ring
holds (1.(R,n))~ = 1.(R,n) & 1.(R,n) is invertible
proof
let R be Ring;
(1.(R,n))*(1.(R,n))=1.(R,n) by MATRIX_3:18;
then 1.(R,n) is_reverse_of 1.(R,n);
hence thesis by Def4;
end;
registration let R be Ring, n be Nat;
cluster invertible for Matrix of n, R;
existence
proof
take 1.(R,n);
thus thesis;
end;
end;
theorem
for R being Ring
holds ((1.(R,n))~)~ = 1.(R,n)
proof
let R be Ring;
(1.(R,n))~ = 1.(R,n) by Th9;
hence thesis;
end;
theorem Th11:
for R being Ring
holds (1.(R,n))@ = 1.(R,n)
proof
let R be Ring;
per cases by NAT_1:3;
suppose
A1: n>0;
A2: len (1.(R,n))=n by MATRIX_0:24;
A3: Indices (1.(R,n)) = [:Seg n, Seg n:] by MATRIX_0:24;
A4: for i,j st [i,j] in Indices (1.(R,n)) holds (1.(R,n))*(i,j)=((1.(R,n))
@)*(i,j)
proof
let i,j;
assume
A5: [i,j] in Indices (1.(R,n));
then i in Seg n & j in Seg n by A3,ZFMISC_1:87;
then
A6: [j,i] in Indices (1.(R,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.(R,n))*(i,j)=0.R & (1.(R,n))*(j,i)=0.R by A5,A6,MATRIX_1:def 3;
hence thesis by A6,MATRIX_0:def 6;
end;
end;
A7: width (1.(R,n))=n by MATRIX_0:24;
then len ((1.(R,n))@)=width (1.(R,n)) & width ((1.(R,n))@)=len (1.(R,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 R being Ring, n being Nat holds ((1.(R,n))@)~ = 1.(R,n)
proof
let R be Ring; let n;
(1.(R,n))@=1.(R,n) by Th11;
hence thesis by Th9;
end;
theorem
for R being commutative Ring, M1,M3 being Matrix of n,R
holds M3 is_reverse_of M1 & n>0 implies M1@ is_reverse_of M3@
proof
let R be commutative Ring;
let M1,M3 be Matrix of n,R;
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.(R,n) by Th11,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 Th14:
for R being commutative Ring, M being Matrix of n,R
holds M is invertible implies M@ is invertible & M@~= M~@
proof
let R be commutative Ring;
let M be Matrix of n,R;
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.(R,n) by A4,Th11;
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
A8: M = 1.(R,n) by MATRIX_0:45; then
A9: M1 = 1.(R,n) by Th11; then
M@~ = 1.(R,n) by Th9;
hence thesis by A8,A9;
end;
end;
registration let K, n;
let M be invertible Matrix of n, K;
cluster M@ -> invertible;
coherence by Th14;
end;
theorem
for K being Ring, 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 be Ring,n be Nat,M1,M2,M3,M4 be Matrix of n,K;
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 Th17:
for R being Ring, n being Nat
for M being Matrix of n,R
holds M is invertible implies M~ is invertible & (M~)~= M
proof
let R be Ring, n be Nat, M be Matrix of n,R;
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 be Ring, n;
let M be invertible Matrix of n, K;
cluster M~ -> invertible;
coherence by Th17;
end;
theorem
for R being Ring, M1,M2 being Matrix of n,R
holds M1*M2=0.(R,n,n) & M1 is invertible implies M1 commutes_with M2
proof
let R be Ring;
let M1,M2 be Matrix of n,R;
assume that
A2: M1*M2=0.(R,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.(R,n))*M2 by MATRIX_3:18
.=(M1~*M1)*M2 by A4
.=M1~*(0.(R,n,n)) by A2,A6,A5,A8,MATRIX_3:33
.=0.(R,n,n) by A7,A8,Th2;
hence thesis by Th3;
end;
theorem
for R being Ring, M1,M2 being Matrix of n,R
holds M1=M1*M2 & M1 is invertible implies M1 commutes_with M2
proof
let R be Ring;
let M1,M2 be Matrix of n,R;
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.(R,n))*M2 by MATRIX_3:18
.=(M1~*M1)*M2 by A3
.=M1~*M1 by A1,A5,A4,MATRIX_3:33
.=1.(R,n) by A3;
hence thesis by Th7;
end;
theorem
for R being Ring, M1,M2 being Matrix of n,R
holds M1=M2*M1 & M1 is invertible implies M1 commutes_with M2
proof
let R be Ring;
let M1,M2 be Matrix of n,R;
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.(R,n)) by MATRIX_3:19
.=M2*(M1*M1~) by A3
.=M1*M1~ by A1,A5,A4,MATRIX_3:33
.=1.(R,n) by A3;
hence thesis by Th7;
end;
definition
let n be Nat, K be Ring;
let M1 be Matrix of n,K;
attr M1 is symmetric means
M1@=M1;
end;
registration
let n be Nat, K be Ring;
cluster 1.(K,n) -> symmetric;
coherence by Th11;
end;
theorem Th21:
for R being Ring, a being Element of R
holds ((n,n)-->a)@ = (n,n)-->a
proof
let R be Ring, a be Element of R;
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
for R being Ring, a being Element of R
holds (n,n)-->a is symmetric by Th21;
theorem
for R being commutative Ring, M1,M2 being Matrix of n,R
holds n > 0 & M1 is symmetric & M2 is symmetric implies
(M1 commutes_with M2 iff M1*M2 is symmetric)
proof
let R be commutative Ring;
let M1,M2 be Matrix of n,R;
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 Th24:
for R being Ring, M1,M2 being Matrix of n,R
holds (M1+M2)@ = M1@+M2@
proof
let R be Ring;
let M1,M2 be Matrix of n,R;
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_1:def 6
.=(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_1:def 6;
hence thesis;
end;
hence thesis by MATRIX_0:27;
end;
theorem
for R being Ring, M1,M2 being Matrix of n,R
st M1 is symmetric & M2 is symmetric holds M1+M2 is symmetric by Th24;
theorem ::: should be a cluster
for R being Ring, M1,M2 being Matrix of n,R
holds M1 is upper_triangular Matrix of n,R &
M1 is lower_triangular Matrix of n,R implies M1 is symmetric
proof
let R be Ring;
let M1,M2 be Matrix of n,R;
assume
A1: M1 is upper_triangular Matrix of n,R & M1 is lower_triangular Matrix
of n,R;
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
i<j;
then M1*(i,j) = 0.R & M1*(j,i) = 0.R by A1,A3,A4,MATRIX_1:def 12,def 13
;
hence thesis by A4,MATRIX_0:def 6;
end;
suppose
i>j;
then M1*(i,j)=0.R & M1*(j,i)=0.R by A1,A3,A4,MATRIX_1:def 12,def 13;
hence thesis by A4,MATRIX_0:def 6;
end;
end;
end;
hence thesis by MATRIX_0:27;
end;
theorem Th27:
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_1:def 4
.=-(M1@*(i,j)) by A4,MATRIX_0:def 6
.=(-(M1@))*(i,j) by A2,MATRIX_1:def 4;
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 Th27;
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 Th24
.=M1+(-M2)@ by A1
.=M1+-(M2@) by Th27
.=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_1:def 4;
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_1:def 4;
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 Th24
.=-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 Th27;
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 Th24
.=-M1+(-M2)@ by A1
.=-M1+-(M2@) by Th27
.=-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 Th24
.=M1@+-((M1@)@) by Th27
.=M1@-M1 by A1,A2,MATRIX_0:57
.=-(M1-M1@) by A2,A3,MATRIX_4:43;
hence thesis;
end;
theorem
M1 commutes_with M2 iff
(M1+M2)*(M1+M2)=M1*M1+M1*M2+M1*M2+M2*M2
proof
A1: len (M1*M2)=n & width (M1*M2)=n by MATRIX_0:24;
A2: len (M1*M1+M1*M2)=n & width (M1*M1+M1*M2)=n by MATRIX_0:24;
A3: len (M1*M2+M2*M2)=n & width (M1*M2+M2*M2)=n by MATRIX_0:24;
A4: len (M1*M1)=n & width (M1*M1)=n by MATRIX_0:24;
A5: len M1 =n & width M1=n by MATRIX_0:24;
A6: len (M1*M1+M2*M1)=n & width (M1*M1+M2*M1)=n by MATRIX_0:24;
A7: len M2=n & width M2=n by MATRIX_0:24;
A8: 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
A9: M1 commutes_with M2;
(M1+M2)*(M1+M2)=(M1+M2)*M1+(M1+M2)*M2 by A5,A7,A8,MATRIX_4:62
.=M1*M1+M2*M1+(M1+M2)*M2 by A5,A7,MATRIX_4:63
.=M1*M1+M2*M1+(M1*M2+M2*M2) by A5,A7,MATRIX_4:63
.=M1*M1+M2*M1+M1*M2+M2*M2 by A1,A6,MATRIX_3:3;
hence thesis by A9;
end;
assume
A10: (M1+M2)*(M1+M2)=M1*M1+M1*M2+M1*M2+M2*M2;
A11: len (M2*M1)=n & width (M2*M1)=n by MATRIX_0:24;
(M1+M2)*(M1+M2)=(M1+M2)*M1+(M1+M2)*M2 by A5,A7,A8,MATRIX_4:62
.=M1*M1+M2*M1+(M1+M2)*M2 by A5,A7,MATRIX_4:63
.=M1*M1+M2*M1+(M1*M2+M2*M2) by A5,A7,MATRIX_4:63
.=M1*M1+M2*M1+M1*M2+M2*M2 by A1,A6,MATRIX_3:3;
then M1*M1+M2*M1+(M1*M2+M2*M2)=M1*M1+M1*M2+M1*M2+M2*M2 by A1,A6,A10,
MATRIX_3:3;
then M1*M1+M2*M1+(M1*M2+M2*M2)=M1*M1+M1*M2+(M1*M2+M2*M2) by A1,A2,MATRIX_3:3;
then M1*M1+M2*M1=M1*M1+M1*M2 by A6,A3,A2,MATRIX_4:4;
then M2*M1+M1*M1=M1*M1+M1*M2 by A4,A11,MATRIX_3:2;
then M2*M1+M1*M1=M1*M2+M1*M1 by A4,A1,MATRIX_3:2;
hence thesis by A4,A1,A11,MATRIX_4:4;
end;
theorem Th37:
for R being Ring, M1,M2 being Matrix of n,R
holds M1 is invertible & M2 is invertible implies M1*M2 is invertible
& (M1*M2)~=(M2~)*(M1~)
proof
let R be Ring;
let M1,M2 be Matrix of n,R;
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.(R,n)))*M1~ by A3
.=M1*M1~ by MATRIX_3:19
.=1.(R,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.(R,n)))*M2 by A4
.=M2~*M2 by MATRIX_3:19
.=1.(R,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
for K being Ring, M1,M2 being Matrix of n,K
holds M1 is invertible & M1*M2=1.(K,n) implies M1 is_reverse_of M2
proof
let K be Ring;
let M1,M2 be Matrix of n,K;
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
for K being Ring, M1,M2 being Matrix of n,K
holds M2 is invertible & M2*M1=1.(K,n) implies M1 is_reverse_of M2
proof
let K be Ring;
let M1,M2 be Matrix of n,K;
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 Th41:
for K being Ring
for M1,M2 being Matrix of n,K holds
M1 is invertible & M1 commutes_with M2 implies M1~ commutes_with M2
proof
let K be Ring;
let M1,M2 be Matrix of n,K;
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 Ring;
let M1 be Matrix of n,K;
attr M1 is Orthogonal means
M1 is invertible & M1@ = M1~;
end;
theorem Th42:
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
let K be Ring;
let M1 be Matrix of n,K;
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 Th43:
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
let K be Ring;
let M1 be Matrix of n,K;
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
for K being Ring
for M1 being Matrix of n,K
holds M1 is Orthogonal implies (M1@)*M1=M1*(M1@)
proof
let K be Ring;
let M1 be Matrix of n,K;
assume
A1: M1 is Orthogonal;
then (M1@)*M1=1.(K,n) by Th43;
hence thesis by A1,Th42;
end;
theorem
for K being Ring
for M1,M2 being Matrix of n,K
holds M1 is Orthogonal & M1 commutes_with M2 implies M1@ commutes_with M2
by Th41;
theorem Th46:
for K being Ring
for M1,M2 being Matrix of n,K
holds M1 is invertible & M2 is invertible implies M1*M2 is invertible
& (M1*M2)~=M2~*M1~
proof
let K be Ring;
let M1,M2 be Matrix of n,K;
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
for K being commutative Ring
for M1,M2 being Matrix of n,K holds
n > 0 & M1 is Orthogonal & M2 is Orthogonal implies M1*M2 is Orthogonal
proof
let K be commutative Ring;
let M1,M2 be Matrix of n,K;
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 Th46;
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
for K being Ring
for M1,M2 being Matrix of n,K holds
M1 is Orthogonal & M1 commutes_with M2 implies M1@ commutes_with M2
proof
let K be Ring;
let M1,M2 be Matrix of n,K;
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
for R being Ring, M1,M2 being Matrix of n,R
holds M1 commutes_with M2 implies M1+M1 commutes_with M2
proof
let R be Ring;
let M1,M2 be Matrix of n,R;
assume
A1: M1 commutes_with M2;
A2: width M2=n by MATRIX_0:24;
A3: len M1=n by MATRIX_0:24;
width M1=n & len M2=n by MATRIX_0:24;
then (M1+M1)*M2=M1*M2+M1*M2 by MATRIX_4:63
.=M2*M1+M1*M2 by A1
.=M2*M1+M2*M1 by A1
.=M2*(M1+M1) by A2,A3,MATRIX_4:62;
hence thesis;
end;
theorem
for R being Ring, M1,M2 being Matrix of n,R
holds M1 commutes_with M2 implies M1+M2 commutes_with M2
proof
let R be Ring;
let M1,M2 be Matrix of n,R;
assume that
A1: M1 commutes_with M2;
A2: width M2=n & len M1=n by MATRIX_0:24;
A3: width M1=n & len M2=n by MATRIX_0:24;
then (M1+M2)*M2=M1*M2+M2*M2 by A2,MATRIX_4:63
.=M2*M1+M2*M2 by A1
.=M2*(M1+M2) by A3,A2,MATRIX_4:62;
hence thesis;
end;
theorem
for R being Ring, M1,M2 being Matrix of n,R
holds M1 commutes_with M2 implies M1+M1 commutes_with M2+M2
proof
let R be Ring;
let M1,M2 be Matrix of n,R;
assume that
A1: M1 commutes_with M2;
A2: len M2=n by MATRIX_0:24;
A3: len (M1+M1)=n by MATRIX_0:24;
A4: width M2=n by MATRIX_0:24;
A5: 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 A2,MATRIX_4:62
.=M1*M2+M1*M2+(M1+M1)*M2 by A2,A5,MATRIX_4:63
.=M1*M2+M1*M2+(M1*M2+M1*M2) by A2,A5,MATRIX_4:63
.=M2*M1+M1*M2+(M1*M2+M1*M2) by A1
.=M2*M1+M2*M1+(M1*M2+M1*M2) by A1
.=M2*M1+M2*M1+(M2*M1+M2*M1) by A1
.=M2*(M1+M1)+(M2*M1+M2*M1) by A4,A5,MATRIX_4:62
.=M2*(M1+M1)+M2*(M1+M1) by A4,A5,MATRIX_4:62
.=(M2+M2)*(M1+M1) by A4,A3,MATRIX_4:63;
hence thesis;
end;
theorem
for R being Ring, M1,M2 being Matrix of n,R
holds M1 commutes_with M2 implies M1+M2 commutes_with M2+M2
proof
let R be Ring;
let M1,M2 be Matrix of n,R;
assume that
A1: M1 commutes_with M2;
A2: len M2=n & width M2=n by MATRIX_0:24;
A3: len (M1+M2)=n by MATRIX_0:24;
A4: 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 A2,MATRIX_4:62
.=M1*M2+M2*M2+(M1+M2)*M2 by A2,A4,MATRIX_4:63
.=M1*M2+M2*M2+(M1*M2+M2*M2) by A2,A4,MATRIX_4:63
.=M2*M1+M2*M2+(M1*M2+M2*M2) by A1
.=M2*M1+M2*M2+(M2*M1+M2*M2) by A1
.=M2*(M1+M2)+(M2*M1+M2*M2) by A2,A4,MATRIX_4:62
.=M2*(M1+M2)+M2*(M1+M2) by A2,A4,MATRIX_4:62
.=(M2+M2)*(M1+M2) by A2,A3,MATRIX_4:63;
hence thesis;
end;
theorem
for R being Ring, M1,M2 being Matrix of n,R
holds M1 commutes_with M2 implies M1*M2 commutes_with M2
proof
let R be Ring;
let M1,M2 be Matrix of n,R;
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
for R being Ring, M1,M2 being Matrix of n,R
holds M1 commutes_with M2 implies M1*M1 commutes_with M2
proof
let R be Ring;
let M1,M2 be Matrix of n,R;
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
for R being Ring, M1,M2 being Matrix of n,R
holds M1 commutes_with M2 implies M1*M1 commutes_with M2*M2
proof
let R be Ring;
let M1,M2 be Matrix of n,R;
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
for R being commutative Ring, M1,M2 being Matrix of n,R
holds n>0 & M1 commutes_with M2 implies M1@ commutes_with M2@
proof
let R be commutative Ring;
let M1,M2 be Matrix of n,R;
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 Th57:
for R being Ring, M1,M2,M3 being Matrix of n,R
holds M1 is invertible & M2 is invertible & M3 is invertible implies
M1*M2*M3 is invertible & (M1*M2*M3)~=M3~*M2~*M1~
proof
let R be Ring;
let M1,M2,M3 be Matrix of n,R;
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.(R,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.(R,n)))*M3 by A5
.=M3~*M3 by MATRIX_3:19
.=1.(R,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.(R,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.(R,n)))*M1~ by A5
.=M1*M1~ by MATRIX_3:19
.=1.(R,n) by A4;
then
A24: M5 is_reverse_of M4 by A23;
then M4 is invertible;
hence thesis by A24,Def4;
end;
theorem
for R being commutative Ring, M1,M2,M3 being Matrix of n,R
holds n > 0 & M1 is Orthogonal & M2 is Orthogonal & M3 is Orthogonal implies
M1*M2*M3 is Orthogonal
proof
let R be commutative Ring;
let M1,M2,M3 be Matrix of n,R;
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,Th57;
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
for K being Ring holds 1.(K,n) is Orthogonal
proof
let K be Ring;
A1: (1.(K,n))@=1.(K,n) by Th11;
(1.(K,n))~=1.(K,n) & 1.(K,n) is invertible by Th9;
hence thesis by A1;
end;
theorem
for R being commutative Ring, M1,M2 being Matrix of n,R
holds n > 0 & M1 is Orthogonal & M2 is Orthogonal implies
M1~*M2 is Orthogonal
proof
let R be commutative Ring;
let M1,M2 be Matrix of n,R;
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,Th37;
(M1~*M2)~=M2~*(M1~)~ by A6,A5,Th37;
then
A8: (M1~*M2)~=M2~*M1 by A4,Th17;
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;