:: 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-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, 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_4, MATRIX_6, FVSUM_1, XXREAL_0;
 constructors BINOP_1, REAL_1, NAT_1, FVSUM_1, MATRIX_6, MATRIX_1, MATRIX_3,
      MATRIX_4;
 registrations RELSET_1, XREAL_0, INT_1, STRUCT_0, MATRIX_6, ORDINAL1,
      MATRIX_0;
 requirements NUMERALS, SUBSET, ARITHM;


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
:: MATRIX_8:def 1

  M1*M1=M1;
  attr M1 is Nilpotent means
:: MATRIX_8:def 2

  M1*M1=0.(K,n);
  attr M1 is Involutory means
:: MATRIX_8:def 3

  M1*M1=1.(K,n);
  attr M1 is Self_Reversible means
:: MATRIX_8:def 4

  M1 is invertible & M1~=M1;
end;

theorem :: MATRIX_8:1
  1.(K,n) is Idempotent Involutory;

theorem :: MATRIX_8:2
  0.(K,n) is Idempotent Nilpotent;

registration
  let n be Nat, K be Field;
  cluster 1.(K,n) -> Idempotent Involutory;
  cluster 0.(K,n) -> Idempotent Nilpotent;
end;

theorem :: MATRIX_8:3
  n>0 implies (M1 is Idempotent iff M1@ is Idempotent);

theorem :: MATRIX_8:4
  M1 is Involutory implies M1 is invertible;

theorem :: MATRIX_8:5
  M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 implies M1*
  M1 commutes_with M2*M2;

theorem :: MATRIX_8:6
  n>0 & M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 & M1*
  M2=0.(K,n) implies M1+M2 is Idempotent;

theorem :: MATRIX_8:7
  M1 is Idempotent & M2 is Idempotent & M1*M2=-(M2*M1) implies M1+M2 is
  Idempotent;

theorem :: MATRIX_8:8
  M1 is Idempotent & M2 is invertible implies (M2~)*M1*M2 is Idempotent;

theorem :: MATRIX_8:9
  M1 is invertible Idempotent implies M1~ is Idempotent;

theorem :: MATRIX_8:10
  M1 is invertible Idempotent implies M1=1.(K,n);

theorem :: MATRIX_8:11
  M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 implies M1*
  M2 is Idempotent;

theorem :: MATRIX_8:12
  M1 is Idempotent & M2 is Idempotent & M1 commutes_with M2 implies M1@*
  M2@ is Idempotent;

theorem :: MATRIX_8:13
  M1 is Idempotent & M2 is Idempotent & M1 is invertible implies M1*M2
  is Idempotent;

theorem :: MATRIX_8:14
  M1 is Idempotent Orthogonal implies M1 is symmetric;

theorem :: MATRIX_8:15
  M2*M1=1.(K,n) implies M1*M2 is Idempotent;

theorem :: MATRIX_8:16
  M1 is Idempotent Orthogonal implies M1=1.(K,n);

theorem :: MATRIX_8:17
  M1 is symmetric implies M1*M1@ is symmetric;

theorem :: MATRIX_8:18
  M1 is symmetric implies M1@*M1 is symmetric;

theorem :: MATRIX_8:19
  M1 is invertible & M1*M2=M1*M3 implies M2=M3;

theorem :: MATRIX_8:20
  M1 is invertible & M2*M1=M3*M1 implies M2=M3;

theorem :: MATRIX_8:21
  M1 is invertible & M2*M1=0.(K,n) implies M2=0.(K,n);

theorem :: MATRIX_8:22
  M1 is invertible & M2*M1=0.(K,n) implies M2=0.(K,n);

theorem :: MATRIX_8:23
  M1 is Nilpotent & M1 commutes_with M2 & n>0 implies M1*M2 is Nilpotent;

theorem :: MATRIX_8:24
  n>0 & M1 is Nilpotent & M2 is Nilpotent & M1 commutes_with M2 & M1*M2=
  0.(K,n) implies M1+M2 is Nilpotent;

theorem :: MATRIX_8:25
  M1 is Nilpotent & M2 is Nilpotent & M1*M2=-M2*M1 & n>0 implies M1+M2
  is Nilpotent;

theorem :: MATRIX_8:26
  M1 is Nilpotent & n>0 implies M1@ is Nilpotent;

theorem :: MATRIX_8:27
  M1 is Nilpotent Idempotent implies M1=0.(K,n);

theorem :: MATRIX_8:28
  n>0 implies 0.(K,n)<>1.(K,n);

theorem :: MATRIX_8:29
  n>0 & M1 is Nilpotent implies not M1 is invertible;

theorem :: MATRIX_8:30
  M1 is Self_Reversible implies M1 is Involutory;

