:: Invertibility of Matrices of Field Elements
::  by Yatsuka Nakamura , Kunio Oniumi and Wenpai Chang
::
:: Received April 2, 2008
:: Copyright (c) 2008-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 NUMBERS, XBOOLE_0, SUBSET_1, VECTSP_1, STRUCT_0, EUCLID,
      FINSEQ_1, FINSEQ_2, SUPINF_2, RELAT_1, ALGSTR_0, ARYTM_3, ARYTM_1,
      RVSUM_1, FUNCT_1, PARTFUN1, TARSKI, ZFMISC_1, NAT_1, XXREAL_0, GROUP_1,
      ORDINAL4, CARD_1, FVSUM_1, CARD_3, MATRIX_1, PRALG_1, MESFUNC1, MATRIX_6,
      TREES_1, MATRIXR2, AFINSQ_1, FUNCOP_1, QC_LANG1, FINSOP_1, INCSP_1,
      FUNCT_7, RFINSEQ, MATRIX_3, MATRIX14;
 notations TARSKI, XBOOLE_0, SUBSET_1, XXREAL_0, RELAT_1, FUNCT_1, BINOP_1,
      ALGSTR_0, ZFMISC_1, MATRIX_0, FVSUM_1, PARTFUN1, FUNCT_3, ORDINAL1,
      NUMBERS, FINSEQ_7, FUNCT_2, FUNCOP_1, FINSEQ_1, STRUCT_0, GROUP_1,
      MATRIX_1, MATRIX_3, MATRIX_6, XCMPLX_0, NAT_1, NAT_D, VECTSP_1, FINSEQ_2,
      FINSOP_1, RFINSEQ;
 constructors FUNCT_3, FINSEQ_7, SETWISEO, FINSOP_1, JORDAN3, RFINSEQ,
      MATRIX_6, NAT_D, RELSET_1, FVSUM_1, MATRIX_1, MATRIX_3, BINOP_1;
 registrations FINSEQ_2, XREAL_0, NAT_1, FUNCOP_1, STRUCT_0, VECTSP_1,
      ORDINAL1, RELAT_1, CARD_1, FINSEQ_1, MATRIX_6, MATRIX_0;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Preparation

reserve

  k,n,m,i,j for Element of NAT,
  K for Field;

definition
  let K be non empty ZeroStr, n;
  func 0*(K,n) -> FinSequence of K equals
:: MATRIX14:def 1
  n |-> (0.K);
end;

definition
  let K be non empty ZeroStr;
  let n;
  redefine func 0*(K,n) -> Element of n-tuples_on (the carrier of K);
end;

reserve L for non empty addLoopStr;

theorem :: MATRIX14:1
  for x being FinSequence of L holds x is Element of (len x)
  -tuples_on the carrier of L;

theorem :: MATRIX14:2
  for x1,x2 being FinSequence of L st len x1=len x2 holds len (x1+ x2)=len x1;

theorem :: MATRIX14:3
  for x1,x2 being FinSequence of L st len x1=len x2 holds len (x1- x2)=len x1;

reserve G for non empty multLoopStr;

theorem :: MATRIX14:4
  for x1,x2 being FinSequence of G,i st i in dom mlt(x1,x2) holds
  mlt(x1,x2).i = (x1/.i)*(x2/.i) & (mlt(x1,x2))/.i=(x1/.i)*(x2/.i);

theorem :: MATRIX14:5
  for x1,x2 being FinSequence of L,i being Nat st len x1=len x2 & 1
  <=i & i<=len x1 holds (x1+x2).i=x1/.i + x2/.i & (x1-x2).i=x1/.i - x2/.i;

theorem :: MATRIX14:6
  for a being Element of K, x being FinSequence of K holds -a*x = (
  -a)*x & -a*x = a*(-x);

theorem :: MATRIX14:7
  for x1,x2,y1,y2 being FinSequence of G st len x1=len x2 & len y1=
  len y2 holds mlt(x1^y1,x2^y2)=(mlt(x1,x2))^(mlt(y1,y2));

notation
  let K;
  let e1,e2 be FinSequence of K;
  synonym |( e1,e2 )| for e1 "*" e2;
end;

theorem :: MATRIX14:8
  for x,y being FinSequence of K,a being Element of K st len x=len
  y holds mlt(a*x,y)=a*(mlt(x,y)) & mlt(x,a*y)=a*(mlt(x,y));

