:: Some Properties Of Some Special Matrices, Part {II}
:: by Xiaopeng Yue , Dahai Hu , Xiquan Liang and Zhongpin Sun
::
:: Received January 4, 2006
:: Copyright (c) 2006-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 NAT_1, VECTSP_1, MATRIX_1, RELAT_1, SUPINF_2, MESFUNC1, ALGSTR_0,
TREES_1, FINSEQ_1, XXREAL_0, CARD_1, QC_LANG1, MATRIX_6, REWRITE1,
ARYTM_3, ARYTM_1, RELAT_2, FUNCOP_1, ZFMISC_1, FSM_1, COHSP_1, SUBSET_1,
CARD_3, MATRIX_3, FUNCT_1, PARTFUN1, MATRIX_8;
notations TARSKI, ZFMISC_1, PARTFUN1, ORDINAL1, NUMBERS, FINSEQ_1, STRUCT_0,
RLVECT_1, NAT_1, VECTSP_1, MATRIX_0, FUNCT_1, MATRIX_1, MATRIX_3,
MATRIX_6, FVSUM_1, XXREAL_0;
constructors BINOP_1, REAL_1, NAT_1, FVSUM_1, MATRIX_6, MATRIX_1, MATRIX_3;
registrations RELSET_1, XREAL_0, INT_1, STRUCT_0, MATRIX_6, ORDINAL1,
MATRIX_0;
requirements NUMERALS, SUBSET, ARITHM;
equalities MATRIX_0, MATRIX_1, MATRIX_3, FINSEQ_1, FVSUM_1, ALGSTR_0;
theorems ZFMISC_1, RLVECT_1, MATRIX_0, MATRIX_4, MATRIX_3, FUNCOP_1, FINSEQ_1,
INT_1, MATRIX_6, POLYNOM1, MATRLIN, NAT_1, PARTFUN1, MATRIX_1;
begin
reserve i,n for Nat,
K for Field,
M1,M2,M3,M4 for Matrix of n,K;
definition
let n be Nat, K be Field, M1 be Matrix of n,K;
attr M1 is Idempotent means
M1*M1=M1;
attr M1 is Nilpotent means
M1*M1=0.(K,n);
attr M1 is Involutory means
M1*M1=1.(K,n);
attr M1 is Self_Reversible means
M1 is invertible & M1~=M1;
end;
theorem Th1:
1.(K,n) is Idempotent Involutory
by MATRIX_3:18;
theorem Th2:
0.(K,n) is Idempotent Nilpotent
proof
width 0.(K,n,n)=n & len 0.(K,n,n)=n by MATRIX_0:24;
then 0.(K,n,n)*(0.(K,n))=0.(K,n,n) by MATRIX_6:1;
hence thesis;
end;
registration
let n be Nat, K be Field;
cluster 1.(K,n) -> Idempotent Involutory;
coherence by Th1;
cluster 0.(K,n) -> Idempotent Nilpotent;
coherence by Th2;
end;
theorem
n>0 implies (M1 is Idempotent iff M1@ is Idempotent)
proof
assume
A1: n>0;
set M2=M1@;
A2: width M1=n & len M1=n by MATRIX_0:24;
thus M1 is Idempotent implies M2 is Idempotent
by A1,A2,MATRIX_3:22;
A3: width M2=n & len M2=n by MATRIX_0:24;
assume
A4: M2 is Idempotent;
M1=M2@ by A1,A2,MATRIX_0:57
.=(M2*M2)@ by A4
.=M2@*M2@ by A1,A3,MATRIX_3:22
.=M1*(M1@)@ by A1,A2,MATRIX_0:57
.=M1*M1 by A1,A2,MATRIX_0:57;
hence thesis;
end;
theorem
M1 is Involutory implies M1 is invertible
by MATRIX_6:def 2,def 3;
theorem
M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 implies M1*
M1 commutes_with M2*M2;
theorem
M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 & M1*
M2=0.(K,n) implies M1+M2 is Idempotent
proof
assume that
A2: M1 is Idempotent & M2 is Idempotent and
A3: M1 commutes_with M2 and
A4: M1*M2=0.(K,n);
A5: M1*M2=0.(K,n,n) by A4;
A6: M1*M1=M1 & M2*M2=M2 by A2;
(M1+M2)*(M1+M2)=M1*M1+0.(K,n)+0.(K,n)+M2*M2 by A3,A4,MATRIX_6:35
.=M1*M1+0.(K,n)+M2*M2 by A5,MATRIX_3:4
.=M1+M2 by A6,A5,MATRIX_3:4;
hence thesis;
end;
theorem
M1 is Idempotent & M2 is Idempotent & M1*M2=-(M2*M1) implies M1+M2 is
Idempotent
proof
assume that
A1: M1 is Idempotent & M2 is Idempotent and
A2: M1*M2=-(M2*M1);
A3: M1*M1=M1 & M2*M2=M2 by A1;
A5: len (M1*M2)=n & width (M1*M2)=n by MATRIX_0:24;
A6: len M2=n & width M2=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*M1)=n & width (M2*M1)=n by MATRIX_0:24;
A9: len (M1*M1)=n & width (M1*M1)=n by MATRIX_0:24;
A10: len M1=n & width M1=n by MATRIX_0:24;
len (M1+M2)=n & width (M1+M2)=n by MATRIX_0:24;
then (M1+M2)*(M1+M2)=(M1+M2)*M1+(M1+M2)*M2 by A10,A6,MATRIX_4:62
.=M1*M1+M2*M1+(M1+M2)*M2 by A10,A6,MATRIX_4:63
.=M1*M1+M2*M1+(M1*M2+M2*M2) by A10,A6,MATRIX_4:63
.=M1*M1+M2*M1+M1*M2+M2*M2 by A5,A7,MATRIX_3:3
.=(M1*M1+(M2*M1+(-(M2*M1))))+M2*M2 by A2,A9,A8,MATRIX_3:3
.=M1*M1+0.(K,n,n)+M2*M2 by A8,MATRIX_4:2
.=M1+M2 by A3,MATRIX_3:4;
hence thesis;
end;
theorem
M1 is Idempotent & M2 is invertible implies (M2~)*M1*M2 is Idempotent
proof
assume that
A1: M1 is Idempotent and
A2: M2 is invertible;
A3: M2~ is_reverse_of M2 by A2,MATRIX_6:def 4;
A4: width M2=n by MATRIX_0:24;
A5: len M2=n by MATRIX_0:24;
A6: len (M1*M2)=n & width ((M2~)*M1*M2)=n by MATRIX_0:24;
A7: len (M2~)=n by MATRIX_0:24;
A8: width (M2~*M1)=n by MATRIX_0:24;
A9: width (M2~)=n by MATRIX_0:24;
A10: len M1=n & width M1=n by MATRIX_0:24;
then ((M2~)*M1*M2)*((M2~)*M1*M2) =(((M2~)*M1)*M2)*((M2~)*(M1*M2))by A5,A9,
MATRIX_3:33
.=((((M2~)*M1)*M2)*(M2~))*(M1*M2) by A7,A9,A6,MATRIX_3:33
.=(((M2~)*M1)*(M2*(M2~)))*(M1*M2) by A5,A4,A7,A8,MATRIX_3:33
.=(((M2~)*M1)*(1.(K,n)))*(M1*M2) by A3,MATRIX_6:def 2
.=((M2~)*M1)*(M1*M2) by MATRIX_3:19
.=((M2~)*M1*M1)*M2 by A10,A5,A8,MATRIX_3:33
.=((M2~)*(M1*M1))*M2 by A10,A9,MATRIX_3:33
.=M2~*M1*M2 by A1;
hence thesis;
end;
theorem
M1 is invertible Idempotent implies M1~ is Idempotent
by MATRIX_6:36;
theorem Th10:
M1 is invertible Idempotent implies M1=1.(K,n)
proof
A1: len M1=n & width M1=n by MATRIX_0:24;
A2: width (M1~)=n by MATRIX_0:24;
assume
A3: M1 is invertible Idempotent;
then
A4: M1~ is_reverse_of M1 by MATRIX_6:def 4;
M1*M1=M1 by A3;
then 1.(K,n)=M1~*(M1*M1) by A4,MATRIX_6:def 2
.=(M1~*M1)*M1 by A1,A2,MATRIX_3:33
.=(1.(K,n))*M1 by A4,MATRIX_6:def 2
.=M1 by MATRIX_3:18;
hence thesis;
end;
theorem
M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 implies M1*
M2 is Idempotent
proof
assume that
A1: M1 is Idempotent and
A2: M2 is Idempotent and
A3: M1 commutes_with M2;
A4: len M1=n by MATRIX_0:24;
A5: width M2=n by MATRIX_0:24;
A6: width M1=n & len M2=n by MATRIX_0:24;
width (M1*M2)=n by MATRIX_0:24;
then (M1*M2)*(M1*M2)=((M1*M2)*M1)*M2 by A4,A6,MATRIX_3:33
.=(M1*(M2*M1))*M2 by A4,A6,A5,MATRIX_3:33
.=(M1*(M1*M2))*M2 by A3,MATRIX_6:def 1
.=((M1*M1)*M2)*M2 by A4,A6,MATRIX_3:33
.=(M1*M2)*M2 by A1
.=M1*(M2*M2) by A6,A5,MATRIX_3:33
.=M1*M2 by A2;
hence thesis;
end;
theorem
M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 implies M1@*
M2@ is Idempotent
proof
assume that
A1: M1 is Idempotent and
A2: M2 is Idempotent and
A3: M1 commutes_with M2;
set M3=M1@*M2@;
per cases by NAT_1:3;
suppose
A4: n>0;
A5: M1*M1=M1 by A1;
A6: len M1=n by MATRIX_0:24;
A7: len (M1@)=n by MATRIX_0:24;
A8: width (M2@)=n by MATRIX_0:24;
A9: width M2=n by MATRIX_0:24;
A10: len M2=n by MATRIX_0:24;
A11: width M1=n by MATRIX_0:24;
A12: width (M1@)=n & len (M2@)=n by MATRIX_0:24;
width M3=n by MATRIX_0:24;
then M3*M3=((M1@*M2@)*M1@)*M2@ by A7,A12,MATRIX_3:33
.=(M1@*(M2@*M1@))*M2@ by A7,A12,A8,MATRIX_3:33
.=(M1@*((M1*M2)@))*M2@ by A4,A11,A10,A9,MATRIX_3:22
.=(M1@*((M2*M1)@))*M2@ by A3,MATRIX_6:def 1
.=(M1@*(M1@*M2@))*M2@ by A4,A6,A11,A9,MATRIX_3:22
.=((M1@*M1@)*M2@)*M2@ by A7,A12,MATRIX_3:33
.=(((M1*M1)@)*M2@)*M2@ by A4,A6,A11,MATRIX_3:22
.=(M1@)*(M2@*M2@) by A5,A12,A8,MATRIX_3:33
.=(M1@)*((M2*M2)@) by A4,A10,A9,MATRIX_3:22
.=M1@*M2@ by A2;
hence thesis;
end;
suppose
n=0;
then (M1@*M2@)*(M1@*M2@) = M1@*M2@ by MATRIX_0:45;
hence thesis;
end;
end;
theorem
M1 is Idempotent & M2 is Idempotent & M1 is invertible implies M1*M2
is Idempotent
proof
assume that
A1: M1 is Idempotent and
A2: M2 is Idempotent and
A3: M1 is invertible;
M1=1.(K,n) by A1,A3,Th10;
hence thesis by A2,MATRIX_3:18;
end;
theorem
M1 is Idempotent Orthogonal implies M1 is symmetric
proof
assume
A1: M1 is Idempotent Orthogonal;
then M1 is invertible by MATRIX_6:def 7;
then M1=1.(K,n) by A1,Th10;
hence thesis;
end;
theorem
M2*M1=1.(K,n) implies M1*M2 is Idempotent
proof
assume
A1: M2*M1=1.(K,n);
A2: len M1=n & width M1=n by MATRIX_0:24;
A3: width M2=n by MATRIX_0:24;
A4: len M2=n by MATRIX_0:24;
width (M1*M2)=n by MATRIX_0:24;
then M1*M2*(M1*M2)=(M1*M2*M1)*M2 by A2,A4,MATRIX_3:33
.=(M1*(1.(K,n)))*M2 by A1,A2,A4,A3,MATRIX_3:33
.=M1*M2 by MATRIX_3:19;
hence thesis;
end;
theorem
M1 is Idempotent Orthogonal implies M1=1.(K,n) by Th10,MATRIX_6:def 7;
theorem
M1 is symmetric implies M1*M1@ is symmetric
proof
assume
A1: M1 is symmetric;
per cases by NAT_1:3;
suppose
A2: n>0;
A3: width M1=n & len M1=n by MATRIX_0:24;
(M1*M1@)@=(M1*M1)@ by A1,MATRIX_6:def 5
.=M1@*M1@ by A2,A3,MATRIX_3:22
.=M1*M1@ by A1,MATRIX_6:def 5;
hence thesis by MATRIX_6:def 5;
end;
suppose
n=0;
then (M1*M1@)@=M1*M1@ by MATRIX_0:45;
hence thesis by MATRIX_6:def 5;
end;
end;
theorem
M1 is symmetric implies M1@*M1 is symmetric
proof
assume
A1: M1 is symmetric;
per cases by NAT_1:3;
suppose
A2: n>0;
A3: width M1=n & len M1=n by MATRIX_0:24;
(M1@*M1)@=(M1*M1)@ by A1,MATRIX_6:def 5
.=M1@*M1@ by A2,A3,MATRIX_3:22
.=M1@*M1 by A1,MATRIX_6:def 5;
hence thesis by MATRIX_6:def 5;
end;
suppose
n=0;
then (M1@*M1)@=M1@*M1 by MATRIX_0:45;
hence thesis by MATRIX_6:def 5;
end;
end;
theorem
M1 is invertible & M1*M2=M1*M3 implies M2=M3
proof
assume that
A1: M1 is invertible and
A2: M1*M2=M1*M3;
A3: M1~ is_reverse_of M1 by A1,MATRIX_6:def 4;
A4: len M2=n by MATRIX_0:24;
A5: width M1=n & len M1=n by MATRIX_0:24;
A6: len M3=n by MATRIX_0:24;
A7: width (M1~)=n by MATRIX_0:24;
M2=(1.(K,n))*M2 by MATRIX_3:18
.=(M1~*M1)*M2 by A3,MATRIX_6:def 2
.=M1~*(M1*M3) by A2,A5,A4,A7,MATRIX_3:33
.=(M1~*M1)*M3 by A5,A6,A7,MATRIX_3:33
.=(1.(K,n))*M3 by A3,MATRIX_6:def 2
.=M3 by MATRIX_3:18;
hence thesis;
end;
theorem
M1 is invertible & M2*M1=M3*M1 implies M2=M3
proof
assume that
A1: M1 is invertible and
A2: M2*M1=M3*M1;
A3: M1~ is_reverse_of M1 by A1,MATRIX_6:def 4;
A4: width M2=n by MATRIX_0:24;
A5: width M1=n & len M1=n by MATRIX_0:24;
A6: width M3=n by MATRIX_0:24;
A7: len (M1~)=n by MATRIX_0:24;
M2=M2*(1.(K,n)) by MATRIX_3:19
.=M2*(M1*M1~) by A3,MATRIX_6:def 2
.=(M3*M1)*M1~ by A2,A5,A4,A7,MATRIX_3:33
.=M3*(M1*M1~) by A5,A6,A7,MATRIX_3:33
.=M3*(1.(K,n)) by A3,MATRIX_6:def 2
.=M3 by MATRIX_3:19;
hence thesis;
end;
theorem
M1 is invertible & M2*M1=0.(K,n) implies M2=0.(K,n)
proof
assume that
A1: M1 is invertible and
A2: M2*M1=0.(K,n);
A3: M1~ is_reverse_of M1 by A1,MATRIX_6:def 4;
A4: width M2=n by MATRIX_0:24;
A5: width M1=n & len M1=n by MATRIX_0:24;
A6: width (M1~)=n by MATRIX_0:24;
A7: len (M1~)=n by MATRIX_0:24;
M2=M2*(1.(K,n)) by MATRIX_3:19
.=M2*(M1*M1~) by A3,MATRIX_6:def 2
.=(M2*M1)*M1~ by A5,A4,A7,MATRIX_3:33
.=(0.(K,n,n)) by A2,A6,A7,MATRIX_6:1
.=0.(K,n);
hence thesis;
end;
theorem
M1 is invertible & M2*M1=0.(K,n) implies M2=0.(K,n)
proof
assume that
A1: M1 is invertible and
A2: M2*M1=0.(K,n);
A3: M1~ is_reverse_of M1 by A1,MATRIX_6:def 4;
A4: width M2=n by MATRIX_0:24;
A5: width M1=n & len M1=n by MATRIX_0:24;
A6: width (M1~)=n by MATRIX_0:24;
A7: len (M1~)=n by MATRIX_0:24;
M2=M2*(1.(K,n)) by MATRIX_3:19
.=M2*(M1*M1~) by A3,MATRIX_6:def 2
.=(M2*M1)*M1~ by A5,A4,A7,MATRIX_3:33
.=(0.(K,n,n)) by A2,A6,A7,MATRIX_6:1
.=0.(K,n);
hence thesis;
end;
theorem
M1 is Nilpotent & M1 commutes_with M2 implies M1*M2 is Nilpotent
proof
assume that
A1: M1 is Nilpotent and
A2: M1 commutes_with M2;
A4: len M1=n & width M1=n by MATRIX_0:24;
A5: width M2=n by MATRIX_0:24;
A6: width (M2*M1)=n by MATRIX_0:24;
A7: len M2=n by MATRIX_0:24;
(M1*M2)*(M1*M2)=(M2*M1)*(M1*M2) by A2,MATRIX_6:def 1
.=(M2*M1*M1)*M2 by A4,A7,A6,MATRIX_3:33
.=(M2*(M1*M1))*M2 by A4,A5,MATRIX_3:33
.=(M2*(0.(K,n)))*M2 by A1
.=(0.(K,n,n))*M2 by A7,A5,MATRIX_6:2
.=0.(K,n) by A7,A5,MATRIX_6:1;
hence thesis;
end;
theorem
M1 is Nilpotent & M2 is Nilpotent & M1 commutes_with M2 & M1*M2=
0.(K,n) implies M1+M2 is Nilpotent
proof
assume that
A2: M1 is Nilpotent & M2 is Nilpotent and
A3: M1 commutes_with M2 and
A4: M1*M2=0.(K,n);
A5: M1*M2=0.(K,n,n) by A4;
A6: M1*M1=0.(K,n) & M2*M2=0.(K,n) by A2;
(M1+M2)*(M1+M2)=M1*M1+0.(K,n)+0.(K,n)+M2*M2 by A3,A4,MATRIX_6:35
.=M1*M1+0.(K,n)+M2*M2 by A5,MATRIX_3:4
.=0.(K,n)+0.(K,n) by A6,A5,MATRIX_3:4
.=0.(K,n,n) by MATRIX_3:4
.=0.(K,n);
hence thesis;
end;
theorem
M1 is Nilpotent & M2 is Nilpotent & M1*M2=-M2*M1 implies
M1+M2 is Nilpotent
proof
assume that
A1: M1 is Nilpotent & M2 is Nilpotent and
A2: M1*M2=-M2*M1;
A4: M1*M1=0.(K,n) & M2*M2=0.(K,n) by A1;
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*M1)=n & width (M2*M1)=n by MATRIX_0:24;
A9: len (M1*M2)=n & width (M1*M2)=n by MATRIX_0:24;
A10: len M2=n & width M2=n by MATRIX_0:24;
len (M1+M2)=n & width (M1+M2)=n by MATRIX_0:24;
then (M1+M2)*(M1+M2)=(M1+M2)*M1+(M1+M2)*M2 by A6,A10,MATRIX_4:62
.=M1*M1+M2*M1+(M1+M2)*M2 by A6,A10,MATRIX_4:63
.=M1*M1+M2*M1+(M1*M2+M2*M2) by A6,A10,MATRIX_4:63
.=M1*M1+M2*M1+M1*M2+M2*M2 by A9,A7,MATRIX_3:3
.=(M1*M1+(M2*M1+(-(M2*M1))))+M2*M2 by A2,A5,A8,MATRIX_3:3
.=M1*M1+0.(K,n,n)+M2*M2 by A8,MATRIX_4:2
.=0.(K,n)+0.(K,n) by A4,MATRIX_3:4
.=0.(K,n,n) by MATRIX_3:4
.=0.(K,n);
hence thesis;
end;
theorem
M1 is Nilpotent & n>0 implies M1@ is Nilpotent
proof
assume that
A1: M1 is Nilpotent and
A2: n>0;
len M1=n & width M1=n by MATRIX_0:24;
then M1@*M1@=(M1*M1)@ by A2,MATRIX_3:22
.=(0.(K,n))@ by A1
.=(n,n)-->0.K by MATRIX_6:20
.=0.(K,n);
hence thesis;
end;
theorem
M1 is Nilpotent Idempotent implies M1=0.(K,n);
theorem Th28:
n>0 implies 0.(K,n)<>1.(K,n)
proof
A1: Indices (1.(K,n))=[:Seg n,Seg n:] by MATRIX_0:24;
assume n>0;
then n >=0+1 by INT_1:7;
then 1 in Seg n;
then
A2: [1,1] in [:Seg n, Seg n:] by ZFMISC_1:87;
assume
A3: 0.(K,n)=1.(K,n);
Indices (0.(K,n))=Indices (1.(K,n)) by MATRIX_0:26;
then (0.(K,n))*(1,1)=0.K by A2,A1,MATRIX_1:1;
then 0.K=1.K by A2,A3,A1,MATRIX_1:def 3;
hence contradiction;
end;
theorem
n>0 & M1 is Nilpotent implies not M1 is invertible
proof
assume that
A1: n>0 and
A2: M1 is Nilpotent;
A3: len M1=n & width M1=n by MATRIX_0:24;
assume M1 is invertible;
then consider M2 being Matrix of n,K such that
A4: M1 is_reverse_of M2 by MATRIX_6:def 3;
A5: width M2=n by MATRIX_0:24;
A6: len M2=n by MATRIX_0:24;
M1=M1*(1.(K,n)) by MATRIX_3:19
.=M1*(M1*M2) by A4,MATRIX_6:def 2
.=(M1*M1)*M2 by A3,A6,MATRIX_3:33
.=(0.(K,n))*M2 by A2
.=0.(K,n,n) by A6,A5,MATRIX_6:1;
then
A7: M1*M2=0.(K,n) by A6,A5,MATRIX_6:1;
M1*M2= 1.(K,n) by A4,MATRIX_6:def 2;
hence contradiction by A1,A7,Th28;
end;
theorem
M1 is Self_Reversible implies M1 is Involutory
proof
assume
A1: M1 is Self_Reversible;
then M1 is invertible;
then M1~ is_reverse_of M1 by MATRIX_6:def 4;
then
A2: M1*M1~=1.(K,n) by MATRIX_6:def 2;
M1*M1=M1*M1~ by A1;
hence thesis by A2;
end;
theorem
1.(K,n) is Self_Reversible
by MATRIX_6:8;
theorem
M1 is Self_Reversible Idempotent implies M1=1.(K,n)
proof
assume
A1: M1 is Self_Reversible Idempotent;
then M1 is invertible;
then M1~ is_reverse_of M1 by MATRIX_6:def 4;
then 1.(K,n)=M1*M1~ by MATRIX_6:def 2
.=M1*M1 by A1;
hence thesis by A1;
end;
theorem
M1 is Self_Reversible symmetric implies M1 is Orthogonal
proof
assume
A1: M1 is Self_Reversible symmetric;
then
A2: M1=M1@ by MATRIX_6:def 5;
M1 is invertible & M1=M1~ by A1;
hence thesis by A2,MATRIX_6:def 7;
end;
definition
let n be Nat, K be Field, M1,M2 be Matrix of n,K;
pred M1 is_similar_to M2 means
ex M be Matrix of n,K st M is invertible & M1=M~*M2*M;
reflexivity
proof
let M1 be Matrix of n, K;
take 1.(K,n);
(1.(K,n))~*M1*(1.(K,n))=(1.(K,n))*M1*(1.(K,n)) by MATRIX_6:8
.=M1*(1.(K,n)) by MATRIX_3:18
.=M1 by MATRIX_3:19;
hence thesis;
end;
symmetry
proof
let M1,M2 be Matrix of n,K;
given M be Matrix of n,K such that
A1: M is invertible and
A2: M1=M~*M2*M;
A3: M~ is_reverse_of M by A1,MATRIX_6:def 4;
take M~;
A4: width M2=n by MATRIX_0:24;
A5: len M=n by MATRIX_0:24;
A6: len M2=n & width (M~)=n by MATRIX_0:24;
A7: width M=n by MATRIX_0:24;
A8: len (M~*M2)=n & width (M~*M2)=n by MATRIX_0:24;
A9: len (M~)=n by MATRIX_0:24;
M~~*M1*M~=(M*(M~*M2*M))*M~ by A1,A2,MATRIX_6:16
.=((M*(M~*M2))*M)*M~ by A5,A7,A8,MATRIX_3:33
.=(((M*M~)*M2)*M)*M~ by A7,A9,A6,MATRIX_3:33
.=(((1.(K,n))*M2)*M)*M~ by A3,MATRIX_6:def 2
.=(M2*M)*M~ by MATRIX_3:18
.=M2*(M*M~) by A4,A5,A7,A9,MATRIX_3:33
.=M2*(1.(K,n)) by A3,MATRIX_6:def 2
.=M2 by MATRIX_3:19;
hence thesis by A1;
end;
end;
theorem
M1 is_similar_to M2 & M2 is_similar_to M3 implies M1 is_similar_to M3
proof
assume that
A1: M1 is_similar_to M2 and
A2: M2 is_similar_to M3;
consider M4 be Matrix of n,K such that
A3: M4 is invertible and
A4: M1=M4~*M2* M4 by A1;
consider M5 be Matrix of n,K such that
A5: M5 is invertible and
A6: M2=M5~*M3*M5 by A2;
A7: len M5=n by MATRIX_0:24;
take M5*M4;
A8: width ((M5*M4)~)=n by MATRIX_0:24;
A9: len (M3*M5)=n & width (M3*M5)=n by MATRIX_0:24;
A10: len M4=n by MATRIX_0:24;
A11: width M5=n by MATRIX_0:24;
A12: len M3=n by MATRIX_0:24;
A13: len (M5*M4)=n by MATRIX_0:24;
A14: width (M4~)=n by MATRIX_0:24;
A15: len (M5~)=n & width (M5~)=n by MATRIX_0:24;
A16: width M3=n by MATRIX_0:24;
len (M5~*M3)=n & width (M5~*M3)=n by MATRIX_0:24;
then M1=((M4~*(M5~*M3))*M5)*M4 by A4,A6,A7,A14,MATRIX_3:33
.=(((M4~*M5~)*M3)*M5)*M4 by A12,A14,A15,MATRIX_3:33
.=(((M5*M4)~*M3)*M5)*M4 by A3,A5,MATRIX_6:36
.=((M5*M4)~*(M3*M5))*M4 by A12,A16,A7,A8,MATRIX_3:33
.=(M5*M4)~*((M3*M5)*M4) by A10,A8,A9,MATRIX_3:33
.=(M5*M4)~*(M3*(M5*M4)) by A16,A10,A7,A11,MATRIX_3:33
.=(M5*M4)~*M3*(M5*M4) by A12,A16,A8,A13,MATRIX_3:33;
hence thesis by A3,A5,MATRIX_6:36;
end;
theorem
M1 is_similar_to M2 & M2 is Idempotent implies M1 is Idempotent
proof
assume that
A1: M1 is_similar_to M2 and
A2: M2 is Idempotent;
consider M4 be Matrix of n,K such that
A3: M4 is invertible and
A4: M1=M4~*M2*M4 by A1;
A5: M4~ is_reverse_of M4 by A3,MATRIX_6:def 4;
A6: width M4=n by MATRIX_0:24;
A7: len M2=n & width M2=n by MATRIX_0:24;
A8: len (M2*M4)=n & width (M4~*M2*M4)=n by MATRIX_0:24;
A9: len (M4~)=n by MATRIX_0:24;
A10: width (M4~*M2)=n by MATRIX_0:24;
A11: width (M4~)=n by MATRIX_0:24;
A12: len M4=n by MATRIX_0:24;
then M1*M1=(M4~*M2*M4)*(M4~*(M2*M4)) by A4,A7,A11,MATRIX_3:33
.=((M4~*M2*M4)*M4~)*(M2*M4) by A9,A11,A8,MATRIX_3:33
.=((M4~*M2)*(M4*M4~))*(M2*M4) by A12,A6,A9,A10,MATRIX_3:33
.=((M4~*M2)*(1.(K,n)))*(M2*M4) by A5,MATRIX_6:def 2
.=(M4~*M2)*(M2*M4) by MATRIX_3:19
.=((M4~*M2)*M2)*M4 by A12,A7,A10,MATRIX_3:33
.=(M4~*(M2*M2))*M4 by A7,A11,MATRIX_3:33
.=M1 by A2,A4;
hence thesis;
end;
theorem
M1 is_similar_to M2 & M2 is Nilpotent implies M1 is Nilpotent
proof
assume that
A1: M1 is_similar_to M2 and
A2: M2 is Nilpotent;
consider M4 be Matrix of n,K such that
A4: M4 is invertible and
A5: M1=M4~*M2*M4 by A1;
A6: M4~ is_reverse_of M4 by A4,MATRIX_6:def 4;
A7: width M4=n by MATRIX_0:24;
A8: width (M4~)=n by MATRIX_0:24;
A9: width (M4~*M2)=n by MATRIX_0:24;
A10: len (M4~)=n by MATRIX_0:24;
A11: len (M2*M4)=n & width (M4~*M2*M4)=n by MATRIX_0:24;
A12: len M4=n by MATRIX_0:24;
A13: len M2=n & width M2=n by MATRIX_0:24;
then M1*M1=(M4~*M2*M4)*(M4~*(M2*M4)) by A5,A12,A8,MATRIX_3:33
.=((M4~*M2*M4)*M4~)*(M2*M4) by A10,A8,A11,MATRIX_3:33
.=((M4~*M2)*(M4*M4~))*(M2*M4) by A12,A7,A10,A9,MATRIX_3:33
.=((M4~*M2)*(1.(K,n)))*(M2*M4) by A6,MATRIX_6:def 2
.=(M4~*M2)*(M2*M4) by MATRIX_3:19
.=((M4~*M2)*M2)*M4 by A12,A13,A9,MATRIX_3:33
.=(M4~*(M2*M2))*M4 by A13,A8,MATRIX_3:33
.=M4~*(0.(K,n))*M4 by A2
.=(0.(K,n,n))*M4 by A10,A8,MATRIX_6:2
.=0.(K,n) by A12,A7,MATRIX_6:1;
hence thesis;
end;
theorem
M1 is_similar_to M2 & M2 is Involutory implies M1 is Involutory
proof
assume that
A1: M1 is_similar_to M2 and
A2: M2 is Involutory;
consider M4 be Matrix of n,K such that
A3: M4 is invertible and
A4: M1=M4~*M2*M4 by A1;
A5: M4~ is_reverse_of M4 by A3,MATRIX_6:def 4;
A6: width (M4~*M2)=n by MATRIX_0:24;
A7: width (M4~)=n by MATRIX_0:24;
A8: len (M2*M4)=n & width (M4~*M2*M4)=n by MATRIX_0:24;
A9: len (M4~)=n by MATRIX_0:24;
A10: width M4=n by MATRIX_0:24;
A11: len M2=n & width M2=n by MATRIX_0:24;
A12: len M4=n by MATRIX_0:24;
then M1*M1=(M4~*M2*M4)*(M4~*(M2*M4)) by A4,A11,A7,MATRIX_3:33
.=((M4~*M2*M4)*M4~)*(M2*M4) by A9,A7,A8,MATRIX_3:33
.=((M4~*M2)*(M4*M4~))*(M2*M4) by A12,A10,A9,A6,MATRIX_3:33
.=((M4~*M2)*(1.(K,n)))*(M2*M4) by A5,MATRIX_6:def 2
.=(M4~*M2)*(M2*M4) by MATRIX_3:19
.=((M4~*M2)*M2)*M4 by A12,A11,A6,MATRIX_3:33
.=(M4~*(M2*M2))*M4 by A11,A7,MATRIX_3:33
.=M4~*(1.(K,n))*M4 by A2
.=M4~*M4 by MATRIX_3:19
.=1.(K,n) by A5,MATRIX_6:def 2;
hence thesis;
end;
theorem
M1 is_similar_to M2 implies M1+1.(K,n) is_similar_to M2+1.(K,n)
proof
assume M1 is_similar_to M2; then
consider M4 be Matrix of n,K such that
A3: M4 is invertible and
A4: M1=M4~*M2*M4;
A5: M4~ is_reverse_of M4 by A3,MATRIX_6:def 4;
A6: len (1.(K,n))=n & width (1.(K,n))=n by MATRIX_0:24;
A7: width (M4~*M2)=n by MATRIX_0:24;
A8: len M4=n & len (M4~*M2)=n by MATRIX_0:24;
take M4;
A9: len (M4~)=n & width (M4~)=n by MATRIX_0:24;
len M2=n & width M2=n by MATRIX_0:24;
then M4~*(M2+1.(K,n))*M4=(M4~*M2+M4~*(1.(K,n)))*M4 by A9,A6,MATRIX_4:62
.=(M4~*M2+M4~)*M4 by MATRIX_3:19
.=M4~*M2*M4 +M4~*M4 by A9,A8,A7,MATRIX_4:63
.=M1+1.(K,n) by A4,A5,MATRIX_6:def 2;
hence thesis by A3;
end;
theorem
M1 is_similar_to M2 implies M1+M1 is_similar_to M2+M2
proof
assume M1 is_similar_to M2; then
consider M4 be Matrix of n,K such that
A3: M4 is invertible and
A4: M1=M4~*M2*M4;
A5: width (M4~*M2)=n by MATRIX_0:24;
take M4;
A6: len M4=n & len (M4~*M2)=n by MATRIX_0:24;
A7: len M2=n & width M2=n by MATRIX_0:24;
len (M4~)=n & width (M4~)=n by MATRIX_0:24;
then M4~*(M2+M2)*M4=(M4~*M2+M4~*M2)*M4 by A7,MATRIX_4:62
.=M1+M1 by A4,A6,A5,MATRIX_4:63;
hence thesis by A3;
end;
theorem
M1 is_similar_to M2 implies M1+M1+M1 is_similar_to M2+M2+M2
proof
assume M1 is_similar_to M2; then
consider M4 be Matrix of n,K such that
A3: M4 is invertible and
A4: M1=M4~*M2*M4;
A5: len M4=n & len (M4~*M2)=n by MATRIX_0:24;
A6: width (M4~*M2)=n by MATRIX_0:24;
A7: len M2=n & width M2=n by MATRIX_0:24;
A8: len (M4~)=n & width (M4~)=n by MATRIX_0:24;
then
A9: M4~*(M2+M2)*M4=(M4~*M2+M4~*M2)*M4 by A7,MATRIX_4:62
.=M1+M1 by A4,A5,A6,MATRIX_4:63;
take M4;
A10: len (M4~*(M2+M2))=n & width (M4~*(M2+M2))=n by MATRIX_0:24;
len (M2+M2)=n & width (M2+M2)=n by MATRIX_0:24;
then M4~*(M2+M2+M2)*M4=(M4~*(M2+M2)+M4~*M2)*M4 by A7,A8,MATRIX_4:62
.=M1+M1+M1 by A4,A5,A6,A10,A9,MATRIX_4:63;
hence thesis by A3;
end;
theorem
M1 is invertible implies M2*M1 is_similar_to M1*M2
proof
A1: len M2=n & width (M1~)=n by MATRIX_0:24;
assume
A2: M1 is invertible;
then
A3: M1~ is_reverse_of M1 by MATRIX_6:def 4;
take M1;
len M1=n & width M1=n by MATRIX_0:24;
then M1~*(M1*M2)*M1=((M1~*M1)*M2)*M1 by A1,MATRIX_3:33
.=((1.(K,n))*M2)*M1 by A3,MATRIX_6:def 2
.=M2*M1 by MATRIX_3:18;
hence thesis by A2;
end;
theorem
M2 is invertible & M1 is_similar_to M2 implies M1 is invertible
proof
assume that
A1: M2 is invertible and
A2: M1 is_similar_to M2;
consider M4 be Matrix of n,K such that
A3: M4 is invertible and
A4: M1=M4~*M2*M4 by A2;
M4~ is invertible by A3;
then M4~*M2 is invertible by A1,MATRIX_6:36;
hence thesis by A3,A4,MATRIX_6:36;
end;
theorem
M2 is invertible & M1 is_similar_to M2 implies M1~ is_similar_to M2~
proof
assume that
A1: M2 is invertible and
A2: M1 is_similar_to M2;
consider M4 be Matrix of n,K such that
A3: M4 is invertible and
A4: M1=M4~*M2*M4 by A2;
A5: M4~ is invertible & M4~~=M4 by A3,MATRIX_6:16;
take M4;
A6: width (M4~)=n & len M4=n by MATRIX_0:24;
A7: len M2=n & width M2=n by MATRIX_0:24;
M2*M4 is invertible & M4~*M2~=(M2*M4)~ by A1,A3,MATRIX_6:36;
then M4~*M2~*M4=(M4~*(M2*M4))~ by A5,MATRIX_6:36
.=M1~ by A4,A6,A7,MATRIX_3:33;
hence thesis by A3;
end;
definition
let n be Nat, K be Field, M1,M2 be Matrix of n,K;
pred M1 is_congruent_Matrix_of M2 means
ex M be Matrix of n,K st M is invertible & M1=M@*M2*M;
reflexivity
proof
set M = 1.(K,n);
let M1 be Matrix of n,K;
M@*M1*M=M*M1*M by MATRIX_6:10
.=M1*M by MATRIX_3:18
.=M1 by MATRIX_3:19;
hence thesis;
end;
end;
theorem
M1 is_congruent_Matrix_of M2 & n>0 implies M2 is_congruent_Matrix_of M1
proof
assume that
A1: M1 is_congruent_Matrix_of M2 and
A2: n>0;
consider M be Matrix of n,K such that
A3: M is invertible and
A4: M1=M@*M2*M by A1;
A5: M~ is_reverse_of M by A3,MATRIX_6:def 4;
take M~;
A6: width (M~)=n by MATRIX_0:24;
A7: len (M@)=n & width (M@)=n by MATRIX_0:24;
A8: width (M)=n by MATRIX_0:24;
A9: len (M~)=n by MATRIX_0:24;
len (M)=n & width (M@*M2)=n by MATRIX_0:24;
then
A10: M1*M~=(M@*M2)*(M*M~) by A4,A8,A9,MATRIX_3:33
.=(M@*M2)*(1.(K,n)) by A5,MATRIX_6:def 2
.=M@*M2 by MATRIX_3:19;
A11: len M2=n by MATRIX_0:24;
A12: width (M~@)=n by MATRIX_0:24;
len M1=n & width M1=n by MATRIX_0:24;
then M~@*M1*M~=M~@*(M1*M~) by A9,A12,MATRIX_3:33
.=(M~@*M@)*M2 by A7,A11,A12,A10,MATRIX_3:33
.=(M*M~)@*M2 by A2,A8,A9,A6,MATRIX_3:22
.=(1.(K,n))@*M2 by A5,MATRIX_6:def 2
.=(1.(K,n))*M2 by MATRIX_6:10
.=M2 by MATRIX_3:18;
hence thesis by A3;
end;
theorem
M1 is_congruent_Matrix_of M2 & M2 is_congruent_Matrix_of M3 & n>0
implies M1 is_congruent_Matrix_of M3
proof
assume that
A1: M1 is_congruent_Matrix_of M2 and
A2: M2 is_congruent_Matrix_of M3 and
A3: n>0;
A4: len M2=n & width M2=n by MATRIX_0:24;
consider M4 be Matrix of n,K such that
A5: M4 is invertible and
A6: M1=M4@*M2*M4 by A1;
A7: len M4=n by MATRIX_0:24;
consider M5 be Matrix of n,K such that
A8: M5 is invertible and
A9: M2=M5@*M3*M5 by A2;
A10: len M5=n by MATRIX_0:24;
A11: len M3=n & len (M5@)=n by MATRIX_0:24;
A12: width M5=n by MATRIX_0:24;
take M5*M4;
A13: len (M5@*M3)=n & len (M5*M4)=n by MATRIX_0:24;
A14: width (M4@)=n by MATRIX_0:24;
A15: width (M5@)=n by MATRIX_0:24;
A16: width (M5@*M3)=n by MATRIX_0:24;
width M4=n by MATRIX_0:24;
then (M5*M4)@*M3*(M5*M4)=(((M4@)*(M5@))*M3)*(M5*M4) by A3,A7,A12,MATRIX_3:22
.=M4@*(M5@*M3)*(M5*M4) by A14,A11,A15,MATRIX_3:33
.=M4@*((M5@*M3)*(M5*M4)) by A14,A16,A13,MATRIX_3:33
.=M4@*((M5@*M3*M5)*M4) by A7,A10,A12,A16,MATRIX_3:33
.=M1 by A6,A9,A4,A7,A14,MATRIX_3:33;
hence thesis by A5,A8,MATRIX_6:36;
end;
theorem
M1 is_congruent_Matrix_of M2 implies M1+M1 is_congruent_Matrix_of M2+M2
proof
assume M1 is_congruent_Matrix_of M2; then
consider M4 be Matrix of n,K such that
A3: M4 is invertible and
A4: M1=M4@*M2*M4;
A5: width (M4@*M2)=n by MATRIX_0:24;
take M4;
A6: len M4=n & len (M4@*M2)=n by MATRIX_0:24;
A7: len M2=n & width M2=n by MATRIX_0:24;
len (M4@)=n & width (M4@)=n by MATRIX_0:24;
then M4@*(M2+M2)*M4=(M4@*M2+M4@*M2)*M4 by A7,MATRIX_4:62
.=M1+M1 by A4,A6,A5,MATRIX_4:63;
hence thesis by A3;
end;
theorem
M1 is_congruent_Matrix_of M2 implies
M1+M1+M1 is_congruent_Matrix_of M2+M2+M2
proof
assume M1 is_congruent_Matrix_of M2; then
consider M4 be Matrix of n,K such that
A3: M4 is invertible and
A4: M1=M4@*M2*M4;
A5: len M4=n & len (M4@*M2)=n by MATRIX_0:24;
A6: width (M4@*M2)=n by MATRIX_0:24;
A7: len M2=n & width M2=n by MATRIX_0:24;
A8: len (M4@)=n & width (M4@)=n by MATRIX_0:24;
then
A9: M4@*(M2+M2)*M4=(M4@*M2+M4@*M2)*M4 by A7,MATRIX_4:62
.=M1+M1 by A4,A5,A6,MATRIX_4:63;
take M4;
A10: len (M4@*(M2+M2))=n & width (M4@*(M2+M2))=n by MATRIX_0:24;
len (M2+M2)=n & width (M2+M2)=n by MATRIX_0:24;
then M4@*(M2+M2+M2)*M4=(M4@*(M2+M2)+M4@*M2)*M4 by A7,A8,MATRIX_4:62
.=M1+M1+M1 by A4,A5,A6,A10,A9,MATRIX_4:63;
hence thesis by A3;
end;
theorem
M1 is Orthogonal implies M2*M1 is_congruent_Matrix_of M1*M2
proof
A1: len M2=n & width (M1~)=n by MATRIX_0:24;
assume
A2: M1 is Orthogonal;
then M1 is invertible by MATRIX_6:def 7;
then
A3: M1~ is_reverse_of M1 by MATRIX_6:def 4;
take M1;
len M1=n & width M1=n by MATRIX_0:24;
then M1~*(M1*M2)*M1 =((M1~*M1)*M2)*M1 by A1,MATRIX_3:33
.=((1.(K,n))*M2)*M1 by A3,MATRIX_6:def 2
.=M2*M1 by MATRIX_3:18;
hence thesis by A2,MATRIX_6:def 7;
end;
theorem
M2 is invertible & M1 is_congruent_Matrix_of M2 & n>0 implies M1 is
invertible
proof
assume that
A1: M2 is invertible and
A2: M1 is_congruent_Matrix_of M2 and
A3: n>0;
consider M4 be Matrix of n,K such that
A4: M4 is invertible and
A5: M1=M4@*M2*M4 by A2;
set M6=M4~@;
set M5=M4@;
A6: width M4=n & width (M4~)=n by MATRIX_0:24;
len M4=n by MATRIX_0:24;
then
A7: ((M4~)*M4)@=(M4@)*(M4~@) by A3,A6,MATRIX_3:22;
A8: M4~ is_reverse_of M4 by A4,MATRIX_6:def 4;
then (M4~)*M4=1.(K,n) by MATRIX_6:def 2;
then
A9: M5*M6=1.(K,n) by A7,MATRIX_6:10;
len (M4~)=n by MATRIX_0:24;
then (M4*(M4~))@=(M4~@)*(M4@) by A3,A6,MATRIX_3:22;
then M5*M6=M6*M5 by A8,A7,MATRIX_6:def 2;
then M5 is_reverse_of M6 by A9,MATRIX_6:def 2;
then M5 is invertible by MATRIX_6:def 3;
then M5*M2 is invertible by A1,MATRIX_6:36;
hence thesis by A4,A5,MATRIX_6:36;
end;
theorem
M1 is_congruent_Matrix_of M2 & n>0 implies M1@ is_congruent_Matrix_of M2@
proof
assume that
A1: M1 is_congruent_Matrix_of M2 and
A2: n>0;
consider M4 be Matrix of n,K such that
A3: M4 is invertible and
A4: M1=M4@*M2*M4 by A1;
A5: width (M4@)=n by MATRIX_0:24;
A6: width (M2*M4)=n & len (M2*M4)=n by MATRIX_0:24;
A7: len M2=n by MATRIX_0:24;
A8: width M2=n by MATRIX_0:24;
take M4;
A9: len M4=n by MATRIX_0:24;
A10: width M4=n by MATRIX_0:24;
then M4@*M2@*M4=M4@*M2@*(M4@)@ by A2,A9,MATRIX_0:57
.=(M2*M4)@*(M4@)@ by A2,A10,A9,A8,MATRIX_3:22
.=(M4@*(M2*M4))@ by A2,A5,A6,MATRIX_3:22
.=M1@ by A4,A9,A8,A7,A5,MATRIX_3:33;
hence thesis by A3;
end;
theorem
M4 is Orthogonal implies M4@*M2*M4 is_similar_to M2
proof
assume
A1: M4 is Orthogonal;
take M4;
thus thesis by A1,MATRIX_6:def 7;
end;
definition
let n be Nat, K be Field, M be Matrix of n,K;
func Trace M -> Element of K equals
Sum diagonal_of_Matrix M;
coherence;
end;
theorem
Trace M1=Trace M1@
proof
A1: for i be Nat st i in Seg n holds (diagonal_of_Matrix M1).i=(
diagonal_of_Matrix M1@).i
proof
let i be Nat;
assume
A2: i in Seg n;
then
A3: (diagonal_of_Matrix M1).i=M1*(i,i) & (diagonal_of_Matrix M1@).i=M1@*(i
,i) by MATRIX_3:def 10;
Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
then [i,i] in Indices M1 by A2,ZFMISC_1:87;
hence thesis by A3,MATRIX_0:def 6;
end;
len diagonal_of_Matrix M1@ = n by MATRIX_3:def 10;
then
A4: dom (diagonal_of_Matrix M1@) = Seg n by FINSEQ_1:def 3;
len diagonal_of_Matrix M1 = n by MATRIX_3:def 10;
then dom (diagonal_of_Matrix M1) = Seg n by FINSEQ_1:def 3;
hence thesis by A1,A4,FINSEQ_1:13;
end;
theorem Th53:
Trace (M1+M2)=Trace M1+Trace M2
proof
A1: len diagonal_of_Matrix M1=n by MATRIX_3:def 10;
then
A2: dom diagonal_of_Matrix M1 = Seg n by FINSEQ_1:def 3;
len diagonal_of_Matrix (M1+M2)=n by MATRIX_3:def 10;
then
A3: dom diagonal_of_Matrix (M1+M2)=Seg n by FINSEQ_1:def 3;
A4: len diagonal_of_Matrix M2=n by MATRIX_3:def 10;
then dom diagonal_of_Matrix M2=Seg n by FINSEQ_1:def 3;
then
A5: dom ((diagonal_of_Matrix M1)+(diagonal_of_Matrix M2)) =Seg n by A2,
POLYNOM1:1;
for i be Nat st i in dom diagonal_of_Matrix M1 holds ((
diagonal_of_Matrix M1)+(diagonal_of_Matrix M2)).i =(diagonal_of_Matrix (M1+M2))
.i
proof
let i be Nat;
assume i in dom diagonal_of_Matrix M1;
then
A6: i in Seg n by A1,FINSEQ_1:def 3;
then
A7: (diagonal_of_Matrix (M1+M2)).i=(M1+M2)*(i,i) by MATRIX_3:def 10;
Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
then
A8: [i,i] in Indices M1 by A6,ZFMISC_1:87;
(diagonal_of_Matrix M1).i=M1*(i,i) & (diagonal_of_Matrix M2).i=M2*(i,
i) by A6,MATRIX_3:def 10;
then
((diagonal_of_Matrix M1)+(diagonal_of_Matrix M2)).i =M1*(i,i)+M2*(i,i
) by A5,A6,FUNCOP_1:22
.=(diagonal_of_Matrix (M1+M2)).i by A8,A7,MATRIX_1:def 6;
hence thesis;
end;
then Trace (M1+M2)=Sum ((diagonal_of_Matrix M1)+(diagonal_of_Matrix M2)) by
A2,A3,A5,FINSEQ_1:13
.=Sum (diagonal_of_Matrix M1)+Sum (diagonal_of_Matrix M2) by A1,A4,
MATRIX_4:61;
hence thesis;
end;
theorem
Trace (M1+M2+M3)=Trace M1+Trace M2+Trace M3
proof
Trace (M1+M2+M3) =Trace (M1+M2)+Trace M3 by Th53;
hence thesis by Th53;
end;
theorem Th55:
Trace (0.(K,n))=0.K
proof
len (diagonal_of_Matrix 0.(K,n))=n by MATRIX_3:def 10;
then
A1: dom (diagonal_of_Matrix 0.(K,n))= Seg n by FINSEQ_1:def 3;
for i st i in dom (diagonal_of_Matrix 0.(K,n)) holds (diagonal_of_Matrix
0.(K,n))/.i=0.K
proof
let i;
assume
A2: i in dom (diagonal_of_Matrix 0.(K,n));
Indices (0.(K,n))=[:Seg n, Seg n:] by MATRIX_0:24;
then [i,i] in Indices (0.(K,n,n)) by A1,A2,ZFMISC_1:87;
then
A3: (0.(K,n))*(i,i)=0.K by MATRIX_3:1;
(diagonal_of_Matrix 0.(K,n)).i=(0.(K,n))*(i,i) by A1,A2,MATRIX_3:def 10;
hence thesis by A2,A3,PARTFUN1:def 6;
end;
hence thesis by MATRLIN:11;
end;
theorem Th56:
Trace (-M1) = -Trace M1
proof
A1: len M1=n & width M1=n by MATRIX_0:24;
Trace M1+Trace (-M1)=Trace (M1+(-M1)) by Th53
.=Trace (0.(K,n,n)) by A1,MATRIX_4:2
.=Trace (0.(K,n))
.=0.K by Th55;
hence thesis by RLVECT_1:6;
end;
theorem
-(Trace (-M1))=Trace M1
proof
A1: len M1=n & width M1=n by MATRIX_0:24;
Trace M1+Trace (-M1)=Trace (M1+(-M1)) by Th53
.=Trace (0.(K,n,n)) by A1,MATRIX_4:2
.=Trace (0.(K,n))
.=0.K by Th55;
hence thesis by RLVECT_1:6;
end;
theorem
Trace (M1+-M1)=0.K
proof
len M1=n & width M1=n by MATRIX_0:24;
then Trace (M1+(-M1))=Trace (0.(K,n,n)) by MATRIX_4:2
.=Trace (0.(K,n))
.=0.K by Th55;
hence thesis;
end;
theorem Th59:
Trace (M1-M2)=Trace M1-Trace M2
proof
Trace (M1-M2)=Trace M1+Trace (-M2) by Th53
.=Trace M1+-Trace M2 by Th56;
hence thesis;
end;
theorem
Trace (M1-M2+M3)=Trace M1-Trace M2+Trace M3
proof
Trace (M1-M2+M3)=Trace (M1-M2)+Trace M3 by Th53
.=Trace M1-Trace M2+Trace M3 by Th59;
hence thesis;
end;
theorem
Trace (M1+M2-M3)=Trace M1+Trace M2-Trace M3
proof
Trace (M1+M2-M3)=Trace (M1+M2)-Trace M3 by Th59
.=Trace M1+Trace M2-Trace M3 by Th53;
hence thesis;
end;
theorem
Trace (M1-M2-M3)=Trace M1-Trace M2-Trace M3
proof
Trace (M1-M2-M3)=Trace (M1-M2)-Trace M3 by Th59
.=Trace M1-Trace M2-Trace M3 by Th59;
hence thesis;
end;