:: Some Properties Of Some Special Matrices :: by Xiaopeng Yue , Xiquan Liang and Zhongpin Sun :: :: Received December 7, 2005 :: Copyright (c) 2005-2021 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; 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 :: MATRIX_6:def 1 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 :: MATRIX_6:def 2 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 :: MATRIX_6:def 3 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; end; registration let n; let K be Ring; let M1,M2 be Matrix of n,K; cluster M1+M2 -> (n,n)-size; end; registration let n; let K be Field; let M1,M2 be Matrix of n,K; cluster M1-M2 -> (n,n)-size; end; registration let n; let K be Ring; let M1,M2 be Matrix of n,K; cluster M1*M2 -> (n,n)-size; end; theorem :: MATRIX_6:1 for K being Field, A being Matrix of K holds (0.(K,len A,len A))*A = 0.(K,len A,width A); theorem :: MATRIX_6:2 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); theorem :: MATRIX_6:3 M1 commutes_with 0.(K,n,n); theorem :: MATRIX_6:4 M1 commutes_with M2 & M2 commutes_with M3 & M1 commutes_with M3 implies M1 commutes_with M2*M3; theorem :: MATRIX_6:5 M1 commutes_with M2 & M1 commutes_with M3 & n>0 implies M1 commutes_with M2+M3; theorem :: MATRIX_6:6 M1 commutes_with 1.(K,n); theorem :: MATRIX_6:7 M2 is_reverse_of M3 & M1 is_reverse_of M3 implies M1=M2; definition let n be Nat, K be Field, M1 be Matrix of n,K; assume M1 is invertible; func M1~ -> Matrix of n,K means :: MATRIX_6:def 4 it is_reverse_of M1; end; theorem :: MATRIX_6:8 (1.(K,n))~ = 1.(K,n) & 1.(K,n) is invertible; registration let K be Field, n be Nat; cluster 1.(K,n) -> invertible; end; registration let K be Field, n be Nat; cluster invertible for Matrix of n, K; end; theorem :: MATRIX_6:9 ((1.(K,n))~)~ = 1.(K,n); theorem :: MATRIX_6:10 (1.(K,n))@ = 1.(K,n); theorem :: MATRIX_6:11 for K being Field, n being Nat holds ((1.(K,n))@)~ = 1.(K,n); theorem :: MATRIX_6:12 M3 is_reverse_of M1 & n>0 implies M1@ is_reverse_of M3@; theorem :: MATRIX_6:13 M is invertible implies M@ is invertible & M@~= M~@; registration let K, n; let M be invertible Matrix of n, K; cluster M@ -> invertible; end; theorem :: MATRIX_6:14 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; theorem :: MATRIX_6:15 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 :: MATRIX_6:16 M is invertible implies M~ is invertible & (M~)~= M; registration let K, n; let M be invertible Matrix of n, K; cluster M~ -> invertible; end; theorem :: MATRIX_6:17 n > 0 & M1*M2=0.(K,n,n) & M1 is invertible implies M1 commutes_with M2; theorem :: MATRIX_6:18 M1=M1*M2 & M1 is invertible implies M1 commutes_with M2; theorem :: MATRIX_6:19 M1=M2*M1 & M1 is invertible implies M1 commutes_with M2; definition let n be Nat, K be Field; let M1 be Matrix of n,K; attr M1 is symmetric means :: MATRIX_6:def 5 M1@=M1; end; registration let n be Nat, K be Field; cluster 1.(K,n) -> symmetric; end; theorem :: MATRIX_6:20 ((n,n)-->a)@ = (n,n)-->a; theorem :: MATRIX_6:21 (n,n)-->a is symmetric; theorem :: MATRIX_6:22 n > 0 & M1 is symmetric & M2 is symmetric implies (M1 commutes_with M2 iff M1*M2 is symmetric); theorem :: MATRIX_6:23 (M1+M2)@=M1@+M2@; theorem :: MATRIX_6:24 M1 is symmetric & M2 is symmetric implies M1+M2 is symmetric; theorem :: MATRIX_6:25 ::: should be a cluster M1 is upper_triangular Matrix of n,K & M1 is lower_triangular Matrix of n,K implies M1 is symmetric; theorem :: MATRIX_6:26 for K being Field,n being Nat,M1 being Matrix of n,K holds (-M1) @=-(M1@); theorem :: MATRIX_6:27 for K being Field, n being Nat, M1 being Matrix of n,K st M1 is symmetric holds -M1 is symmetric; theorem :: MATRIX_6:28 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; definition let n be Nat,K be Field; let M1 be Matrix of n,K; attr M1 is antisymmetric means :: MATRIX_6:def 6 M1@=-M1; end; theorem :: MATRIX_6:29 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); theorem :: MATRIX_6:30 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; theorem :: MATRIX_6:31 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; theorem :: MATRIX_6:32 for K being Field,n being Nat,M1 being Matrix of n,K st M1 is antisymmetric holds -M1 is antisymmetric; theorem :: MATRIX_6:33 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; theorem :: MATRIX_6:34 n>0 implies M1-M1@ is antisymmetric; theorem :: MATRIX_6:35 n>0 implies (M1 commutes_with M2 iff (M1+M2)*(M1+M2)=M1*M1+M1*M2+M1*M2 +M2*M2); theorem :: MATRIX_6:36 M1 is invertible & M2 is invertible implies M1*M2 is invertible & (M1*M2)~=(M2~)*(M1~); theorem :: MATRIX_6:37 M1 is invertible & M2 is invertible & M1 commutes_with M2 implies M1* M2 is invertible & (M1*M2)~ = (M1~)*(M2~); theorem :: MATRIX_6:38 M1 is invertible & M1*M2=1.(K,n) implies M1 is_reverse_of M2; theorem :: MATRIX_6:39 M2 is invertible & M2*M1=1.(K,n) implies M1 is_reverse_of M2; theorem :: MATRIX_6:40 M1 is invertible & M1 commutes_with M2 implies M1~ commutes_with M2; definition let n be Nat, K be Field; let M1 be Matrix of n,K; attr M1 is Orthogonal means :: MATRIX_6:def 7 M1 is invertible & M1@ = M1~; end; theorem :: MATRIX_6:41 M1*(M1@)=1.(K,n) & M1 is invertible iff M1 is Orthogonal; theorem :: MATRIX_6:42 M1 is invertible & (M1@)*M1=1.(K,n) iff M1 is Orthogonal; theorem :: MATRIX_6:43 M1 is Orthogonal implies (M1@)*M1=M1*(M1@); theorem :: MATRIX_6:44 M1 is Orthogonal & M1 commutes_with M2 implies M1@ commutes_with M2; theorem :: MATRIX_6:45 M1 is invertible & M2 is invertible implies M1*M2 is invertible & (M1*M2)~=M2~*M1~; theorem :: MATRIX_6:46 n > 0 & M1 is Orthogonal & M2 is Orthogonal implies M1*M2 is Orthogonal; theorem :: MATRIX_6:47 M1 is Orthogonal & M1 commutes_with M2 implies M1@ commutes_with M2; theorem :: MATRIX_6:48 n > 0 & M1 commutes_with M2 implies M1+M1 commutes_with M2; theorem :: MATRIX_6:49 n >0 & M1 commutes_with M2 implies M1+M2 commutes_with M2; theorem :: MATRIX_6:50 n >0 & M1 commutes_with M2 implies M1+M1 commutes_with M2+M2; theorem :: MATRIX_6:51 n >0 & M1 commutes_with M2 implies M1+M2 commutes_with M2+M2; theorem :: MATRIX_6:52 M1 commutes_with M2 implies M1*M2 commutes_with M2; theorem :: MATRIX_6:53 M1 commutes_with M2 implies M1*M1 commutes_with M2; theorem :: MATRIX_6:54 M1 commutes_with M2 implies M1*M1 commutes_with M2*M2; theorem :: MATRIX_6:55 n>0 & M1 commutes_with M2 implies M1@ commutes_with M2@; theorem :: MATRIX_6:56 M1 is invertible & M2 is invertible & M3 is invertible implies M1*M2*M3 is invertible & (M1*M2*M3)~=M3~*M2~*M1~; theorem :: MATRIX_6:57 n > 0 & M1 is Orthogonal & M2 is Orthogonal & M3 is Orthogonal implies M1*M2*M3 is Orthogonal; theorem :: MATRIX_6:58 1.(K,n) is Orthogonal; theorem :: MATRIX_6:59 n > 0 & M1 is Orthogonal & M2 is Orthogonal implies M1~*M2 is Orthogonal;