theorem :: MATRIX14:9
  for x,y being FinSequence of K,a being Element of K st len x=len y
  holds |(a*x,y)| = a*|(x,y)|;

theorem :: MATRIX14:10
  for x,y being FinSequence of K,a being Element of K st len x=len
  y holds |(x,a*y)| = a*|(x,y)|;

theorem :: MATRIX14:11
  for x,y1,y2 being FinSequence of K,a being Element of K st len x
  =len y1 & len x=len y2 holds |(x,y1+y2)| = |(x,y1)| + |(x,y2)|;

theorem :: MATRIX14:12
  for x1,x2,y1,y2 being FinSequence of K st len x1=len x2 & len y1
  =len y2 holds |( x1^y1, x2^y2 )| = |(x1,x2)| + |(y1,y2)|;

theorem :: MATRIX14:13
  for p1 being Element of n-tuples_on the carrier of K holds mlt(
  p1,(n |-> (0.K)))=n |-> (0.K);

notation
  let n;
  let K;
  let A be Matrix of n,K;
  synonym Inv A for A~;
end;

begin :: Zero Vectors and Base Vectors of Field Elements

theorem :: MATRIX14:14
  1.(K,0)=0.(K,0) & 1.(K,0)={};

theorem :: MATRIX14:15
  for A being Matrix of 0,K holds A={} & A=1.(K,0) & A=0.(K,0);

theorem :: MATRIX14:16
  for A being Matrix of 0,K holds A is invertible;

theorem :: MATRIX14:17
  for A,B,C being Matrix of n,K holds A*B*C=A*(B*C);

theorem :: MATRIX14:18
  for A,B being Matrix of n,K holds A is invertible & B=A~ iff B*A
  =1.(K,n) & A*B=1.(K,n);

theorem :: MATRIX14:19
  for A being Matrix of n,K holds A is invertible iff ex B being
  Matrix of n,K st B*A=1.(K,n) & A*B=1.(K,n);

theorem :: MATRIX14:20
  for x being FinSequence of K holds |(x, 0*(K,len x))| = 0.K;

theorem :: MATRIX14:21
  for x being FinSequence of K holds |(0*(K,len x),x)| = 0.K;

theorem :: MATRIX14:22
  for a being Element of K holds |( <* 0.K *>, <* a *> )|=0.K;

definition
  let K;
  let n,i be Nat;
  func Base_FinSeq(K,n,i) -> FinSequence of K equals
:: MATRIX14:def 2
  Replace((n |-> 0.K),i,1.K);
end;

theorem :: MATRIX14:23
  for n, i being Nat holds len Base_FinSeq(K,n,i)=n;

theorem :: MATRIX14:24
  for i, n being Nat st 1<=i & i<=n holds (Base_FinSeq(K,n,i)).i= 1.K;

theorem :: MATRIX14:25
  for i,j,n be Nat st 1<=j & j<=n & i<>j holds (Base_FinSeq(K,n,i) ).j=0.K;

theorem :: MATRIX14:26
  for i,n being Nat st 1<=i & i<=n holds (1.(K,n)).i=Base_FinSeq(K ,n,i);

theorem :: MATRIX14:27
  for i,j st 1<=i & i<=n & 1<=j & j<=n holds (1.(K,n))*(i,j)=(
  Base_FinSeq(K,n,i)).j;

theorem :: MATRIX14:28
  for A being Matrix of n,K holds A=0.(K,n) iff for i,j being Element of
  NAT st 1<=i & i<=n & 1<=j & j<=n holds A*(i,j)=0.K;

theorem :: MATRIX14:29
  for A being Matrix of n,K holds A=1.(K,n) iff for i,j being
  Nat st 1<=i & i<=n & 1<=j & j<=n holds A*(i,j)=IFEQ(i,j,1.K,0.K);

begin :: Conditions of Invertibility

theorem :: MATRIX14:30
  for A,B being Matrix of n,K holds (A*B)@=(B@)*(A@);

theorem :: MATRIX14:31
  for A being Matrix of n,K st A is invertible holds A@ is
  invertible & (A@)~ =(A~)@;

theorem :: MATRIX14:32
  for x being FinSequence of K, a being Element of K st (ex i st 1
<=i & i<=len x & x.i=a & (for j st j<>i & 1<=j & j<=len x holds x.j=0.K)) holds
  Sum x=a;

