:: Invertibility of Matrices of Field Elements
:: by Yatsuka Nakamura , Kunio Oniumi and Wenpai Chang
::
:: Received April 2, 2008
:: Copyright (c) 2008-2017 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*0 & a<>0.K &
P*(1,1)= a" & (for i st 1**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 10 & 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**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** 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*