theorem :: MATRIX_8:31
  1.(K,n) is Self_Reversible;

theorem :: MATRIX_8:32
  M1 is Self_Reversible Idempotent implies M1=1.(K,n);

theorem :: MATRIX_8:33
  M1 is Self_Reversible symmetric implies M1 is Orthogonal;

definition
  let n be Nat, K be Field, M1,M2 be Matrix of n,K;
  pred M1 is_similar_to M2 means
:: MATRIX_8:def 5

  ex M be Matrix of n,K st M is invertible & M1=M~*M2*M;
  reflexivity;
  symmetry;
end;

theorem :: MATRIX_8:34
  M1 is_similar_to M2 & M2 is_similar_to M3 implies M1 is_similar_to M3;

theorem :: MATRIX_8:35
  M1 is_similar_to M2 & M2 is Idempotent implies M1 is Idempotent;

theorem :: MATRIX_8:36
  M1 is_similar_to M2 & M2 is Nilpotent & n>0 implies M1 is Nilpotent;

theorem :: MATRIX_8:37
  M1 is_similar_to M2 & M2 is Involutory implies M1 is Involutory;

theorem :: MATRIX_8:38
  M1 is_similar_to M2 & n>0 implies M1+1.(K,n) is_similar_to M2+1.(K,n);

theorem :: MATRIX_8:39
  M1 is_similar_to M2 & n>0 implies M1+M1 is_similar_to M2+M2;

theorem :: MATRIX_8:40
  M1 is_similar_to M2 & n>0 implies M1+M1+M1 is_similar_to M2+M2+M2;

theorem :: MATRIX_8:41
  M1 is invertible implies M2*M1 is_similar_to M1*M2;

theorem :: MATRIX_8:42
  M2 is invertible & M1 is_similar_to M2 implies M1 is invertible;

theorem :: MATRIX_8:43
  M2 is invertible & M1 is_similar_to M2 implies M1~ is_similar_to M2~;

definition
  let n be Nat, K be Field, M1,M2 be Matrix of n,K;
  pred M1 is_congruent_Matrix_of M2 means
:: MATRIX_8:def 6

  ex M be Matrix of n,K st M is invertible & M1=M@*M2*M;
  reflexivity;
end;

theorem :: MATRIX_8:44
  M1 is_congruent_Matrix_of M2 & n>0 implies M2 is_congruent_Matrix_of M1;

theorem :: MATRIX_8:45
  M1 is_congruent_Matrix_of M2 & M2 is_congruent_Matrix_of M3 & n>0
  implies M1 is_congruent_Matrix_of M3;

theorem :: MATRIX_8:46
  M1 is_congruent_Matrix_of M2 & n>0 implies M1+M1 is_congruent_Matrix_of M2+M2
;

theorem :: MATRIX_8:47
  M1 is_congruent_Matrix_of M2 & n>0 implies M1+M1+M1
  is_congruent_Matrix_of M2+M2+M2;

theorem :: MATRIX_8:48
  M1 is Orthogonal implies M2*M1 is_congruent_Matrix_of M1*M2;

theorem :: MATRIX_8:49
  M2 is invertible & M1 is_congruent_Matrix_of M2 & n>0 implies M1 is
  invertible;

theorem :: MATRIX_8:50
  M1 is_congruent_Matrix_of M2 & n>0 implies M1@ is_congruent_Matrix_of M2@;

theorem :: MATRIX_8:51
  M4 is Orthogonal implies M4@*M2*M4 is_similar_to M2;

definition
  let n be Nat, K be Field, M be Matrix of n,K;
  func Trace M -> Element of K equals
:: MATRIX_8:def 7
  Sum diagonal_of_Matrix M;
end;

theorem :: MATRIX_8:52
  Trace M1=Trace M1@;

theorem :: MATRIX_8:53
  Trace (M1+M2)=Trace M1+Trace M2;

theorem :: MATRIX_8:54
  Trace (M1+M2+M3)=Trace M1+Trace M2+Trace M3;

theorem :: MATRIX_8:55
  Trace (0.(K,n))=0.K;

theorem :: MATRIX_8:56
  Trace (-M1) = -Trace M1;

theorem :: MATRIX_8:57
  -(Trace (-M1))=Trace M1;

theorem :: MATRIX_8:58
  Trace (M1+-M1)=0.K;

theorem :: MATRIX_8:59
  Trace (M1-M2)=Trace M1-Trace M2;

theorem :: MATRIX_8:60
  Trace (M1-M2+M3)=Trace M1-Trace M2+Trace M3;

theorem :: MATRIX_8:61
  Trace (M1+M2-M3)=Trace M1+Trace M2-Trace M3;

theorem :: MATRIX_8:62
  Trace (M1-M2-M3)=Trace M1-Trace M2-Trace M3;