theorem :: MATRIX14:33
  for f1,f2 being FinSequence of K holds dom mlt(f1,f2) = dom f1 /\ dom
  f2 & for i st i in dom (mlt(f1,f2)) holds (mlt(f1,f2)).i = (f1/.i) * (f2/.i);

theorem :: MATRIX14:34
  for x,y being FinSequence of K,i st len x=m & y=mlt (x,
  Base_FinSeq(K,m,i)) & 1<=i & i<=m holds y.i=x.i & for j st j<>i & 1<=j & j<=m
  holds y.j= 0.K;

theorem :: MATRIX14:35
  for x being FinSequence of K st len x=m & 1<=i & i<=m holds |( x
  ,Base_FinSeq(K,m,i) )|=x.i & |( x,Base_FinSeq(K,m,i) )|=x/.i;

theorem :: MATRIX14:36
  for m,i st 1<=i & i<=m holds |( Base_FinSeq(K,m,i),Base_FinSeq(K
  ,m,i) )|= 1.K;

theorem :: MATRIX14:37
  for a being Element of K,P,Q being Matrix of n,K st n>0 & a<>0.K
& P*(1,1)= a" & (for i st 1<i & i<=n holds P.i=Base_FinSeq(K,n,i)) & Q*(1,1)=a
  & (for j st 1<j & j<=n holds Q*(1,j)= -a*(P*(1,j))) & (for i st 1<i & i<=n
  holds Q.i=Base_FinSeq(K,n,i)) holds P is invertible & Q=P~;

theorem :: MATRIX14:38
  for a being Element of K,P being Matrix of n,K st n>0 & a<>0.K &
  P*(1,1)= a" & (for i st 1<i & i<=n holds P.i=Base_FinSeq(K,n,i)) holds P is
  invertible;

theorem :: MATRIX14:39
  for A being Matrix of n,K st n>0 & A*(1,1)<>0.K ex P being
Matrix of n,K st P is invertible & (A*P)*(1,1)=1.K & (for j st 1<j & j<=n holds
  (A*P)*(1,j)= 0.K)& for i st 1<i & i<=n & A*(i,1)= 0.K holds (A*P)*(i,1)= 0.K;

theorem :: MATRIX14:40
  for A being Matrix of n,K st n>0 & A*(1,1)<>0.K ex P being
Matrix of n,K st P is invertible & (P*A)*(1,1)=1.K & (for i st 1<i & i<=n holds
  (P*A)*(i,1)= 0.K)& for j st 1<j & j<=n & A*(1,j)= 0.K holds (P*A)*(1,j)= 0.K;

theorem :: MATRIX14:41
  for A being Matrix of n,K st n>0 & A*(1,1)<>0.K ex P,Q being
Matrix of n,K st P is invertible & Q is invertible & (P*A*Q)*(1,1)=1.K & (for i
st 1<i & i<=n holds (P*A*Q)*(i,1)= 0.K)& for j st 1<j & j<=n holds (P*A*Q)*(1,j
  )= 0.K;

begin :: A Transformation of Matrix to Some Canonical Form

theorem :: MATRIX14:42
  for D being non empty set,m,n,i,j being Element of NAT, A being
  Matrix of m,n,D holds Swap(A,i,j) is Matrix of m,n,D;

definition
  let K;
  let n be Element of NAT, i0 be Nat;
  func SwapDiagonal(K,n,i0) -> Matrix of n,K equals
:: MATRIX14:def 3
  Swap(1.(K,n),1,i0);
end;

theorem :: MATRIX14:43
  for n being Element of NAT,i0 being Nat,A being Matrix of n,K st
1<=i0 & i0<=n & A= SwapDiagonal(K,n,i0) holds for i,j being Nat st 1<=i & i<=n
& 1<=j & j<=n holds (i0<>1 implies (i=1 & j=i0 implies A*(i,j)=1.K)& (i=i0 & j=
1 implies A*(i,j)=1.K)& (i=1 & j=1 implies A*(i,j)=0.K)& (i=i0 & j=i0 implies A
*(i,j)=0.K)& (not ((i=1 or i=i0) &(j=1 or j=i0)) implies (i=j implies A*(i,j)=
  1.K)& (i<>j implies A*(i,j)=0.K)));

