:: Invertibility of Matrices of Field Elements
:: by Yatsuka Nakamura , Kunio Oniumi and Wenpai Chang
::
:: Received April 2, 2008
:: Copyright (c) 2008-2026 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); :: redefines 0* (MATRIX14, definition)
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_1:def 6
,MATRIX_3:def 1;
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_1:def 6;
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<i holds f.j=0.K
proof
defpred P[Nat] means 1<=$1 & $1<i implies f.$1=0.K;
let j be Nat;
assume
A9: 1<=j & j<i;
A10: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A11: P[k];
per cases;
suppose
A12: not(1<=k & k<i);
now
per cases by A12;
suppose
A13: 1>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;
then k+1< len x by A2,XXREAL_0:2;
hence thesis by A4,A5,A15;
end;
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;
then
A17: k+1<=i by NAT_1:13;
A18: k<len x by A2,A16,XXREAL_0:2;
now
per cases by A17,XXREAL_0:1;
suppose
A19: k+1<i;
then
A20: k+1< len x by A2,XXREAL_0:2;
f.(k + 1) = (the addF of K).(f.k,x.(k + 1)) by A6,A16,A18
.= 0.K+0.K by A4,A11,A16,A19,A20,NAT_1:12
.= 0.K by RLVECT_1:4;
hence thesis;
end;
suppose
k+1=i;
hence thesis;
end;
end;
hence thesis;
end;
end;
A21: P[0];
for l being Nat holds P[l] from NAT_1:sch 2(A21,A10);
hence thesis by A9;
end;
for j st i<=j & j<=len x holds f.j=a
proof
defpred P[Nat] means i<=$1 & $1<=len x implies f.$1=a;
let j;
assume
A22: i<=j & j<=len x;
A23: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A24: P[k];
per cases;
suppose
not(i<=k+1 & k+1<=len x);
hence thesis;
end;
suppose
A25: i<=k+1 & k+1<=len x;
then
A26: k<len x by NAT_1:13;
A27: 1<=k+1 by A1,A25,XXREAL_0:2;
now
per cases by A25,XXREAL_0:1;
suppose
A28: i<k+1;
A29: k<len x by A25,NAT_1:13;
i<=k by A28,NAT_1:13;
then f.(k + 1) = (the addF of K).(f.k,x.(k + 1)) by A1,A6,A29
.= a+0.K by A4,A24,A25,A27,A28,NAT_1:13
.= a by RLVECT_1:4;
hence thesis;
end;
suppose
A30: i=k+1;
then
A31: k<i by NAT_1:13;
now
per cases;
suppose
A32: 1<=k;
then f.(k + 1) = (the addF of K).(f.k,x.(k + 1)) by A6,A26
.= 0.K+a by A3,A8,A30,A31,A32
.= a by RLVECT_1:4;
hence thesis;
end;
suppose
k<1;
then
A33: k+1<=1 by NAT_1:13;
1<=1+k by NAT_1:12;
then i=1 by A30,A33,XXREAL_0:1;
hence thesis by A3,A5,A33,XXREAL_0:1;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
A34: P[0] by A1;
for l being Nat holds P[l] from NAT_1:sch 2(A34,A23);
hence thesis by A22;
end;
then f.(len x)=a by A2;
hence thesis by A7,FVSUM_1:def 8;
end;
theorem
for f1,f2 being FinSequence of K holds dom mlt(f1,f2) = dom f1 /\ dom
f2 & for i st i in dom (mlt(f1,f2)) holds (mlt(f1,f2)).i = (f1/.i) * (f2/.i)
proof
let f1,f2 be FinSequence of K;
A1: rng (f2) c= the carrier of K by FINSEQ_1:def 4;
dom (the multF of K)=[:the carrier of K,the carrier of K:] & rng (f1) c=
the carrier of K by FINSEQ_1:def 4,FUNCT_2:def 1;
then mlt(f1,f2)=(the multF of K).:(f1,f2) & [:rng (f1), rng (f2):] c= dom (
the multF of K) by A1,FVSUM_1:def 7,ZFMISC_1:96;
hence dom (mlt(f1,f2))= dom (f1) /\ dom (f2) by FUNCOP_1:69;
thus thesis by Th4;
end;
theorem Th34:
for x,y being FinSequence of K,i st len x=m & y=mlt (x,
Base_FinSeq(K,m,i)) & 1<=i & i<=m holds y.i=x.i & for j st j<>i & 1<=j & j<=m
holds y.j= 0.K
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<i & i<=n holds P.i=Base_FinSeq(K,n,i)) & Q*(1,1)=a
& (for j st 1<j & j<=n holds Q*(1,j)= -a*(P*(1,j))) & (for i st 1<i & i<=n
holds Q.i=Base_FinSeq(K,n,i)) holds P is invertible & Q=P~
proof
let a be Element of K,P,Q be Matrix of n,K;
assume that
A1: n>0 and
A2: a<>0.K and
A3: P*(1,1)= a" and
A4: for i st 1<i & i<=n holds P.i=Base_FinSeq(K,n,i) and
A5: Q*(1,1)=a and
A6: for j st 1<j & j<=n holds Q*(1,j)= -a*(P*(1,j)) and
A7: for i st 1<i & i<=n holds Q.i=Base_FinSeq(K,n,i);
A8: 0+1<=n by A1,NAT_1:13;
A9: len (Base_FinSeq(K,n,1))=n by Th23;
A10: len P=n by MATRIX_0:24;
A11: len ((a")*(Base_FinSeq(K,n,1)))=len (Base_FinSeq(K,n,1)) by MATRIXR1:16
.= n by Th23;
A12: for k be Nat st 1<=k & k<=n holds (Col(P,1)).k=((a")*(Base_FinSeq(K,n,
1))).k
proof
let k be Nat;
A13: k in NAT by ORDINAL1:def 12;
assume that
A14: 1<=k and
A15: k<=n;
A16: k in Seg n by A14,A15,FINSEQ_1:1;
then
A17: k in dom P by A10,FINSEQ_1:def 3;
A18: now
[k,1] in Indices P by A8,A14,A15,MATRIX_0:31;
then
A19: ex p being FinSequence of K st p = P.k & P*(k,1) = p.1 by MATRIX_0:def 5;
assume
A20: k<>1;
then 1<k by A14,XXREAL_0:1;
then P*(k,1)=(Base_FinSeq(K,n,k)).1 by A4,A13,A15,A19
.= 0.K by A8,A20,Th25;
hence (Col(P,1)).k= 0.K by A17,MATRIX_0:def 8;
end;
A21: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by A9,A14,A15,
FINSEQ_4:15;
A22: now
assume
A23: k=1;
k in dom ((a")*(Base_FinSeq(K,n,1))) by A11,A16,FINSEQ_1:def 3;
hence ((a")*(Base_FinSeq(K,n,1))).k =(a")*((Base_FinSeq(K,n,1))/.k) by
A21,FVSUM_1:50
.=(a")*(1.K) by A15,A21,A23,Th24
.= a";
end;
A24: k in dom ((a")*(Base_FinSeq(K,n,1))) by A11,A14,A15,FINSEQ_3:25;
A25: now
assume
A26: k<>1;
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 & j<=n holds P*(1,j)= -(a")*(Q*(1,j))
proof
let j;
assume 1<j & j<=n;
then -(a")*(Q*(1,j))= -(a")*( -a*(P*(1,j))) by A6;
then -(a")*(Q*(1,j))= -(a")*( (-a)*(P*(1,j))) by VECTSP_1:9;
then -(a")*(Q*(1,j))= (-(a"))*( (-a)*(P*(1,j))) by VECTSP_1:9;
then -(a")*(Q*(1,j))= ((-(a"))*(-a))*(P*(1,j)) by GROUP_1:def 3;
then -(a")*(Q*(1,j))= ((a)*(a"))*(P*(1,j)) by VECTSP_1:10;
then -(a")*(Q*(1,j))= (1.K)*(P*(1,j)) by A2,VECTSP_1:def 10;
hence thesis;
end;
A35: for j st 1<j & j<=n holds (Q*P)*(1,j)= 0.K
proof
let j;
assume that
A36: 1<j and
A37: j<=n;
A38: 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;
A39: j in Seg n by A36,A37,FINSEQ_1:1;
A40: 1<=n by A36,A37,XXREAL_0:2;
then
A41: 1 in Seg width Q by A31,FINSEQ_1:1;
len Line(Q,1) = n by A31,MATRIX_0:def 7;
then
A42: (Line(Q,1))/.j = (Line(Q,1)).j by A36,A37,FINSEQ_4:15;
A43: (Line(Q,1))/.1 = (Line(Q,1)).1 by A32,A40,FINSEQ_4:15
.= a by A5,A41,MATRIX_0:def 7;
A44: len (Col(P,j))=len P by MATRIX_0:def 8
.=n by MATRIX_0:24;
reconsider p=Col(P,j),q=-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1)) +Base_FinSeq(
K,n,j) as FinSequence of K;
A45: len (Base_FinSeq(K,n,j))=n by Th23;
A46: len ((-(a")*(Q*(1,j)))*(Base_FinSeq(K,n,1))) =len Base_FinSeq(K,n,1)
by MATRIXR1:16
.=n by Th23;
A47: for k be Nat st 1 <=k & k <= n holds p.k=q.k
proof
A48: len ((-(a")*(Q*(1,j)))*(Base_FinSeq(K,n,1))) = len (Base_FinSeq(K,
n,1)) by MATRIXR1:16
.=n by Th23;
let k be Nat;
assume that
A49: 1 <=k and
A50: k <= n;
A51: k in dom ((-(a")*(Q*(1,j)))*(Base_FinSeq(K,n,1))) by A46,A49,A50,
FINSEQ_3:25;
len (Base_FinSeq(K,n,1))=n by Th23;
then
A52: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by A49,A50,FINSEQ_4:15
;
k in dom P by A10,A49,A50,FINSEQ_3:25;
then
A53: p.k=P*(k,j) by MATRIX_0:def 8;
A54: (-(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 A51,A52,FVSUM_1:50;
per cases by A49,XXREAL_0:1;
suppose
A55: 1=k;
then 1 <= len (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))) by A50,A48,Th6;
then
A56: (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1)))/.1 =(-(a")*(Q*(1,j)))*((
Base_FinSeq(K,n,1))/.1) by A54,A55,FINSEQ_4:15
.=(-(a")*(Q*(1,j)))*(1.K) by A27,A52,A55,Th24
.=-(a")*(Q*(1,j));
A57: p.1=-(a")*(Q*(1,j)) by A34,A36,A37,A53,A55;
(Base_FinSeq(K,n,j))/.1 = (Base_FinSeq(K,n,j)).1 by A45,A50,A55,
FINSEQ_4:15
.= 0.K by A36,A50,A55,Th25;
then q.1= -(a")*(Q*(1,j)) + 0.K by A38,A45,A50,A55,A56,Th5;
hence thesis by A55,A57,RLVECT_1:4;
end;
suppose
A58: 1<k;
[k,j] in Indices P by A36,A37,A49,A50,MATRIX_0:31;
then
A59: ex p2 being FinSequence of K st p2 = P.k & P*(k,j) = p2. j by
MATRIX_0:def 5;
k in NAT by ORDINAL1:def 12;
then
A60: p.k= (Base_FinSeq(K,n,k)).j by A4,A50,A53,A58,A59;
now
per cases;
suppose
A61: 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 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<i & i<=n & i=j holds (Q*P)*(i,j)=1.K
proof
let i,j;
assume that
A72: 1<i and
A73: i<=n and
A74: i=j;
A75: 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;
[i,j] in Indices Q by A72,A73,A74,MATRIX_0:31;
then consider p1 being FinSequence of K such that
A76: p1 = Q.i and
A77: Q*(i,j) = p1.j by MATRIX_0:def 5;
p1=Base_FinSeq(K,n,i) by A7,A72,A73,A76;
then
A78: p1.j=1.K by A72,A73,A74,Th24;
[i,1] in Indices Q by A8,A72,A73,MATRIX_0:31;
then consider p2 being FinSequence of K such that
A79: p2 = Q.i and
A80: Q*(i,1) = p2.1 by MATRIX_0:def 5;
A81: width Q=n by MATRIX_0:24;
A82: j in Seg n by A72,A73,A74,FINSEQ_1:1;
A83: len (Col(P,j))=len P by MATRIX_0:def 8
.=n by MATRIX_0:24;
reconsider p=Col(P,j),q=-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1)) +Base_FinSeq(
K,n,j) as FinSequence of K;
A84: len (Base_FinSeq(K,n,j))=n by Th23;
A85: len ((-(a")*(Q*(1,j)))*(Base_FinSeq(K,n,1))) =len (Base_FinSeq(K,n,1
)) by MATRIXR1:16
.=n by Th23;
A86: for k be Nat st 1 <=k & k <= n holds p.k=q.k
proof
A87: len ((-(a")*(Q*(1,j)))*(Base_FinSeq(K,n,1))) = len (Base_FinSeq(K,
n,1)) by MATRIXR1:16
.=n by Th23;
let k be Nat;
assume that
A88: 1 <=k and
A89: k <= n;
k in Seg n by A88,A89,FINSEQ_1:1;
then
A90: k in dom ((-(a")*(Q*(1,j)))*(Base_FinSeq(K,n,1))) by A85,FINSEQ_1:def 3;
len (Base_FinSeq(K,n,1))=n by Th23;
then
A91: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by A88,A89,FINSEQ_4:15
;
k in dom P by A10,A88,A89,FINSEQ_3:25;
then
A92: p.k=P*(k,j) by MATRIX_0:def 8;
A93: (-(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 A90,A91,FVSUM_1:50;
per cases by A88,XXREAL_0:1;
suppose
A94: 1=k;
k <= len (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1))) by A89,A87,Th6;
then
A95: (-(a")*(Q*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-(a")*(Q*(1,j)))*((
Base_FinSeq(K,n,1))/.k) by A88,A93,FINSEQ_4:15
.=(-(a")*(Q*(1,j)))*(1.K) by A27,A91,A94,Th24
.=-(a")*(Q*(1,j));
(Base_FinSeq(K,n,j))/.k = (Base_FinSeq(K,n,j)).k by A84,A88,A89,
FINSEQ_4:15
.= 0.K by A72,A74,A89,A94,Th25;
then
A96: q.k= -(a")*(Q*(1,j)) + 0.K by A75,A84,A88,A89,A95,Th5;
p.k=-(a")*(Q*(1,j)) by A34,A72,A73,A74,A92,A94;
hence thesis by A96,RLVECT_1:4;
end;
suppose
A97: 1<k;
[k,j] in Indices P by A72,A73,A74,A88,A89,MATRIX_0:31;
then
A98: ex p2 being FinSequence of K st p2 = P.k & P*(k,j) = p2. j by
MATRIX_0:def 5;
k in NAT by ORDINAL1:def 12;
then
A99: p.k=(Base_FinSeq(K,n,k)).j by A4,A89,A92,A97,A98;
now
per cases;
suppose
A100: 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
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<i & i<=n & 1<=j & j<=n & i<>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<i and
A118: i<=n and
A119: 1<=j and
A120: j<=n and
A121: i<>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<k;
[k,j] in Indices P by A119,A120,A132,A133,MATRIX_0:31;
then
A143: ex p2 being FinSequence of K st p2 = P.k & P*(k,j) = p2. j by
MATRIX_0:def 5;
k in NAT by ORDINAL1:def 12;
then
A144: p.k=(Base_FinSeq(K,n,k)).j by A4,A133,A136,A142,A143;
now
per cases;
suppose
A145: 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
.= 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<k;
[k,j] in Indices P by A114,A123,A165,ZFMISC_1:87;
then
A170: ex p2 being FinSequence of K st p2 = P.k & P*(k,j) = p2. j by
MATRIX_0:def 5;
k in NAT by ORDINAL1:def 12;
then
A171: p.k=(Base_FinSeq(K,n,k)).j by A4,A162,A167,A169,A170;
now
per cases;
suppose
A172: k <> 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<i;
now
per cases;
suppose
A192: i<>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;
A198: (1.(K,n))*(i,j)=(Base_FinSeq(K,n,i0)).j0 by A186,A187,A189,A190,Th27
.= 0.K by A189,A190,A197,Th25;
thus (Q*P)*(i,j)=(Q*P)*(i0,j0)
.=(1.(K,n))*(i,j) by A35,A190,A196,A197,A198;
end;
suppose
A199: 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<k by A206,XXREAL_0:1;
then Q*(k,1)=(Base_FinSeq(K,n,k)).1 by A7,A207,A212,A215
.= 0.K by A8,A216,Th25;
hence (Col(Q,1)).k= 0.K by A213,MATRIX_0:def 8;
end;
A217: now
assume
A218: k=1;
thus (a*(Base_FinSeq(K,n,1))).k=a*((Base_FinSeq(K,n,1))/.k) by A208,A209,
FVSUM_1:50
.= a*(1.K) by A207,A208,A218,Th24
.= a;
end;
1<=n by A206,A207,XXREAL_0:2;
then 1 in dom Q by A202,FINSEQ_3:25;
hence thesis by A5,A210,A217,A214,MATRIX_0:def 8;
end;
A219: 0+1<=n by A1,NAT_1:13;
A220: len P=n by MATRIX_0:24;
then
A221: 1 in Seg len P by A219,FINSEQ_1:1;
then
A222: 1 in dom P by FINSEQ_1:def 3;
A223: width P=n by MATRIX_0:24;
then
A224: len Line(P,1)=n by MATRIX_0:def 7;
then
A225: 1 in dom (Line(P,1)) by A220,A221,FINSEQ_1:def 3;
A226: 1 in Seg width P by A223,A219,FINSEQ_1:1;
A227: for j st 1<j & j<=n holds (P*Q)*(1,j)= 0.K
proof
let j;
assume that
A228: 1<j and
A229: j<=n;
A230: 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;
reconsider p=Col(Q,j),q=-a*(P*(1,j))*(Base_FinSeq(K,n,1)) +Base_FinSeq(K,n
,j) as FinSequence of K;
A231: len (Base_FinSeq(K,n,j))=n by Th23;
A232: len ((-a*(P*(1,j)))*(Base_FinSeq(K,n,1))) =len (Base_FinSeq(K,n,1))
by MATRIXR1:16
.= n by Th23;
A233: for k be Nat st 1 <=k & k <= n holds p.k=q.k
proof
let k be Nat;
assume that
A234: 1 <=k and
A235: k <= n;
A236: k in dom Q by A202,A234,A235,FINSEQ_3:25;
len (Base_FinSeq(K,n,1))=n by Th23;
then
A237: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by A234,A235,
FINSEQ_4:15;
A238: k in dom ((-a*(P*(1,j)))*(Base_FinSeq(K,n,1))) & ((Base_FinSeq(K,n,
1))/.k)=( (Base_FinSeq(K,n,1)).k) by A203,A232,A234,A235,FINSEQ_3:25
,FINSEQ_4:15;
A239: (-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 A238,FVSUM_1:50;
per cases by A234,XXREAL_0:1;
suppose
A240: 1=k;
(Base_FinSeq(K,n,j))/.k = (Base_FinSeq(K,n,j)).k by A231,A234,A235,
FINSEQ_4:15
.= 0.K by A228,A235,A240,Th25;
then q.k=(-a*(P*(1,j))*(Base_FinSeq(K,n,1)))/.k +0.K by A230,A231,A234
,A235,Th5;
then
A241: q.k=(-a*(P*(1,j))*(Base_FinSeq(K,n,1)))/.k by RLVECT_1:4;
A242: (-a*(P*(1,j))*(Base_FinSeq(K,n,1))).k =(-a*(P*(1,j)))*(1_K) by A235
,A239,A237,A240,Th24
.=-a*(P*(1,j));
p.k=Q*(1,j) by A236,A240,MATRIX_0:def 8
.=-a*(P*(1,j)) by A6,A228,A229;
hence thesis by A230,A234,A235,A242,A241,FINSEQ_4:15;
end;
suppose
A243: 1<k;
[k,j] in Indices Q by A228,A229,A234,A235,MATRIX_0:31;
then consider p2 being FinSequence of K such that
A244: p2 = Q.k and
A245: Q*(k,j) = p2.j by MATRIX_0:def 5;
A246: k in NAT by ORDINAL1:def 12;
A247: p.k=p2.j by A236,A245,MATRIX_0:def 8
.= (Base_FinSeq(K,n,k)).j by A7,A235,A243,A244,A246;
now
per cases;
suppose
A248: 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
.= 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<i & i<=n & i=j holds (P*Q)*(i,j)=1.K
proof
let i,j;
assume that
A259: 1<i and
A260: i<=n and
A261: i=j;
A262: 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;
reconsider p=Col(Q,j),q=-a*(P*(1,j))*(Base_FinSeq(K,n,1)) +Base_FinSeq(K,n
,j) as FinSequence of K;
A263: len (Base_FinSeq(K,n,j))=n by Th23;
A264: j in Seg n by A259,A260,A261,FINSEQ_1:1;
A265: for k be Nat st 1 <=k & k <= n holds p.k=q.k
proof
A266: len ((-a*(P*(1,j)))*(Base_FinSeq(K,n,1))) = len (Base_FinSeq(K,n,1
)) by MATRIXR1:16
.=n by Th23;
let k be Nat;
assume that
A267: 1 <=k and
A268: k <= n;
A269: k in Seg n by A267,A268,FINSEQ_1:1;
len ((-a*(P*(1,j)))*(Base_FinSeq(K,n,1))) =len (Base_FinSeq(K,n,1)
) by MATRIXR1:16
.= n by Th23;
then
A270: k in dom ((-a*(P*(1,j)))*(Base_FinSeq(K,n,1))) by A267,A268,FINSEQ_3:25;
A271: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by A203,A267,A268,
FINSEQ_4:15;
len (Base_FinSeq(K,n,1))=n by Th23;
then
A272: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by A267,A268,
FINSEQ_4:15;
k in dom Q by A202,A267,A268,FINSEQ_3:25;
then
A273: p.k=Q*(k,j) by MATRIX_0:def 8;
A274: (-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 A270,A271,FVSUM_1:50;
per cases by A267,XXREAL_0:1;
suppose
A275: 1=k;
k <= len (-a*(P*(1,j))*(Base_FinSeq(K,n,1))) by A268,A266,Th6;
then
A276: (-a*(P*(1,j))*(Base_FinSeq(K,n,1)))/.k = (-a*(P*(1,j)))*((
Base_FinSeq(K,n,1))/.k) by A267,A274,FINSEQ_4:15
.= (-a*(P*(1,j)))*(1.K) by A219,A272,A275,Th24;
(Base_FinSeq(K,n,j))/.k = (Base_FinSeq(K,n,j)).k by A263,A267,A268,
FINSEQ_4:15
.= 0.K by A259,A261,A268,A275,Th25;
then q.k= (-a*(P*(1,j)))*(1.K)+ 0.K by A262,A263,A267,A268,A276,Th5
.= (-a*(P*(1,j)))*(1.K) by RLVECT_1:4
.= -a*(P*(1,j));
hence thesis by A6,A259,A260,A261,A273,A275;
end;
suppose
A277: 1<k;
[k,j] in Indices Q by A257,A264,A269,ZFMISC_1:87;
then
A278: ex p2 being FinSequence of K st p2 = Q.k & Q*(k,j) = p2. j by
MATRIX_0:def 5;
k in NAT by ORDINAL1:def 12;
then
A279: p.k= (Base_FinSeq(K,n,k)).j by A7,A268,A273,A277,A278;
now
per cases;
suppose
A280: k <> 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<i & i<=n & 1<=j & j<=n & i<>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<i and
A306: i<=n and
A307: 1<=j and
A308: j<=n and
A309: i<>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<k;
[k,j] in Indices Q by A307,A308,A319,A320,MATRIX_0:31;
then
A330: ex p2 being FinSequence of K st p2 = Q.k & Q*(k,j) = p2. j by
MATRIX_0:def 5;
k in NAT by ORDINAL1:def 12;
then
A331: p.k=(Base_FinSeq(K,n,k)).j by A7,A320,A326,A329,A330;
A332: k <= len (-a*(P*(1,j))*(Base_FinSeq(K,n,1))) by A320,A322,Th6;
now
per cases;
suppose
A333: k <> 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<k;
[k,j] in Indices Q by A307,A308,A353,A354,MATRIX_0:31;
then
A362: ex p2 being FinSequence of K st p2 = Q.k & Q*(k,j) = p2. j by
MATRIX_0:def 5;
A363: k in NAT by ORDINAL1:def 12;
A364: p.k=Q*(k,j) by A355,MATRIX_0:def 8
.= (Base_FinSeq(K,n,k)).j by A7,A354,A361,A362,A363;
now
per cases;
suppose
A365: k <> 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<i;
now
per cases;
suppose
A382: i<>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;
A388: (1.(K,n))*(i,j)=(Base_FinSeq(K,n,i0)).j0 by A376,A377,A379,A380,Th27
.= 0.K by A379,A380,A387,Th25;
thus (P*Q)*(i,j)=(P*Q)*(i0,j0)
.=(1.(K,n))*(i,j) by A227,A380,A386,A387,A388;
end;
suppose
A389: 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<i & i<=n holds P.i=Base_FinSeq(K,n,i)) holds P is
invertible
proof
let a be Element of K,P be Matrix of n,K;
assume that
A1: n>0 and
A2: a<>0.K & P*(1,1)= a" & for i st 1<i & i<=n holds P.i=Base_FinSeq(K,n ,i);
defpred P[Nat,Nat,Element of K] means ($1=1 implies (($2=1 implies $3=a)& (
$2<>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 1<j & j<=n holds Q0*(1,j)= -a*(P*(1,j))
proof
let j;
assume that
A12: 1<j and
A13: j<=n;
[1,j] in Indices Q0 by A10,A12,A13,MATRIX_0:31;
hence thesis by A9,A12;
end;
A14: Indices Q0=[:Seg n,Seg n:] & 1 in Seg n by A10,FINSEQ_1:1,MATRIX_0:24;
A15: for i st 1<i & i<=n holds Q0.i=Base_FinSeq(K,n,i)
proof
let i;
assume that
A16: 1<i and
A17: i<=n;
i in Seg n by A16,A17,FINSEQ_1:1;
then [i,1] in Indices Q0 by A14,ZFMISC_1:87;
then consider p being FinSequence of K such that
A18: p = Q0.i and
Q0*(i,1) = p.1 by MATRIX_0:def 5;
A19: for j be Nat st 1<=j & j<=n holds p.j=(Base_FinSeq(K,n,i)).j
proof
let j be Nat;
assume 1<=j & j<=n;
then
A20: [i,j] in Indices Q0 by A16,A17,MATRIX_0:31;
then ex p2 being FinSequence of K st p2 = Q0.i & Q0*(i,j) = p2.j by
MATRIX_0:def 5;
hence thesis by A9,A16,A18,A20;
end;
len Q0 = n by MATRIX_0:def 2;
then i in Seg len Q0 by A16,A17,FINSEQ_1:1;
then i in dom Q0 by FINSEQ_1:def 3;
then p in rng Q0 by A18,FUNCT_1:def 3;
then
A21: len p=n by MATRIX_0:def 2;
len (Base_FinSeq(K,n,i))= n by Th23;
hence thesis by A18,A21,A19,FINSEQ_1:14;
end;
[1,1] in Indices Q0 by A10,MATRIX_0:31;
then Q0*(1,1)=a by A9;
hence thesis by A1,A2,A11,A15,Th37;
end;
theorem Th39:
for A being Matrix of n,K st n>0 & A*(1,1)<>0.K ex P being
Matrix of n,K st P is invertible & (A*P)*(1,1)=1.K & (for j st 1<j & j<=n holds
(A*P)*(1,j)= 0.K)& for i st 1<i & i<=n & A*(i,1)= 0.K holds (A*P)*(i,1)= 0.K
proof
let A be Matrix of n,K;
assume that
A1: n>0 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<i & i<=n holds P0.i=Base_FinSeq(K,n,i)
proof
let i;
assume that
A11: 1<i and
A12: i<=n;
[i,1] in Indices P0 by A9,A11,A12,MATRIX_0:31;
then consider p being FinSequence of K such that
A13: p = P0.i and
P0*(i,1) = p.1 by MATRIX_0:def 5;
A14: for j be Nat st 1<=j & j<=n holds p.j=(Base_FinSeq(K,n,i)).j
proof
let j be Nat;
assume 1<=j & j<=n;
then
A15: [i,j] in Indices P0 by A11,A12,MATRIX_0:31;
then ex p2 being FinSequence of K st p2 = P0.i & P0*(i,j) = p2.j by
MATRIX_0:def 5;
hence thesis by A8,A11,A13,A15;
end;
len P0 = n by MATRIX_0:def 2;
then i in Seg len P0 by A11,A12,FINSEQ_1:1;
then i in dom P0 by FINSEQ_1:def 3;
then p in rng P0 by A13,FUNCT_1:def 3;
then
A16: len p=n by MATRIX_0:def 2;
len (Base_FinSeq(K,n,i))= n by Th23;
hence thesis by A13,A16,A14,FINSEQ_1:14;
end;
A17: len ((a")*(Base_FinSeq(K,n,1))) =len (Base_FinSeq(K,n,1)) by MATRIXR1:16
.=n by Th23;
A18: Indices P0=[: Seg n,Seg n :] by MATRIX_0:24;
A19: len (Base_FinSeq(K,n,1))=n by Th23;
A20: [1,1] in Indices P0 by A9,MATRIX_0:31;
then
A21: P0*(1,1)= a" by A8;
then
A22: P0 is invertible by A1,A2,A10,Th38;
A23: len P0=n by MATRIX_0:24;
then
A24: 1 in Seg len P0 by A9,FINSEQ_1:1;
A25: for k be Nat st 1<=k & k<=n holds (Col(P0,1)).k=((a")*(Base_FinSeq(K,n,
1))).k
proof
let k be Nat;
assume that
A26: 1<=k and
A27: k<=n;
A28: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by A19,A26,A27,
FINSEQ_4:15;
k in Seg n by A26,A27,FINSEQ_1:1;
then
A29: k in dom ((a")*(Base_FinSeq(K,n,1))) by A17,FINSEQ_1:def 3;
A30: now
assume
A31: k<>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<k by A26,ORDINAL1:def 12,XXREAL_0:1;
then P0*(k,1)=(Base_FinSeq(K,n,k)).1 by A10,A27,A34
.= 0.K by A9,A35,Th25;
hence (Col(P0,1)).k= 0.K by A32,MATRIX_0:def 8;
end;
A36: now
assume
A37: k=1;
hence ((a")*(Base_FinSeq(K,n,1))).k =(a")*((Base_FinSeq(K,n,1))/.1) by
A29,A28,FVSUM_1:50
.=(a")*(1.K) by A27,A28,A37,Th24
.= a";
end;
1<=n by A26,A27,XXREAL_0:2;
then 1 in dom P0 by A23,FINSEQ_3:25;
hence thesis by A21,A30,A36,A33,MATRIX_0:def 8;
end;
A38: len A=n by MATRIX_0:24;
then
A39: 1 in Seg len A by A3,FINSEQ_1:1;
then
A40: 1 in dom A by FINSEQ_1:def 3;
A41: width A=n by MATRIX_0:24;
then
A42: len (Line(A,1))=n by MATRIX_0:def 7;
then
A43: 1 in dom (Line(A,1)) by A38,A39,FINSEQ_1:def 3;
A44: 1 in Seg width A by A41,A3,FINSEQ_1:1;
A45: for i st 1<i & i<=n & A*(i,1)= 0.K holds (A*P0)*(i,1)= 0.K
proof
set Q=A,P=P0;
let i;
assume that
A46: 1<i & i<=n and
A47: A*(i,1)= 0.K;
A48: 1<=n by A46,XXREAL_0:2;
reconsider p=Col(P,1),q=a"*(Base_FinSeq(K,n,1)) as FinSequence of K;
A49: len (Col(P,1))=len P by MATRIX_0:def 8
.=n by MATRIX_0:24;
A50: len ((a")*(Base_FinSeq(K,n,1))) =len (Base_FinSeq(K,n,1)) by MATRIXR1:16
.=n by Th23;
A51: for k be Nat st 1 <=k & k <= n holds p.k=q.k
proof
let k be Nat;
assume that
A52: 1 <=k and
A53: k <= n;
A54: len (Base_FinSeq(K,n,1))=n by Th23;
then
A55: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by A52,A53,FINSEQ_4:15
;
k in dom P by A23,A52,A53,FINSEQ_3:25;
then
A56: p.k=P*(k,1) by MATRIX_0:def 8;
k in dom ((a")*(Base_FinSeq(K,n,1))) by A50,A52,A53,FINSEQ_3:25;
then
A57: ((a")*(Base_FinSeq(K,n,1))).k = (a")*((Base_FinSeq(K,n,1))/.k) by A55,
FVSUM_1:50;
per cases by A52,XXREAL_0:1;
suppose
A58: 1=k;
then q.k= (a")*(1.K) by A53,A55,A57,Th24
.=a";
hence thesis by A8,A20,A56,A58;
end;
suppose
A59: 1<k;
((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by A52,A53,A54,
FINSEQ_4:15;
then
A60: (a")*(Base_FinSeq(K,n,1))/.k = a"*(0.K) by A53,A59,Th25
.= 0.K;
[k,1] in Indices P by A48,A52,A53,MATRIX_0:31;
then
A61: ex p2 being FinSequence of K st p2 = P.k & P*(k,1) = p2. 1 by
MATRIX_0:def 5;
k in NAT by ORDINAL1:def 12;
then p.k=(Base_FinSeq(K,n,k)).1 by A10,A53,A56,A59,A61;
hence thesis by A48,A57,A59,A60,Th25;
end;
end;
A62: width Q=n by MATRIX_0:24;
then
A63: len Line(Q,i) = n by MATRIX_0:def 7;
then
A64: (Line(Q,i))/.1 = (Line(Q,i)).1 by A3,FINSEQ_4:15
.= Q*(i,1) by A44,MATRIX_0:def 7;
[i,1] in Indices (Q*P) by A46,A48,MATRIX_0:31;
hence (Q*P)*(i,1)= |( Line(Q,i), Col(P,1) )| by A23,A62,MATRIX_3:def 4
.= |( Line(Q,i), a"*(Base_FinSeq(K,n,1)) )| by A49,A50,A51,FINSEQ_1:14
.= a"* |( Line(Q,i), (Base_FinSeq(K,n,1)) )| by A19,A63,Th10
.= a"* (Q*(i,1)) by A3,A63,A64,Th35
.= 0.K by A47;
end;
A65: for j st 1<j & j<=n holds (A*P0)*(1,j)= 0.K
proof
let j;
assume that
A66: 1<j and
A67: j<=n;
A68: len (Base_FinSeq(K,n,j))=n by Th23;
reconsider p=Col(P0,j),q=-(a")*(A*(1,j))*(Base_FinSeq(K,n,1)) +Base_FinSeq
(K,n,j) as FinSequence of K;
A69: len ((-(a")*(A*(1,j)))*(Base_FinSeq(K,n,1))) =len (Base_FinSeq(K,n,1)
) by MATRIXR1:16
.=n by Th23;
A70: len (-(a")*(A*(1,j))*(Base_FinSeq(K,n,1))) =len ((-(a")*(A*(1,j)))*(
Base_FinSeq(K,n,1))) by Th6
.=len (Base_FinSeq(K,n,1)) by MATRIXR1:16
.=n by Th23;
A71: [1,j] in Indices P0 by A9,A66,A67,MATRIX_0:31;
A72: for k be Nat st 1 <=k & k <= n holds p.k=q.k
proof
A73: len ((-(a")*(A*(1,j)))*(Base_FinSeq(K,n,1))) = len (Base_FinSeq(K,n
,1)) by MATRIXR1:16
.=n by Th23;
let k be Nat;
assume that
A74: 1 <=k and
A75: k <= n;
k in Seg n by A74,A75,FINSEQ_1:1;
then
A76: k in dom ((-(a")*(A*(1,j)))*(Base_FinSeq(K,n,1))) by A69,FINSEQ_1:def 3;
len (Base_FinSeq(K,n,1))=n by Th23;
then
A77: ((Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by A74,A75,FINSEQ_4:15
;
A78: (-(a")*(A*(1,j))*(Base_FinSeq(K,n,1))).k =((-(a")*(A*(1,j)))*(
Base_FinSeq(K,n,1))).k by Th6
.=(-(a")*(A*(1,j)))*((Base_FinSeq(K,n,1))/.k) by A76,A77,FVSUM_1:50;
len (Base_FinSeq(K,n,1))=n by Th23;
then
A79: (
(Base_FinSeq(K,n,1))/.k)=((Base_FinSeq(K,n,1)).k) by A74,A75,FINSEQ_4:15;
k in dom P0 by A23,A74,A75,FINSEQ_3:25;
then
A80: p.k=P0*(k,j) by MATRIX_0:def 8;
per cases by A74,XXREAL_0:1;
suppose
A81: 1=k;
k <= len (-(a")*(A*(1,j))*(Base_FinSeq(K,n,1))) by A75,A73,Th6;
then
A82: (-(a")*(A*(1,j))*(Base_FinSeq(K,n,1)))/.k =(-(a")*(A*(1,j)))*((
Base_FinSeq(K,n,1))/.k) by A74,A78,FINSEQ_4:15
.=(-(a")*(A*(1,j)))*(1.K) by A75,A79,A81,Th24
.=-(a")*(A*(1,j));
A83: p.k=-(a")*(A*(1,j)) by A8,A66,A71,A80,A81;
(Base_FinSeq(K,n,j))/.k = (Base_FinSeq(K,n,j)).k by A68,A74,A75,
FINSEQ_4:15
.= 0.K by A66,A75,A81,Th25;
then q.k= -(a")*(A*(1,j)) + 0.K by A70,A68,A74,A75,A82,Th5;
hence thesis by A83,RLVECT_1:4;
end;
suppose
A84: 1<k;
[k,j] in Indices P0 & k in NAT by A66,A67,A74,A75,MATRIX_0:31
,ORDINAL1:def 12;
then
A85: p.k=(Base_FinSeq(K,n,k)).j by A8,A80,A84;
per cases;
suppose
A86: 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
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<i & i<=n holds
(P*A)*(i,1)= 0.K)& for j st 1<j & j<=n & A*(1,j)= 0.K holds (P*A)*(1,j)= 0.K
proof
let A be Matrix of n,K;
assume that
A1: n>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<i & i<=n holds (B*P0)*(1,i)= 0.K and
A7: for j st 1<j & j<=n & B*(j,1)= 0.K holds (B*P0)*(j,1)= 0.K by A1,A2,Th39;
A8: [1,1] in Indices (B*P0) by A3,MATRIX_0:31;
A9: for j st 1<j & j<=n & A*(1,j)= 0.K holds ((P0@)*A)*(1,j)= 0.K
proof
let j;
assume that
A10: 1<j & j<=n and
A11: A*(1,j)= 0.K;
[1,j] in Indices A by A3,A10,MATRIX_0:31;
then B*(j,1)=A*(1,j) by MATRIX_0:def 6;
then
A12: (B*P0)*(j,1)= 0.K by A7,A10,A11;
[j,1] in Indices (B*P0) by A3,A10,MATRIX_0:31;
then ((B*P0)@)*(1,j)= 0.K by A12,MATRIX_0:def 6;
then ((P0@)*(B@))*(1,j)= 0.K by Th30;
hence thesis by MATRIXR2:29;
end;
A13: for i st 1<i & i<=n holds ((P0@)*A)*(i,1)= 0.K
proof
let i;
assume 1<i & i<=n;
then
A14: [1,i] in Indices (B*P0) & (B*P0)*(1,i)= 0.K by A3,A6,MATRIX_0:31;
(B*P0)@=(P0@)*(B@) by Th30
.=(P0@)*A by MATRIXR2:29;
hence thesis by A14,MATRIX_0:def 6;
end;
A15: P0@ is invertible by A4;
((P0@)*A)*(1,1)=((P0@)*(B@))*(1,1) by MATRIXR2:29
.=((B*P0)@)*(1,1) by Th30
.=1.K by A5,A8,MATRIX_0:def 6;
hence thesis by A13,A15,A9;
end;
theorem Th41:
for A being Matrix of n,K st n>0 & A*(1,1)<>0.K ex P,Q being
Matrix of n,K st P is invertible & Q is invertible & (P*A*Q)*(1,1)=1.K & (for i
st 1<i & i<=n holds (P*A*Q)*(i,1)= 0.K)& for j st 1<j & j<=n holds (P*A*Q)*(1,j
)= 0.K
proof
let A be Matrix of n,K;
assume that
A1: n>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<i & i<=n holds (P*A)*(i,1)= 0.K and
for j st 1<j & j<=n & A*(1,j)= 0.K holds (P*A)*(1,j)= 0.K by A1,A2,Th40;
consider Q being Matrix of n,K such that
A6: Q is invertible & ((P*A)*Q)*(1,1)=1.K & for j st 1<j & j<=n holds ((
P*A) *Q)*(1,j)= 0.K and
A7: for i st 1<i & i<=n & (P*A)*(i,1)= 0.K holds ((P*A)*Q)*(i,1)= 0.K by A1,A4
,Th39;
for i st 1<i & i<=n holds (P*A*Q)*(i,1)= 0.K
proof
let i;
assume
A8: 1<i & i<=n;
then (P*A)*(i,1)= 0.K by A5;
hence thesis by A7,A8;
end;
hence thesis by A3,A6;
end;
begin :: A Transformation of Matrix to Some Canonical Form
theorem Th42:
for D being non empty set,m,n,i,j being Element of NAT, A being
Matrix of m,n,D holds Swap(A,i,j) is Matrix of m,n,D
proof
let D be non empty set,m,n,i,j being Element of NAT, A be Matrix of m,n,D;
A1: for p being FinSequence of D st p in rng (Swap(A,i,j)) holds len p = n
proof
let p be FinSequence of D;
A2: rng (Swap(A,i,j))= rng A by FINSEQ_7:22;
assume p in rng (Swap(A,i,j));
hence thesis by A2,MATRIX_0:def 2;
end;
rng Swap(A,i,j)=rng A by FINSEQ_7:22;
then ex n3 being Nat st for x being object st x in rng Swap(A,i,j)
ex p being
FinSequence of D st x = p & len p = n3 by MATRIX_0:9;
then
A3: Swap(A,i,j) is Matrix of D by MATRIX_0:9;
len A=m & len (Swap(A,i,j))=len A by FINSEQ_7:18,MATRIX_0:def 2;
hence thesis by A3,A1,MATRIX_0:def 2;
end;
definition
let K;
let n be Element of NAT, i0 be Nat;
func SwapDiagonal(K,n,i0) -> 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<i0 by A5,A8,A10,XXREAL_0:1;
then A.i=((<*f/.i0*>)^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;
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<i;
now
per cases;
suppose
A14: i<>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_1:def 6
.= 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<i & i<=n holds (B*A*C)*(i,1)= 0.K)& for j st 1<j & j<=n holds (B*A*C)*(1
,j)= 0.K
proof
let A be Matrix of n,K;
assume A<> 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<i & i<=n holds (P*A3*Q)*(i,1)= 0.K
)& for j st 1<j & j<=n holds (P*A3*Q)*(1,j)= 0.K by A1,A3,Th41;
set B0=P*(SwapDiagonal(K,n,i0)),C0=(SwapDiagonal(K,n,j0))*Q;
SwapDiagonal(K,n,i0) is invertible by A1,Th49;
then
A7: B0 is invertible by A4,MATRIX_6:36;
SwapDiagonal(K,n,j0) is invertible by A2,Th49;
then
A8: C0 is invertible by A5,MATRIX_6:36;
(B0*A*C0)=(P*((SwapDiagonal(K,n,i0))*A)*((SwapDiagonal(K,n,j0))*Q)) by Th17
.=(P*((SwapDiagonal(K,n,i0))*A)*(SwapDiagonal(K,n,j0))*Q) by Th17
.=(P*A3*Q) by Th17;
hence thesis by A6,A7,A8;
end;
theorem Th54:
for A,B being Matrix of n,K st B*A=1.(K,n)
ex B2 being Matrix of n,K st A*B2=1.(K,n)
proof
let A,B be Matrix of n,K;
thus B*A=1.(K,n) implies ex B2 being Matrix of n,K st A*B2=1.(K,n)
proof
defpred P[Nat] means for D,B3 being Matrix of $1,K st B3*D=1.(K
,$1) holds ex B4 being Matrix of $1,K st D*B4=1.(K,$1);
assume
A1: B*A=1.(K,n);
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A3: P[k];
for A2,B3 being Matrix of k+1,K st B3*A2=1.(K,k+1) holds ex B4 being
Matrix of k+1,K st A2*B4=1.(K,k+1)
proof
let A2,B2 be Matrix of (k+1),K;
A4: Indices (1.(K,k+1))= [: Seg (k+1),Seg (k+1) :] by MATRIX_0:24;
assume
A5: B2*A2=1.(K,k+1);
then
A6: (Det B2)*(Det A2)= Det(1.(K,k+1)) by MATRIXR2:45;
now
assume A2=0.(K,k+1);
then A2=0.(K,k+1,k+1) by MATRIX_3:def 1;
then Det(A2)= 0.K by MATRIX_7:15,NAT_1:12;
then
A7: (Det B2)*(Det A2)=0.K;
not 0.K = 1_K;
hence contradiction by A6,A7,MATRIX_7:16,NAT_1:12;
end;
then consider B,C being Matrix of (k+1),K such that
A8: B is invertible and
A9: C is invertible and
A10: (B*A2*C)*(1,1) =1.K and
A11: for i st 1<i & i<=k+1 holds (B*A2*C)*(i,1)= 0.K and
A12: for j st 1<j & j<=k+1 holds (B*A2*C)*(1,j)= 0.K by Th53;
set A3=B*A2*C,B3=(C~)*B2*(B~);
A13: width B3=k+1 by MATRIX_0:24;
A14: width A3=k+1 by MATRIX_0:24;
A15: for j be Nat st 1<=j & j<=len (Line(A3,1)) holds (Line(A3,1)).j=
(Base_FinSeq(K,k+1,1)).j
proof
let j be Nat;
assume that
A16: 1<=j and
A17: j<=len (Line(A3,1));
A18: j<=k+1 by A14,A17,MATRIX_0:def 7;
len (Line(A3,1))=width A3 by MATRIX_0:def 7;
then
A19: j in Seg width A3 by A16,A17,FINSEQ_1:1;
per cases by A16,XXREAL_0:1;
suppose
A20: 1=j;
then (Line(A3,1)).j=1.K by A10,A19,MATRIX_0:def 7;
hence thesis by A18,A20,Th24;
end;
suppose
A21: 1<j;
A22: j in NAT by ORDINAL1:def 12;
(Line(A3,1)).j=A3*(1,j) by A19,MATRIX_0:def 7
.=0.K by A12,A18,A21,A22;
hence thesis by A18,A21,Th25;
end;
end;
A23: len (<* 0.K *>)=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<i & i<=k+1 holds B3*(i,1)=(1.(K,k+1))*(i,1)
proof
A32: len (Base_FinSeq(K,k+1,1))=k+1 by Th23;
let i be Nat;
A33: len (Col(A3,1))=len A3 by MATRIX_0:def 8
.=k+1 by MATRIX_0:24;
A34: len A3=k+1 by MATRIX_0:24;
A35: for k2 being Nat st 1<=k2 & k2<=len (Col(A3,1)) holds (Col(A3,1
)).k2=(Base_FinSeq(K,k+1,1)).k2
proof
let k2 be Nat;
assume that
A36: 1<=k2 and
A37: k2<=len (Col(A3,1));
A38: k2 in NAT by ORDINAL1:def 12;
A39: now
per cases by A36,XXREAL_0:1;
suppose
k2=1;
hence A3*(k2,1)=(Base_FinSeq(K,k+1,1)).k2 by A10,A33,A37,Th24;
end;
suppose
A40: 1<k2;
hence A3*(k2,1)= 0.K by A11,A33,A38,A37
.=(Base_FinSeq(K,k+1,1)).k2 by A33,A37,A40,Th25;
end;
end;
k2 in Seg len A3 by A34,A33,A36,A37,FINSEQ_1:1;
then k2 in dom A3 by FINSEQ_1:def 3;
hence thesis by A39,MATRIX_0:def 8;
end;
A41: len (Line(B3,i))=width B3 by MATRIX_0:def 7
.= k+1 by MATRIX_0:24;
assume
A42: 1<i & i<=k+1;
then
A43: 1<=k+1 by XXREAL_0:2;
A44: width B3=k+1 by MATRIX_0:24;
then
A45: 1 in Seg width B3 by A43,FINSEQ_1:1;
[i,1] in Indices (B3*A3) by A42,A43,MATRIX_0:31;
then (B3*A3)*(i,1)= |( Line(B3,i),Col(A3,1) )| by A44,A34,
MATRIX_3:def 4
.= |( Line(B3,i),Base_FinSeq(K,k+1,1) )| by A33,A32,A35,FINSEQ_1:14
.= (Line(B3,i)).1 by A43,A41,Th35
.= B3*(i,1) by A45,MATRIX_0:def 7;
hence thesis by A30;
end;
A46: k in NAT by ORDINAL1:def 12;
for i,j being Nat st 1<=i & i<=k & 1<=j & j<=k holds (
G*F)*(i,j)=IFEQ(i,j,1.K,0.K)
proof
let i,j be Nat;
assume that
A47: 1<=i and
A48: i<=k and
A49: 1<=j and
A50: j<=k;
A51: [i,j] in Indices (G*F) by A47,A48,A49,A50,MATRIX_0:31;
A52: for k2 being Nat st k2 in dom (<* 0.K *>) holds (Col(A3,j+1)).
k2=(<* 0.K *>).k2
proof
j+1<=k+1 & 1<j+1 by A49,A50,NAT_1:13,XREAL_1:7;
then
A53: A3*(1,j+1) = 0.K by A12;
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
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;
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<i+1 by A47,NAT_1:13;
1<=1+k by NAT_1:11;
then
A59: [i+1,1] in Indices (1.(K,k+1)) by A56,A58,MATRIX_0:31;
A60: B3*(i+1,1) = (1.(K,k+1))*(i+1,1) by A31,A56,A58
.= 0.K by A58,A59,MATRIX_1:def 3;
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
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;
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: 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,0.K,G2*(j-'1,1-'1)) by A100,FUNCOP_1:def 8
.=0.K by FUNCOP_1:def 8;
hence thesis by A96,A100,Th25;
end;
end;
A101: width (A3*B4)=k+1 by MATRIX_0:24;
A102: Indices (A3*B4)=[:Seg (k+1),Seg (k+1):] by MATRIX_0:24;
len (Line(A3,1))=width A3 by MATRIX_0:def 7
.=k+1 by MATRIX_0:24;
then
A103: len (Line(A3,1))=len (Base_FinSeq(K,k+1,1)) by Th23;
then
A104: Line(A3,1)=Base_FinSeq(K,k+1,1) by A15,FINSEQ_1:14;
A105: width F=k by MATRIX_0:24;
A106: 1<=k+1 by NAT_1:11;
len (Col(B4,1))=len B4 by MATRIX_0:def 8
.=k+1 by MATRIX_0:24;
then
A107: len (Col(B4,1))=len (Base_FinSeq(K,k+1,1)) by Th23;
then
A108: Col(B4,1)=Base_FinSeq(K,k+1,1) by A93,FINSEQ_1:14;
for i,j being Nat st [i,j] in Indices (A3*B4) holds (A3*B4)*(i,j
) = (1.(K,k+1))*(i,j)
proof
let i,j be Nat;
reconsider i0=i,j0=j as Element of NAT by ORDINAL1:def 12;
A109: len (Line(F,i-'1))=width F by MATRIX_0:def 7
.=k by MATRIX_0:24;
A110: len (Col(G2,j-'1)) = len G2 by MATRIX_0:def 8
.=k by MATRIX_0:24;
A111: len (Line(A3,i))=width A3 by MATRIX_0:def 7
.=k+1 by MATRIX_0:24;
A112: len (Col(B4,j))=len B4 by MATRIX_0:def 8
.=k+1 by MATRIX_0:24;
assume
A113: [i,j] in Indices (A3*B4);
then
A114: [i,j] in [:Seg (k+1),Seg (k+1) :] by MATRIX_0:24;
then
A115: [i,j] in Indices (1.(K,k+1)) by MATRIX_0:24;
A116: i in Seg (k+1) by A102,A113,ZFMISC_1:87;
then
A117: 1<=i by FINSEQ_1:1;
A118: i<=k+1 by A116,FINSEQ_1:1;
A119: j in Seg (k+1) by A101,A113,ZFMISC_1:87;
then
A120: 1<=j by FINSEQ_1:1;
A121: len B4=k+1 by MATRIX_0:24;
A122: width A3=k+1 by MATRIX_0:24;
A123: j<=k+1 by A119,FINSEQ_1:1;
A124: [i,j] in Indices B4 by A102,A113,MATRIX_0:24;
now
per cases by A117,XXREAL_0:1;
suppose
A125: i=1;
now
per cases by A120,XXREAL_0:1;
suppose
A126: j=1;
(A3*B4)*(i,j)=|( Line(A3,i0),Col(B4,j0) )| by A113,A121,A122,
MATRIX_3:def 4
.=1.K by A104,A108,A106,A125,A126,Th36;
hence thesis by A115,A125,A126,MATRIX_1:def 3;
end;
suppose
A127: j>1;
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<i;
then
A130: 1+1<=i by NAT_1:13;
now
per cases by A120,XXREAL_0:1;
suppose
A131: j=1;
A132: 1 in Seg width A3 by A14,A106,FINSEQ_1:1;
A133: len (Line(A3,i))=width A3 by MATRIX_0:def 7
.=k+1 by MATRIX_0:24;
(A3*B4)*(i,j)=|( Line(A3,i0),Col(B4,j0) )| by A113,A121,A122,
MATRIX_3:def 4
.=|( Line(A3,i),Base_FinSeq(K,k+1,1) )| by A107,A93,A131,
FINSEQ_1:14
.=(Line(A3,i)).1 by A106,A133,Th35
.=(B*A2*C)*(i0,1) by A132,MATRIX_0:def 7
.= 0.K by A11,A118,A129;
hence thesis by A115,A129,A131,MATRIX_1:def 3;
end;
suppose
A134: j>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;
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;
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<k2+1 by NAT_1:13;
k2 in Seg k by A158,A160,FINSEQ_1:def 3;
then
A162: k2 in dom G2 by A89,FINSEQ_1:def 3;
k2<=k by A158,A160,FINSEQ_3:25;
then
A163: 1<=k2+1 & k2+1<=k+1 by NAT_1:11,XREAL_1:7;
then [k2+1,j] in Indices B4 by A120,A123,MATRIX_0:31;
then B4*(k2+1,j) = IFEQ(k2+1,1, IFEQ(j,1,1.K,0.K), IFEQ(j
,1,0.K,G2*(k2+1-'1,j-'1))) by A90;
then B4*(k2+1,j) = IFEQ(j,1,0.K,G2*(k2+1-'1,j-'1)) by A161,
FUNCOP_1:def 8
.= G2*(k2+1-'1,j-'1) by A134,FUNCOP_1:def 8
.= G2*(k2,j-'1) by NAT_D:34;
then
A164: B4*(k2+1,j-'1+1)=(Col(G2,j-'1)).k2 by A152,A162,
MATRIX_0:def 8;
k2+1 in dom B4 by A121,A163,FINSEQ_3:25;
then (Col(B4,j-'1+1)).(k2+1) = (Col(G2,j-'1)).k2 by A164,
MATRIX_0:def 8;
hence thesis by FINSEQ_1:40;
end;
dom (Col(B4,j-'1+1)) = Seg len (Col(B4,j-'1+1)) by
FINSEQ_1:def 3
.=Seg (len (<* 0.K *>) + 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;