:: Invertibility of Matrices of Field Elements
:: by Yatsuka Nakamura , Kunio Oniumi and Wenpai Chang
::
:: Received April 2, 2008
:: Copyright (c) 2008-2019 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;
equalities XBOOLE_0, MATRIX_0, MATRIX_1, ALGSTR_0;
theorems MATRIX_3, VECTSP_1, MATRIX_0, MATRIX_4, GROUP_1, FUNCT_1, FINSEQ_1,
NAT_1, FINSEQ_7, FINSEQ_2, TARSKI, FINSOP_1, FVSUM_1, FUNCT_2, XBOOLE_0,
ZFMISC_1, MATRIX_7, MATRIXR1, FINSEQ_3, XXREAL_0, ORDINAL1, FINSEQ_4,
MATRIXR2, XREAL_1, FUNCOP_1, RLVECT_1, MATRIX_6, MATRIX12, POLYNOM1,
PARTFUN1, NAT_D, CARD_1, MATRIX_1;
schemes NAT_1, MATRIX_0;
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
n |-> (0.K);
coherence;
end;
definition
let K be non empty ZeroStr;
let n;
redefine func 0*(K,n) -> Element of n-tuples_on (the carrier of K);
coherence;
end;
reserve L for non empty addLoopStr;
theorem Th1:
for x being FinSequence of L holds x is Element of (len x)
-tuples_on the carrier of L
proof
let x be FinSequence of L;
x is Element of (the carrier of L)* by FINSEQ_1:def 11;
then x in { s where s is Element of (the carrier of L)*: len s = len x };
hence thesis by FINSEQ_2:def 4;
end;
theorem Th2:
for x1,x2 being FinSequence of L st len x1=len x2 holds len (x1+ x2)=len x1
proof
let x1,x2 be FinSequence of L;
set n=len x1;
reconsider z1=x1 as Element of (len x1)-tuples_on (the carrier of L) by
FINSEQ_2:92;
assume len x1=len x2;
then reconsider z2=x2 as Element of n-tuples_on (the carrier of L) by
FINSEQ_2:92;
dom (z1+z2)=Seg n by FINSEQ_2:124;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th3:
for x1,x2 being FinSequence of L st len x1=len x2 holds len (x1- x2)=len x1
proof
let x1,x2 be FinSequence of L;
set n=len x1;
reconsider z1=x1 as Element of (len x1)-tuples_on (the carrier of L) by
FINSEQ_2:92;
assume len x1=len x2;
then reconsider z2=x2 as Element of n-tuples_on (the carrier of L) by
FINSEQ_2:92;
dom (z1-z2)=Seg n by FINSEQ_2:124;
hence thesis by FINSEQ_1:def 3;
end;
reserve G for non empty multLoopStr;
theorem Th4:
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)
proof
let x1,x2 be FinSequence of G,i;
assume
A1: i in dom mlt(x1,x2);
A2: mlt(x1,x2)=(the multF of G).:(x1,x2) by FVSUM_1:def 7;
A3: rng x2 c= the carrier of G by FINSEQ_1:def 4;
dom (the multF of G)=[:the carrier of G,the carrier of G:] & rng x1 c=
the carrier of G by FINSEQ_1:def 4,FUNCT_2:def 1;
then [:rng x1, rng x2:] c= dom the multF of G by A3,ZFMISC_1:96;
then
A4: dom mlt(x1,x2) = dom x1 /\ dom x2 by A2,FUNCOP_1:69;
then i in dom x2 by A1,XBOOLE_0:def 4;
then
A5: x2/.i=x2.i by PARTFUN1:def 6;
i in dom x1 by A1,A4,XBOOLE_0:def 4;
then x1/.i=x1.i by PARTFUN1:def 6;
hence mlt(x1,x2).i = (x1/.i)*(x2/.i) by A1,A5,FVSUM_1:60;
hence thesis by A1,PARTFUN1:def 6;
end;
theorem Th5:
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
proof
let x1,x2 be FinSequence of L,i be Nat;
assume that
A1: len x1=len x2 and
A2: 1<=i & i<=len x1;
reconsider x10=x1,x20=x2 as Element of (len x1)-tuples_on the carrier of L
by A1,Th1;
A3: x10/.i=x10.i & x20/.i=x20.i by A1,A2,FINSEQ_4:15;
i in Seg len x1 by A2,FINSEQ_1:1;
then i in Seg len (x1+x2) by A1,Th2;
then i in dom (x1+x2) by FINSEQ_1:def 3;
hence (x1+x2).i=x1/.i + x2/.i by A3,FVSUM_1:17;
i in Seg len x1 by A2,FINSEQ_1:1;
then i in Seg len (x1-x2) by A1,Th3;
then i in dom (x1-x2) by FINSEQ_1:def 3;
hence thesis by A3,FVSUM_1:32;
end;
theorem Th6:
for a being Element of K, x being FinSequence of K holds -a*x = (
-a)*x & -a*x = a*(-x)
proof
let a be Element of K, x be FinSequence of K;
set n=len x;
reconsider x0=x as Element of n-tuples_on (the carrier of K) by Th1;
reconsider y=a*x0 as Element of (n-tuples_on (the carrier of K));
thus -a*x=(-1_K)*y by FVSUM_1:59
.=((-1_K)*a)*x0 by FVSUM_1:54
.=(- 1_K *a)*x0 by VECTSP_1:8
.=(- a)*x;
thus -a*x= (-1_K)*y by FVSUM_1:59
.=((-1_K)*a)*x0 by FVSUM_1:54
.=a*((-1_K)*x0) by FVSUM_1:54
.=a*(-x) by FVSUM_1:59;
end;
theorem Th7:
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))
proof
let x1,x2,y1,y2 be FinSequence of G;
assume that
A1: len x1=len x2 and
A2: len y1=len y2;
A3: (the multF of G).:(x1^y1,x2^y2)=(the multF of G) * (<: x1^y1,x2^y2 :>)
by FUNCOP_1:def 3;
A4: dom (x1^y1)=Seg len (x1^y1) by FINSEQ_1:def 3;
A5: rng (x2^y2) c= the carrier of G by FINSEQ_1:def 4;
dom (the multF of G)=[:the carrier of G,the carrier of G:] & rng (x1^y1)
c= the carrier of G by FINSEQ_1:def 4,FUNCT_2:def 1;
then [:rng (x1^y1), rng (x2^y2):] c= dom (the multF of G) by A5,ZFMISC_1:96;
then
A6: dom ((the multF of G) * (<: x1^y1,x2^y2 :>)) =dom (x1^y1) /\ dom (x2^y2)
by A3,FUNCOP_1:69;
A7: len (x2^y2)=len x2+len y2 by FINSEQ_1:22;
dom (x2^y2)=Seg len (x2^y2) by FINSEQ_1:def 3;
then dom (x1^y1)=dom (x2^y2) by A1,A2,A7,A4,FINSEQ_1:22;
then
A8: dom (mlt(x1^y1,x2^y2))= dom (x1^y1) by A3,A6,FVSUM_1:def 7;
A9: (the multF of G).:(y1,y2)=(the multF of G) * (<:y1,y2:>) by FUNCOP_1:def 3;
A10: dom (the multF of G)=[:the carrier of G,the carrier of G:] by
FUNCT_2:def 1;
rng y1 c= the carrier of G & rng y2 c= the carrier of G by FINSEQ_1:def 4;
then [:rng y1, rng y2:] c= dom the multF of G by A10,ZFMISC_1:96;
then
A11: dom ((the multF of G) * (<:y1,y2:>)) =dom y1 /\ dom y2 by A9,FUNCOP_1:69;
dom y2=Seg len y1 by A2,FINSEQ_1:def 3
.=dom y1 by FINSEQ_1:def 3;
then
A12: dom mlt(y1,y2) =dom y1 by A9,A11,FVSUM_1:def 7;
then dom (mlt(y1,y2))=Seg len y1 by FINSEQ_1:def 3;
then
A13: len (mlt(y1,y2))= len y1 by FINSEQ_1:def 3;
A14: (the multF of G).:(x1,x2)=(the multF of G) * (<:x1,x2:>) by FUNCOP_1:def 3
;
rng (x1) c= the carrier of G & rng (x2) c= the carrier of G by FINSEQ_1:def 4
;
then [:rng (x1), rng (x2):] c= dom (the multF of G) by A10,ZFMISC_1:96;
then
A15: dom ((the multF of G) * (<:x1,x2:>)) =dom (x1) /\ dom (x2) by A14,
FUNCOP_1:69;
A16: len (x1^y1)=len x1+len y1 by FINSEQ_1:22;
dom x2=Seg len x1 by A1,FINSEQ_1:def 3
.=dom x1 by FINSEQ_1:def 3;
then
A17: dom (mlt(x1,x2)) =dom x1 by A14,A15,FVSUM_1:def 7;
then
A18: dom (mlt(x1,x2))=Seg len x1 by FINSEQ_1:def 3;
A19: for i being Nat st 1<=i & i<=len (mlt(x1^y1,x2^y2)) holds (mlt(x1^y1,x2
^y2)).i=((mlt(x1,x2))^(mlt(y1,y2))).i
proof
let i be Nat;
assume that
A20: 1<=i and
A21: i<=len (mlt(x1^y1,x2^y2));
i in Seg len (mlt(x1^y1,x2^y2)) by A20,A21,FINSEQ_1:1;
then
A22: i in dom (mlt(x1^y1,x2^y2)) by FINSEQ_1:def 3;
then i<=len (x1^y1) by A4,A8,FINSEQ_1:1;
then
A23: (x1^y1)/.i= (x1^y1).i by A20,FINSEQ_4:15;
i<=len (x2^y2) by A1,A2,A16,A7,A4,A8,A22,FINSEQ_1:1;
then
A24: (x2^y2)/.i= (x2^y2).i by A20,FINSEQ_4:15;
A25: i<=len x1+len y1 by A16,A4,A8,A22,FINSEQ_1:1;
now
per cases;
suppose
A26: i<=len x1;
then
A27: i in Seg len x1 by A20,FINSEQ_1:1;
then
A28: i in dom x1 by FINSEQ_1:def 3;
i in dom x2 by A1,A27,FINSEQ_1:def 3;
then
A29: (x2^y2).i=x2.i by FINSEQ_1:def 7;
A30: i in dom (mlt(x1,x2)) by A17,A27,FINSEQ_1:def 3;
then
A31: ((mlt(x1,x2))^(mlt(y1,y2))).i =(mlt(x1,x2)).i by FINSEQ_1:def 7
.=(x1/.i)*(x2/.i) by A30,Th4;
x1/.i=x1.i & x2/.i=x2.i by A1,A20,A26,FINSEQ_4:15;
hence ((x1^y1)/.i)*((x2^y2)/.i)=((mlt(x1,x2))^(mlt(y1,y2))).i by A23
,A24,A28,A29,A31,FINSEQ_1:def 7;
end;
suppose
A32: i>len x1;
i<=len (x2^y2) by A1,A2,A16,A7,A4,A8,A22,FINSEQ_1:1;
then
A33: (x2^y2)/.i= (x2^y2).i by A20,FINSEQ_4:15;
i<=len (x1^y1) by A4,A8,A22,FINSEQ_1:1;
then
A34: (x1^y1)/.i= (x1^y1).i by A20,FINSEQ_4:15;
set k=i -' len x1;
A35: k=i-len x1 by A32,XREAL_1:233;
then
A36: i= len x1 +k;
i-len x1 <=len x1 + len y1 - len x1 by A25,XREAL_1:13;
then
A37: k<=len y1 by A32,XREAL_1:233;
k>0 by A32,A35,XREAL_1:50;
then
A38: 0+1<=k by NAT_1:13;
then
A39: k in Seg len y1 by A37,FINSEQ_1:1;
then
A40: k in dom (mlt(y1,y2)) by A12,FINSEQ_1:def 3;
i=len (mlt(x1,x2)) +k by A18,A36,FINSEQ_1:def 3;
then
A41: ((mlt(x1,x2))^(mlt(y1,y2))).i =(mlt(y1,y2)).k by A40,FINSEQ_1:def 7
.=(y1/.k)*(y2/.k) by A40,Th4;
k in dom y1 by A39,FINSEQ_1:def 3;
then
A42: (x1^y1).i=y1.k by A36,FINSEQ_1:def 7;
k in Seg len y1 by A38,A37,FINSEQ_1:1;
then
A43: k in dom y2 by A2,FINSEQ_1:def 3;
y1/.k=y1.k & y2/.k=y2.k by A2,A38,A37,FINSEQ_4:15;
hence
((x1^y1)/.i)*((x2^y2)/.i)=((mlt(x1,x2))^(mlt(y1,y2))).i by A1,A36,A43
,A42,A34,A33,A41,FINSEQ_1:def 7;
end;
end;
hence thesis by A22,Th4;
end;
len (mlt(x1^y1,x2^y2))=len (x1^y1) by A4,A8,FINSEQ_1:def 3
.=len x1 + len y1 by FINSEQ_1:22;
then len (mlt(x1^y1,x2^y2)) =len (mlt(x1,x2))+ len(mlt(y1,y2)) by A18,A13,
FINSEQ_1:def 3;
then len (mlt(x1^y1,x2^y2))=len ((mlt(x1,x2))^(mlt(y1,y2))) by FINSEQ_1:22;
hence thesis by A19,FINSEQ_1:14;
end;
notation
let K;
let e1,e2 be FinSequence of K;
synonym |( e1,e2 )| for e1 "*" e2;
end;
theorem Th8:
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))
proof
let x,y be FinSequence of K,a be Element of K;
assume len x=len y;
then reconsider y0=y as Element of (len x)-tuples_on (the carrier of K) by
Th1;
reconsider x0=x as Element of (len x)-tuples_on (the carrier of K) by Th1;
thus mlt(a*x,y)=a*(mlt(x0,y0)) by FVSUM_1:69
.=a*(mlt(x,y));
thus mlt(x,a*y)=a*(mlt(x0,y0)) by FVSUM_1:69
.=a*(mlt(x,y));
end;
theorem
for x,y being FinSequence of K,a being Element of K st len x=len y
holds |(a*x,y)| = a*|(x,y)|
proof
let x,y be FinSequence of K,a be Element of K;
assume len x=len y;
then Sum mlt(a*x,y) = Sum (a*(mlt(x,y))) by Th8;
then Sum mlt(a*x,y) =a*(Sum mlt(x,y)) by FVSUM_1:73;
then Sum mlt(a*x,y) =a*|(x,y)| by FVSUM_1:def 9;
hence thesis by FVSUM_1:def 9;
end;
theorem Th10:
for x,y being FinSequence of K,a being Element of K st len x=len
y holds |(x,a*y)| = a*|(x,y)|
proof
let x,y be FinSequence of K,a be Element of K;
assume len x=len y;
then Sum mlt(x,a*y) =(Sum (a*(mlt(x,y)))) by Th8;
then Sum mlt(x,a*y) =a*(Sum mlt(x,y)) by FVSUM_1:73;
then Sum mlt(x,a*y) =a*|(x,y)| by FVSUM_1:def 9;
hence thesis by FVSUM_1:def 9;
end;
theorem Th11:
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)|
proof
let x,y1,y2 be FinSequence of K,a be Element of K;
reconsider x0=x as Element of (len x)-tuples_on (the carrier of K) by Th1;
assume
A1: len x=len y1 & len x=len y2;
then reconsider
y10=y1,y20=y2 as Element of (len x)-tuples_on (the carrier of K)
by Th1;
Sum mlt(x,y1+y2) = Sum (mlt(x0,y10) + mlt(x0,y20)) by A1,MATRIX_4:57;
then Sum mlt(x,y1+y2) = Sum mlt(x0,y10) + Sum mlt(x0,y20) by FVSUM_1:76;
then Sum mlt(x,y1+y2) = Sum mlt(x,y1) + |(x,y2)| by FVSUM_1:def 9;
then Sum mlt(x,y1+y2) = |(x,y1)| + |(x,y2)| by FVSUM_1:def 9;
hence thesis by FVSUM_1:def 9;
end;
theorem Th12:
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)|
proof
let x1,x2,y1,y2 be FinSequence of K;
A1: Sum ((mlt(x1,x2))^(mlt(y1,y2)))=Sum mlt(x1,x2) + Sum mlt(y1,y2) by
RLVECT_1:41;
assume len x1=len x2 & len y1=len y2;
then Sum mlt(x1^y1,x2^y2) = Sum mlt(x1,x2) + Sum mlt(y1,y2) by A1,Th7;
then |( x1^y1, x2^y2 )| = Sum mlt(x1,x2) + Sum mlt(y1,y2) by FVSUM_1:def 9;
then |( x1^y1, x2^y2 )| = Sum mlt(x1,x2) + |(y1,y2)| by FVSUM_1:def 9;
hence thesis by FVSUM_1:def 9;
end;
theorem Th13:
for p1 being Element of n-tuples_on the carrier of K holds mlt(
p1,(n |-> (0.K)))=n |-> (0.K)
proof
let p1 be Element of n-tuples_on (the carrier of K);
thus mlt(p1,(n |-> (0.K)))= mlt(p1,(0.K)*(0*(K,n))) by FVSUM_1:58
.= (0.K)*(mlt(p1,0*(K,n))) by FVSUM_1:69
.= n |-> (0.K) by FVSUM_1:58;
end;
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 Th14:
1.(K,0)=0.(K,0) & 1.(K,0)={}
proof
A1: len 1.(K,0) = 0 by MATRIX_0:24;
hence 1.(K,0)=0.(K,0);
thus thesis by A1;
end;
theorem Th15:
for A being Matrix of 0,K holds A={} & A=1.(K,0) & A=0.(K,0)
proof
let A be Matrix of 0,K;
A1: len A=0 by MATRIX_0:24;
hence A={};
hence A=1.(K,0) by Th14;
thus thesis by A1;
end;
theorem
for A being Matrix of 0,K holds A is invertible
proof
let A be Matrix of 0,K;
A*A= 1.(K,0) by Th15;
then A is_reverse_of A by MATRIX_6:def 2;
hence thesis by MATRIX_6:def 3;
end;
theorem Th17:
for A,B,C being Matrix of n,K holds A*B*C=A*(B*C)
proof
let A,B,C be Matrix of n,K;
A1: width B=n & len C =n by MATRIX_0:24;
width A=n & len B=n by MATRIX_0:24;
hence thesis by A1,MATRIX_3:33;
end;
theorem Th18:
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)
proof
let A,B be Matrix of n,K;
hereby
assume A is invertible & B=A~;
then B is_reverse_of A by MATRIX_6:def 4;
hence B*A=1.(K,n) & A*B=1.(K,n) by MATRIX_6:def 2;
end;
hereby
assume B*A=1.(K,n) & A*B=1.(K,n);
then
A1: B is_reverse_of A by MATRIX_6:def 2;
hence A is invertible by MATRIX_6:def 3;
hence B=A~ by A1,MATRIX_6:def 4;
end;
end;
theorem Th19:
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)
proof
let A be Matrix of n,K;
thus A is invertible implies ex B being Matrix of n,K st B*A=1.(K,n) & A*B=
1.(K,n)
proof
assume A is invertible;
then (A~)*A=1.(K,n) & A*(A~)=1.(K,n) by Th18;
hence thesis;
end;
thus thesis by Th18;
end;
theorem Th20:
for x being FinSequence of K holds |(x, 0*(K,len x))| = 0.K
proof
let x be FinSequence of K;
set n=len x;
reconsider p1=x as Element of n-tuples_on (the carrier of K) by FINSEQ_2:92;
|(x, 0*(K,n))| = Sum mlt(p1,0*(K,n)) by FVSUM_1:def 9
.= Sum 0*(K,n) by Th13
.= 0.K by MATRIX_3:11;
hence thesis;
end;
theorem Th21:
for x being FinSequence of K holds |(0*(K,len x),x)| = 0.K
proof
let x be FinSequence of K;
thus |(0*(K,len x),x)| = |(x,0*(K,len x))| by FVSUM_1:90
.= 0.K by Th20;
end;
theorem Th22:
for a being Element of K holds |( <* 0.K *>, <* a *> )|=0.K
proof
let a be Element of K;
A1: len (<* a *>) =1 by FINSEQ_1:39;
thus |( <* 0.K *>, <* a *> )| =|( 0*(K,1),<* a *> )| by FINSEQ_2:59
.= 0.K by A1,Th21;
end;
definition
let K;
let n,i be Nat;
func Base_FinSeq(K,n,i) -> FinSequence of K equals
Replace((n |-> 0.K),i,1.K);
coherence;
end;
theorem Th23:
for n, i being Nat holds len Base_FinSeq(K,n,i)=n
proof
let n, i be Nat;
len (Replace((n |-> (0.K)),i,1.K)) = len (n |-> (0.K)) by FINSEQ_7:5
.= n by CARD_1:def 7;
hence thesis;
end;
theorem Th24:
for i, n being Nat st 1<=i & i<=n holds (Base_FinSeq(K,n,i)).i= 1.K
proof
let i, n be Nat;
assume
A1: 1<=i & i<=n;
A2: len (n |-> (0.K))=n by CARD_1:def 7;
len (Replace((n |-> (0.K)),i,1.K)) = len (n |-> 0.K) by FINSEQ_7:5
.= n by CARD_1:def 7;
hence (Base_FinSeq(K,n,i)).i = (Replace((n |-> (0.K)),i,1.K))/.i by A1,
FINSEQ_4:15
.= 1.K by A1,A2,FINSEQ_7:8;
end;
theorem Th25:
for i,j,n be Nat st 1<=j & j<=n & i<>j holds (Base_FinSeq(K,n,i) ).j=0.K
proof
let i,j,n be Nat;
assume that
A1: 1<=j & j<=n and
A2: i<>j;
A3: j in Seg n by A1,FINSEQ_1:1;
A4: len (n |-> (0.K))=n by CARD_1:def 7;
len (Replace((n |-> (0.K)),i,(1.K))) = len (n |-> (0.K)) by FINSEQ_7:5
.= n by CARD_1:def 7;
hence (Base_FinSeq(K,n,i)).j = (Replace((n |-> (0.K)),i,(1.K)))/.j by A1,
FINSEQ_4:15
.= ((n |-> (0.K)))/.j by A1,A2,A4,FINSEQ_7:10
.=((n |-> (0.K))).j by A1,A4,FINSEQ_4:15
.= 0.K by A3,FINSEQ_2:57;
end;
theorem Th26:
for i,n being Nat st 1<=i & i<=n holds (1.(K,n)).i=Base_FinSeq(K ,n,i)
proof
let i,n be Nat;
assume
A1: 1<=i & i<=n;
then 1<=n by XXREAL_0:2;
then [i,1] in Indices (1.(K,n)) by A1,MATRIX_0:31;
then consider q being FinSequence of K such that
A2: q = (1.(K,n)).i and
(1.(K,n))*(i,1) = q.1 by MATRIX_0:def 5;
len (1.(K,n))=n by MATRIX_0:24;
then i in dom (1.(K,n)) by A1,FINSEQ_3:25;
then q in rng (1.(K,n)) by A2,FUNCT_1:def 3;
then
A3: len q=n by MATRIX_0:def 2;
A4: for j be Nat st 1<=j & j<=n holds q.j=(Base_FinSeq(K,n,i)).j
proof
let j be Nat;
assume
A5: 1<=j & j<=n;
then
A6: [i,j] in Indices (1.(K,n)) by A1,MATRIX_0:31;
then
A7: ex q0 being FinSequence of K st q0 = (1.(K,n)).i & (1.(K, n))*(i,j) =
q0.j by MATRIX_0:def 5;
per cases;
suppose
A8: i=j;
then (1.(K,n))*(i,i) = 1_(K) by A6,MATRIX_1:def 3;
hence thesis by A1,A2,A7,A8,Th24;
end;
suppose
A9: i<>j;
then q.j=0.K by A2,A6,A7,MATRIX_1:def 3;
hence thesis by A5,A9,Th25;
end;
end;
len Base_FinSeq(K,n,i)=n by Th23;
hence thesis by A2,A3,A4,FINSEQ_1:14;
end;
theorem Th27:
for i,j st 1<=i & i<=n & 1<=j & j<=n holds (1.(K,n))*(i,j)=(
Base_FinSeq(K,n,i)).j
proof
let i,j;
assume that
A1: 1<=i & i<=n and
A2: 1<=j & j<=n;
[i,j] in Indices (1.(K,n)) by A1,A2,MATRIX_0:31;
then
ex p3 being FinSequence of K st p3 = (1.(K,n)).i & 1.(K,n)*(i,j) = p3.j
by MATRIX_0:def 5;
hence thesis by A1,Th26;
end;
theorem
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
proof
let A be Matrix of n,K;
thus A=0.(K,n) implies for i,j being Element of NAT st 1<=i & i<=n & 1<=j &
j<=n holds A*(i,j)=0.K
proof
set A2=0.(K,n),B2=0.(K,n);
set A3=0.(K,n,n);
assume
A1: A=0.(K,n);
let i,j be Element of NAT;
assume 1<=i & i<=n & 1<=j & j<=n;
then [i,j] in Indices A2 by MATRIX_0:31;
then A3=A2 & (A2+B2)*(i,j)=A2*(i,j)+B2*(i,j) by MATRIX_3:def 1,def 3;
then A2*(i,j)=A2*(i,j)+A2*(i,j) by MATRIX_3:4;
then A2*(i,j) - A2*(i,j) = A2*(i,j) +(A2*(i,j) - A2*(i,j)) by RLVECT_1:28
.=A2*(i,j) +0.K by RLVECT_1:15
.=A2*(i,j) by RLVECT_1:4;
hence thesis by A1,RLVECT_1:15;
end;
A2: len A=n by MATRIX_0:24;
A3: Indices A=[: Seg n,Seg n :] by MATRIX_0:24;
A4: width A=n by MATRIX_0:24;
assume
A5: for i,j being Element of NAT st 1<=i & i<=n & 1<=j & j<=n holds A*(i
,j)=0.K;
for i,j being Nat st [i,j] in Indices A holds A*(i,j) = A*(i,j) + A*(i, j)
proof
let i,j be Nat;
reconsider i0=i,j0=j as Element of NAT by ORDINAL1:def 12;
assume
A6: [i,j] in Indices A;
then j in Seg n by A4,ZFMISC_1:87;
then
A7: 1<=j & j<=n by FINSEQ_1:1;
i in Seg n by A3,A6,ZFMISC_1:87;
then 1<=i & i<=n by FINSEQ_1:1;
then A*(i0,j0)=0.K by A5,A7;
hence thesis by RLVECT_1:4;
end;
then A=A+A by A2,MATRIX_3:def 3;
then A = 0.(K,len A,width A) by MATRIX_4:6;
hence thesis by A2,A4,MATRIX_3:def 1;
end;
theorem Th29:
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)
proof
let A be Matrix of n,K;
A1: Indices A=[: Seg n,Seg n :] by MATRIX_0:24;
thus A=1.(K,n) implies 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)
proof
assume
A2: A=1.(K,n);
let i,j be Nat;
assume 1<=i & i<=n & 1<=j & j<=n;
then
A3: [i,j] in Indices A by MATRIX_0:31;
per cases;
suppose
A4: i=j;
then A*(i,j)=1.K by A2,A3,MATRIX_1:def 3;
hence thesis by A4,FUNCOP_1:def 8;
end;
suppose
A5: i<>j;
then A*(i,j)=0.K by A2,A3,MATRIX_1:def 3;
hence thesis by A5,FUNCOP_1:def 8;
end;
end;
A6: len (1.(K,n))=n & width (1.(K,n))=n by MATRIX_0:24;
A7: Indices (1.(K,n))=[: Seg n,Seg n :] by MATRIX_0:24;
A8: width A=n by MATRIX_0:24;
thus (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)) implies A=1.(K,n)
proof
assume
A9: 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);
A10: for i,j being Nat st [i,j] in Indices A holds A*(i,j) = (1.(K,n))*(i, j)
proof
let i,j be Nat;
reconsider i0=i,j0=j as Element of NAT by ORDINAL1:def 12;
assume
A11: [i,j] in Indices A;
then j in Seg n by A8,ZFMISC_1:87;
then
A12: 1<=j & j<=n by FINSEQ_1:1;
i in Seg n by A1,A11,ZFMISC_1:87;
then 1<=i & i<=n by FINSEQ_1:1;
then
A13: A*(i0,j0)=IFEQ(i0,j0,1.K,0.K) by A9,A12;
per cases;
suppose
A14: i0=j0;
then A*(i0,j0)=1_K by A13,FUNCOP_1:def 8;
hence thesis by A1,A7,A11,A14,MATRIX_1:def 3;
end;
suppose
A15: i0<>j0;
then A*(i0,j0)=0.K by A13,FUNCOP_1:def 8;
hence thesis by A1,A7,A11,A15,MATRIX_1:def 3;
end;
end;
len A = len (1.(K,n)) & width A = width (1.(K,n)) by A6,MATRIX_0:24;
hence thesis by A10,MATRIX_0:21;
end;
end;
begin :: Conditions of Invertibility
theorem Th30:
for A,B being Matrix of n,K holds (A*B)@=(B@)*(A@)
proof
let A,B be Matrix of n,K;
per cases;
suppose
A1: n<>0;
A2: width B=n by MATRIX_0:24;
len B=n & width A=n by MATRIX_0:24;
hence thesis by A1,A2,MATRIX_3:22;
end;
suppose
A3: n=0;
hence (A*B)@=1.(K,n) by Th15
.=(B@)*(A@) by A3,Th15;
end;
end;
theorem
for A being Matrix of n,K st A is invertible holds A@ is
invertible & (A@)~ =(A~)@
proof
let A be Matrix of n,K;
assume A is invertible;
then consider B being Matrix of n,K such that
A1: B*A=1.(K,n) and
A2: A*B=1.(K,n) by Th19;
(A*B)@ = (B@)*(A@) by Th30;
then
A3: (B@)*(A@)=1.(K,n) by A2,MATRIX_6:10;
(B*A)@ = (A@)*(B@) by Th30;
then
A4: (A@)*(B@)=1.(K,n) by A1,MATRIX_6:10;
B=A~ by A1,A2,Th18;
hence thesis by A3,A4,Th18;
end;
theorem Th32:
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
proof
let x be FinSequence of K, a be Element of K;
given i such that
A1: 1<=i and
A2: i<=len x and
A3: x.i=a and
A4: for j st j<>i & 1<=j & j<=len x holds x.j=0.K;
1<=len x by A1,A2,XXREAL_0:2;
then consider f being sequence of (the carrier of K) such that
A5: f.1 = x.1 and
A6: for n being Nat st 0 <> n & n < len x
holds f.(n + 1) = (the addF of K).(f.n,x.(n + 1)) and
A7: (the addF of K) "**" x = f.(len x) by FINSOP_1:def 1;
A8: for j being Nat st 1<=j & j*k;
A14: 1<=1+k by NAT_1:12;
1>=k+1 by A13,NAT_1:13;
then
A15: k+1=1 by A14,XXREAL_0:1;
now
per cases;
suppose
k+1**=i;
hence thesis;
end;
end;
hence thesis;
end;
suppose
k>=i;
hence thesis by NAT_1:12;
end;
end;
hence thesis;
end;
suppose
A16: 1<=k & k**i & 1<=j & j<=m
holds y.j= 0.K
proof
let x,y be FinSequence of K,i;
assume that
A1: len x=m and
A2: y=mlt (x,Base_FinSeq(K,m,i)) and
A3: 1<=i and
A4: i<=m;
A5: i in dom x by A1,A3,A4,FINSEQ_3:25;
i<=len (Base_FinSeq(K,m,i)) by A4,Th23;
then
A6: (Base_FinSeq(K,m,i))/.i=(Base_FinSeq(K,m,i)).i by A3,FINSEQ_4:15;
A7: rng (Base_FinSeq(K,m,i)) c= the carrier of K by FINSEQ_1:def 4;
A8: len (Base_FinSeq(K,m,i))=m by Th23;
dom (the multF of K)=[:the carrier of K,the carrier of K:] & rng (x) c=
the carrier of K by FINSEQ_1:def 4,FUNCT_2:def 1;
then [:rng (x), rng (Base_FinSeq(K,m,i)):] c= dom (the multF of K) by A7,
ZFMISC_1:96;
then dom ((the multF of K).:(x,Base_FinSeq(K,m,i))) =dom x /\ dom (
Base_FinSeq(K,m,i)) by FUNCOP_1:69;
then
A9: dom (mlt (x,Base_FinSeq(K,m,i)))= dom x /\ dom (Base_FinSeq(K,m,i)) by
FVSUM_1:def 7
.= Seg m /\ dom (Base_FinSeq(K,m,i)) by A1,FINSEQ_1:def 3
.= Seg m /\ Seg m by A8,FINSEQ_1:def 3
.= Seg m;
then i in dom (mlt (x,Base_FinSeq(K,m,i))) by A3,A4,FINSEQ_1:1;
then (mlt (x,Base_FinSeq(K,m,i))).i=(x/.i)*((Base_FinSeq(K,m,i))/.i) by Th4
.= (x/.i)* 1.K by A3,A4,A6,Th24
.= x/.i
.= x.i by A5,PARTFUN1:def 6;
hence y.i=x.i by A2;
let j;
assume that
A10: j<>i and
A11: 1<=j and
A12: j<=m;
j<=len (Base_FinSeq(K,m,i)) by A12,Th23;
then
A13: (Base_FinSeq(K,m,i))/.j = (Base_FinSeq(K,m,i)).j by A11,FINSEQ_4:15
.= 0.K by A10,A11,A12,Th25;
j in dom (mlt (x,Base_FinSeq(K,m,i))) by A9,A11,A12,FINSEQ_1:1;
then (mlt (x,Base_FinSeq(K,m,i))).j = (x/.j)*((Base_FinSeq(K,m,i))/.j) by Th4
.= 0.K by A13;
hence thesis by A2;
end;
theorem Th35:
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
proof
let x be FinSequence of K;
assume that
A1: len x=m and
A2: 1<=i & i<=m;
A3: for j st j<>i & 1<=j & j<=m holds (mlt (x,Base_FinSeq(K,m,i))).j= 0.K
by A1,A2,Th34;
A4: len (Base_FinSeq(K,m,i))=m by Th23;
A5: rng (Base_FinSeq(K,m,i)) c= the carrier of K by FINSEQ_1:def 4;
dom (the multF of K)=[:the carrier of K,the carrier of K:] & rng (x) c=
the carrier of K by FINSEQ_1:def 4,FUNCT_2:def 1;
then [:rng (x), rng (Base_FinSeq(K,m,i)):] c= dom (the multF of K) by A5,
ZFMISC_1:96;
then dom ((the multF of K).:(x,Base_FinSeq(K,m,i))) =dom x /\ dom (
Base_FinSeq(K,m,i)) by FUNCOP_1:69;
then dom (mlt (x,Base_FinSeq(K,m,i)))= dom x /\ dom (Base_FinSeq(K,m,i)) by
FVSUM_1:def 7
.= Seg m /\ dom (Base_FinSeq(K,m,i)) by A1,FINSEQ_1:def 3
.= Seg m /\ Seg m by A4,FINSEQ_1:def 3
.= Seg m;
then
A6: len (mlt (x,Base_FinSeq(K,m,i)))=m by FINSEQ_1:def 3;
A7: x/.i=x.i by A1,A2,FINSEQ_4:15;
then (mlt(x,Base_FinSeq(K,m,i))).i=x/.i by A1,A2,Th34;
then
A8: Sum (mlt (x,Base_FinSeq(K,m,i)))=x.i by A2,A7,A6,A3,Th32;
hence |( x,Base_FinSeq(K,m,i) )|=x.i by FVSUM_1:def 9;
x.i=x/.i by A1,A2,FINSEQ_4:15;
hence thesis by A8,FVSUM_1:def 9;
end;
theorem Th36:
for m,i st 1<=i & i<=m holds |( Base_FinSeq(K,m,i),Base_FinSeq(K
,m,i) )|= 1.K
proof
let m,i;
assume
A1: 1<=i & i<=m;
len (Base_FinSeq(K,m,i))=m by Th23;
hence
|( Base_FinSeq(K,m,i),Base_FinSeq(K,m,i) )| = (Base_FinSeq(K,m,i)).i by A1
,Th35
.=1.K by A1,Th24;
end;
theorem Th37:
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 and
A2: a<>0.K and
A3: P*(1,1)= a" and
A4: for i st 1**1;
then 11;
thus ((a")*(Base_FinSeq(K,n,1))).k = (a")*((Base_FinSeq(K,n,1))/.k) by
A24,A21,FVSUM_1:50
.= (a")*(0.K) by A14,A15,A21,A26,Th25
.= 0.K;
end;
1<=n by A14,A15,XXREAL_0:2;
then 1 in dom P by A10,FINSEQ_3:25;
hence thesis by A3,A25,A22,A18,MATRIX_0:def 8;
end;
A27: 0+1<=n by A1,NAT_1:13;
A28: len Q=n by MATRIX_0:24;
then
A29: 1 in Seg len Q by A27,FINSEQ_1:1;
then
A30: 1 in dom Q by FINSEQ_1:def 3;
A31: width Q=n by MATRIX_0:24;
then
A32: len (Line(Q,1))=n by MATRIX_0:def 7;
then
A33: 1 in dom (Line(Q,1)) by A28,A29,FINSEQ_1:def 3;
A34: for j st 1 j;
len (Base_FinSeq(K,n,1))=n by Th23;
then ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by A49,A50,
FINSEQ_4:15;
then
A62: (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))).k =(-(a")*(Q*(1,j)))*
(0.K) by A50,A54,A58,Th25
.= 0.K;
A63: (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-(a")*(Q*(1,j))*
(Base_FinSeq(K,n,1))).k by A38,A49,A50,FINSEQ_4:15;
A64: p.k= 0.K by A36,A37,A60,A61,Th25;
(Base_FinSeq(K,n,j))/.k = (Base_FinSeq(K,n,j)).k by A45,A49,A50,
FINSEQ_4:15
.= 0.K by A49,A50,A61,Th25;
then q.k= 0.K + 0.K by A38,A45,A49,A50,A63,A62,Th5;
hence thesis by A64,RLVECT_1:4;
end;
suppose
A65: k=j;
then
A66: p.k=1.K by A49,A50,A60,Th24;
A67: (-(a")*(Q*(1,k))*(Base_FinSeq(K,n,1)))/.k =(-(a")*(Q*(1,k))*
(Base_FinSeq(K,n,1))).k by A38,A49,A50,A65,FINSEQ_4:15;
len (Base_FinSeq(K,n,1))=n by Th23;
then ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by A49,A50,
FINSEQ_4:15;
then
A68: (-(a")*(Q*(1,k))*(Base_FinSeq(K,n,1))).k =(-(a")*(Q*(1,k)))*
(0.K) by A50,A54,A58,A65,Th25
.= 0.K;
(Base_FinSeq(K,n,k))/.k = (Base_FinSeq(K,n,k)).k by A45,A49,A50,A65
,FINSEQ_4:15
.= 1.K by A36,A37,A65,Th24;
then q.k= 0.K + 1.K by A38,A45,A49,A50,A65,A67,A68,Th5;
hence thesis by A66,RLVECT_1:4;
end;
end;
hence thesis;
end;
end;
len (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))+Base_FinSeq(K,n,j)) =n by A38,A45
,Th2;
then
A69: Col(P,j)=-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))+Base_FinSeq(K,n,j) by A44
,A47,FINSEQ_1:14;
[1,j] in Indices (Q*P) by A27,A36,A37,MATRIX_0:31;
then (Q*P)*(1,j)= |( Line(Q,1), Col(P,j) )| by A10,A31,MATRIX_3:def 4
.= |( Line(Q,1), -(a")*(Q*(1,j))*(Base_FinSeq(K,n,1)) )| +|( Line(Q,1)
, Base_FinSeq(K,n,j) )| by A32,A38,A45,A69,Th11
.= |( Line(Q,1), (-(a")*(Q*(1,j)))*(Base_FinSeq(K,n,1)) )| +|( Line(Q,
1), Base_FinSeq(K,n,j) )| by Th6
.=(-(a")*(Q*(1,j)))* |( Line(Q,1), (Base_FinSeq(K,n,1)) )| +|( Line(Q,
1), Base_FinSeq(K,n,j) )| by A32,A9,Th10
.=(-(a")*(Q*(1,j)))* a +|( Line(Q,1), Base_FinSeq(K,n,j) )| by A32,A27
,A43,Th35
.= -((a")*(Q*(1,j)))* a +|( Line(Q,1), Base_FinSeq(K,n,j) )| by
VECTSP_1:9
.= -((Q*(1,j))*((a")* a)) +|( Line(Q,1), Base_FinSeq(K,n,j) )| by
GROUP_1:def 3
.= -((Q*(1,j))*(1.K)) +|( Line(Q,1), Base_FinSeq(K,n,j) )| by A2,
VECTSP_1:def 10
.= -((Q*(1,j))*(1.K)) + ( Line(Q,1))/.j by A32,A36,A37,Th35
.= -(Q*(1,j)) + ( Line(Q,1))/.j
.= -(Q*(1,j)) + Q*(1,j) by A31,A39,A42,MATRIX_0:def 7
.= 0.K by RLVECT_1:5;
hence thesis;
end;
A70: 1 in Seg width Q by A31,A27,FINSEQ_1:1;
A71: for i,j st 1** j;
len (Base_FinSeq(K,n,1))=n by Th23;
then ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by A88,A89,
FINSEQ_4:15;
then
A101: (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))).k =(-(a")*(Q*(1,j)))*
(0.K) by A89,A93,A97,Th25
.= 0.K;
A102: (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-(a")*(Q*(1,j))*
(Base_FinSeq(K,n,1))).k by A75,A88,A89,FINSEQ_4:15;
A103: p.k= 0.K by A72,A73,A74,A99,A100,Th25;
(Base_FinSeq(K,n,j))/.k = (Base_FinSeq(K,n,j)).k by A84,A88,A89,
FINSEQ_4:15
.= 0.K by A88,A89,A100,Th25;
then q.k= 0.K + 0.K by A75,A84,A88,A89,A102,A101,Th5;
hence thesis by A103,RLVECT_1:4;
end;
suppose
A104: k=j;
len (Base_FinSeq(K,n,1))=n by Th23;
then ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by A88,A89,
FINSEQ_4:15;
then
A105: (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))).k =(-(a")*(Q*(1,j)))*
(0.K) by A89,A93,A97,Th25
.= 0.K;
A106: (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-(a")*(Q*(1,j))*
(Base_FinSeq(K,n,1))).k by A75,A88,A89,FINSEQ_4:15;
A107: p.k=1.K by A88,A89,A99,A104,Th24;
(Base_FinSeq(K,n,j))/.k = (Base_FinSeq(K,n,j)).k by A84,A88,A89,
FINSEQ_4:15
.= 1.K by A88,A89,A104,Th24;
then q.k= 0.K + 1.K by A75,A84,A88,A89,A106,A105,Th5;
hence thesis by A107,RLVECT_1:4;
end;
end;
hence thesis;
end;
end;
len (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))+Base_FinSeq(K,n,j)) =n by A75,A84
,Th2;
then
A108: Col(P,j)=-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))+Base_FinSeq(K,n,j) by A83
,A86,FINSEQ_1:14;
A109: len Line(Q,i)=n by A31,MATRIX_0:def 7;
then
A110: (Line(Q,i))/.1 = (Line(Q,i)).1 by A27,FINSEQ_4:15
.= Q*(i,1) by A70,MATRIX_0:def 7;
A111: (Line(Q,i))/.j = (Line(Q,i)).j by A72,A73,A74,A109,FINSEQ_4:15
.= Q*(i,j) by A82,A81,MATRIX_0:def 7;
[i,j] in Indices (Q*P) by A72,A73,A74,MATRIX_0:31;
then
A112: (Q*P)*(i,j)= |( Line(Q,i), Col(P,j) )| by A10,A81,MATRIX_3:def 4
.= |( Line(Q,i), -(a")*(Q*(1,j))*(Base_FinSeq(K,n,1)) )| +|( Line(Q,i)
, Base_FinSeq(K,n,j) )| by A75,A84,A108,A109,Th11
.= |( Line(Q,i), (-(a")*(Q*(1,j)))*(Base_FinSeq(K,n,1)) )| +|( Line(Q,
i), Base_FinSeq(K,n,j) )| by Th6
.=(-(a")*(Q*(1,j)))* |( Line(Q,i), (Base_FinSeq(K,n,1)) )| +|( Line(Q,
i), Base_FinSeq(K,n,j) )| by A9,A109,Th10
.=(-(a")*(Q*(1,j)))* (Q*(i,1)) +|( Line(Q,i), Base_FinSeq(K,n,j) )| by
A27,A109,A110,Th35
.= -((Q*(1,j))*(a")* (Q*(i,1))) +|( Line(Q,i), Base_FinSeq(K,n,j) )|
by VECTSP_1:9
.= -((Q*(1,j))*((a")* (Q*(i,1)))) +|( Line(Q,i), Base_FinSeq(K,n,j) )|
by GROUP_1:def 3
.= -(Q*(1,j))*((a")* (Q*(i,1))) + Q*(i,j) by A72,A73,A74,A109,A111,Th35;
A113: 1<=n by A72,A73,XXREAL_0:2;
p2=Base_FinSeq(K,n,i) by A7,A72,A73,A79;
hence (Q*P)*(i,j)= -(Q*(1,j))*((a")* ( 0.K)) + Q*(i,j) by A72,A113,A112,A80
,Th25
.= -(Q*(1,j))*(( 0.K)) + Q*(i,j)
.= -(0.K) + Q*(i,j)
.= (0.K) + 1.K by A77,A78,RLVECT_1:12
.= 1.K by RLVECT_1:4;
end;
A114: Indices P=[: Seg n,Seg n :] by MATRIX_0:24;
A115: for i,j st 1**j holds (Q*P)*(i,j)= 0.K
proof
A116: len ((a")*(Base_FinSeq(K,n,1))) =len Base_FinSeq(K,n,1) by MATRIXR1:16
.=n by Th23;
let i,j;
assume that
A117: 1**j;
A122: [i,j] in Indices (Q*P) by A117,A118,A119,A120,MATRIX_0:31;
A123: j in Seg n by A119,A120,FINSEQ_1:1;
A124: len ((-(a")*(Q*(1,j)))*(Base_FinSeq(K,n,1))) =len (Base_FinSeq(K,n,1
)) by MATRIXR1:16
.=n by Th23;
A125: len (Col(P,j))=len P by MATRIX_0:def 8
.=n by MATRIX_0:24;
A126: [i,1] in Indices Q by A27,A117,A118,MATRIX_0:31;
A127: len (Base_FinSeq(K,n,j))=n by Th23;
A128: len (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))) =len ((-(a")*(Q*(1,j)))*(
Base_FinSeq(K,n,1))) by Th6
.=len (Base_FinSeq(K,n,1)) by MATRIXR1:16
.=n by Th23;
then
A129: len (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))+Base_FinSeq(K,n,j)) =n by A127
,Th2;
A130: [i,j] in Indices Q by A117,A118,A119,A120,MATRIX_0:31;
now
per cases;
suppose
A131: j>1;
reconsider p=Col(P,j),q=-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1)) +
Base_FinSeq(K,n,j) as FinSequence of K;
for k be Nat st 1 <=k & k <= n holds p.k=q.k
proof
let k be Nat;
assume that
A132: 1 <=k and
A133: k <= n;
k in Seg n by A132,A133,FINSEQ_1:1;
then
A134: k
in dom ((-(a")*(Q*(1,j)))*(Base_FinSeq(K,n,1))) by A124,FINSEQ_1:def 3;
len (Base_FinSeq(K,n,1))=n by Th23;
then
A135: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by A132,A133,
FINSEQ_4:15;
k in dom P by A10,A132,A133,FINSEQ_3:25;
then
A136: p.k=P*(k,j) by MATRIX_0:def 8;
A137: (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))).k =((-(a")*(Q*(1,j)))*(
Base_FinSeq(K,n,1))).k by Th6
.=(-(a")*(Q*(1,j)))*((Base_FinSeq(K,n,1))/.k) by A134,A135,
FVSUM_1:50;
len (Base_FinSeq(K,n,1))=n by Th23;
then
A138: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by A132,A133,
FINSEQ_4:15;
per cases by A132,XXREAL_0:1;
suppose
A139: 1=k;
then
A140: (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))).k =(-(a")*(Q*(1,j)))*(
1.K) by A27,A135,A137,Th24;
A141: (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-(a")*(Q*(1,j))*
(Base_FinSeq(K,n,1))).k by A128,A132,A133,FINSEQ_4:15;
(Base_FinSeq(K,n,j))/.k = (Base_FinSeq(K,n,j)).k by A127,A132,A133,
FINSEQ_4:15
.= 0.K by A131,A133,A139,Th25;
then q.k= (-(a")*(Q*(1,j)))*(1.K)+ 0.K by A128,A127,A132,A133,A141
,A140,Th5
.= (-(a")*(Q*(1,j)))*(1.K) by RLVECT_1:4
.=-(a")*(Q*(1,j));
hence thesis by A34,A120,A131,A136,A139;
end;
suppose
A142: 1 j;
(-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-(a")*(Q*(1,
j)))*((Base_FinSeq(K,n,1))/.k) by A128,A132,A133,A137,FINSEQ_4:15
.=(-(a")*(Q*(1,j)))*(0.K) by A133,A138,A142,Th25
.= 0.K;
then q.k = 0.K +(Base_FinSeq(K,n,j))/.k by A128,A127,A132,A133
,Th5
.= (Base_FinSeq(K,n,j))/.k by RLVECT_1:4
.= (Base_FinSeq(K,n,j)).k by A127,A132,A133,FINSEQ_4:15
.= 0.K by A132,A133,A145,Th25;
hence thesis by A119,A120,A144,A145,Th25;
end;
suppose
A146: k=j;
(-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-(a")*(Q*(1,
j)))*((Base_FinSeq(K,n,1))/.k) by A128,A132,A133,A137,FINSEQ_4:15
.=(-(a")*(Q*(1,j)))*(0.K) by A133,A138,A142,Th25
.= 0.K;
then q.k = 0.K +(Base_FinSeq(K,n,j))/.k by A128,A127,A132,A133
,Th5
.= (Base_FinSeq(K,n,j))/.k by RLVECT_1:4
.= (Base_FinSeq(K,n,j)).k by A127,A132,A133,FINSEQ_4:15
.= 1.K by A119,A120,A146,Th24;
hence thesis by A132,A133,A144,A146,Th24;
end;
end;
hence thesis;
end;
end;
then
A147: Col(P,j)=-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))+Base_FinSeq(K,n,j)
by A125,A129,FINSEQ_1:14;
A148: 1<=n by A117,A118,XXREAL_0:2;
A149: width Q=n by MATRIX_0:24;
then
A150: len Line(Q,i) = n by MATRIX_0:def 7;
then
A151: (Line(Q,i))/.j = ( Line(Q,i)).j by A119,A120,FINSEQ_4:15
.= Q*(i,j) by A123,A149,MATRIX_0:def 7;
A152: (Line(Q,i))/.1 = (Line(Q,i)).1 by A27,A150,FINSEQ_4:15
.= Q*(i,1) by A70,MATRIX_0:def 7;
A153: (Q*P)*(i,j)= |( Line(Q,i), Col(P,j) )| by A10,A122,A149,MATRIX_3:def 4
.= |( Line(Q,i), -(a")*(Q*(1,j))*(Base_FinSeq(K,n,1)) )| +|( Line(
Q,i), Base_FinSeq(K,n,j) )| by A128,A127,A147,A150,Th11
.= |( Line(Q,i), (-(a")*(Q*(1,j)))*(Base_FinSeq(K,n,1)) )| +|(
Line(Q,i), Base_FinSeq(K,n,j) )| by Th6
.=(-(a")*(Q*(1,j)))* |( Line(Q,i), (Base_FinSeq(K,n,1)) )| +|(
Line(Q,i), Base_FinSeq(K,n,j) )| by A9,A150,Th10
.=(-(a")*(Q*(1,j)))* (Q*(i,1)) +|( Line(Q,i), Base_FinSeq(K,n,j)
)| by A27,A150,A152,Th35
.= -((Q*(1,j))*(a")* (Q*(i,1))) +|( Line(Q,i), Base_FinSeq(K,n,j)
)| by VECTSP_1:9
.= -((Q*(1,j))*((a")* (Q*(i,1)))) +|( Line(Q,i), Base_FinSeq(K,n,j
) )| by GROUP_1:def 3
.= -(Q*(1,j))*((a")* (Q*(i,1))) + Q*(i,j) by A119,A120,A150,A151,Th35
;
consider p2 being FinSequence of K such that
A154: p2 = Q.i and
A155: Q*(i,1) = p2.1 by A126,MATRIX_0:def 5;
consider p1 being FinSequence of K such that
A156: p1 = Q.i and
A157: Q*(i,j) = p1.j by A130,MATRIX_0:def 5;
p1=Base_FinSeq(K,n,i) by A7,A117,A118,A156;
then
A158: p1.j= 0.K by A119,A120,A121,Th25;
p2=Base_FinSeq(K,n,i) by A7,A117,A118,A154;
hence (Q*P)*(i,j) = -(Q*(1,j))*((a")* (0.K)) + Q*(i,j) by A117,A148
,A153,A155,Th25
.= -(Q*(1,j))*((0.K)) + Q*(i,j)
.= -(0.K) + Q*(i,j)
.= 0.K + 0.K by A157,A158,RLVECT_1:12
.= 0.K by RLVECT_1:4;
end;
suppose
A159: j<=1;
reconsider p=Col(P,j),q=a"*(Base_FinSeq(K,n,1)) as FinSequence of K;
A160: for k be Nat st 1 <=k & k <= n holds p.k=q.k
proof
let k be Nat;
assume that
A161: 1 <=k and
A162: k <= n;
A163: len (Base_FinSeq(K,n,1))=n by Th23;
then
A164: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by A161,A162,
FINSEQ_4:15;
A165: k in Seg n by A161,A162,FINSEQ_1:1;
then k in dom ((a")*(Base_FinSeq(K,n,1))) by A116,FINSEQ_1:def 3;
then
A166: ((a")*(Base_FinSeq(K,n,1))).k = (a")*((Base_FinSeq(K,n,1))/.k)
by A164,FVSUM_1:50;
k in dom P by A10,A161,A162,FINSEQ_3:25;
then
A167: p.k=P*(k,j) by MATRIX_0:def 8;
per cases by A161,XXREAL_0:1;
suppose
A168: 1=k;
then q.k= (a")*(1.K) by A162,A164,A166,Th24
.=a";
hence thesis by A3,A119,A159,A167,A168,XXREAL_0:1;
end;
suppose
A169: 1 j;
((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by A161,A162
,A163,FINSEQ_4:15;
then (a")*(Base_FinSeq(K,n,1))/.k = a"*(0.K) by A162,A169,Th25
.= 0.K;
hence thesis by A119,A120,A166,A171,A172,Th25;
end;
suppose
k=j;
hence thesis by A159,A169;
end;
end;
hence thesis;
end;
end;
A173: 1<=n by A117,A118,XXREAL_0:2;
A174: width Q=n by MATRIX_0:24;
then
A175: len Line(Q,i) = n by MATRIX_0:def 7;
then
A176: (Line(Q,i))/.1 = (Line(Q,i)).1 by A27,FINSEQ_4:15
.= Q*(i,1) by A70,MATRIX_0:def 7;
A177: (Q*P)*(i,j)= |( Line(Q,i), Col(P,j) )| by A10,A122,A174,MATRIX_3:def 4
.= |( Line(Q,i), a"*(Base_FinSeq(K,n,1)) )| by A125,A116,A160,
FINSEQ_1:14
.= a"* |( Line(Q,i), (Base_FinSeq(K,n,1)) )| by A9,A175,Th10
.= a"* (Q*(i,1)) by A27,A175,A176,Th35;
consider p2 being FinSequence of K such that
A178: p2 = Q.i and
A179: Q*(i,1) = p2.1 by A126,MATRIX_0:def 5;
p2=Base_FinSeq(K,n,i) by A7,A117,A118,A178;
hence (Q*P)*(i,j)=a"* (0.K) by A117,A173,A177,A179,Th25
.= 0.K;
end;
end;
hence thesis;
end;
len (Col(P,1))=len P by MATRIX_0:def 8
.=n by MATRIX_0:24;
then
A180: Col(P,1)=(a")*(Base_FinSeq(K,n,1)) by A11,A12,FINSEQ_1:14;
A181: Indices (Q*P)=[: Seg n,Seg n :] by MATRIX_0:24;
A182: len ((a")*(Line(Q,1)))=len ((Line(Q,1))) by MATRIXR1:16
.= n by A31,MATRIX_0:def 7;
Indices Q=[: Seg n,Seg n :] & [1,1] in Indices Q by A27,MATRIX_0:24,31;
then
A183: (Q*P)*(1,1)= |( Line(Q,1), Col(P,1) )| by A10,A31,A181,MATRIX_3:def 4
.= (a")*( |( Line(Q,1), Base_FinSeq(K,n,1) )| ) by A32,A9,A180,Th10
.=(a")*(Line(Q,1))/.1 by A32,A27,Th35
.=((a")*(Line(Q,1)))/.1 by A33,POLYNOM1:def 1
.=((a")*(Line(Q,1))).1 by A27,A182,FINSEQ_4:15
.=(a")*(Q*(1,1)) by A70,A30,MATRIX12:3
.=1.K by A2,A5,VECTSP_1:def 10;
for i,j being Nat st [i,j] in Indices (Q*P) holds (Q*P)*(i,j)=(1.(K,n)
)*(i,j)
proof
let i,j be Nat;
reconsider i0=i,j0=j as Element of NAT by ORDINAL1:def 12;
assume
A184: [i,j] in Indices (Q*P);
then
A185: i in Seg n by A181,ZFMISC_1:87;
then
A186: 1<=i by FINSEQ_1:1;
A187: i<=n by A185,FINSEQ_1:1;
A188: j in Seg n by A181,A184,ZFMISC_1:87;
then
A189: 1<=j by FINSEQ_1:1;
A190: j<=n by A188,FINSEQ_1:1;
per cases by A186,XXREAL_0:1;
suppose
A191: 1**j;
A193: (1.(K,n))*(i,j)=(Base_FinSeq(K,n,i0)).j0 by A186,A187,A189,A190,Th27
.= 0.K by A189,A190,A192,Th25;
thus (Q*P)*(i,j)=(Q*P)*(i0,j0)
.=(1.(K,n))*(i,j) by A115,A187,A189,A190,A191,A192,A193;
end;
suppose
A194: i=j;
A195: (1.(K,n))*(i,j)=(Base_FinSeq(K,n,i0)).j0 by A186,A187,A189,A190,Th27
.=1.K by A189,A190,A194,Th24;
thus (Q*P)*(i,j)=(Q*P)*(i0,j0)
.=(1.(K,n))*(i,j) by A71,A190,A191,A194,A195;
end;
end;
hence thesis;
end;
suppose
A196: 1=i;
now
per cases;
suppose
A197: i=j;
then
A200: i=j by A189,A196,XXREAL_0:1;
(1.(K,n))*(i,j)=(Base_FinSeq(K,n,i0)).j0 by A186,A187,A189,A190,Th27
.=1.K by A189,A190,A200,Th24;
hence thesis by A183,A189,A196,A199,XXREAL_0:1;
end;
end;
hence thesis;
end;
end;
then
A201: Q*P=1.(K,n) by MATRIX_0:27;
A202: len Q=n by MATRIX_0:24;
A203: len Base_FinSeq(K,n,1)=n by Th23;
A204: len (a*(Base_FinSeq(K,n,1)))=len (Base_FinSeq(K,n,1)) by MATRIXR1:16
.= n by Th23;
A205: for k be Nat st 1<=k & k<=n holds (Col(Q,1)).k=(a*(Base_FinSeq(K,n,1)))
.k
proof
let k be Nat;
assume that
A206: 1<=k and
A207: k<=n;
A208: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by A203,A206,A207,
FINSEQ_4:15;
A209: k in dom (a*(Base_FinSeq(K,n,1))) by A204,A206,A207,FINSEQ_3:25;
A210: now
assume
A211: k<>1;
thus (a*(Base_FinSeq(K,n,1))).k= a*((Base_FinSeq(K,n,1))/.k) by A208,A209
,FVSUM_1:50
.= a*(0.K) by A206,A207,A208,A211,Th25
.= 0.K;
end;
A212: k in NAT by ORDINAL1:def 12;
k in Seg n by A206,A207,FINSEQ_1:1;
then
A213: k in dom Q by A202,FINSEQ_1:def 3;
A214: now
[k,1] in Indices Q by A8,A206,A207,MATRIX_0:31;
then
A215: ex p being FinSequence of K st p = Q.k & Q*(k,1) = p.1 by MATRIX_0:def 5;
assume
A216: k<>1;
then 1 j;
(-a*(P*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-a*(P*(1,j)))*((
Base_FinSeq(K,n,1))/.k) by A230,A234,A235,A239,FINSEQ_4:15
.=(-a*(P*(1,j)))*(0.K) by A235,A237,A243,Th25
.= 0.K;
then q.k = 0.K +(Base_FinSeq(K,n,j))/.k by A230,A231,A234,A235,Th5
.= (Base_FinSeq(K,n,j))/.k by RLVECT_1:4
.= (Base_FinSeq(K,n,j)).k by A231,A234,A235,FINSEQ_4:15
.= 0.K by A234,A235,A248,Th25;
hence thesis by A228,A229,A247,A248,Th25;
end;
suppose
A249: k=j;
(-a*(P*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-a*(P*(1,j)))*((
Base_FinSeq(K,n,1))/.k) by A230,A234,A235,A239,FINSEQ_4:15
.=(-a*(P*(1,j)))*(0.K) by A235,A237,A243,Th25
.= 0.K;
then q.k = 0.K +(Base_FinSeq(K,n,j))/.k by A230,A231,A234,A235,Th5
.= (Base_FinSeq(K,n,j))/.k by RLVECT_1:4
.= (Base_FinSeq(K,n,j)).k by A231,A234,A235,FINSEQ_4:15
.= 1.K by A234,A235,A249,Th24;
hence thesis by A234,A235,A247,A249,Th24;
end;
end;
hence thesis;
end;
end;
A250: width P=n by MATRIX_0:24;
then
A251: len Line(P,1) = n by MATRIX_0:def 7;
then
A252: (Line(P,1))/.1 = (Line(P,1)).1 by A219,FINSEQ_4:15
.=a" by A3,A226,MATRIX_0:def 7;
A253: j in Seg n by A228,A229,FINSEQ_1:1;
A254: len (Col(Q,j))=len Q by MATRIX_0:def 8
.=n by MATRIX_0:24;
len (-a*(P*(1,j))*(Base_FinSeq(K,n,1))+Base_FinSeq(K,n,j)) =n by A230,A231
,Th2;
then
A255: Col(Q,j)=-a*(P*(1,j))*(Base_FinSeq(K,n,1))+Base_FinSeq(K,n,j) by A254
,A233,FINSEQ_1:14;
A256: (Line(P,1))/.j = ( Line(P,1)).j by A228,A229,A251,FINSEQ_4:15
.= P*(1,j) by A253,A250,MATRIX_0:def 7;
[1,j] in Indices (P*Q) by A219,A228,A229,MATRIX_0:31;
then (P*Q)*(1,j)= |( Line(P,1), Col(Q,j) )| by A202,A250,MATRIX_3:def 4
.= |( Line(P,1), -a*(P*(1,j))*(Base_FinSeq(K,n,1)) )| +|( Line(P,1),
Base_FinSeq(K,n,j) )| by A224,A230,A231,A255,Th11
.= |( Line(P,1), (-a*(P*(1,j)))*(Base_FinSeq(K,n,1)) )| +|( Line(P,1),
Base_FinSeq(K,n,j) )| by Th6
.=(-a*(P*(1,j)))* |( Line(P,1), (Base_FinSeq(K,n,1)) )| +|( Line(P,1),
Base_FinSeq(K,n,j) )| by A224,A203,Th10
.=(-a*(P*(1,j)))* (a") +|( Line(P,1), Base_FinSeq(K,n,j) )| by A224,A219
,A252,Th35
.= -(a*(P*(1,j)))* (a") +|( Line(P,1), Base_FinSeq(K,n,j) )| by
VECTSP_1:9
.= -((P*(1,j))*(a* (a"))) +|( Line(P,1), Base_FinSeq(K,n,j) )| by
GROUP_1:def 3
.= -((P*(1,j))*(1_K)) +|( Line(P,1), Base_FinSeq(K,n,j) )| by A2,
VECTSP_1:def 10
.= -(P*(1,j)*(1.K)) + (Line(P,1))/.j by A224,A228,A229,Th35
.= -(P*(1,j)) + P*(1,j) by A256
.= 0.K by RLVECT_1:5;
hence thesis;
end;
A257: Indices Q=[: Seg n,Seg n :] by MATRIX_0:24;
A258: for i,j st 1** j;
then
A281: p.k= 0.K by A259,A260,A261,A279,Th25;
A282: (-a*(P*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-a*(P*(1,j))*(
Base_FinSeq(K,n,1))).k by A262,A267,A268,FINSEQ_4:15;
A283: (-a*(P*(1,j))*(Base_FinSeq(K,n,1))).k =(-a*(P*(1,j)))*(0.K)
by A268,A271,A274,A277,Th25
.= 0.K;
(Base_FinSeq(K,n,j))/.k = (Base_FinSeq(K,n,j)).k by A263,A267,A268,
FINSEQ_4:15
.= 0.K by A267,A268,A280,Th25;
then q.k=0.K + 0.K by A262,A263,A267,A268,A282,A283,Th5;
hence thesis by A281,RLVECT_1:4;
end;
suppose
A284: k=j;
then
A285: p.k=1.K by A267,A268,A279,Th24;
A286: (-a*(P*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-a*(P*(1,j))*(
Base_FinSeq(K,n,1))).k by A262,A267,A268,FINSEQ_4:15;
A287: (-a*(P*(1,j))*(Base_FinSeq(K,n,1))).k =(-a*(P*(1,j)))*(0.K)
by A268,A271,A274,A277,Th25
.= 0.K;
(Base_FinSeq(K,n,j))/.k = (Base_FinSeq(K,n,j)).k by A263,A267,A268,
FINSEQ_4:15
.= 1.K by A259,A260,A261,A284,Th24;
then q.k= 0.K + 1.K by A262,A263,A267,A268,A286,A287,Th5;
hence thesis by A285,RLVECT_1:4;
end;
end;
hence thesis;
end;
end;
[i,j] in Indices P by A259,A260,A261,MATRIX_0:31;
then consider p1 being FinSequence of K such that
A288: p1 = P.i and
A289: P*(i,j) = p1.j by MATRIX_0:def 5;
p1=Base_FinSeq(K,n,i) by A4,A259,A260,A288;
then
A290: p1.j=1.K by A259,A260,A261,Th24;
A291: len (Col(Q,j))=len Q by MATRIX_0:def 8
.=n by MATRIX_0:24;
len (-a*(P*(1,j))*(Base_FinSeq(K,n,1))+Base_FinSeq(K,n,j)) =n by A262,A263
,Th2;
then
A292: Col(Q,j)=-a*(P*(1,j))*(Base_FinSeq(K,n,1))+Base_FinSeq(K,n,j) by A291
,A265,FINSEQ_1:14;
A293: width P=n by MATRIX_0:24;
then
A294: len Line(P,i) = n by MATRIX_0:def 7;
then
A295: (Line(P,i))/.1 = (Line(P,i)).1 by A219,FINSEQ_4:15
.= P*(i,1) by A226,MATRIX_0:def 7;
A296: (Line(P,i))/.j = (Line(P,i)).j by A259,A260,A261,A294,FINSEQ_4:15
.= P*(i,j) by A264,A293,MATRIX_0:def 7;
[i,j] in Indices (P*Q) by A259,A260,A261,MATRIX_0:31;
then
A297: (P*Q)*(i,j)= |( Line(P,i), Col(Q,j) )| by A202,A293,MATRIX_3:def 4
.= |( Line(P,i), -a*(P*(1,j))*(Base_FinSeq(K,n,1)) )| +|( Line(P,i),
Base_FinSeq(K,n,j) )| by A262,A263,A292,A294,Th11
.= |( Line(P,i), (-a*(P*(1,j)))*(Base_FinSeq(K,n,1)) )| +|( Line(P,i),
Base_FinSeq(K,n,j) )| by Th6
.=(-a*(P*(1,j)))* |( Line(P,i), (Base_FinSeq(K,n,1)) )| +|( Line(P,i),
Base_FinSeq(K,n,j) )| by A203,A294,Th10
.=(-a*(P*(1,j)))* (P*(i,1)) +|( Line(P,i), Base_FinSeq(K,n,j) )| by A219
,A294,A295,Th35
.= -(a*(P*(1,j)))* (P*(i,1)) +|( Line(P,i), Base_FinSeq(K,n,j) )| by
VECTSP_1:9
.= -((P*(1,j))*(a* (P*(i,1)))) +|( Line(P,i), Base_FinSeq(K,n,j) )| by
GROUP_1:def 3
.= -(P*(1,j))*(a* (P*(i,1))) + P*(i,j) by A259,A260,A261,A294,A296,Th35;
A298: 1<=n by A259,A260,XXREAL_0:2;
[i,1] in Indices P by A8,A259,A260,MATRIX_0:31;
then consider p2 being FinSequence of K such that
A299: p2 = P.i and
A300: P*(i,1) = p2.1 by MATRIX_0:def 5;
p2=Base_FinSeq(K,n,i) by A4,A259,A260,A299;
hence (P*Q)*(i,j)= -(P*(1,j))*(a* (0.K)) + P*(i,j) by A259,A298,A297,A300
,Th25
.= -(P*(1,j))*((0.K)) + P*(i,j)
.= -((0.K)) + P*(i,j)
.= 0.K + 1.K by A289,A290,RLVECT_1:12
.= 1.K by RLVECT_1:4;
end;
len (Col(Q,1))=len Q by MATRIX_0:def 8
.=n by MATRIX_0:24;
then
A301: Col(Q,1)=a*(Base_FinSeq(K,n,1)) by A204,A205,FINSEQ_1:14;
A302: Indices (P*Q)=[: Seg n,Seg n :] by MATRIX_0:24;
A303: for i,j st 1**j holds (P*Q)*(i,j)= 0.K
proof
A304: len (a*(Base_FinSeq(K,n,1))) =len (Base_FinSeq(K,n,1)) by MATRIXR1:16
.=n by Th23;
let i,j;
assume that
A305: 1**j;
A310: [i,j] in Indices (P*Q) by A305,A306,A307,A308,MATRIX_0:31;
A311: j in Seg n by A307,A308,FINSEQ_1:1;
A312: len (Col(Q,j))=len Q by MATRIX_0:def 8
.=n by MATRIX_0:24;
A313: [i,1] in Indices P by A8,A305,A306,MATRIX_0:31;
A314: len (Base_FinSeq(K,n,j))=n by Th23;
A315: len (-a*(P*(1,j))*(Base_FinSeq(K,n,1))) =len ((-a*(P*(1,j)))*(
Base_FinSeq(K,n,1))) by Th6
.=len (Base_FinSeq(K,n,1)) by MATRIXR1:16
.=n by Th23;
then
A316: len (-a*(P*(1,j))*(Base_FinSeq(K,n,1))+Base_FinSeq(K,n,j)) =n by A314,Th2
;
A317: [i,j] in Indices P by A305,A306,A307,A308,MATRIX_0:31;
now
per cases;
suppose
A318: j>1;
reconsider p=Col(Q,j),q=-a*(P*(1,j))*(Base_FinSeq(K,n,1)) +Base_FinSeq
(K,n,j) as FinSequence of K;
for k be Nat st 1 <=k & k <= n holds p.k=q.k
proof
let k be Nat;
assume that
A319: 1 <=k and
A320: k <= n;
A321: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by A203,A319,A320,
FINSEQ_4:15;
A322: len ((-a*(P*(1,j)))*(Base_FinSeq(K,n,1))) = len (Base_FinSeq(K
,n,1)) by MATRIXR1:16
.=n by Th23;
then
A323: k in dom ((-a*(P*(1,j)))*(Base_FinSeq(K,n,1))) by A319,A320,
FINSEQ_3:25;
A324: (-a*(P*(1,j))*(Base_FinSeq(K,n,1))).k =((-a*(P*(1,j)))*(
Base_FinSeq(K,n,1))).k by Th6
.=(-a*(P*(1,j)))*((Base_FinSeq(K,n,1))/.k) by A323,A321,FVSUM_1:50;
len (Base_FinSeq(K,n,1))=n by Th23;
then
A325: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by A319,A320,
FINSEQ_4:15;
k in dom Q by A202,A319,A320,FINSEQ_3:25;
then
A326: p.k=Q*(k,j) by MATRIX_0:def 8;
per cases by A319,XXREAL_0:1;
suppose
A327: 1=k;
k <= len (-a*(P*(1,j))*(Base_FinSeq(K,n,1))) by A320,A322,Th6;
then
A328: (-a*(P*(1,j))*(Base_FinSeq(K,n,1)))/.k = (-a*(P*(1,j)))*((
Base_FinSeq(K,n,1))/.k) by A319,A324,FINSEQ_4:15
.= (-a*(P*(1,j)))*(1.K) by A219,A325,A327,Th24;
(Base_FinSeq(K,n,j))/.k = (Base_FinSeq(K,n,j)).k by A314,A319,A320,
FINSEQ_4:15
.= 0.K by A318,A320,A327,Th25;
then q.k= (-a*(P*(1,j)))*(1.K)+ 0.K by A315,A314,A319,A320,A328,Th5
.= (-a*(P*(1,j)))*(1_K) by RLVECT_1:4
.= (-a*(P*(1,j)));
hence thesis by A6,A308,A318,A326,A327;
end;
suppose
A329: 1 j;
(Base_FinSeq(K,n,j))/.k =(Base_FinSeq(K,n,j)).k by A314,A319
,A320,FINSEQ_4:15
.= 0.K by A319,A320,A333,Th25;
then q.k = (-a*(P*(1,j))*(Base_FinSeq(K,n,1)))/.k +0.K by A315
,A314,A319,A320,Th5;
then
A334: q.k = (-a*(P*(1,j))*(Base_FinSeq(K,n,1)))/.k by RLVECT_1:4
.= (-a*(P*(1,j))*(Base_FinSeq(K,n,1))).k by A319,A332,
FINSEQ_4:15;
(-a*(P*(1,j))*(Base_FinSeq(K,n,1))).k =(-a*(P*(1,j)))*(
0.K) by A320,A324,A325,A329,Th25
.= 0.K;
hence thesis by A307,A308,A331,A333,A334,Th25;
end;
suppose
A335: k=j;
then
A336: p.k=1.K by A319,A320,A331,Th24;
A337: (-a*(P*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-a*(P*(1,j))*(
Base_FinSeq(K,n,1))).k by A315,A319,A320,FINSEQ_4:15;
A338: (-a*(P*(1,j))*(Base_FinSeq(K,n,1))).k =(-a*(P*(1,j)))*(
0.K) by A320,A321,A324,A329,Th25
.= 0.K;
(Base_FinSeq(K,n,j))/.k = (Base_FinSeq(K,n,j)).k by A314,A319
,A320,FINSEQ_4:15
.= 1.K by A319,A320,A335,Th24;
then q.k= 0.K + 1.K by A315,A314,A319,A320,A337,A338,Th5;
hence thesis by A336,RLVECT_1:4;
end;
end;
hence thesis;
end;
end;
then
A339: Col(Q,j)=-a*(P*(1,j))*(Base_FinSeq(K,n,1))+Base_FinSeq(K,n,j) by A312
,A316,FINSEQ_1:14;
A340: 1<=n by A305,A306,XXREAL_0:2;
A341: width P=n by MATRIX_0:24;
then
A342: len Line(P,i) = n by MATRIX_0:def 7;
then
A343: (Line(P,i))/.j = (Line(P,i)).j by A307,A308,FINSEQ_4:15
.= P*(i,j) by A311,A341,MATRIX_0:def 7;
A344: (Line(P,i))/.1 = (Line(P,i)).1 by A219,A342,FINSEQ_4:15
.= P*(i,1) by A226,MATRIX_0:def 7;
A345: (P*Q)*(i,j)= |( Line(P,i), Col(Q,j) )| by A202,A310,A341,MATRIX_3:def 4
.= |( Line(P,i), -a*(P*(1,j))*(Base_FinSeq(K,n,1)) )| +|( Line(P,i
), Base_FinSeq(K,n,j) )| by A315,A314,A339,A342,Th11
.= |( Line(P,i), (-a*(P*(1,j)))*(Base_FinSeq(K,n,1)) )| +|( Line(P
,i), Base_FinSeq(K,n,j) )| by Th6
.=(-a*(P*(1,j)))* |( Line(P,i), (Base_FinSeq(K,n,1)) )| +|( Line(P
,i), Base_FinSeq(K,n,j) )| by A203,A342,Th10
.=(-a*(P*(1,j)))* (P*(i,1)) +|( Line(P,i), Base_FinSeq(K,n,j) )|
by A219,A342,A344,Th35
.= -(a*(P*(1,j)))* (P*(i,1)) +|( Line(P,i), Base_FinSeq(K,n,j) )|
by VECTSP_1:9
.= -((P*(1,j))*(a* (P*(i,1)))) +|( Line(P,i), Base_FinSeq(K,n,j)
)| by GROUP_1:def 3
.= -(P*(1,j))*(a* (P*(i,1))) + P*(i,j) by A307,A308,A342,A343,Th35;
consider p2 being FinSequence of K such that
A346: p2 = P.i and
A347: P*(i,1) = p2.1 by A313,MATRIX_0:def 5;
consider p1 being FinSequence of K such that
A348: p1 = P.i and
A349: P*(i,j) = p1.j by A317,MATRIX_0:def 5;
p1=Base_FinSeq(K,n,i) by A4,A305,A306,A348;
then
A350: p1.j= 0.K by A307,A308,A309,Th25;
p2=Base_FinSeq(K,n,i) by A4,A305,A306,A346;
then (P*Q)*(i,j)= -(P*(1,j))*(a* (0.K)) + P*(i,j) by A305,A340,A345
,A347,Th25
.= -(P*(1,j))*(0.K) + P*(i,j)
.= - (0.K) + P*(i,j)
.= 0.K + 0.K by A349,A350,RLVECT_1:12
.= 0.K by RLVECT_1:4;
hence thesis;
end;
suppose
A351: j<=1;
reconsider p=Col(Q,j),q=a*(Base_FinSeq(K,n,1)) as FinSequence of K;
A352: for k be Nat st 1 <=k & k <= n holds p.k=q.k
proof
let k be Nat;
assume that
A353: 1 <=k and
A354: k <= n;
A355: k in dom Q by A202,A353,A354,FINSEQ_3:25;
A356: len (Base_FinSeq(K,n,1))=n by Th23;
then
A357: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by A353,A354,
FINSEQ_4:15;
k in dom (a*(Base_FinSeq(K,n,1))) by A204,A353,A354,FINSEQ_3:25;
then
A358: (a*(Base_FinSeq(K,n,1))).k =a*((Base_FinSeq(K,n,1))/.k) by A357,
FVSUM_1:50;
per cases by A353,XXREAL_0:1;
suppose
A359: 1=k;
then
A360: q.k= (a)*(1.K) by A354,A357,A358,Th24
.=a;
p.k=Q*(1,j) by A355,A359,MATRIX_0:def 8
.=a by A5,A307,A351,XXREAL_0:1;
hence thesis by A360;
end;
suppose
A361: 1 j;
((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by A353,A354
,A356,FINSEQ_4:15;
then a*(Base_FinSeq(K,n,1))/.k = a*(0.K) by A354,A361,Th25
.= 0.K;
hence thesis by A307,A308,A358,A364,A365,Th25;
end;
suppose
k=j;
hence thesis by A351,A361;
end;
end;
hence thesis;
end;
end;
A366: 1<=n by A305,A306,XXREAL_0:2;
A367: len (Line(P,i))=n by A223,MATRIX_0:def 7;
then
A368: (Line(P,i))/.1 = (Line(P,i)).1 by A219,FINSEQ_4:15
.= P*(i,1) by A226,MATRIX_0:def 7;
A369: (P*Q)*(i,j)= |( Line(P,i), Col(Q,j) )| by A202,A223,A310,MATRIX_3:def 4
.= |( Line(P,i), a*(Base_FinSeq(K,n,1)) )| by A312,A304,A352,
FINSEQ_1:14
.= a* |( Line(P,i), (Base_FinSeq(K,n,1)) )| by A203,A367,Th10
.= a* (P*(i,1)) by A219,A367,A368,Th35;
consider p2 being FinSequence of K such that
A370: p2 = P.i and
A371: P*(i,1) = p2.1 by A313,MATRIX_0:def 5;
p2=Base_FinSeq(K,n,i) by A4,A305,A306,A370;
hence (P*Q)*(i,j)= a*(0.K) by A305,A366,A369,A371,Th25
.=0.K;
end;
end;
hence thesis;
end;
A372: len (a*(Line(P,1)))=len ((Line(P,1))) by MATRIXR1:16
.= n by A223,MATRIX_0:def 7;
Indices P=[: Seg n,Seg n :] & [1,1] in Indices P by A219,MATRIX_0:24,31;
then
A373: (P*Q)*(1,1)= |( Line(P,1), Col(Q,1) )| by A202,A223,A302,MATRIX_3:def 4
.= a*( |( Line(P,1), Base_FinSeq(K,n,1) )| ) by A224,A203,A301,Th10
.=a*(Line(P,1))/.1 by A224,A219,Th35
.=(a*(Line(P,1)))/.1 by A225,POLYNOM1:def 1
.=(a*(Line(P,1))).1 by A219,A372,FINSEQ_4:15
.=a*(P*(1,1)) by A226,A222,MATRIX12:3
.=1.K by A2,A3,VECTSP_1:def 10;
for i,j being Nat st [i,j] in Indices (P*Q) holds (P*Q)*(i,j)=(1.(K,n)
)*(i,j)
proof
let i,j be Nat;
reconsider i0=i,j0=j as Element of NAT by ORDINAL1:def 12;
assume
A374: [i,j] in Indices (P*Q);
then
A375: i in Seg n by A302,ZFMISC_1:87;
then
A376: 1<=i by FINSEQ_1:1;
A377: i<=n by A375,FINSEQ_1:1;
A378: j in Seg n by A302,A374,ZFMISC_1:87;
then
A379: 1<=j by FINSEQ_1:1;
A380: j<=n by A378,FINSEQ_1:1;
per cases by A376,XXREAL_0:1;
suppose
A381: 1**j;
A383: (1.(K,n))*(i,j)=(Base_FinSeq(K,n,i0)).j0 by A376,A377,A379,A380,Th27
.= 0.K by A379,A380,A382,Th25;
thus (P*Q)*(i,j)=(P*Q)*(i0,j0)
.=(1.(K,n))*(i,j) by A303,A377,A379,A380,A381,A382,A383;
end;
suppose
A384: i=j;
A385: (1.(K,n))*(i,j)=(Base_FinSeq(K,n,i0)).j0 by A376,A377,A379,A380,Th27
.=1.K by A379,A380,A384,Th24;
thus (P*Q)*(i,j)=(P*Q)*(i0,j0)
.=(1.(K,n))*(i,j) by A258,A380,A381,A384,A385;
end;
end;
hence thesis;
end;
suppose
A386: 1=i;
now
per cases;
suppose
A387: i=j;
then
A390: i=j by A379,A386,XXREAL_0:1;
(1.(K,n))*(i,j)=(Base_FinSeq(K,n,i0)).j0 by A376,A377,A379,A380,Th27
.=1.K by A379,A380,A390,Th24;
hence thesis by A373,A379,A386,A389,XXREAL_0:1;
end;
end;
hence thesis;
end;
end;
then
A391: P*Q=1.(K,n) by MATRIX_0:27;
hence P is invertible by A201,Th19;
thus thesis by A391,A201,Th18;
end;
theorem Th38:
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**0 and
A2: a<>0.K & P*(1,1)= a" & for i st 1**1 implies $3=- a*( P*(1,$2) )))) & ($1 <>1 implies for i0 being Element of
NAT st i0=$1 holds $3= (Base_FinSeq(K,n,i0)).$2);
A3: for i,j being Nat st [i,j] in [:Seg n, Seg n:] ex x being Element of K
st P[i,j,x]
proof
let i,j be Nat;
reconsider i0=i,j0=j as Element of NAT by ORDINAL1:def 12;
assume [i,j] in [:Seg n, Seg n:];
then j0 in Seg n by ZFMISC_1:87;
then
A4: 1<=j0 & j0<=n by FINSEQ_1:1;
per cases;
suppose
A5: i=1;
now
per cases;
case
A6: j=1;
set x1=a;
thus (i=1 implies (j=1 implies x1=a)& (j<>1 implies x1=- a*(P*(1,j)
)) ) & (i <>1 implies for i1 being Element of NAT st i1=i holds x1= (
Base_FinSeq(K,n,i1)).j) by A5,A6;
end;
case
A7: j<>1;
set x1= -(a)*( P*(1,j) );
thus (i=1 implies (j=1 implies x1=a)& (j<>1 implies x1=- a*(P*(1,j))
) ) & (i <>1 implies for i1 being Element of NAT st i1=i holds x1= (Base_FinSeq
(K,n,i1)).j) by A5,A7;
end;
end;
hence thesis;
end;
suppose
A8: i<>1;
len (Base_FinSeq(K,n,i0))=n by Th23;
then (Base_FinSeq(K,n,i0))/.j0= (Base_FinSeq(K,n,i0)).j0 by A4,
FINSEQ_4:15;
then reconsider x1= (Base_FinSeq(K,n,i0)).j0 as Element of K;
i <>1 implies for i1 being Element of NAT st i1=i holds x1= (
Base_FinSeq(K,n,i1)).j;
hence thesis by A8;
end;
end;
consider Q0 being Matrix of n,n,K such that
A9: for i,j being Nat st [i,j] in Indices Q0 holds P[i,j,Q0*(i,j)] from
MATRIX_0:sch 2(A3);
A10: 0+1<=n by A1,NAT_1:13;
A11: for j st 10 & 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 and
A2: A*(1,1)<>0.K;
A3: 0+1<=n by A1,NAT_1:13;
set a=A*(1,1);
defpred P[Nat,Nat,Element of K] means ($1=1 implies (($2=1 implies $3=a")& (
$2<>1 implies $3=- (a")*( A*(1,$2) )))) & ($1 <>1 implies for i0 being Element
of NAT st i0=$1 holds $3= (Base_FinSeq(K,n,i0)).$2);
A4: for i,j being Nat st [i,j] in [:Seg n, Seg n:] ex x being Element of K
st P[i,j,x]
proof
let i,j be Nat;
reconsider i0=i,j0=j as Element of NAT by ORDINAL1:def 12;
assume [i,j] in [:Seg n, Seg n:];
then j0 in Seg n by ZFMISC_1:87;
then
A5: 1<=j0 & j0<=n by FINSEQ_1:1;
per cases;
suppose
A6: i=1;
per cases;
suppose
j=1;
hence thesis by A6;
end;
suppose
j<>1;
hence thesis by A6;
end;
end;
suppose
A7: i<>1;
set x1= (Base_FinSeq(K,n,i0))/.j0;
len (Base_FinSeq(K,n,i0))=n by Th23;
then
for i1 being Element of NAT st i1=i holds x1= (Base_FinSeq(K,n,i1))
.j by A5,FINSEQ_4:15;
hence thesis by A7;
end;
end;
consider P0 being Matrix of n,n,K such that
A8: for i,j being Nat st [i,j] in Indices P0 holds P[i,j,P0*(i,j)] from
MATRIX_0:sch 2(A4);
A9: 0+1<=n by A1,NAT_1:13;
A10: for i st 1**1;
thus ((a")*(Base_FinSeq(K,n,1))).k = (a")*((Base_FinSeq(K,n,1))/.k) by
A29,A28,FVSUM_1:50
.= (a")*(0.K) by A26,A27,A28,A31,Th25
.= 0.K;
end;
k in Seg n by A26,A27,FINSEQ_1:1;
then
A32: k in dom P0 by A23,FINSEQ_1:def 3;
A33: now
k in Seg n by A26,A27,FINSEQ_1:1;
then [k,1] in Indices P0 by A23,A24,A18,ZFMISC_1:87;
then
A34: ex p being FinSequence of K st p = P0.k & P0*(k,1) = p.1 by
MATRIX_0:def 5;
assume
A35: k<>1;
then k in NAT & 1 j;
len (Base_FinSeq(K,n,1))=n by Th23;
then ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by A74,A75,
FINSEQ_4:15;
then
A87: (-(a")*(A*(1,j))*(Base_FinSeq(K,n,1))).k =(-(a")*(A*(1,j)))*(
0.K) by A75,A78,A84,Th25
.= 0.K;
A88: (-(a")*(A*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-(a")*(A*(1,j))*(
Base_FinSeq(K,n,1))).k by A70,A74,A75,FINSEQ_4:15;
A89: p.k= 0.K by A66,A67,A85,A86,Th25;
(Base_FinSeq(K,n,j))/.k = (Base_FinSeq(K,n,j)).k by A68,A74,A75,
FINSEQ_4:15
.= 0.K by A74,A75,A86,Th25;
then q.k= 0.K + 0.K by A70,A68,A74,A75,A88,A87,Th5;
hence thesis by A89,RLVECT_1:4;
end;
suppose
A90: k=j;
len (Base_FinSeq(K,n,1))=n by Th23;
then ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by A74,A75,
FINSEQ_4:15;
then
A91: (-(a")*(A*(1,j))*(Base_FinSeq(K,n,1))).k =(-(a")*(A*(1,j)))*(
0.K) by A75,A78,A84,Th25
.= 0.K;
A92: (-(a")*(A*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-(a")*(A*(1,j))*(
Base_FinSeq(K,n,1))).k by A70,A74,A75,FINSEQ_4:15;
A93: p.k=1.K by A74,A75,A85,A90,Th24;
(Base_FinSeq(K,n,j))/.k = (Base_FinSeq(K,n,j)).k by A68,A74,A75,
FINSEQ_4:15
.= 1.K by A74,A75,A90,Th24;
then q.k= 0.K + 1.K by A70,A68,A74,A75,A92,A91,Th5;
hence thesis by A93,RLVECT_1:4;
end;
end;
end;
A94: width A=n by MATRIX_0:24;
then
A95: len Line(A,1) = n by MATRIX_0:def 7;
then
A96: (Line(A,1))/.1 = (Line(A,1)).1 by A3,FINSEQ_4:15
.= a by A44,MATRIX_0:def 7;
A97: j in Seg n by A66,A67,FINSEQ_1:1;
A98: len (Col(P0,j))=len P0 by MATRIX_0:def 8
.=n by MATRIX_0:24;
len (-(a")*(A*(1,j))*(Base_FinSeq(K,n,1))+Base_FinSeq(K,n,j)) =n by A70,A68
,Th2;
then
A99: Col(P0,j)=-(a")*(A*(1,j))*(Base_FinSeq(K,n,1))+Base_FinSeq(K,n,j) by A98
,A72,FINSEQ_1:14;
A100: (Line(A,1))/.j = (Line(A,1)).j by A66,A67,A95,FINSEQ_4:15
.= A*(1,j) by A97,A94,MATRIX_0:def 7;
[1,j] in Indices (A*P0) by A9,A66,A67,MATRIX_0:31;
then (A*P0)*(1,j)= |( Line(A,1), Col(P0,j) )| by A23,A94,MATRIX_3:def 4
.= |( Line(A,1), -(a")*(A*(1,j))*(Base_FinSeq(K,n,1)) )| +|( Line(A,1)
, Base_FinSeq(K,n,j) )| by A42,A70,A68,A99,Th11
.= |( Line(A,1), (-(a")*(A*(1,j)))*(Base_FinSeq(K,n,1)) )| +|( Line(A,
1), Base_FinSeq(K,n,j) )| by Th6
.=(-(a")*(A*(1,j)))* |( Line(A,1), (Base_FinSeq(K,n,1)) )| +|( Line(A,
1), Base_FinSeq(K,n,j) )| by A42,A19,Th10
.=(-(a")*(A*(1,j)))* a +|( Line(A,1), Base_FinSeq(K,n,j) )| by A42,A3,A96
,Th35
.= -((a")*(A*(1,j)))* a +|( Line(A,1), Base_FinSeq(K,n,j) )| by
VECTSP_1:9
.= -((A*(1,j))*((a")* a)) +|( Line(A,1), Base_FinSeq(K,n,j) )| by
GROUP_1:def 3
.= -((A*(1,j))*(1.K)) +|( Line(A,1), Base_FinSeq(K,n,j) )| by A2,
VECTSP_1:def 10
.= -((A*(1,j))*(1.K)) +( Line(A,1))/.j by A42,A66,A67,Th35
.= -(A*(1,j)) + A*(1,j) by A100
.= 0.K by RLVECT_1:5;
hence thesis;
end;
A101: Indices A=[: Seg n,Seg n :] & Indices (A*P0)=[: Seg n,Seg n :] by
MATRIX_0:24;
A102: len (Col(P0,1))=len P0 by MATRIX_0:def 8
.=n by MATRIX_0:24;
len ((a")*(Base_FinSeq(K,n,1)))=len (Base_FinSeq(K,n,1)) by MATRIXR1:16
.= n by Th23;
then
A103: Col(P0,1)=(a")*(Base_FinSeq(K,n,1)) by A102,A25,FINSEQ_1:14;
A104: len ((a")*(Line(A,1)))=len ((Line(A,1))) by MATRIXR1:16
.= n by A41,MATRIX_0:def 7;
[1,1] in Indices A by A3,MATRIX_0:31;
then (A*P0)*(1,1)= |( Line(A,1), Col(P0,1) )| by A23,A41,A101,MATRIX_3:def 4
.= (a")*( |( Line(A,1), Base_FinSeq(K,n,1) )| ) by A42,A19,A103,Th10
.=(a")*(Line(A,1))/.1 by A42,A3,Th35
.=((a")*(Line(A,1)))/.1 by A43,POLYNOM1:def 1
.=((a")*(Line(A,1))).1 by A3,A104,FINSEQ_4:15
.=(a")*(A*(1,1)) by A44,A40,MATRIX12:3
.=1.K by A2,VECTSP_1:def 10;
hence thesis by A22,A65,A45;
end;
theorem Th40:
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**0 and
A2: A*(1,1)<>0.K;
set B=A@;
A3: 0+1<=n by A1,NAT_1:13;
then [1,1] in Indices A by MATRIX_0:31;
then B*(1,1)=A*(1,1) by MATRIX_0:def 6;
then consider P0 being Matrix of n,K such that
A4: P0 is invertible and
A5: (B*P0)*(1,1)=1.K and
A6: 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**0 and
A2: A*(1,1)<>0.K;
consider P being Matrix of n,K such that
A3: P is invertible and
A4: (P*A)*(1,1)=1.K and
A5: for i st 1** Matrix of n,K equals
Swap(1.(K,n),1,i0);
correctness
proof
i0 in NAT by ORDINAL1:def 12;
hence thesis by Th42;
end;
end;
theorem Th43:
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)))
proof
let n be Element of NAT,i0 be Nat,A be Matrix of n,K;
assume
A1: 1<=i0 & i0<=n;
assume
A2: A= SwapDiagonal(K,n,i0);
let i,j be Nat;
assume that
A3: 1<=i and
A4: i<=n and
A5: 1<=j and
A6: j<=n;
A7: [i,j] in Indices A by A3,A4,A5,A6,MATRIX_0:31;
assume
A8: i0<>1;
thus i=1 & j=i0 implies A*(i,j)=1.K
proof
reconsider j0=i0-'2 as Element of NAT;
reconsider f=1.(K,n) as FinSequence of (the carrier of K)*;
assume that
A9: i=1 and
A10: j=i0;
reconsider qq=(f/.i0) as FinSequence of (the carrier of K) by
FINSEQ_1:def 11;
i0 <= len f by A6,A10,MATRIX_0:def 2;
then f/.i0=f.i0 by A5,A10,FINSEQ_4:15
.=Base_FinSeq(K,n,i0) by A5,A6,A10,Th26;
then
A11: qq.j=1.K by A5,A6,A10,Th24;
reconsider g=f/^1 as FinSequence of (the carrier of K)*;
A12: len f=n by MATRIX_0:def 2;
reconsider h= (g|j0) as FinSequence of (the carrier of K)*;
len ((<*f/.i0*>)^h) = len (<*f/.i0*>)+len (h) by FINSEQ_1:22
.= 1+len (h) by FINSEQ_1:39;
then
A13: 1<= len ((<*f/.i0*>)^h) by NAT_1:11;
A14: 1= len (<*f/.i0*>) by FINSEQ_1:39;
1)^h^<*f/.1*>^(f/^i0)).i by A2,A6,A10,A12,FINSEQ_7:28
.= ((<*f/.i0*>)^h^(<*f/.1*>^(f/^i0))).i by FINSEQ_1:32
.= (<*f/.i0*>^h).1 by A9,A13,FINSEQ_1:64
.= (<*f/.i0*>).1 by A14,FINSEQ_1:64
.= f/.i0 by FINSEQ_1:def 8;
hence thesis by A7,A11,MATRIX_0:def 5;
end;
A15: len A=n by MATRIX_0:24;
A16: 1<=n by A3,A4,XXREAL_0:2;
thus i=i0 & j=1 implies A*(i,j)=1.K
proof
reconsider f=1.(K,n) as FinSequence of (the carrier of K)*;
assume that
A17: i=i0 and
A18: j=1;
reconsider qq=(f/.1) as FinSequence of (the carrier of K) by
FINSEQ_1:def 11;
A19: len f=n by MATRIX_0:def 2;
then f/.1=f.1 by A16,FINSEQ_4:15
.=Base_FinSeq(K,n,1) by A16,Th26;
then
A20: qq.j=1.K by A6,A18,Th24;
A.i=A/.i by A15,A3,A4,FINSEQ_4:15
.=f/.1 by A2,A3,A4,A6,A17,A18,A19,FINSEQ_7:31;
hence thesis by A7,A20,MATRIX_0:def 5;
end;
thus i=1 & j=1 implies A*(i,j)=0.K
proof
reconsider f=1.(K,n) as FinSequence of (the carrier of K)*;
assume that
A21: i=1 and
A22: j=1;
reconsider qq=(f/.i0) as FinSequence of (the carrier of K) by
FINSEQ_1:def 11;
A23: len f=n by MATRIX_0:def 2;
then f/.i0=f.i0 by A1,FINSEQ_4:15
.=Base_FinSeq(K,n,i0) by A1,Th26;
then
A24: qq.j=0.K by A4,A8,A21,A22,Th25;
A.i=A/.i by A15,A3,A4,FINSEQ_4:15
.=f/.i0 by A1,A2,A4,A21,A23,FINSEQ_7:31;
hence thesis by A7,A24,MATRIX_0:def 5;
end;
thus i=i0 & j=i0 implies A*(i,j)=0.K
proof
reconsider f=1.(K,n) as FinSequence of (the carrier of K)*;
assume that
A25: i=i0 and
A26: j=i0;
reconsider qq=(f/.1) as FinSequence of (the carrier of K) by
FINSEQ_1:def 11;
A27: len f=n by MATRIX_0:def 2;
then f/.1=f.1 by A16,FINSEQ_4:15
.=Base_FinSeq(K,n,1) by A16,Th26;
then
A28: qq.j=0.K by A1,A8,A26,Th25;
A.i=A/.i by A15,A3,A4,FINSEQ_4:15
.=f/.1 by A2,A3,A4,A16,A25,A27,FINSEQ_7:31;
hence thesis by A7,A28,MATRIX_0:def 5;
end;
assume
A29: not ((i=1 or i=i0) &(j=1 or j=i0));
per cases by A29;
suppose
A30: i<>1 & i<>i0;
thus i=j implies A*(i,j)=1.K
proof
reconsider f=1.(K,n) as FinSequence of (the carrier of K)*;
assume
A31: i=j;
reconsider qq=(f/.i) as FinSequence of (the carrier of K) by
FINSEQ_1:def 11;
j <= len f by A6,MATRIX_0:def 2;
then f/.i=f.i by A5,A31,FINSEQ_4:15
.=Base_FinSeq(K,n,i) by A3,A4,Th26;
then
A32: qq.j=1.K by A3,A4,A31,Th24;
A33: len f=n by MATRIX_0:def 2;
A.i=A/.i by A15,A3,A4,FINSEQ_4:15
.=f/.i by A2,A3,A4,A30,A33,FINSEQ_7:30;
hence thesis by A7,A32,MATRIX_0:def 5;
end;
thus i<>j implies A*(i,j)=0.K
proof
reconsider f=1.(K,n) as FinSequence of (the carrier of K)*;
assume
A34: i<>j;
reconsider qq=(f/.i) as FinSequence of (the carrier of K) by
FINSEQ_1:def 11;
A35: len f=n by MATRIX_0:def 2;
then f/.i=f.i by A3,A4,FINSEQ_4:15
.=Base_FinSeq(K,n,i) by A3,A4,Th26;
then
A36: qq.j=0.K by A5,A6,A34,Th25;
A.i=A/.i by A15,A3,A4,FINSEQ_4:15
.=f/.i by A2,A3,A4,A30,A35,FINSEQ_7:30;
hence thesis by A7,A36,MATRIX_0:def 5;
end;
end;
suppose
A37: j<>1 & j<>i0;
thus i=j implies A*(i,j)=1.K
proof
reconsider f=1.(K,n) as FinSequence of (the carrier of K)*;
assume
A38: i=j;
reconsider qq=(f/.i) as FinSequence of (the carrier of K) by
FINSEQ_1:def 11;
j <= len f by A6,MATRIX_0:def 2;
then f/.i=f.i by A5,A38,FINSEQ_4:15
.=Base_FinSeq(K,n,i) by A3,A4,Th26;
then
A39: qq.j=1.K by A3,A4,A38,Th24;
A40: len f=n by MATRIX_0:def 2;
A.i=A/.i by A15,A3,A4,FINSEQ_4:15
.=f/.i by A2,A3,A4,A37,A38,A40,FINSEQ_7:30;
hence thesis by A7,A39,MATRIX_0:def 5;
end;
thus i<>j implies A*(i,j)=0.K
proof
assume
A41: i<>j;
per cases;
suppose
A42: not(i=1 or i=i0);
reconsider f=1.(K,n) as FinSequence of (the carrier of K)*;
reconsider qq=(f/.i) as FinSequence of (the carrier of K) by
FINSEQ_1:def 11;
A43: len f=n by MATRIX_0:def 2;
then f/.i=f.i by A3,A4,FINSEQ_4:15
.=Base_FinSeq(K,n,i) by A3,A4,Th26;
then
A44: qq.j=0.K by A5,A6,A41,Th25;
A.i=A/.i by A15,A3,A4,FINSEQ_4:15
.=f/.i by A2,A3,A4,A42,A43,FINSEQ_7:30;
hence thesis by A7,A44,MATRIX_0:def 5;
end;
suppose
A45: i=1 or i=i0;
per cases by A45;
suppose
A46: i=1;
reconsider f=1.(K,n) as FinSequence of (the carrier of K)*;
reconsider qq=(f/.i0) as FinSequence of (the carrier of K) by
FINSEQ_1:def 11;
A47: len f=n by MATRIX_0:def 2;
then f/.i0=f.i0 by A1,FINSEQ_4:15
.=Base_FinSeq(K,n,i0) by A1,Th26;
then
A48: qq.j=0.K by A5,A6,A37,Th25;
A.i=A/.i by A15,A3,A4,FINSEQ_4:15
.=f/.i0 by A1,A2,A4,A46,A47,FINSEQ_7:31;
hence thesis by A7,A48,MATRIX_0:def 5;
end;
suppose
A49: i=i0;
reconsider f=1.(K,n) as FinSequence of (the carrier of K)*;
reconsider qq=(f/.1) as FinSequence of (the carrier of K) by
FINSEQ_1:def 11;
A50: len f=n by MATRIX_0:def 2;
then f/.1=f.1 by A16,FINSEQ_4:15
.=Base_FinSeq(K,n,1) by A16,Th26;
then
A51: qq.j=0.K by A5,A6,A37,Th25;
A.i=A/.i by A15,A3,A4,FINSEQ_4:15
.=f/.1 by A2,A3,A4,A16,A49,A50,FINSEQ_7:31;
hence thesis by A7,A51,MATRIX_0:def 5;
end;
end;
end;
end;
end;
theorem Th44:
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
proof
let n be Element of NAT, A be Matrix of n,K;
set A= SwapDiagonal(K,n,1);
let i be Nat;
assume 1<=i & i<=n;
then A=1.(K,n) & [i,i] in Indices A by FINSEQ_7:19,MATRIX_0:31;
hence thesis by MATRIX_1:def 3;
end;
theorem Th45:
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)
proof
let n be Element of NAT, A be Matrix of n,K;
set A= SwapDiagonal(K,n,1);
let i,j be Nat;
assume 1<=i & i<=n & 1<=j & j<=n;
then
A1: [i,j] in Indices A by MATRIX_0:31;
A=1.(K,n) by FINSEQ_7:19;
hence thesis by A1,MATRIX_1:def 3;
end;
theorem Th46:
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)
proof
let K;
let n,i0 be Element of NAT,A be Matrix of n,K;
assume
A1: i0 = 1;
assume
A2: 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);
for i,j being Nat st [i,j] in Indices A holds A*(i,j) = (SwapDiagonal(K,
n,i0))*(i,j)
proof
let i,j be Nat;
assume
A3: [i,j] in Indices A;
Indices A = [:Seg n, Seg n:] by MATRIX_0:24;
then i in Seg n by A3,ZFMISC_1:87;
then
A4: 1<=i & i<=n by FINSEQ_1:1;
then
A5: i=j implies A*(i,j)=1.K by A2;
width A = n by MATRIX_0:24;
then j in Seg n by A3,ZFMISC_1:87;
then
A6: 1<=j & j<=n by FINSEQ_1:1;
then i<>j implies A*(i,j)=0.K by A2,A4;
hence thesis by A1,A4,A6,A5,Th44,Th45;
end;
hence thesis by MATRIX_0:27;
end;
theorem Th47:
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)
proof
let K;
let n,i0 be Element of NAT,A be Matrix of n,K;
assume
A1: 1<=i0 & i0<=n & i0<>1;
assume
A2: 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));
for i,j being Nat st [i,j] in Indices A holds A*(i,j) = (SwapDiagonal(K,
n,i0))*(i,j)
proof
let i,j be Nat;
assume
A3: [i,j] in Indices A;
Indices A = [:Seg n, Seg n:] by MATRIX_0:24;
then
A4: i in Seg n by A3,ZFMISC_1:87;
then
A5: 1<=i by FINSEQ_1:1;
A6: i=i0 & j=i0 implies (SwapDiagonal(K,n,i0))*(i,j)=0.K by A1,Th43;
width A = n by MATRIX_0:24;
then
A7: j in Seg n by A3,ZFMISC_1:87;
then
A8: 1<=j by FINSEQ_1:1;
A9: i<=n by A4,FINSEQ_1:1;
then
A10: i=i0 & j=i0 implies A*(i,j)=0.K by A2,A5;
A11: j<=n by A7,FINSEQ_1:1;
then
A12: i=1 & j=i0 implies A*(i,j)=1.K by A2,A9,A8;
A13: i=1 & j=1 implies (SwapDiagonal(K,n,i0))*(i,j)=0.K by A1,A9,Th43;
A14: i=1 & j=1 implies A*(i,j)=0.K by A2,A9;
A15: i=i0 & j=1 implies A*(i,j)=1.K by A2,A5,A9,A11;
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) by A2,A5,A9,A8,A11;
hence thesis by A1,A5,A9,A8,A11,A12,A15,A14,A10,A13,A6,Th43;
end;
hence thesis by MATRIX_0:27;
end;
theorem Th48:
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))
proof
let A be (Matrix of n,K),i0 be Element of NAT;
assume that
A1: 1<=i0 and
A2: i0 <=n;
thus 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)
proof
set Q=(SwapDiagonal(K,n,i0)) ,P=A;
let j;
A3: width Q=n by MATRIX_0:24;
A4: 1<=n by A1,A2,XXREAL_0:2;
A5: for j2 being Nat st j2 in Seg width Q holds (Base_FinSeq(K,n,i0)).j2
= Q*(1,j2)
proof
let j2 be Nat;
reconsider j3=j2 as Element of NAT by ORDINAL1:def 12;
assume
A6: j2 in Seg width Q;
then
A7: 1<=j2 by FINSEQ_1:1;
A8: j2<=n by A3,A6,FINSEQ_1:1;
now
per cases;
suppose
A9: i0<>1;
now
per cases;
suppose
i0=1 & j2=i0;
hence thesis by A9;
end;
suppose
A10: i0=i0 & j2=1;
then (SwapDiagonal(K,n,i0))*(1,j3)=0.K by A1,A2,A8,A9,Th43;
hence thesis by A4,A9,A10,Th25;
end;
suppose
i0=1 & j2=1;
hence thesis by A9;
end;
suppose
A11: i0=i0 & j2=i0;
then (SwapDiagonal(K,n,i0))*(1,j3)=1.K by A1,A2,A4,A9,Th43;
hence thesis by A7,A8,A11,Th24;
end;
suppose
A12: not ((i0=1 or i0=i0) &(j2=1 or j2=i0));
now
per cases;
suppose
i0=j2;
hence thesis by A12;
end;
suppose
A13: i0<>j2;
(SwapDiagonal(K,n,i0))*(1,j3)=0.K by A1,A2,A4,A7,A8,A9,A12
,Th43;
hence thesis by A7,A8,A13,Th25;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose
A14: i0=1;
now
per cases;
suppose
A15: i0=j2;
then (SwapDiagonal(K,n,i0))*(1,j3)=1.K by A8,A14,Th44;
hence thesis by A7,A8,A15,Th24;
end;
suppose
A16: i0<>j2;
then (SwapDiagonal(K,n,i0))*(1,j3)=0.K by A2,A7,A8,A14,Th45;
hence thesis by A7,A8,A16,Th25;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
assume
A17: 1<=j & j<=n;
then 1<=n by XXREAL_0:2;
then
A18: Indices (Q*P)=[: Seg n,Seg n :] & 1 in Seg n by FINSEQ_1:1,MATRIX_0:24;
A19: 1<=n by A1,A2,XXREAL_0:2;
A20: for j2 being Nat st j2 in Seg width Q holds (Base_FinSeq(K,n,1)).j2 =
Q*(i0,j2)
proof
let j2 be Nat;
reconsider j3=j2 as Element of NAT by ORDINAL1:def 12;
assume
A21: j2 in Seg width Q;
then
A22: 1<=j2 by FINSEQ_1:1;
A23: j2<=n by A3,A21,FINSEQ_1:1;
now
per cases;
suppose
A24: i0<>1;
now
per cases;
suppose
i0=1 & j2=i0;
hence thesis by A24;
end;
suppose
A25: i0=i0 & j2=1;
then (SwapDiagonal(K,n,i0))*(i0,j3)=1.K by A1,A2,A19,A24,Th43;
hence thesis by A23,A25,Th24;
end;
suppose
i0=1 & j2=1;
hence thesis by A24;
end;
suppose
A26: i0=i0 & j2=i0;
then (SwapDiagonal(K,n,i0))*(i0,j3)=0.K by A22,A23,A24,Th43;
hence thesis by A1,A2,A24,A26,Th25;
end;
suppose
A27: not ((i0=1 or i0=i0) &(j2=1 or j2=i0));
now
(SwapDiagonal(K,n,i0))*(i0,j3)=0.K by A1,A2,A22,A23,A24,A27
,Th43;
hence thesis by A22,A23,A27,Th25;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose
A28: i0=1;
now
per cases;
suppose
A29: i0=j2;
then (SwapDiagonal(K,n,i0))*(i0,j3)=1.K by A23,A28,Th44;
hence thesis by A23,A28,A29,Th24;
end;
suppose
A30: i0<>j2;
then (SwapDiagonal(K,n,1))*(i0,j3)=0.K by A1,A2,A22,A23,Th45;
hence thesis by A22,A23,A28,A30,Th25;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
len (Base_FinSeq(K,n,1)) = n by Th23
.= width Q by MATRIX_0:24;
then
A31: Line(Q,i0)=Base_FinSeq(K,n,1) by A20,MATRIX_0:def 7;
A32: len P=n by MATRIX_0:24;
then
A33: len (Col(P,j))=n by MATRIX_0:def 8;
A34: 1<=n by A17,XXREAL_0:2;
then 1 in Seg n by FINSEQ_1:1;
then
A35: 1 in dom P by A32,FINSEQ_1:def 3;
j in Seg n by A17,FINSEQ_1:1;
then
A36: [1,j] in Indices (Q*P) by A18,ZFMISC_1:87;
[i0,j] in Indices (Q*P) by A1,A2,A17,MATRIX_0:31;
hence ((SwapDiagonal(K,n,i0))*A)*(i0,j) = |( Base_FinSeq(K,n,1),Col(P,j))|
by A3,A32,A31,MATRIX_3:def 4
.= |( Col(P,j),Base_FinSeq(K,n,1) )| by FVSUM_1:90
.= (Col(P,j)).1 by A34,A33,Th35
.=A*(1,j) by A35,MATRIX_0:def 8;
i0 in Seg n by A1,A2,FINSEQ_1:1;
then
A37: i0 in dom P by A32,FINSEQ_1:def 3;
len (Base_FinSeq(K,n,i0)) = n by Th23
.= width Q by MATRIX_0:24;
then Line(Q,1)=Base_FinSeq(K,n,i0) by A5,MATRIX_0:def 7;
hence ((SwapDiagonal(K,n,i0))*A)*(1,j) = |( Base_FinSeq(K,n,i0),Col(P,j))|
by A3,A32,A36,MATRIX_3:def 4
.= |( Col(P,j),Base_FinSeq(K,n,i0) )| by FVSUM_1:90
.= (Col(P,j)).i0 by A1,A2,A33,Th35
.=A*(i0,j) by A37,MATRIX_0:def 8;
end;
thus 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)
proof
set Q=(SwapDiagonal(K,n,i0)) ,P=A;
let i,j;
assume that
A38: i<>1 and
A39: i<>i0 and
A40: 1<=i & i<=n and
A41: 1<=j & j<=n;
A42: len P=n by MATRIX_0:24;
then
A43: len (Col(P,j))=n by MATRIX_0:def 8;
A44: width Q=n by MATRIX_0:24;
A45: for j2 being Nat st j2 in Seg width Q holds (Base_FinSeq(K,n,i)).j2 =
Q*(i,j2)
proof
let j2 be Nat;
reconsider j3=j2 as Element of NAT by ORDINAL1:def 12;
assume j2 in Seg width Q;
then
A46: 1<=j2 & j2<=n by A44,FINSEQ_1:1;
now
per cases;
suppose
A47: i0<>1;
now
per cases;
suppose
i=1 & j2=i0;
hence thesis by A38;
end;
suppose
i=i0 & j2=1;
hence thesis by A39;
end;
suppose
i=1 & j2=1;
hence thesis by A38;
end;
suppose
i=i0 & j2=i0;
hence thesis by A39;
end;
suppose
A48: not ((i=1 or i=i0) &(j2=1 or j2=i0));
now
per cases;
suppose
A49: i=j2;
then
(SwapDiagonal(K,n,i0))*(i,j3)=1.K by A1,A2,A46,A47,A48,Th43;
hence thesis by A40,A49,Th24;
end;
suppose
A50: i<>j2;
then
(SwapDiagonal(K,n,i0))*(i,j3)=0.K by A1,A2,A38,A39,A40,A46
,A47,Th43;
hence thesis by A46,A50,Th25;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose
A51: i0=1;
now
per cases;
suppose
A52: i=j2;
then (SwapDiagonal(K,n,i0))*(i,j3)=1.K by A46,A51,Th44;
hence thesis by A46,A52,Th24;
end;
suppose
A53: i<>j2;
then (SwapDiagonal(K,n,i0))*(i,j3)=0.K by A40,A46,A51,Th45;
hence thesis by A46,A53,Th25;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
i in Seg n by A40,FINSEQ_1:1;
then
A54: i in dom P by A42,FINSEQ_1:def 3;
len (Base_FinSeq(K,n,i)) = n by Th23
.= width Q by MATRIX_0:24;
then
A55: Line(Q,i)=Base_FinSeq(K,n,i) by A45,MATRIX_0:def 7;
[i,j] in Indices (Q*P) by A40,A41,MATRIX_0:31;
hence ((SwapDiagonal(K,n,i0))*A)*(i,j) = |( Base_FinSeq(K,n,i),Col(P,j))|
by A44,A42,A55,MATRIX_3:def 4
.= |( Col(P,j),Base_FinSeq(K,n,i) )| by FVSUM_1:90
.= (Col(P,j)).i by A40,A43,Th35
.=A*(i,j) by A54,MATRIX_0:def 8;
end;
end;
theorem Th49:
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)
proof
let i0 be Element of NAT;
assume that
A1: 1<=i0 and
A2: i0<=n;
A3: 1<=n by A1,A2,XXREAL_0:2;
set R=(SwapDiagonal(K,n,i0))*(SwapDiagonal(K,n,i0));
A4: Indices R=[: Seg n,Seg n :] by MATRIX_0:24;
A5: width R=n by MATRIX_0:24;
A6: for i4,j4 being Nat st [i4,j4] in Indices R holds R*(i4,j4) = (1.(K,n))
*(i4,j4)
proof
let i4,j4 be Nat;
reconsider i=i4,j=j4 as Element of NAT by ORDINAL1:def 12;
assume
A7: [i4,j4] in Indices R;
then
A8: [i,j] in Indices (1.(K,n)) by A4,MATRIX_0:24;
j in Seg n by A5,A7,ZFMISC_1:87;
then
A9: 1<=j & j<=n by FINSEQ_1:1;
A10: i in Seg n by A4,A7,ZFMISC_1:87;
then
A11: 1<=i by FINSEQ_1:1;
A12: i<=n by A10,FINSEQ_1:1;
per cases by A11,XXREAL_0:1;
suppose
A13: 1**i0;
now
per cases;
suppose
A15: i=j;
A16: now
per cases;
suppose
i0<>1;
hence (SwapDiagonal(K,n,i0))*(i,j)=1.K by A1,A2,A12,A13,A14
,A15,Th43;
end;
suppose
i0=1;
hence (SwapDiagonal(K,n,i0))*(i,j)=1.K by A11,A12,A15,Th44;
end;
end;
(1.(K,n))*(i,j)= 1.K by A8,A15,MATRIX_1:def 3;
hence R*(i,j) = (1.(K,n))*(i,j) by A1,A2,A12,A9,A13,A14,A16,Th48;
end;
suppose
A17: i<>j;
A18: now
per cases;
suppose
i0=1;
hence (SwapDiagonal(K,n,i0))*(i,j)=0.K by A11,A12,A9,A17,Th45
;
end;
suppose
i0<>1;
hence (SwapDiagonal(K,n,i0))*(i,j)=0.K by A1,A2,A12,A9,A13
,A14,A17,Th43;
end;
end;
(1.(K,n))*(i,j)=0.K by A8,A17,MATRIX_1:def 3;
hence R*(i,j) = (1.(K,n))*(i,j) by A1,A2,A12,A9,A13,A14,A18,Th48;
end;
end;
hence R*(i,j) = (1.(K,n))*(i,j);
end;
suppose
A19: i=i0;
now
per cases;
suppose
A20: i=j;
A21: now
per cases;
suppose
i0=1;
hence (SwapDiagonal(K,n,i0))*(1,i0)=1.K by A13,A19;
end;
suppose
i0<>1;
hence (SwapDiagonal(K,n,i0))*(1,i0)=1.K by A1,A2,A3,Th43;
end;
end;
(1.(K,n))*(i,j)=1.K by A8,A20,MATRIX_1:def 3;
hence R*(i,j) = (1.(K,n))*(i,j) by A1,A2,A19,A20,A21,Th48;
end;
suppose
A22: i<>j;
A23: now
now
per cases;
suppose
j=1;
hence (SwapDiagonal(K,n,i0))*(1,j)=0.K by A2,A3,A13,A19
,Th43;
end;
suppose
j<>1;
hence
(SwapDiagonal(K,n,i0))*(1,j)=0.K by A3,A12,A9,A13,A19,A22
,Th43;
end;
end;
hence (SwapDiagonal(K,n,i0))*(1,j)=0.K;
end;
(1.(K,n))*(i,j)=0.K by A8,A22,MATRIX_1:def 3;
hence R*(i,j) = (1.(K,n))*(i,j) by A11,A12,A9,A19,A23,Th48;
end;
end;
hence R*(i,j) = (1.(K,n))*(i,j);
end;
end;
hence thesis;
end;
suppose
A24: 1=i;
now
per cases;
suppose
A25: i0<>1;
per cases;
suppose
A26: j<>1;
A27: now
per cases;
suppose
j=i0;
hence (SwapDiagonal(K,n,i0))*(i0,j)=0.K by A9,A26,Th43;
end;
suppose
j<>i0;
hence (SwapDiagonal(K,n,i0))*(i0,j)=0.K by A1,A2,A9,A25,A26
,Th43;
end;
end;
(1.(K,n))*(i,j)=0.K by A8,A24,A26,MATRIX_1:def 3;
hence R*(i,j) = (1.(K,n))*(i,j) by A1,A2,A9,A24,A27,Th48;
end;
suppose
j=1;
then (1.(K,n))*(i,j)= 1.K & (SwapDiagonal(K,n,i0))*(i0,j)=1.K by A1
,A2,A3,A8,A24,A25,Th43,MATRIX_1:def 3;
hence R*(i,j) = (1.(K,n))*(i,j) by A1,A2,A9,A24,Th48;
end;
end;
suppose
A28: i0=1;
now
per cases;
suppose
i<>j;
then (1.(K,n))*(i,j)=0.K & (SwapDiagonal(K,n,1))*(1,j)=0.K by A12
,A9,A8,A24,Th45,MATRIX_1:def 3;
hence R*(i,j) = (1.(K,n))*(i,j) by A12,A9,A24,A28,Th48;
end;
suppose
A29: i=j;
then
A30: (1.(K,n))*(j,j)= 1.K by A8,MATRIX_1:def 3;
((SwapDiagonal(K,n,i0))*(SwapDiagonal(K,n,i0)))*(1,j) =(
SwapDiagonal(K,n,i0))*(i0,j) by A1,A2,A9,Th48;
hence R*(i,j) = (1.(K,n))*(i,j) by A2,A24,A28,A29,A30,Th44;
end;
end;
hence R*(i,j) = (1.(K,n))*(i,j);
end;
end;
hence thesis;
end;
end;
width (1.(K,n))=n by MATRIX_0:24;
then
A31: width R = width (1.(K,n)) by MATRIX_0:24;
len (1.(K,n))=n by MATRIX_0:24;
then len R = len (1.(K,n)) by MATRIX_0:24;
then
A32: (SwapDiagonal(K,n,i0))*(SwapDiagonal(K,n,i0))=1.(K,n) by A31,A6,
MATRIX_0:21;
hence SwapDiagonal(K,n,i0) is invertible by Th19;
thus thesis by A32,Th18;
end;
theorem Th50:
for i0 being Element of NAT st 1<=i0 & i0<=n holds (SwapDiagonal
(K,n,i0))@=(SwapDiagonal(K,n,i0))
proof
let i0 be Element of NAT;
assume
A1: 1<=i0 & i0<=n;
per cases;
suppose
A2: i0<> 1;
for i,j being Nat st 1<=i & i<=n & 1<=j & j<=n holds (i=1 & j=i0
implies (SwapDiagonal(K,n,i0))@ *(i,j)=1.K)& (i=i0 & j=1 implies (SwapDiagonal(
K,n,i0))@ *(i,j)=1.K)& (i=1 & j=1 implies (SwapDiagonal(K,n,i0))@ *(i,j)= 0.K)&
(i=i0 & j=i0 implies (SwapDiagonal(K,n,i0))@ *(i,j)= 0.K)& (not ((i=1 or i=i0)
&(j=1 or j=i0)) implies (i=j implies SwapDiagonal(K,n,i0)@ *(i,j)=1.K)& (i<>j
implies SwapDiagonal(K,n,i0)@*(i,j)=0.K))
proof
A3: Indices (SwapDiagonal(K,n,i0))=[: Seg n,Seg n :] by MATRIX_0:24;
let i,j be Nat;
assume that
A4: 1<=i and
A5: i<=n and
A6: 1<=j and
A7: j<=n;
A8: i in Seg n & j in Seg n by A4,A5,A6,A7,FINSEQ_1:1;
hereby
assume
A9: i=1 & j=i0;
[j,i] in Indices (SwapDiagonal(K,n,i0)) by A8,A3,ZFMISC_1:87;
hence (SwapDiagonal(K,n,i0))@ *(i,j)=(SwapDiagonal(K,n,i0)) *(j,i) by
MATRIX_0:def 6
.=1.K by A2,A5,A6,A7,A9,Th43;
end;
hereby
assume
A10: i=i0 & j=1;
[j,i] in Indices (SwapDiagonal(K,n,i0)) by A8,A3,ZFMISC_1:87;
hence (SwapDiagonal(K,n,i0))@ *(i,j)=(SwapDiagonal(K,n,i0)) *(j,i) by
MATRIX_0:def 6
.=1.K by A2,A4,A5,A7,A10,Th43;
end;
hereby
assume
A11: i=1 & j=1;
[j,i] in Indices (SwapDiagonal(K,n,i0)) by A8,A3,ZFMISC_1:87;
hence (SwapDiagonal(K,n,i0))@ *(i,j)=(SwapDiagonal(K,n,i0)) *(j,i) by
MATRIX_0:def 6
.= 0.K by A1,A2,A5,A11,Th43;
end;
hereby
assume
A12: i=i0 & j=i0;
[j,i] in Indices (SwapDiagonal(K,n,i0)) by A8,A3,ZFMISC_1:87;
hence (SwapDiagonal(K,n,i0))@ *(i,j)=(SwapDiagonal(K,n,i0)) *(j,i) by
MATRIX_0:def 6
.= 0.K by A2,A4,A5,A12,Th43;
end;
hereby
assume
A13: not ((i=1 or i=i0) &(j=1 or j=i0));
A14: [j,i] in Indices (SwapDiagonal(K,n,i0)) by A8,A3,ZFMISC_1:87;
A15: now
assume
A16: i=j;
thus (SwapDiagonal(K,n,i0))@ *(i,j)=(SwapDiagonal(K,n,i0)) *(j,i) by
A14,MATRIX_0:def 6
.=1.K by A1,A2,A4,A5,A13,A16,Th43;
end;
now
assume
A17: i<>j;
thus (SwapDiagonal(K,n,i0))@ *(i,j)=(SwapDiagonal(K,n,i0)) *(j,i) by
A14,MATRIX_0:def 6
.= 0.K by A1,A2,A4,A5,A6,A7,A13,A17,Th43;
end;
hence
(i=j implies (SwapDiagonal(K,n,i0))@ *(i,j)=1.K)& (i<>j implies (
SwapDiagonal(K,n,i0))@ *(i,j)= 0.K) by A15;
end;
end;
hence thesis by A1,A2,Th47;
end;
suppose
A18: i0=1;
for i,j being Nat st 1<=i & i<=n & 1<=j & j<=n holds (i=j implies (
SwapDiagonal(K,n,i0))@ *(i,j)=1.K)& (i<>j implies (SwapDiagonal(K,n,i0))@ *(i,j
)= 0.K)
proof
A19: Indices (SwapDiagonal(K,n,i0))=[: Seg n,Seg n :] by MATRIX_0:24;
let i,j be Nat;
assume that
A20: 1<=i & i<=n and
A21: 1<=j & j<=n;
i in Seg n & j in Seg n by A20,A21,FINSEQ_1:1;
then
A22: [j,i] in Indices (SwapDiagonal(K,n,i0)) by A19,ZFMISC_1:87;
hereby
assume
A23: i=j;
thus (SwapDiagonal(K,n,i0))@ *(i,j)=(SwapDiagonal(K,n,i0)) *(j,i) by
A22,MATRIX_0:def 6
.=1.K by A18,A20,A23,Th44;
end;
hereby
assume
A24: i<>j;
thus (SwapDiagonal(K,n,i0))@ *(i,j)=(SwapDiagonal(K,n,i0)) *(j,i) by
A22,MATRIX_0:def 6
.= 0.K by A18,A20,A21,A24,Th45;
end;
end;
hence thesis by A18,Th46;
end;
end;
theorem Th51:
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))
proof
let A be (Matrix of n,K),j0 be Element of NAT;
assume
A1: 1<=j0 & j0 <=n;
A2: ((SwapDiagonal(K,n,j0))*(A@))@=(A@@)*((SwapDiagonal(K,n,j0))@) by Th30
.= A*((SwapDiagonal(K,n,j0))@) by MATRIXR2:29
.= A*(SwapDiagonal(K,n,j0)) by A1,Th50;
A3: 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)
proof
let i;
assume
A4: 1<=i & i<=n;
then
A5: 1<=n by XXREAL_0:2;
then
A6: [i,1] in Indices A by A4,MATRIX_0:31;
[j0,i] in Indices ((SwapDiagonal(K,n,j0))*(A@)) by A1,A4,MATRIX_0:31;
hence (A*(SwapDiagonal(K,n,j0)))*(i,j0) =(((SwapDiagonal(K,n,j0))*(A@)))*(
j0,i) by A2,MATRIX_0:def 6
.=(A@)*(1,i) by A1,A4,Th48
.=A*(i,1) by A6,MATRIX_0:def 6;
A7: [i,j0] in Indices A by A1,A4,MATRIX_0:31;
[1,i] in Indices ((SwapDiagonal(K,n,j0))*(A@)) by A4,A5,MATRIX_0:31;
hence
(A*(SwapDiagonal(K,n,j0)))*(i,1) =(((SwapDiagonal(K,n,j0))*(A@)))*(1,
i) by A2,MATRIX_0:def 6
.=(A@)*(j0,i) by A1,A4,Th48
.=A*(i,j0) by A7,MATRIX_0:def 6;
end;
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)
proof
let i,j;
assume that
A8: j<>1 & j<>j0 and
A9: 1<=i & i<=n & 1<=j & j<=n;
A10: [i,j] in Indices A by A9,MATRIX_0:31;
[j,i] in Indices ((SwapDiagonal(K,n,j0))*(A@)) by A9,MATRIX_0:31;
hence
(A*(SwapDiagonal(K,n,j0)))*(i,j) =(((SwapDiagonal(K,n,j0))*(A@)))*(j,
i) by A2,MATRIX_0:def 6
.=(A@)*(j,i) by A1,A8,A9,Th48
.=A*(i,j) by A10,MATRIX_0:def 6;
end;
hence thesis by A3;
end;
theorem Th52:
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
proof
let A be Matrix of n,K;
A1: width A=n by MATRIX_0:24;
thus A=0.(K,n) implies for i,j st 1<=i & i<=n & 1<=j & j<=n holds A*(i,j)=
0.K
proof
assume A=0.(K,n);
then
A2: A=0.(K,n,n) by MATRIX_3:def 1;
thus for i,j st 1<=i & i<=n & 1<=j & j<=n holds A*(i,j)= 0.K
proof
let i,j;
assume 1<=i & i<=n & 1<=j & j<=n;
then [i,j] in Indices A by MATRIX_0:31;
hence thesis by A2,MATRIX_3:1;
end;
end;
assume
A3: for i,j st 1<=i & i<=n & 1<=j & j<=n holds A*(i,j)=0.K;
A4: Indices A=[: Seg n,Seg n :] by MATRIX_0:24;
A5: for i,j being Nat st [i,j] in Indices A holds A*(i,j)=(A+A)*(i,j)
proof
let i,j be Nat;
reconsider i0=i,j0=j as Element of NAT by ORDINAL1:def 12;
assume
A6: [i,j] in Indices A;
then j in Seg n by A1,ZFMISC_1:87;
then
A7: 1<=j & j<=n by FINSEQ_1:1;
i in Seg n by A4,A6,ZFMISC_1:87;
then 1<=i & i<=n by FINSEQ_1:1;
then A*(i0,j0)= 0.K by A3,A7;
then (A+A)*(i,j) = 0.K+(A*(i,j)) by A6,MATRIX_3:def 3
.= A*(i,j) by RLVECT_1:4;
hence thesis;
end;
len A=n by MATRIX_0:24;
then A = 0.(K,n,n) by A1,A5,MATRIX_0:27,MATRIX_4:6;
hence thesis by MATRIX_3:def 1;
end;
begin :: Left/Right Invertibility and Invertibility
theorem Th53:
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** 0.(K,n);
then consider i0,j0 being Element of NAT such that
A1: 1<=i0 & i0<=n and
A2: 1<=j0 & j0<=n and
A3: A*(i0,j0)<>0.K by Th52;
set A3=((SwapDiagonal(K,n,i0))*A)*(SwapDiagonal(K,n,j0));
set A2= ((SwapDiagonal(K,n,i0))*A);
1<=n by A1,XXREAL_0:2;
then
(((SwapDiagonal(K,n,i0))*A)*(SwapDiagonal(K,n,j0)))*(1,1) =A2*(1,j0) by A2
,Th51
.=A*(i0,j0) by A1,A2,Th48;
then consider P,Q being Matrix of n,K such that
A4: P is invertible and
A5: Q is invertible and
A6: ( (P*A3*Q)*(1,1)=1.K & for i st 1**)=1 by FINSEQ_1:40;
deffunc f(Nat,Nat)=A3*($1+1,$2+1);
A24: len (A2*C)= k+1 by MATRIX_0:24;
consider F being Matrix of k,k,K such that
A25: for i,j being Nat st [i,j] in Indices F holds F*(i,j) = f(i,j
) from MATRIX_0:sch 1;
A26: len F=k by MATRIX_0:24;
deffunc g(Nat,Nat)=B3*($1+1,$2+1);
A27: len C=k+1 by MATRIX_0:24;
consider G being Matrix of k,k,K such that
A28: for i,j being Nat st [i,j] in Indices G holds G*(i,j) = g(i,j
) from MATRIX_0:sch 1;
A29: len A3=k+1 by MATRIX_0:24;
A30: B3*A3=(((C~))*B2*((B~)))*(B*(A2*C)) by Th17
.=(Inv(C))*B2*(Inv(B))*B*(A2*C) by Th17
.=(Inv(C))*B2*((Inv(B))*B)*(A2*C) by Th17
.=(Inv(C))*B2*(1.(K,k+1))*(A2*C) by A8,Th18
.=(Inv(C))*B2*((1.(K,k+1))*(A2*C)) by Th17
.=(Inv(C))*B2*(A2*C) by A24,MATRIXR2:68
.=(Inv(C))*B2*A2*C by Th17
.=(Inv(C))*(1.(K,k+1))*C by A5,Th17
.=(Inv(C))*((1.(K,k+1))*C) by Th17
.=(Inv(C))*C by A27,MATRIXR2:68
.=1.(K,k+1) by A9,Th18;
A31: for i be Nat st 1**) holds (Col(A3,j+1)).
k2=(<* 0.K *>).k2
proof
j+1<=k+1 & 1);
then k2 in Seg len (<* 0.K *>) by FINSEQ_1:def 3;
then k2 in {1} by FINSEQ_1:2,40;
then
A54: k2=1 by TARSKI:def 1;
1<=k+1 by NAT_1:11;
then k2 in Seg len A3 by A29,A54,FINSEQ_1:1;
then k2 in dom A3 by FINSEQ_1:def 3;
then (Col(A3,j+1)).k2= 0.K by A54,A53,MATRIX_0:def 8;
hence thesis by A54,FINSEQ_1:40;
end;
A55: len (Col(F,j)) = len F by MATRIX_0:def 8
.=k by MATRIX_0:24;
A56: i+1<=k+1 by A48,XREAL_1:7;
A57: for k2 being Nat st k2 in dom (<* 0.K *>) holds (Line(B3,i+1)).
k2=(<* 0.K *>).k2
proof
let k2 be Nat;
A58: 1**);
then k2 in Seg len (<* 0.K *>) by FINSEQ_1:def 3;
then k2 in {1} by FINSEQ_1:2,40;
then
A61: k2=1 by TARSKI:def 1;
1<=k+1 by NAT_1:11;
then k2 in Seg width B3 by A13,A61,FINSEQ_1:1;
then (Line(B3,i+1)).k2= 0.K by A61,A60,MATRIX_0:def 7;
hence thesis by A61,FINSEQ_1:40;
end;
A62: for k2 being Nat st k2 in dom (Col(F,j)) holds (Col(A3,j+1)).(
len (<* 0.K *>) + k2) = (Col(F,j)).k2
proof
reconsider j0=j+1 as Element of NAT;
let k2 be Nat;
A63: len (Col(F,j0-'1))=len F by MATRIX_0:def 8;
A64: j0-'1=j by NAT_D:34;
assume
A65: k2 in dom (Col(F,j));
then
A66: k2 in Seg len (Col(F,j0-'1)) by A64,FINSEQ_1:def 3;
then
A67: k2<=k by A26,A63,FINSEQ_1:1;
then 1<=k2+1 & k2+1<=k+1 by NAT_1:11,XREAL_1:7;
then
A68: k2+1 in dom A3 by A29,FINSEQ_3:25;
1<=k2 by A66,FINSEQ_1:1;
then [k2,j] in Indices F by A49,A50,A67,MATRIX_0:31;
then [k2,j0-'1] in Indices F by NAT_D:34;
then
A69: A3*(k2+1,j0-'1+1) = F*(k2,j0-'1) by A25;
k2 in Seg k by A26,A65,A63,A64,FINSEQ_1:def 3;
then k2 in dom F by A26,FINSEQ_1:def 3;
then A3*(k2+1,j0-'1+1)=(Col(F,j0-'1)).k2 by A69,MATRIX_0:def 8;
hence thesis by A23,A64,A68,MATRIX_0:def 8;
end;
A70: len (Line(G,i))=width G by MATRIX_0:def 7
.=k by MATRIX_0:24;
A71: k+1=len (<* 0.K *>) +k by FINSEQ_1:39;
A72: for k2 being Nat st k2 in dom (Line(G,i)) holds (Line(B3,i+1)).
(len (<* 0.K *>) + k2) = (Line(G,i)).k2
proof
let k2 be Nat;
A73: width B3=k+1 & 1<=k2+1 by MATRIX_0:24,NAT_1:11;
assume
A74: k2 in dom (Line(G,i));
then
A75: k2 in Seg len (Line(G,i)) by FINSEQ_1:def 3;
A76: len (Line(G,i))=width G by MATRIX_0:def 7
.=k by MATRIX_0:24;
then
A77: k2<=k by A75,FINSEQ_1:1;
1<=k2 by A75,FINSEQ_1:1;
then [i,k2] in Indices G by A47,A48,A77,MATRIX_0:31;
then
A78: B3*(i+1,k2+1) = G*(i,k2) by A28;
k2 in Seg k by A74,A76,FINSEQ_1:def 3;
then k2 in Seg width G by MATRIX_0:24;
then
A79: B3*(i+1,k2+1)=(Line(G,i)).k2 by A78,MATRIX_0:def 7;
k2+1<=k+1 by A77,XREAL_1:7;
then k2+1 in Seg width B3 by A73,FINSEQ_1:1;
then (Line(B3,i+1)).(k2+1) = (Line(G,i)).k2 by A79,MATRIX_0:def 7;
hence thesis by FINSEQ_1:40;
end;
A80: width G=k by MATRIX_0:24;
len (Line(B3,i+1))=width B3 & len (Line(G,i))=width G by
MATRIX_0:def 7;
then
dom (Line(B3,i+1)) = Seg (len (<* 0.K *>) + len (Line(G,i))) by A13
,A80,A71,FINSEQ_1:def 3;
then
A81: (<* 0.K *>) ^ Line(G,i)= (Line(B3,i+1)) by A57,A72,FINSEQ_1:def 7;
A82: 1<=i+1 & 1<=j+1 by NAT_1:11;
A83: j+1<=k+1 by A50,XREAL_1:7;
A84: now
per cases;
suppose
A85: i=j;
[i+1,j+1] in Indices (1.(K,k+1)) by A82,A56,A83,MATRIX_0:31;
then (1.(K,k+1))*(i+1,j+1)= 1.K by A85,MATRIX_1:def 3;
hence (1.(K,k+1))*(i+1,j+1)=IFEQ(i,j,1.K,0.K) by A85,
FUNCOP_1:def 8;
end;
suppose
A86: i<>j;
[i+1,j+1] in Indices (1.(K,k+1)) by A82,A56,A83,MATRIX_0:31;
then i+1 <> j+1 implies (1.(K,k+1))*(i+1,j+1) = 0.K by
MATRIX_1:def 3;
hence (1.(K,k+1))*(i+1,j+1)=IFEQ(i,j,1.K,0.K) by A86,
FUNCOP_1:def 8;
end;
end;
len (Col(A3,j+1))=len A3 & len (Col(F,j))=len F by MATRIX_0:def 8;
then dom (Col(A3,j+1)) = Seg (len (<* 0.K *>) + len (Col(F,j))) by
A29,A26,A71,FINSEQ_1:def 3;
then
A87: (<* 0.K *>) ^ Col(F,j)= (Col(A3,j+1)) by A52,A62,FINSEQ_1:def 7;
[i+1,j+1] in Indices (B3*A3) by A82,A56,A83,MATRIX_0:31;
then (B3*A3)*(i+1,j+1) =|( Line(B3,i+1),Col(A3,j+1) )| by A13,A29,
MATRIX_3:def 4
.=|( <* 0.K *>, <* 0.K *> )| + |( Line(G,i), Col(F,j) )| by A23,A81
,A87,A70,A55,Th12
.= 0.K +|( Line(G,i), Col(F,j) )| by Th22
.= |( Line(G,i), Col(F,j) )| by RLVECT_1:4;
hence thesis by A30,A26,A51,A80,A84,MATRIX_3:def 4;
end;
then G*F=1.(K,k) by Th29,A46;
then consider G2 being Matrix of k,K such that
A88: F*G2=1.(K,k) by A3;
deffunc h(Nat,Nat) = IFEQ($1,1,IFEQ($2,1,1.K,0.K), IFEQ($2,1,0.K,G2*(
$1-'1,$2-'1)));
A89: len G2=k by MATRIX_0:24;
consider B4 being Matrix of k+1,k+1,K such that
A90: for i,j being Nat st [i,j] in Indices B4 holds B4*(i,j) = h(
i,j) from MATRIX_0:sch 1;
A91: len B4=k+1 by MATRIX_0:24;
A92: width B4=k+1 by MATRIX_0:24;
A93: for j be Nat st 1<=j & j<=len (Col(B4,1)) holds (Col(B4,1)).j=(
Base_FinSeq(K,k+1,1)).j
proof
let j be Nat;
assume that
A94: 1<=j and
A95: j<=len (Col(B4,1));
A96: j<=k+1 by A91,A95,MATRIX_0:def 8;
then 1<=k+1 by A94,XXREAL_0:2;
then
A97: [j,1] in Indices B4 by A94,A96,MATRIX_0:31;
len (Col(B4,1))=len B4 by MATRIX_0:def 8;
then j in Seg width B4 by A91,A92,A94,A95,FINSEQ_1:1;
then
A98: j in dom B4 by A91,A92,FINSEQ_1:def 3;
per cases by A94,XXREAL_0:1;
suppose
A99: 1=j;
(Col(B4,1)).j=B4*(j,1) by A98,MATRIX_0:def 8
.=IFEQ(j,1, IFEQ(1,1,1.K,0.K),IFEQ(1,1,0.K,G2*(j-'1,1-'1))) by
A90,A97
.=IFEQ(1,1,1.K,0.K) by A99,FUNCOP_1:def 8
.=1.K by FUNCOP_1:def 8;
hence thesis by A96,A99,Th24;
end;
suppose
A100: 11;
1<=len B4 by A106,MATRIX_0:24;
then
A128: 1 in dom B4 by FINSEQ_3:25;
(A3*B4)*(i,j)=|( Line(A3,i0),Col(B4,j0) )| by A113,A121,A122,
MATRIX_3:def 4
.=|(Base_FinSeq(K,k+1,1),Col(B4,j0))| by A103,A15,A125,
FINSEQ_1:14
.=|(Col(B4,j0),Base_FinSeq(K,k+1,1))| by FVSUM_1:90
.=(Col(B4,j0)).1 by A106,A112,Th35
.= B4*(1,j) by A128,MATRIX_0:def 8
.= IFEQ(i,1,IFEQ(j,1,1.K,0.K), IFEQ(j,1,0.K,G2*(i-'1,j-'
1))) by A90,A124,A125
.=IFEQ(j,1,1.K,0.K) by A125,FUNCOP_1:def 8
.= 0.K by A127,FUNCOP_1:def 8;
hence thesis by A4,A114,A125,A127,MATRIX_1:def 3;
end;
end;
hence thesis;
end;
suppose
A129: 1**1;
then 1+1<=j by NAT_1:13;
then
A135: 1<=j-1 by XREAL_1:19;
A136: i-'1=i-1 by A129,XREAL_1:233;
then
A137: i-'1<=k by A118,XREAL_1:20;
A138: 1<=i-1 by A130,XREAL_1:19;
then
A139: i-'1 in Seg k by A136,A137,FINSEQ_1:1;
A140: len (Line(F,i-'1))=width F by MATRIX_0:def 7
.=k by MATRIX_0:24;
A141: for k2 being Nat st k2 in dom (Line(F,i-'1)) holds (
Line(A3,i-'1+1)).(len (<* 0.K *>) + k2) = (Line(F,i-'1)).k2
proof
let k2 be Nat;
assume
A142: k2 in dom (Line(F,i-'1));
then
A143: k2 in Seg len (Line(F,i-'1)) by FINSEQ_1:def 3;
then
A144: k2<=k by A140,FINSEQ_1:1;
then 1<=k2+1 & k2+1<=k+1 by NAT_1:11,XREAL_1:7;
then
A145: k2+1 in Seg width A3 by A122,FINSEQ_1:1;
1<=k2 by A143,FINSEQ_1:1;
then [i-'1,k2] in Indices F by A136,A138,A137,A144,
MATRIX_0:31;
then
A146: A3*(i-'1+1,k2+1) = F*(i-'1,k2) by A25;
k2 in Seg width F by A105,A140,A142,FINSEQ_1:def 3;
then A3*(i-'1+1,k2+1)=(Line(F,i-'1)).k2 by A146,
MATRIX_0:def 7;
then (Line(A3,i-'1+1)).(k2+1) = (Line(F,i-'1)).k2 by A145,
MATRIX_0:def 7;
hence thesis by FINSEQ_1:40;
end;
A147: for k2 being Nat st k2 in dom (<* 0.K *>) holds (Line(
A3,i-'1+1)).k2=(<* 0.K *>).k2
proof
let k2 be Nat;
assume k2 in dom (<* 0.K *>);
then k2 in Seg len (<* 0.K *>) by FINSEQ_1:def 3;
then k2 in {1} by FINSEQ_1:2,40;
then
A148: k2=1 by TARSKI:def 1;
A149: A3*(i0,1) = 0.K by A11,A118,A129;
1<=k+1 by NAT_1:11;
then k2 in Seg width A3 by A122,A148,FINSEQ_1:1;
then (Line(A3,i)).k2=0.K by A148,A149,MATRIX_0:def 7;
hence thesis by A136,A148,FINSEQ_1:40;
end;
dom (Line(A3,i-'1+1))= Seg (k+1) by A111,A136,FINSEQ_1:def 3
.=Seg (len (<* 0.K *>) + len (Line(F,i-'1))) by A140,
FINSEQ_1:39;
then
A150: (<* 0.K *>) ^ Line(F,i-'1)= (Line(A3,i-'1+1)) by A147,A141,
FINSEQ_1:def 7;
A151: j-'1+1=j-1+1 by A134,XREAL_1:233
.=j;
A152: j-'1=j-1 by A134,XREAL_1:233;
then j-'1<=k by A123,XREAL_1:20;
then j-'1 in Seg k by A152,A135,FINSEQ_1:1;
then
A153: [i-'1,j-'1] in [:Seg k,Seg k:] by A139,ZFMISC_1:87;
then
A154: [i-'1,j-'1] in Indices (F*G2) by MATRIX_0:24;
A155: for k2 being Nat st k2 in dom (<* 0.K *>) holds (Col(
B4,j-'1+1)).k2=(<* 0.K *>).k2
proof
1<=1+k by NAT_1:11;
then [1,j] in Indices B4 by A120,A123,MATRIX_0:31;
then B4*(1,j) = IFEQ(1,1, IFEQ(j,1,1.K,0.K), IFEQ(j,1,0.K
,G2*(1-'1,j-'1))) by A90;
then
A156: B4*(1,j) = IFEQ(j,1,1.K,0.K) by FUNCOP_1:def 8
.= 0.K by A134,FUNCOP_1:def 8;
let k2 be Nat;
assume k2 in dom (<* 0.K *>);
then k2 in Seg len (<* 0.K *>) by FINSEQ_1:def 3;
then k2 in {1} by FINSEQ_1:2,40;
then
A157: k2=1 by TARSKI:def 1;
1<=k+1 by NAT_1:11;
then k2 in Seg len B4 by A121,A157,FINSEQ_1:1;
then k2 in dom B4 by FINSEQ_1:def 3;
then (Col(B4,j)).k2=0.K by A157,A156,MATRIX_0:def 8;
hence thesis by A152,A157,FINSEQ_1:40;
end;
A158: len (Col(G2,j-'1))=len G2 by MATRIX_0:def 8
.=k by MATRIX_0:24;
A159: for k2 be Nat st k2 in dom (Col(G2,j-'1)) holds (Col(
B4,j-'1+1)).(len (<* 0.K *>) + k2) = (Col(G2,j-'1)).k2
proof
let k2 be Nat;
assume
A160: k2 in dom (Col(G2,j-'1));
then 1<=k2 by FINSEQ_3:25;
then
A161: 1) + len (Col(G2,j-'1))) by A112,A152
,A158,FINSEQ_1:39;
then
A165: (<* 0.K *>) ^ Col(G2,j-'1)= (Col(B4,j-'1+1)) by A155,A159,
FINSEQ_1:def 7;
i-'1+1=i-1+1 by A129,XREAL_1:233
.=i;
then
A166: (A3*B4)*(i,j)=|( Line(A3,i-'1+1),Col(B4,j-'1+1) )| by A113
,A121,A122,A151,MATRIX_3:def 4
.=|( <* 0.K *>, <* 0.K *> )| + |( Line(F,i-'1), Col(G2,j
-'1) )| by A23,A109,A110,A150,A165,Th12
.= 0.K +|( Line(F,i-'1), Col(G2,j-'1) )| by Th22
.= 0.K +(F*G2)*(i-'1,j-'1) by A105,A89,A154,MATRIX_3:def 4
.= (1.(K,k))*(i-'1,j-'1) by A88,RLVECT_1:4;
A167: [i-'1,j-'1] in Indices (1.(K,k)) by A153,MATRIX_0:24;
now
per cases;
suppose
A168: i=j;
then (1.(K,k+1))*(i0,j0) =1.K by A115,MATRIX_1:def 3;
hence thesis by A167,A166,A168,MATRIX_1:def 3;
end;
suppose
A169: i<>j;
then i-1<>j-1;
then i0-'1<> j0-'1 by A129,A152,XREAL_1:233;
then (1.(K,k))*(i0-'1,j0-'1) =0.K by A167,MATRIX_1:def 3;
hence thesis by A115,A166,A169,MATRIX_1:def 3;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
then width Inv B= k+1 & B*A2*C*B4=1.(K,k+1) by MATRIX_0:24,27;
then (Inv(B))*(B*A2*C*B4)=Inv B by MATRIXR2:67;
then (Inv(B))*(B*A2*C*B4)*B=1.(K,k+1) by A8,Th18;
then (Inv(B))*(B*A2*(C*B4))*B=1.(K,k+1) by Th17;
then (Inv(B))*(B*(A2*(C*B4)))*B=1.(K,k+1) by Th17;
then (Inv(B))*B*(A2*(C*B4))*B=1.(K,k+1) by Th17;
then len (A2*(C*B4))=k+1 & (1.(K,k+1))*(A2*(C*B4))*B=1.(K,k+1) by A8
,Th18,MATRIX_0:24;
then A2*(C*B4)*B=1.(K,k+1) by MATRIXR2:68;
then A2*((C*B4)*B)=1.(K,k+1) by Th17;
hence thesis;
end;
hence thesis;
end;
for D,B0 being Matrix of 0,K st B0*D=1.(K,0) holds ex B1 being Matrix
of 0,K st D*B1=1.(K,0)
proof
let D,B0 be Matrix of 0,K;
assume B0*D=1.(K,0);
D*(0.(K,0))=1.(K,0) by Th15;
hence thesis;
end;
then
A170: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A170,A2);
hence thesis by A1;
end;
end;
theorem Th55:
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)
proof
let A be Matrix of n,K;
per cases;
suppose
A1: n>0;
thus (ex B being Matrix of n,K st B*A=1.(K,n)) implies ex B2 being Matrix
of n,K st A*B2=1.(K,n) by Th54;
thus (ex B being Matrix of n,K st A*B=1.(K,n)) implies ex B2 being Matrix
of n,K st B2*A=1.(K,n)
proof
assume ex B being Matrix of n,K st A*B=1.(K,n);
then consider B being Matrix of n,K such that
A2: A*B=1.(K,n);
A3: width A=n & len B=n by MATRIX_0:24;
width B=n & (A*B)@=1.(K,n) by A2,MATRIX_0:24,MATRIX_6:10;
then (B@)*(A@)=1.(K,n) by A1,A3,MATRIX_3:22;
then consider B2 being Matrix of n,K such that
A4: (A@)*B2= 1.(K,n) by Th54;
A5: width (A@) =n & len B2=n by MATRIX_0:24;
width B2=n & ((A@)*B2)@ = 1.(K,n) by A4,MATRIX_0:24,MATRIX_6:10;
then (B2@)*((A@)@) = 1.(K,n) by A1,A5,MATRIX_3:22;
then (B2@)*A= 1.(K,n) by MATRIXR2:29;
hence thesis;
end;
end;
suppose
A6: n=0;
then A*A=1.(K,0) by Th15;
hence thesis by A6;
end;
end;
theorem
for A,B being Matrix of n,K st A*B = 1.(K,n) holds A is invertible & B
is invertible
proof
let A,B be Matrix of n,K;
assume
A1: A*B = 1.(K,n);
then consider B2 being Matrix of n,K such that
A2: B2*A= 1.(K,n) by Th55;
B2=B2*(1.(K,n)) by MATRIX_3:19
.=(B2*A)*B by A1,Th17
.=B by A2,MATRIX_3:18;
then A is_reverse_of B by A1,A2,MATRIX_6:def 2;
hence A is invertible by MATRIX_6:def 3;
consider B3 being Matrix of n,K such that
A3: B*B3= 1.(K,n) by A1,Th54;
B3=(1.(K,n))*B3 by MATRIX_3:18
.=A*(B*B3) by A1,Th17
.=A by A3,MATRIX_3:19;
then B is_reverse_of A by A1,A3,MATRIX_6:def 2;
hence thesis by MATRIX_6:def 3;
end;
*