theorem :: MATRIX14:44
  for n being Element of NAT, A being Matrix of n,K for i being
  Nat st 1<=i & i<=n holds SwapDiagonal(K,n,1)*(i,i)=1.K;

theorem :: MATRIX14:45
  for n being Element of NAT, A being Matrix of n,K for i,j being
Nat st 1<=i & i<=n & 1<=j & j<=n holds (i<>j implies SwapDiagonal(K,n,1)*(i,j)=
  0.K);

theorem :: MATRIX14:46
  for K for n,i0 being Element of NAT,A being Matrix of n,K st i0
= 1 & for i,j being Nat st 1<=i & i<=n & 1<=j & j<=n holds (i=j implies A*(i,j)
  =1.K)& (i<>j implies A*(i,j)=0.K) holds A= SwapDiagonal(K,n,i0);

theorem :: MATRIX14:47
  for K for n,i0 being Element of NAT,A being Matrix of n,K st 1<=
i0 & i0<=n & i0 <> 1 & for i,j being Nat st 1<=i & i<=n & 1<=j & j<=n holds (i=
  1 & j=i0 implies A*(i,j)=1.K)& (i=i0 & j=1 implies A*(i,j)=1.K)& (i=1 & j=1
implies A*(i,j)=0.K)& (i=i0 & j=i0 implies A*(i,j)=0.K)& (not ((i=1 or i=i0) &(
  j=1 or j=i0)) implies (i=j implies A*(i,j)=1.K)& (i<>j implies A*(i,j)=0.K))
  holds A= SwapDiagonal(K,n,i0);

theorem :: MATRIX14:48
  for A being (Matrix of n,K),i0 being Element of NAT st 1<=i0 &
i0 <=n holds (for j st 1<=j & j<=n holds ((SwapDiagonal(K,n,i0))*A)*(i0,j)=A*(1
,j) & ((SwapDiagonal(K,n,i0))*A)*(1,j)=A*(i0,j))& (for i,j st i<>1 & i<>i0 & 1
  <=i & i<=n & 1<=j & j<=n holds ((SwapDiagonal(K,n,i0))*A)*(i,j)=A*(i,j));

theorem :: MATRIX14:49
  for i0 being Element of NAT st 1<=i0 & i0<=n holds SwapDiagonal(
  K,n,i0) is invertible & (SwapDiagonal(K,n,i0))~ =SwapDiagonal(K,n,i0);

theorem :: MATRIX14:50
  for i0 being Element of NAT st 1<=i0 & i0<=n holds (SwapDiagonal
  (K,n,i0))@=(SwapDiagonal(K,n,i0));

theorem :: MATRIX14:51
  for A being (Matrix of n,K),j0 being Element of NAT st 1<=j0 &
j0 <=n holds (for i st 1<=i & i<=n holds (A*(SwapDiagonal(K,n,j0)))*(i,j0)=A*(i
,1) & (A*(SwapDiagonal(K,n,j0)))*(i,1)=A*(i,j0))& (for i,j st j<>1 & j<>j0 & 1
  <=i & i<=n & 1<=j & j<=n holds (A*(SwapDiagonal(K,n,j0)))*(i,j)=A*(i,j));

theorem :: MATRIX14:52
  for A being Matrix of n,K holds A=0.(K,n) iff for i,j st 1<=i &
  i<=n & 1<=j & j<=n holds A*(i,j)= 0.K;

begin :: Left/Right Invertibility and Invertibility

theorem :: MATRIX14:53
  for A being Matrix of n,K st A<> 0.(K,n) holds ex B,C being
Matrix of n,K st B is invertible & C is invertible & (B*A*C)*(1,1) =1.K & (for
i st 1<i & i<=n holds (B*A*C)*(i,1)= 0.K)& for j st 1<j & j<=n holds (B*A*C)*(1
  ,j)= 0.K;

theorem :: MATRIX14:54
  for A,B being Matrix of n,K st B*A=1.(K,n)
    ex B2 being Matrix of n,K st A*B2=1.(K,n);

theorem :: MATRIX14:55
  for A being Matrix of n,K holds (ex B1 being Matrix of n,K st B1
  *A=1.(K,n)) iff ex B2 being Matrix of n,K st A*B2=1.(K,n);

theorem :: MATRIX14:56
  for A,B being Matrix of n,K st A*B = 1.(K,n) holds A is invertible & B
  is invertible;