:: Laplace Expansion
:: by Karol P\c{a}k and Andrzej Trybulec
::
:: Received August 13, 2007
:: Copyright (c) 2007-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, SUBSET_1, NAT_1, XBOOLE_0, MATRIX11, FINSEQ_1, ARYTM_3,
VECTSP_1, MATRIX_1, RELAT_1, FINSEQ_3, ARYTM_1, TREES_1, CARD_1,
XXREAL_0, FUNCT_1, INCSP_1, TARSKI, ALGSTR_0, ZFMISC_1, STRUCT_0,
REALSET1, SETWOP_2, FUNCT_2, FINSUB_1, GROUP_1, SETWISEO, INT_1,
FINSET_1, ABIAN, FINSEQ_2, BINOP_1, QC_LANG1, AFINSQ_1, ABSVALUE,
MATRIX_3, SUPINF_2, CARD_3, FINSOP_1, RVSUM_1, FVSUM_1, MESFUNC1,
MATRIX_6, LAPLACE, FUNCT_7, FUNCSDOM, GCD_1, VECTSP_2, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XXREAL_0, FINSET_1, RELAT_1, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2,
FINSEQ_1, BINOP_1, STRUCT_0, ALGSTR_0, GROUP_1, GCD_1,
VECTSP_1, SETWISEO, VECTSP_2,
SETWOP_2, FINSEQ_2, MATRIX_0, FINSUB_1, MATRIX_1, NAT_1, FVSUM_1,
FINSOP_1, MATRIX_3, CARD_1, FINSEQ_7, NEWTON, MATRIX_7, FINSEQ_3,
MATRIX11, MATRIX_6, NAT_D;
constructors SETWISEO, FINSOP_1, SETWOP_2, ALGSTR_1, FVSUM_1, BINOP_1,
FINSEQ_4, FINSEQ_7, WELLORD2, NEWTON, MATRIX_6, MATRIX_7, MATRIX11,
NAT_D, BINOP_2, RELSET_1, XXREAL_0, NAT_1, VECTSP_2, MATRIX_3,
GCD_1, ORDINAL1;
registrations FUNCT_1, FINSUB_1, FINSET_1, STRUCT_0, FVSUM_1, MATRIX_1,
VECTSP_1, FUNCT_2, PARTFUN1, XBOOLE_0, ORDINAL1, XXREAL_0, NAT_1, INT_1,
RELAT_1, CARD_1, MATRIX11, XCMPLX_0, RELSET_1, FINSEQ_2, FINSEQ_1,
MATRIX_0, MATRIX_6, VECTSP_2, MATRIX_3, GCD_1;
requirements ARITHM, NUMERALS, REAL, BOOLE, SUBSET;
definitions TARSKI;
equalities FINSEQ_2, FINSEQ_1, MATRIX_0, MATRIX_3, FVSUM_1, MATRIX11, RELAT_1,
ALGSTR_0;
expansions FINSEQ_1, TARSKI;
theorems FINSEQ_1, FINSEQ_2, TARSKI, FUNCT_2, NAT_1, FUNCT_1, SETWISEO,
VECTSP_1, ZFMISC_1, FVSUM_1, SETWOP_2, MATRIX_0, MATRIX_1, FINSUB_1,
FINSEQ_3, RELAT_1, FINSOP_1, XBOOLE_0, XBOOLE_1, MATRIX_3, XREAL_1,
MATRIX_7, ORDINAL1, CARD_1, CARD_2, MATRIX_9, FINSEQ_4, SGRAPH1,
CARD_FIN, HURWITZ, NEWTON, COMPUT_1, MATRIX11, GROUP_1, MATRIX_4,
MATRIX_6, MATRIXR1, NAT_D, SUBSET_1, XXREAL_0, MATRIXR2, XREAL_0,
STRUCT_0, ALGSTR_0, GCD_1;
schemes FUNCT_2, NAT_1, FINSEQ_1, FUNCT_1, SETWISEO, MATRIX_0;
begin :: Preliminaries
reserve x,y for object,
N for Element of NAT,
c,i,j,k,m,n for Nat,
D for non empty set,
s for Element of 2Set Seg (n+2),
p for Element of Permutations(n) ,
p1, q1 for Element of Permutations(n+1),
p2 for Element of Permutations(n +2),
K for commutative Ring, ::Field,
a for Element of K,
f for FinSequence of K,
A for (Matrix of K),
AD for Matrix of n,m,D,
pD for FinSequence of D,
M for Matrix of n,K;
theorem Th1:
for f be FinSequence, i be Nat st i in dom f holds len Del(f,i) = len f -' 1
proof
let f be FinSequence, i be Nat;
assume i in dom f;
then ex m be Nat st len f = m + 1 & len Del(f,i) = m by FINSEQ_3:104;
hence thesis by NAT_D:34;
end;
theorem Th2:
for i,j,n being Nat, M being Matrix of n,K st i in dom M holds
len Deleting(M,i,j) = n-'1
proof
let i,j,n be Nat, M be Matrix of n,K;
assume
A1: i in dom M;
A2: len M = n by MATRIX_0:def 2;
thus len Deleting(M,i,j)= len DelLine(M,i) by MATRIX_0:def 13
.= n-'1 by A1,A2,Th1;
end;
theorem Th3:
j in Seg width A implies width DelCol(A,j) = width A-'1
proof
set DC=DelCol(A,j);
A1: len DC = len A by MATRIX_0:def 13;
assume
A2: j in Seg width A;
then Seg width A <> {};
then width A <>0;
then len A > 0 by MATRIX_0:def 3;
then consider t being FinSequence such that
A3: t in rng DC and
A4: len t = width DC by A1,MATRIX_0:def 3;
consider k9 be object such that
A5: k9 in dom DelCol(A,j) and
A6: DC.k9 = t by A3,FUNCT_1:def 3;
k9 in Seg len DC by A5,FINSEQ_1:def 3;
then consider k being Nat such that
A7: k9=k and
1<=k and
k<=len DC;
k in dom A by A1,A5,A7,FINSEQ_3:29;
then
A8: t=Del(Line(A,k),j) by A6,A7,MATRIX_0:def 13;
A9: len Line(A,k)=width A by MATRIX_0:def 7;
then dom Line(A,k)=Seg (width A) by FINSEQ_1:def 3;
hence thesis by A2,A4,A9,A8,Th1;
end;
theorem Th4:
for i be Nat st len A > 1 holds width A = width DelLine(A,i)
proof
let i be Nat;
assume
A1: len A>1;
per cases;
suppose
i in dom A;
then consider m be Nat such that
A2: len A = m + 1 and
A3: len Del(A,i) = m by FINSEQ_3:104;
A4: m>=1 by A1,A2,NAT_1:13;
then
A5: m in dom Del(A,i) by A3,FINSEQ_3:25;
then
A6: DelLine(A,i).m in rng Del(A,i) by FUNCT_1:def 3;
A7: rng Del(A,i) c= rng A by FINSEQ_3:106;
A8: DelLine(A,i).m=Line(DelLine(A,i),m) by A5,MATRIX_0:60;
A is Matrix of len A,width A,K by A1,MATRIX_0:20;
then len Line(DelLine(A,i),m)=width A by A6,A8,A7,MATRIX_0:def 2;
hence thesis by A3,A4,A6,A8,MATRIX_0:def 3;
end;
suppose
not i in dom A;
hence thesis by FINSEQ_3:104;
end;
end;
theorem Th5:
for i being Nat st j in Seg width M holds width Deleting(M,i,j) = n-' 1
proof
let i be Nat;
assume
A1: j in Seg width M;
per cases;
suppose
A2: len M<=1 & i in dom M;
Seg width M <> {} by A1;
then width M <> {};
then len M > 0 by MATRIX_0:def 3;
then
A3: len M=1 by A2,NAT_1:25;
A4: len Deleting(M,i,j)=n-'1 by A2,Th2;
len M=n by MATRIX_0:24;
then len Deleting(M,i,j)=0 by A3,A4,XREAL_1:232;
hence thesis by A4,MATRIX_0:def 3;
end;
suppose
A5: len M>1;
A6: width M=n by MATRIX_0:24;
width M=width DelLine(M,i) by A5,Th4;
hence thesis by A1,A6,Th3;
end;
suppose
A7: not i in dom M;
A8: width M=n by MATRIX_0:24;
DelLine(M,i)=M by A7,FINSEQ_3:104;
hence thesis by A1,A8,Th3;
end;
end;
definition
let G be non empty multMagma;
let B be Function of [:the carrier of G,NAT:], the carrier of G;
let g be Element of G, i be Nat;
redefine func B.(g,i) -> Element of G; :: redefines . (BINOP_1, definition)
coherence
proof
reconsider i as Element of NAT by ORDINAL1:def 12;
B.(g,i) is Element of G;
hence thesis;
end;
end;
theorem Th6:
card Permutations n = n!
proof
set P = Permutations(n);
reconsider N=n as Element of NAT by ORDINAL1:def 12;
set X=finSeg N;
set PER={F where F is Function of X,X:F is Permutation of X};
A1: P c= PER
proof
let x be object;
assume x in P;
then x is Permutation of X by MATRIX_1:def 16;
hence thesis;
end;
PER c= P
proof
let x be object;
assume x in PER;
then ex F be Function of X,X st x=F & F is Permutation of X;
hence thesis by MATRIX_1:def 16;
end;
then P=PER by A1,XBOOLE_0:def 10;
hence card P = card X! by CARD_FIN:8
.= n! by FINSEQ_1:57;
end;
theorem Th7:
for i,j st i in Seg (n+1) & j in Seg (n+1) holds card {p1: p1.i = j} = n!
proof
let i,j such that
A1: i in Seg (n+1) and
A2: j in Seg (n+1);
reconsider N = n as Element of NAT by ORDINAL1:def 12;
set n1=N+1;
set X=finSeg n1;
set Y=X\{j};
A3: Y\/{j}=X by A2,ZFMISC_1:116;
set X9=X\{i};
set P1=Permutations n1;
set F={p where p is Element of P1:p.i=j};
set F9={f where f is Function of X9\/{i},Y\/{j}:f is one-to-one & f.i=j};
A4: X9\/{i}=X by A1,ZFMISC_1:116;
A5: F9 c= F
proof
let x be object;
assume x in F9;
then consider f be Function of X,X such that
A6: f=x and
A7: f is one-to-one and
A8: f.i=j by A4,A3;
card X=card X;
then f is onto by A7,FINSEQ_4:63;
then f in P1 by A7,MATRIX_1:def 16;
hence thesis by A6,A8;
end;
F c= F9
proof
let x be object;
assume x in F;
then consider p be Element of P1 such that
A9: x=p and
A10: p.i=j;
reconsider p as Permutation of X by MATRIX_1:def 16;
p.i=j by A10;
hence thesis by A4,A3,A9;
end;
then
A11: F=F9 by A5,XBOOLE_0:def 10;
A12: card X=n1 by FINSEQ_1:57;
A13: not j in Y by ZFMISC_1:56;
then
A14: card X=card Y+1 by A3,CARD_2:41;
A15: not i in X9 by ZFMISC_1:56;
then
A16: card X=card X9+1 by A4,CARD_2:41;
then Y is empty implies X9 is empty by A14;
hence card {p1: p1.i = j} = card {f where f is Function of X9,Y:f is
one-to-one} by A15,A13,A11,CARD_FIN:5
.= card Y!/((card Y-'card X9)!) by A16,A14,CARD_FIN:7
.= card Y!/1 by A16,A14,NEWTON:12,XREAL_1:232
.= n! by A14,A12;
end;
theorem Th8:
for K be Fanoian domRing
for p2 for X,Y be Element of Fin 2Set Seg
(n+2) st Y={s:s in X & Part_sgn(p2,K).s = -1_K} holds (the multF of K) $$ (X,
Part_sgn(p2,K)) = power(K).(-1_K,card Y)
proof
let K be Fanoian domRing;
let p2;
set n2=n+2;
let X,Y be Element of Fin 2Set Seg n2 such that
A1: Y={s:s in X & Part_sgn(p2,K).s = -1_K};
reconsider ID = id Seg n2 as Element of Permutations(n2) by MATRIX_1:def 16;
set Y9= {s:s in X & Part_sgn(p2,K).s <> Part_sgn(ID,K).s};
A2: for x st x in X holds Part_sgn(ID,K).x = 1_K
proof
A3: X c= 2Set Seg n2 by FINSUB_1:def 5;
let x;
assume x in X;
then consider i,j be Nat such that
A4: i in Seg n2 and
A5: j in Seg n2 and
A6: i < j and
A7: x = {i,j} by A3,MATRIX11:1;
A8: ID.j=j by A5,FUNCT_1:17;
ID.i=i by A4,FUNCT_1:17;
hence thesis by A4,A5,A6,A7,A8,MATRIX11:def 1;
end;
A9: Y9 c= Y
proof
let y be object;
assume y in Y9;
then consider s such that
A10: y=s and
A11: s in X and
A12: Part_sgn(p2,K).s <> Part_sgn(ID,K).s;
Part_sgn(ID,K).s=1_K by A2,A11;
then Part_sgn(p2,K).s =-1_K by A12,MATRIX11:5;
hence thesis by A1,A10,A11;
end;
Y c= Y9
proof
let y be object;
A13: 1_K<>-1_K by MATRIX11:22;
assume y in Y;
then consider s such that
A14: s=y and
A15: s in X and
A16: Part_sgn(p2,K).s = -1_K by A1;
Part_sgn(ID,K).s=1_K by A2,A15;
hence thesis by A14,A15,A16,A13;
end;
then
A17: Y=Y9 by A9,XBOOLE_0:def 10;
per cases by NAT_D:12;
suppose
A18: card Y mod 2 = 0;
then consider t be Nat such that
A19: card Y = 2 * t + 0 and
0 < 2 by NAT_D:def 2;
t is Element of NAT by ORDINAL1:def 12;
hence power(K).(-1_K,card Y)=1_K by A19,HURWITZ:4
.= (the multF of K) $$ (X,Part_sgn(ID,K)) by A2,MATRIX11:4
.= (the multF of K) $$ (X,Part_sgn(p2,K)) by A17,A18,MATRIX11:7;
end;
suppose
A20: card Y mod 2 = 1;
then consider t be Nat such that
A21: card Y = 2 * t + 1 and
1 < 2 by NAT_D:def 2;
t is Element of NAT by ORDINAL1:def 12;
hence power(K).(-1_K,card Y)=-1_K by A21,HURWITZ:4
.= -(the multF of K) $$ (X,Part_sgn(ID,K)) by A2,MATRIX11:4
.= (the multF of K) $$ (X,Part_sgn(p2,K)) by A17,A20,MATRIX11:7;
end;
end;
theorem Th9:
for K be Fanoian domRing
for p2,i,j st i in Seg (n+2) & p2.i=j ex X
be Element of Fin 2Set Seg (n+2) st
X = {{N,i} where N is Nat : {N,i} in 2Set Seg (n+2)} & (
the multF of K) $$ (X,Part_sgn(p2,K)) = power(K).(-1_K,i+j)
proof
let K be Fanoian domRing;
let p2,i,j such that
A1: i in Seg (n+2) and
A2: p2.i=j;
reconsider N=n as Element of NAT by ORDINAL1:def 12;
set n2=N+2;
reconsider p29=p2 as Permutation of finSeg n2 by MATRIX_1:def 16;
A3: rng p29=Seg n2 by FUNCT_2:def 3;
1<=i by A1,FINSEQ_1:1;
then reconsider i1=i-1 as Element of NAT by NAT_1:21;
deffunc F(object)={$1,i};
set Ui=(finSeg n2)\(Seg i);
set Li=finSeg i1;
set SS=2Set Seg(n+2);
set X={{k,i} where k is Nat :{k,i} in 2Set Seg(n+2)};
A4: X c= SS
proof
let x be object;
assume x in X;
then ex k being Nat st x={k,i} & {k,i} in 2Set Seg n2;
hence thesis;
end;
then reconsider X as Element of Fin SS by FINSUB_1:def 5;
set Y={s:s in X & Part_sgn(p2,K).s=-1_K};
A5: Y c= X
proof
let x be object;
assume x in Y;
then ex s st s=x & s in X & Part_sgn(p2,K).s=-1_K;
hence thesis;
end;
then
A6: Y c= SS by A4;
dom p29=Seg n2 by FUNCT_2:52;
then
A7: p2.i in rng p2 by A1,FUNCT_1:def 3;
then 1<= j by A2,A3,FINSEQ_1:1;
then reconsider j1=j-1 as Element of NAT by NAT_1:21;
reconsider Y as Element of Fin SS by A6,FINSUB_1:def 5;
consider f be Function such that
A8: dom f = Li\/Ui &
for x being object st x in Li\/Ui holds f.x = F(x) from FUNCT_1
:sch 3;
A9: f"Y c= dom f by RELAT_1:132;
then reconsider fY=f"Y as finite set by A8;
A10: Li\/Ui c= Seg n2\{i}
proof
let x be object such that
A11: x in Li\/Ui;
per cases by A11,XBOOLE_0:def 3;
suppose
A12: x in Li;
A13: i<=n2 by A1,FINSEQ_1:1;
consider k being Nat such that
A14: x=k and
A15: 1<=k and
A16: k<=i1 by A12;
A17: i1<i1+1 by NAT_1:13;
then k<i by A16,XXREAL_0:2;
then k<=n2 by A13,XXREAL_0:2;
then
A18: k in Seg n2 by A15;
not k in {i} by A16,A17,TARSKI:def 1;
hence thesis by A14,A18,XBOOLE_0:def 5;
end;
suppose
A19: x in Ui;
A20: (i1+1) in Seg i by FINSEQ_1:4;
not x in Seg i by A19,XBOOLE_0:def 5;
then not x in {i} by A20,TARSKI:def 1;
hence thesis by A19,XBOOLE_0:def 5;
end;
end;
for x1,x2 be object st x1 in dom f & x2 in dom f & f.x1 = f.x2 holds x1 = x2
proof
let x1,x2 be object such that
A21: x1 in dom f and
A22: x2 in dom f and
A23: f.x1 = f.x2;
A24: f.x2=F(x2) by A8,A22;
not x1 in {i} by A10,A8,A21,XBOOLE_0:def 5;
then
A25: x1<>i by TARSKI:def 1;
f.x1=F(x1) by A8,A21;
then x1 in {i,x2} by A23,A24,TARSKI:def 2;
hence thesis by A25,TARSKI:def 2;
end;
then f is one-to-one by FUNCT_1:def 4;
then (f.:fY),(fY) are_equipotent by A9,CARD_1:33;
then
A26: card (f.:fY) = card fY by CARD_1:5;
finSeg n2\{i} c= Li\/Ui
proof
let x be object such that
A27: x in finSeg n2\{i};
x in finSeg n2 by A27;
then consider k being Nat such that
A28: x=k and
A29: 1<=k and
A30: k<=n2;
not k in {i} by A27,A28,XBOOLE_0:def 5;
then
A31: k<>i by TARSKI:def 1;
per cases by A31,XXREAL_0:1;
suppose
k<i1+1;
then k<=i1 by NAT_1:13;
then x in Li by A28,A29;
hence thesis by XBOOLE_0:def 3;
end;
suppose
k>i1+1;
then
A32: not x in Seg i by A28,FINSEQ_1:1;
x in Seg n2 by A28,A29,A30;
then x in Ui by A32,XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
end;
then
A33: finSeg n2\{i}=Li\/Ui by A10,XBOOLE_0:def 10;
A34: rng f c= X
proof
let x be object;
assume x in rng f;
then consider y being object such that
A35: y in dom f and
A36: f.y=x by FUNCT_1:def 3;
y in finSeg n2 by A33,A8,A35;
then consider k being Nat such that
A37: k=y and
A38: 1<= k and
A39: k<=n2;
A40: f.k={i,k} by A8,A35,A37;
not y in {i} by A10,A8,A35,XBOOLE_0:def 5;
then i<>k by A37,TARSKI:def 1;
then
A41: k<i or i<k by XXREAL_0:1;
k in Seg n2 by A38,A39;
then {i,k} in SS by A1,A41,MATRIX11:1;
hence thesis by A36,A37,A40;
end;
A42: p29.:((Li\f"Y)\/(Ui/\f"Y)) c= Seg j1
proof
let y be object;
assume y in p29.:((Li\f"Y)\/(Ui/\f"Y));
then consider x being object such that
A43: x in dom p29 and
A44: x in (Li\f"Y)\/(Ui/\f"Y) and
A45: p29.x=y by FUNCT_1:def 6;
dom p29=Seg n2 by FUNCT_2:52;
then consider k being Nat such that
A46: x=k and
A47: 1<=k and
A48: k<=n2 by A43;
per cases by A44,A46,XBOOLE_0:def 3;
suppose
A49: k in (Li\f"Y);
then k<=i1 by FINSEQ_1:1;
then
A50: k<i1+1 by NAT_1:13;
A51: Li c= dom f by A8,XBOOLE_1:7;
A52: k in Li by A49;
then
A53: f.k in rng f by A51,FUNCT_1:def 3;
not k in f"Y by A49,XBOOLE_0:def 5;
then
A54: not f.k in Y by A52,A51,FUNCT_1:def 7;
A55: k in Seg n2 by A47,A48;
dom p29=Seg n2 by FUNCT_2:52;
then
A56: p2.i<>p2.k by A1,A50,A55,FUNCT_1:def 4;
A57: f.k=F(k) by A8,A52,A51;
then F(k) in X by A34,A53;
then ex m being Nat st F(k)={m,i} & {m,i} in SS;
then Part_sgn(p2,K).{k,i}<>-1_K by A34,A54,A53,A57;
then p2.k <= p2.i by A1,A50,A55,MATRIX11:def 1;
then p2.k < j1+1 by A2,A56,XXREAL_0:1;
then
A58: p2.k <= j1 by NAT_1:13;
A59: rng p29=Seg n2 by FUNCT_2:def 3;
p2.k in rng p29 by A43,A46,FUNCT_1:def 3;
then 1<=p2.k by A59,FINSEQ_1:1;
hence thesis by A45,A46,A58;
end;
suppose
A60: k in (Ui/\f"Y);
then k in Ui by XBOOLE_0:def 4;
then
A61: not k in Seg i by XBOOLE_0:def 5;
1<= k by A60,FINSEQ_1:1;
then
A62: i<k by A61;
A63: k in f"Y by A60,XBOOLE_0:def 4;
then f.k in Y by FUNCT_1:def 7;
then consider s such that
A64: s=f.k and
s in X and
A65: Part_sgn(p2,K).s=-1_K;
k in dom f by A63,FUNCT_1:def 7;
then
A66: s = {i,k} by A8,A64;
dom p29=finSeg n2 by FUNCT_2:52;
then
A67: p29.i<>p2.k by A1,A60,A62,FUNCT_1:def 4;
reconsider i,k as Element of NAT by ORDINAL1:def 12;
1_K<>-1_K by MATRIX11:22;
then p2.i>=p2.k by A1,A60,A65,A66,A62,MATRIX11:def 1;
then p2.k <j1+1 by A2,A67,XXREAL_0:1;
then
A68: p2.k<=j1 by NAT_1:13;
A69: rng p29=Seg n2 by FUNCT_2:def 3;
p2.k in rng p29 by A43,A46,FUNCT_1:def 3;
then 1<=p2.k by A69,FINSEQ_1:1;
hence thesis by A45,A46,A68;
end;
end;
take X;
reconsider I=i, J=j as Element of NAT by ORDINAL1:def 12;
set P=power(K);
thus X = {{e,i} where e is Nat :{e,i} in 2Set Seg (n+2)};
A70: Li/\f"Y c= Li by XBOOLE_1:17;
Seg j1 c= p29.:((Li\f"Y)\/(Ui/\f"Y))
proof
let y be object such that
A71: y in Seg j1;
consider k being Nat such that
A72: y=k and
1<=k and
A73: k<=j1 by A71;
A74: j1<j1+1 by NAT_1:13;
then
A75: k < j by A73,XXREAL_0:2;
j <=n2 by A2,A7,A3,FINSEQ_1:1;
then j1<=n2 by A74,XXREAL_0:2;
then Seg j1 c= Seg n2 by FINSEQ_1:5;
then consider x being object such that
A76: x in dom p29 and
A77: y=p29.x by A3,A71,FUNCT_1:def 3;
A78: not x in {i} by A2,A72,A73,A74,A77,TARSKI:def 1;
then
A79: x in dom f by A33,A8,A76,XBOOLE_0:def 5;
then
A80: f.x=F(x) by A8;
A81: f.x in rng f by A79,FUNCT_1:def 3;
then F(x) in X by A34,A80;
then consider m being Nat such that
A82: F(x)={m,i} and
A83: {m,i} in 2Set Seg n2;
A84: m<>i by A83,SGRAPH1:10;
A85: m in Seg n2 by A83,SGRAPH1:10;
m in {x,i} by A82,TARSKI:def 2;
then
A86: m=x by A84,TARSKI:def 2;
reconsider m,i as Element of NAT by ORDINAL1:def 12;
per cases by A83,SGRAPH1:10,XXREAL_0:1;
suppose
A87: m<i;
A88: not m in f"Y
proof
assume m in f"Y;
then {m,i} in Y by A80,A86,FUNCT_1:def 7;
then
A89: ex s st s={m,i} & s in X & Part_sgn(p2,K).s=-1_K;
Part_sgn(p2,K).{m,i}=1_K by A1,A2,A72,A75,A76,A77,A86,A87,
MATRIX11:def 1;
hence thesis by A89,MATRIX11:22;
end;
m<i1+1 by A87;
then
A90: m<=i1 by NAT_1:13;
1<=m by A85,FINSEQ_1:1;
then m in Li by A90;
then x in Li\f"Y by A86,A88,XBOOLE_0:def 5;
then x in (Li\f"Y)\/(Ui/\f"Y) by XBOOLE_0:def 3;
hence thesis by A76,A77,FUNCT_1:def 6;
end;
suppose
A91: m>i;
then not m in Seg i by FINSEQ_1:1;
then
A92: x in Ui by A86,A85,XBOOLE_0:def 5;
Part_sgn(p2,K).{m,i}=-1_K by A1,A2,A72,A75,A76,A77,A86,A91,MATRIX11:def 1
;
then
A93: f.x in Y by A34,A80,A81,A82,A83;
x in dom f by A33,A8,A76,A78,XBOOLE_0:def 5;
then x in f"Y by A93,FUNCT_1:def 7;
then x in Ui/\f"Y by A92,XBOOLE_0:def 4;
then x in (Li\f"Y)\/(Ui/\f"Y) by XBOOLE_0:def 3;
hence thesis by A76,A77,FUNCT_1:def 6;
end;
end;
then
A94: Seg j1 = p29.:((Li\f"Y)\/(Ui/\f"Y)) by A42,XBOOLE_0:def 10;
A95: Seg n2 = dom p29 by FUNCT_2:52;
A96: Li\f"Y=Li\(f"Y/\Li) by XBOOLE_1:47;
i1<i1+1 by NAT_1:13;
then Li c= Seg i by FINSEQ_1:5;
then
A97: Li misses Ui by XBOOLE_1:64,79;
X c= rng f
proof
let x be object;
assume x in X;
then consider k being Nat such that
A98: x={k,i} and
A99: {k,i} in SS;
k<>i by A99,SGRAPH1:10;
then
A100: not k in {i} by TARSKI:def 1;
k in Seg n2 by A99,SGRAPH1:10;
then
A101: k in Li\/Ui by A33,A100,XBOOLE_0:def 5;
then f.k=F(k) by A8;
hence thesis by A8,A98,A101,FUNCT_1:def 3;
end;
then X = rng f by A34,XBOOLE_0:def 10;
then
A102: f.:fY = Y by A5,FUNCT_1:77;
(Li/\f"Y)\/(Ui/\f"Y)=(dom f)/\f"Y by A8,XBOOLE_1:23;
then
A103: (Li/\f"Y)\/(Ui/\f"Y) = f"Y by RELAT_1:132,XBOOLE_1:28;
A104: Ui/\f"Y c= Ui by XBOOLE_1:17;
then (Li\f"Y)\/(Ui/\f"Y) c= finSeg n2\{i} by A33,XBOOLE_1:13;
then finSeg j1,(Li\f"Y)\/(Ui/\f"Y) are_equipotent by A95,A94,CARD_1:33
,XBOOLE_1:1;
then
A105: card (finSeg j1) = card ((Li\f"Y)\/(Ui/\f"Y)) by CARD_1:5
.= card (Li\(f"Y/\Li)) +card (Ui/\f"Y) by A97,A104,A96,CARD_2:40
,XBOOLE_1:64
.= (card Li -card (f"Y/\Li))+card (Ui/\f"Y) by CARD_2:44,XBOOLE_1:17;
per cases;
suppose
j>i;
then reconsider ji=j-i as Element of NAT by NAT_1:21;
card Y = card (Li/\fY)+card (finSeg j1)-card Li+card (fY/\Li) by A97,A70
,A104,A103,A26,A102,A105,CARD_2:40,XBOOLE_1:64
.= 2*card (Li/\fY) +card (finSeg j1)-card Li
.= 2*card (Li/\fY)+j1-card Li by FINSEQ_1:57
.= 2*card (Li/\fY)+j1-i1 by FINSEQ_1:57
.= 2*card (Li/\fY)+ji;
hence (the multF of K) $$ (X,Part_sgn(p2,K)) = P.(-1_K,2*card (Li/\fY)+ji)
by Th8
.= P.(-1_K,2*card (Li/\fY)) * P.(-1_K,ji) by HURWITZ:3
.= 1_K * P.(-1_K,ji) by HURWITZ:4
.= P.(-1_K,2*I)*P.(-1_K,ji) by HURWITZ:4
.= P.(-1_K,2*i+ji) by HURWITZ:3
.= P.(-1_K,i+j);
end;
suppose
j<=i;
then reconsider ij=i-j as Element of NAT by NAT_1:21;
card Y = (card Li+card (Ui/\fY)-card (finSeg j1))+ card(Ui/\fY) by A97,A70
,A104,A103,A26,A102,A105,CARD_2:40,XBOOLE_1:64
.= 2*card (Ui/\fY)-card (finSeg j1)+card Li
.= 2*card (Ui/\fY)-j1+card Li by FINSEQ_1:57
.= 2*card (Ui/\fY)-j1+i1 by FINSEQ_1:57
.= 2*card (Ui/\fY)+ij;
hence (the multF of K) $$ (X,Part_sgn(p2,K)) = P.(-1_K,2*card (Ui/\fY)+ij)
by Th8
.= P.(-1_K,2*card (Ui/\fY)) * P.(-1_K,ij) by HURWITZ:3
.= 1_K * P.(-1_K,ij) by HURWITZ:4
.= P.(-1_K,2*J)*P.(-1_K,ij) by HURWITZ:4
.= P.(-1_K,2*j+ij) by HURWITZ:3
.= P.(-1_K,i+j);
end;
end;
theorem Th10:
for i,j st i in Seg (n+1) & n >= 2 ex Proj be Function of 2Set
Seg n, 2Set Seg(n+1)
st rng Proj = 2Set Seg(n+1)\{{N,i} where N is Nat:{N,i} in 2Set Seg(n+1)}
& Proj is one-to-one & for k,m st k<m & {k,m} in 2Set Seg n holds (m < i & k <
i implies Proj.{k,m} = {k,m} ) & (m >= i & k < i implies Proj.{k,m} = {k,m+1} )
& (m >= i & k >= i implies Proj.{k,m} = {k+1,m+1})
proof
let i,j be Nat such that
A1: i in Seg (n+1) and
A2: n>=2;
defpred P[object,object] means
for k,m being Nat st {k,m}=$1 & k<m holds (m < i &
k < i implies $2={k,m}) & (m >= i & k<i implies $2={k,m+1})&(m >= i & k >= i
implies $2={k+1,m+1});
set X={{N,i} where N is Nat:{N,i} in 2Set Seg(n+1)};
set SS=2Set Seg(n);
set n1=n+1;
set SS1=2Set Seg n1;
A3: for k,m be Nat st {k,m} in X holds k=i or m=i
proof
let k,m be Nat;
assume {k,m} in X;
then consider m1 be Nat such that
A4: {k,m}={m1,i} and
{m1,i} in SS1;
i in {i,m1} by TARSKI:def 2;
hence thesis by A4,TARSKI:def 2;
end;
A5: for x being object st x in SS ex y being object st y in SS1\X & P[x,y]
proof
n<=n+1 by NAT_1:11;
then
A6: Seg n c= Seg n1 by FINSEQ_1:5;
reconsider N=n as Element of NAT by ORDINAL1:def 12;
let x be object;
assume x in SS;
then consider k,m be Nat such that
A7: k in Seg n and
A8: m in Seg n and
A9: k < m and
A10: x={k,m} by MATRIX11:1;
A11: m+1 in Seg (N+1) by A8,FINSEQ_1:60;
reconsider e = k as Element of NAT by ORDINAL1:def 12;
A12: e+1 in Seg(N+1) by A7,FINSEQ_1:60;
per cases;
suppose
A13: m<i & k<i;
then
A14: not {k,m} in X by A3;
{k,m} in SS1 by A7,A8,A9,A6,MATRIX11:1;
then
A15: {k,m} in SS1\X by A14,XBOOLE_0:def 5;
P[{k,m},{k,m}] by A13,ZFMISC_1:6;
hence thesis by A10,A15;
end;
suppose
A16: m>=i & k<i;
A17: P[{k,m},{k,m+1}]
proof
let k9,m9 be Nat such that
A18: {k9,m9}={k,m} and
k9<m9;
k9=k or k9=m by A18,ZFMISC_1:6;
hence thesis by A16,A18,ZFMISC_1:6;
end;
m+1>i by A16,NAT_1:13;
then
A19: not {k,m+1} in X by A3,A16;
m+1>k by A9,NAT_1:13;
then {k,m+1} in SS1 by A7,A6,A11,MATRIX11:1;
then {k,m+1} in SS1\X by A19,XBOOLE_0:def 5;
hence thesis by A10,A17;
end;
suppose
m<i & k>=i;
hence thesis by A9,XXREAL_0:2;
end;
suppose
A20: m>=i & k>=i;
A21: P[{k,m},{k+1,m+1}]
proof
let k9,m9 be Nat such that
A22: {k9,m9}={k,m} and
A23: k9<m9;
k9=k or k9=m by A22,ZFMISC_1:6;
hence thesis by A20,A22,A23,ZFMISC_1:6;
end;
A24: k+1>i by A20,NAT_1:13;
m+1>k+1 by A9,XREAL_1:8;
then
A25: {k+1,m+1} in SS1 by A11,A12,MATRIX11:1;
m+1>i by A20,NAT_1:13;
then not {k+1,m+1} in X by A3,A24;
then {k+1,m+1} in SS1\X by A25,XBOOLE_0:def 5;
hence thesis by A10,A21;
end;
end;
consider f be Function of SS,SS1\X such that
A26: for x being object st x in SS holds P[x,f.x] from FUNCT_2:sch 1(A5);
ex y being object st y in SS1\X & P[{1,2},y] by A2,A5,MATRIX11:3;
then reconsider SSX=SS1\X as non empty set;
reconsider f as Function of SS,SSX;
A27: SSX c= rng f
proof
let x be object such that
A28: x in SSX;
consider k,m be Nat such that
A29: k in Seg n1 and
A30: m in Seg n1 and
A31: k < m and
A32: x={k,m} by A28,MATRIX11:1;
A33: k<>i & m<>i
proof
assume k=i or m=i;
then x in X by A28,A32;
hence thesis by A28,XBOOLE_0:def 5;
end;
A34: 1<=m by A30,FINSEQ_1:1;
1<=k by A29,FINSEQ_1:1;
then reconsider k1=k-1,m1=m-1 as Element of NAT by A34,NAT_1:21;
reconsider m9=m,k9=k as Element of NAT by ORDINAL1:def 12;
per cases by A33,XXREAL_0:1;
suppose
A35: k<i & m<i;
A36: i<=n+1 by A1,FINSEQ_1:1;
then k<n+1 by A35,XXREAL_0:2;
then
A37: k<=n by NAT_1:13;
m <n+1 by A35,A36,XXREAL_0:2;
then
A38: m<=n by NAT_1:13;
1<=m by A30,FINSEQ_1:1;
then
A39: m in Seg n by A38;
A40: dom f=SS by FUNCT_2:def 1;
1<=k by A29,FINSEQ_1:1;
then k in Seg n by A37;
then
A41: {k9,m9} in SS by A31,A39,MATRIX11:1;
then x=f.x by A26,A31,A32,A35;
hence thesis by A32,A41,A40,FUNCT_1:def 3;
end;
suppose
k>i & m<i;
hence thesis by A31,XXREAL_0:2;
end;
suppose
A42: k<i & m>i;
1<=i by A1,FINSEQ_1:1;
then
A43: 1< m1+1 by A42,XXREAL_0:2;
then
A44: i<=m1 by A42,NAT_1:13;
then
A45: k<m1 by A42,XXREAL_0:2;
i<=n+1 by A1,FINSEQ_1:1;
then k<n+1 by A42,XXREAL_0:2;
then
A46: k<=n by NAT_1:13;
A47: dom f=SS by FUNCT_2:def 1;
(m1+1) <= n+1 by A30,FINSEQ_1:1;
then m1 < n+1 by NAT_1:13;
then
A48: m1<=n by NAT_1:13;
1<=m1 by A43,NAT_1:13;
then
A49: m1 in Seg n by A48;
1<=k by A29,FINSEQ_1:1;
then k in Seg n by A46;
then
A50: {k9,m1} in SS by A49,A45,MATRIX11:1;
then f.{k9,m1}={k9,m1+1} by A26,A42,A44,A45;
hence thesis by A32,A50,A47,FUNCT_1:def 3;
end;
suppose
A51: k>i & m>i;
(k1+1) <= n+1 by A29,FINSEQ_1:1;
then k1<n+1 by NAT_1:13;
then
A52: k1<=n by NAT_1:13;
A53: dom f=SS by FUNCT_2:def 1;
(m1+1) <= n+1 by A30,FINSEQ_1:1;
then m1<n+1 by NAT_1:13;
then
A54: m1<=n by NAT_1:13;
A55: k1<m1 by A31,XREAL_1:9;
A56: 1<=i by A1,FINSEQ_1:1;
then
A57: 1<m1+1 by A51,XXREAL_0:2;
A58: 1<k1+1 by A51,A56,XXREAL_0:2;
then
A59: i<=k1 by A51,NAT_1:13;
1<=k1 by A58,NAT_1:13;
then
A60: k1 in Seg n by A52;
1<=m1 by A57,NAT_1:13;
then m1 in Seg n by A54;
then
A61: {k1,m1} in SS by A60,A55,MATRIX11:1;
i<=m1 by A51,A57,NAT_1:13;
then f.{k1,m1}={k1+1,m1+1} by A26,A59,A55,A61;
hence thesis by A32,A61,A53,FUNCT_1:def 3;
end;
end;
A62: rng f c= SSX by RELAT_1:def 19;
then
A63: SSX = rng f by A27,XBOOLE_0:def 10;
dom f=SS by FUNCT_2:def 1;
then reconsider f as Function of SS,SS1 by A63,FUNCT_2:2;
take f;
for x1,x2 be object st x1 in SS & x2 in SS & f.x1 = f.x2 holds x1 = x2
proof
let x1,x2 be object such that
A64: x1 in SS and
A65: x2 in SS and
A66: f.x1 = f.x2;
consider k2,m2 be Nat such that
k2 in Seg n and
m2 in Seg n and
A67: k2 < m2 and
A68: x2={k2,m2} by A65,MATRIX11:1;
consider k1,m1 be Nat such that
k1 in Seg n and
m1 in Seg n and
A69: k1 < m1 and
A70: x1={k1,m1} by A64,MATRIX11:1;
reconsider m1,m2,k1,k2 as Element of NAT by ORDINAL1:def 12;
per cases;
suppose
A71: k1<i & m1<i & k2<i & m2<i;
then f.x1=x1 by A26,A64,A69,A70;
hence thesis by A26,A65,A66,A67,A68,A71;
end;
suppose
A72: k1<i & m1<i & (k2<i or k2>=i) & m2>=i;
then
A73: f.x2={k2,m2+1} or f.x2={k2+1,m2+1} by A26,A65,A67,A68;
f.x1={k1,m1} by A26,A64,A69,A70,A72;
then (k1=k2 or k1=m2+1) & (m1=k2 or m1=m2+1) or (k1=k2+1 or k1=m2+1)&(
m1=k2+1 or m1=m2+1) by A66,A73,ZFMISC_1:6;
hence thesis by A69,A72,NAT_1:13;
end;
suppose
A74: k1<i & m1>=i & k2<i & m2>=i;
then
A75: f.x2={k2,m2+1} by A26,A65,A67,A68;
A76: f.x1={k1,m1+1} by A26,A64,A69,A70,A74;
then
A77: m1+1=k2 or m1+1=m2+1 by A66,A75,ZFMISC_1:6;
k1=k2 or k1=m2+1 by A66,A76,A75,ZFMISC_1:6;
hence thesis by A70,A68,A74,A77,NAT_1:13;
end;
suppose
A78: k1<i & m1>=i & ( k2>=i & m2>=i or k2<i & m2<i );
then
A79: f.x2 = {k2+1,m2+1} or f.x2 = {k2,m2} by A26,A65,A67,A68;
f.x1={k1,m1+1} by A26,A64,A69,A70,A78;
then (k1=k2+1 or k1=m2+1)&(m1+1=k2+1 or m1+1=m2+1) or (k1=k2 or k1=m2)
& (m1+1=k2 or m1+1=m2) by A66,A79,ZFMISC_1:6;
hence thesis by A78,NAT_1:13;
end;
suppose
k1>=i & m1<i or k2>=i & m2<i;
hence thesis by A69,A67,XXREAL_0:2;
end;
suppose
A80: k1>=i & m1>=i & k2>=i & m2>=i;
then
A81: f.x2={k2+1,m2+1} by A26,A65,A67,A68;
A82: f.x1={k1+1,m1+1} by A26,A64,A69,A70,A80;
then
A83: m1+1=k2+1 or m1+1=m2+1 by A66,A81,ZFMISC_1:6;
k1+1=k2+1 or k1+1=m2+1 by A66,A82,A81,ZFMISC_1:6;
hence thesis by A69,A70,A68,A83;
end;
suppose
A84: k1>=i & m1>=i & ( k2<i & m2<i or k2<i & m2>=i );
then
A85: f.x2={k2,m2} or f.x2={k2,m2+1} by A26,A65,A67,A68;
f.x1={k1+1,m1+1} by A26,A64,A69,A70,A84;
then (k1+1=k2 or k1+1=m2) & (m1+1=k2 or m1+1=m2) or (k1+1=k2 or k1+1=m2
+1)&(m1+1=k2 or m1+1=m2+1) by A66,A85,ZFMISC_1:6;
hence thesis by A69,A84,NAT_1:13;
end;
end;
hence thesis by A26,A27,A62,FUNCT_2:19,XBOOLE_0:def 10;
end;
theorem Th11:
n < 2 implies for p be Element of Permutations n holds p is even & p=idseq n
proof
assume
A1: n<2;
let p be Element of Permutations n;
reconsider P=p as Permutation of Seg n by MATRIX_1:def 16;
now
per cases by A1,NAT_1:23;
suppose
A2: n=0;
then
A3: Seg n={};
A4: len Permutations(n)=n by MATRIX_1:9;
P={} by A2;
hence thesis by A4,A3,MATRIX_1:16,RELAT_1:55;
end;
suppose
A5: n=1;
A6: len Permutations(n)=n by MATRIX_1:9;
P=id Seg n by A5,MATRIX_1:10,TARSKI:def 1;
hence thesis by A6,MATRIX_1:16;
end;
end;
hence thesis;
end;
theorem Th12:
for X,Y,D be non empty set for f be Function of X,Fin Y, g be
Function of Fin Y,D, F be BinOp of D st (for A,B be Element of Fin Y st A
misses B holds F.(g.A,g.B) = g.(A \/ B)) & F is commutative associative & F is
having_a_unity & g.{} = the_unity_wrt F for I be Element of Fin X st for x,y st
x in I & y in I & f.x meets f.y holds x = y holds F $$ (I,g*f) = F $$ (f.:I,g)
& F $$ (f.:I,g) = g.union (f.:I) & union (f.:I) is Element of Fin Y
proof
let X,Y,D be non empty set;
let f be Function of X,Fin Y, g be Function of Fin Y,D, F be BinOp of D such
that
A1: for A,B be Element of Fin Y st A misses B holds F.(g.A,g.B)=g.(A \/ B) and
A2: F is commutative associative and
A3: F is having_a_unity and
A4: g.{}=the_unity_wrt F;
defpred P[set] means for I be Element of Fin X st I=$1 & for x,y st x in I &
y in I & f.x meets f.y holds x=y holds F $$ (I,g*f)=F $$ (f.:I,g) & F $$ (f.:I,
g)= g.union (f.:I) & union (f.:I) is Element of Fin Y;
A5: for I be (Element of Fin X), i be Element of X holds P[I] & not i in I
implies P[I \/ {i}]
proof
let A be (Element of Fin X), a be Element of X such that
A6: P[A] and
A7: not a in A;
let I be Element of Fin X such that
A8: A\/{a}=I and
A9: for x,y st x in I & y in I & f.x meets f.y holds x=y;
A10: for x,y st x in A & y in A & f.x meets f.y holds x=y
proof
let x,y such that
A11: x in A and
A12: y in A and
A13: f.x meets f.y;
A c= I by A8,XBOOLE_1:7;
hence thesis by A9,A11,A12,A13;
end;
then
A14: F $$ (A,g*f)=F $$ (f.:A,g) by A6;
A15: union (f.:A) is Element of Fin Y by A6,A10;
dom f=X by FUNCT_2:def 1;
then Im(f,a)={f.a} by FUNCT_1:59;
then
A16: f.:I=f.:A\/{f.a} by A8,RELAT_1:120;
A17: F $$ (f.:A,g)=g.union(f.:A) by A6,A10;
dom (g*f)=X by FUNCT_2:def 1;
then
A18: g.(f.a)=(g*f).a by FUNCT_1:12;
per cases;
suppose
A19: f.a is non empty or not f.a in f.:A;
not f.a in f.:A
proof
A20: A c= I by A8,XBOOLE_1:7;
A21: {a} c= I by A8,XBOOLE_1:7;
A22: a in {a} by TARSKI:def 1;
assume
A23: f.a in f.:A;
then consider x being object such that
x in dom f and
A24: x in A and
A25: f.x=f.a by FUNCT_1:def 6;
f.x meets f.a by A19,A23,A25,XBOOLE_1:66;
hence thesis by A7,A9,A24,A22,A21,A20;
end;
then
A26: F $$ (f.:I,g)=F.(F$$(f.:A,g),(g*f).a) by A2,A3,A16,A18,SETWOP_2:2;
A27: f.a c= Y by FINSUB_1:def 5;
union (f.:A) c= Y by A15,FINSUB_1:def 5;
then
A28: (union (f.:A))\/f.a c= Y by A27,XBOOLE_1:8;
now
let x be set;
assume x in f.:A;
then
A29: ex y being object st y in dom f & y in A & f.y=x by FUNCT_1:def 6;
A30: a in {a} by TARSKI:def 1;
A31: A c= I by A8,XBOOLE_1:7;
A32: {a} c= I by A8,XBOOLE_1:7;
assume x meets f.a;
hence contradiction by A7,A9,A29,A30,A32,A31;
end;
then
A33: union(f.:A) misses f.a by ZFMISC_1:80;
union (f.:I) = union (f.:A)\/union {f.a} by A16,ZFMISC_1:78
.= union (f.:A)\/f.a by ZFMISC_1:25;
hence thesis by A1,A2,A3,A7,A8,A14,A17,A15,A18,A26,A28,A33,FINSUB_1:def 5
,SETWOP_2:2;
end;
suppose
A34: f.a is empty & f.a in f.:A;
then
A35: f.:A\/{f.a}=f.:A by ZFMISC_1:40;
F $$ (I,g*f) = F.(F $$ (f.:A,g),the_unity_wrt F) by A2,A3,A4,A7,A8,A14
,A18,A34,SETWOP_2:2
.= F $$ (f.:I,g) by A3,A16,A35,SETWISEO:15;
hence thesis by A6,A10,A16,A35;
end;
end;
A36: P[{}.X]
proof
A37: {}c= Y;
let I be Element of Fin X such that
A38: {}.X=I and
for x,y st x in I & y in I & f.x meets f.y holds x=y;
A39: f.:I={}.(Fin Y) by A38;
F $$ (I,g*f)=g.{} by A2,A3,A4,A38,SETWISEO:31;
hence thesis by A2,A3,A4,A39,A37,FINSUB_1:def 5,SETWISEO:31,ZFMISC_1:2;
end;
for I be Element of Fin X holds P[I] from SETWISEO:sch 2(A36,A5);
hence thesis;
end;
begin :: Auxiliary notions
definition
let i,j,n be Nat;
let K;
let M be Matrix of n,K;
assume that
A1: i in Seg n and
A2: j in Seg n;
func Delete(M,i,j) -> Matrix of n-'1,K equals
:Def1:
Deleting(M,i,j);
coherence
proof
set D=Deleting(M,i,j);
A3: width M=n by MATRIX_0:24;
len M=n by MATRIX_0:24;
then dom M=Seg n by FINSEQ_1:def 3;
then
A4: len D=n-'1 by A1,Th2;
per cases;
suppose
n-'1=0;
then dom D = Seg 0 by A4,FINSEQ_1:def 3;
then for f st f in rng D holds len f = n-'1 by RELAT_1:42;
hence thesis by A4,MATRIX_0:def 2;
end;
suppose
A5: n-'1>0;
width Deleting(M,i,j)= n-' 1 by A2,A3,Th5;
hence thesis by A4,A5,MATRIX_0:20;
end;
end;
end;
theorem Th13:
for i,j st i in Seg n & j in Seg n for k,m st k in Seg (n-'1) &
m in Seg (n-'1) holds (k < i & m < j implies Delete(M,i,j)*(k,m) = M*(k,m) )& (
k < i & m >= j implies Delete(M,i,j)*(k,m) = M*(k,m+1) )& (k >= i & m < j
implies Delete(M,i,j)*(k,m) = M*(k+1,m) )& (k >= i & m >= j implies Delete(M,i,
j)*(k,m) = M*(k+1,m+1))
proof
let i,j such that
A1: i in Seg n and
A2: j in Seg n;
set DM=Delete(M,i,j);
A3: Deleting(M,i,j)=DM by A1,A2,Def1;
n>0 by A1;
then reconsider n9=n-1 as Element of NAT by NAT_1:20;
set DL=DelLine(M,i);
let k,m such that
A4: k in Seg (n-'1) and
A5: m in Seg (n-'1);
A6: n-'1=n9 by XREAL_0:def 2;
then
A7: k+1 in Seg (n9+1) by A4,FINSEQ_1:60;
reconsider I=i, J=j, K=k, U = m as Element of NAT by ORDINAL1:def 12;
n9<=n9+1 by NAT_1:11;
then
A8: Seg n9 c= Seg n by FINSEQ_1:5;
A9: len M=n by MATRIX_0:24;
then
A10: dom M=Seg n by FINSEQ_1:def 3;
then len DL=n9 by A1,A6,A9,Th1;
then
A11: dom DL=Seg n9 by FINSEQ_1:def 3;
then
A12: Deleting(M,i,j).k=Del(Line(DL,k),j) by A4,A6,MATRIX_0:def 13;
len DM=n9 by A6,MATRIX_0:24;
then dom DM=Seg n9 by FINSEQ_1:def 3;
then
A13: DM.k=Line(DM,k) by A4,A6,MATRIX_0:60;
width DM=n9 by A6,MATRIX_0:24;
then
A14: Line(DM,k).m=DM*(k,m) by A5,A6,MATRIX_0:def 7;
A15: Line(DL,k)=DL.k by A4,A6,A11,MATRIX_0:60;
A16: m+1 in Seg (n9+1) by A5,A6,FINSEQ_1:60;
A17: K>=I implies (U<J implies DM*(K,U)=M*(K+1,U))&(U>=J implies DM*(K,U)=M*
(K+1,U+1))
proof
assume
A18: K >=I;
K<=n9 by A4,A6,FINSEQ_1:1;
then
A19: DL.K=M.(K+1) by A1,A9,A10,A7,A18,FINSEQ_3:111;
A20: M.(K+1)=Line(M,K+1) by A10,A7,MATRIX_0:60;
thus U<J implies DM*(K,U)=M*(K+1,U)
proof
A21: width M=n by MATRIX_0:24;
assume U<J;
then DM*(K,U)=Line(M,K+1).U by A12,A3,A13,A14,A15,A19,A20,FINSEQ_3:110;
hence thesis by A5,A6,A8,A21,MATRIX_0:def 7;
end;
assume
A22: U>=J;
A23: U<=n9 by A5,A6,FINSEQ_1:1;
A24: width M=n by MATRIX_0:24;
A25: len Line(DL,K)=width M by A15,A19,A20,MATRIX_0:def 7;
then J in dom Line(DL,K) by A2,A24,FINSEQ_1:def 3;
then
DM*(K,U)=Line(M,K+1).(U+1) by A12,A3,A13,A14,A15,A7,A19,A20,A22,A25,A23,
FINSEQ_3:111,MATRIX_0:24;
hence thesis by A16,A24,MATRIX_0:def 7;
end;
K<I implies (U<J implies DM*(K,U)=M*(K,U))&(U>=J implies DM*(K,U)=M*(K, U+1))
proof
assume K < I;
then
A26: DL.K=M.K by FINSEQ_3:110;
A27: M.K=Line(M,K) by A4,A6,A10,A8,MATRIX_0:60;
thus U<J implies DM*(K,U) = M*(K,U)
proof
assume
A28: U<J;
A29: width M=n9+1 by MATRIX_0:24;
DM*(K,U)=Line(M,K).U by A12,A3,A13,A14,A15,A26,A27,A28,FINSEQ_3:110;
hence thesis by A5,A6,A8,A29,MATRIX_0:def 7;
end;
assume
A30: U>=J;
A31: U<=n9 by A5,A6,FINSEQ_1:1;
A32: width M=n by MATRIX_0:24;
A33: len Line(DL,K)=width M by A15,A26,A27,MATRIX_0:def 7;
then J in dom Line(DL,K) by A2,A32,FINSEQ_1:def 3;
then DM*(K,U)=Line(M,K).(U+1) by A12,A3,A13,A14,A15,A7,A26,A27,A30,A33,A31,
FINSEQ_3:111,MATRIX_0:24;
hence thesis by A16,A32,MATRIX_0:def 7;
end;
hence thesis by A17;
end;
theorem Th14:
for i,j st i in Seg n & j in Seg n holds Delete(M,i,j)@ = Delete (M@,j,i)
proof
let i,j such that
A1: i in Seg n and
A2: j in Seg n;
n>0 by A1;
then reconsider n1=n-1 as Element of NAT by NAT_1:20;
set X1=Seg n;
reconsider MT=M@ as Matrix of n,K;
set D=Delete(M,i,j);
set n9=n-'1;
reconsider I=i as Element of NAT by ORDINAL1:def 12;
reconsider DT=D@ as Matrix of n9,K;
set D9=Delete(MT,j,i);
set X=Seg n9;
A3: n1+1-'1=n1 by NAT_D:34;
now
n9<=n by NAT_D:35;
then
A4: X c= X1 by FINSEQ_1:5;
let k,m be Nat such that
A5: [k,m] in Indices DT;
[m,k] in Indices D by A5,MATRIX_0:def 6;
then
A6: DT*(k,m)=D*(m,k) by MATRIX_0:def 6;
reconsider k9=k,m9=m as Element of NAT by ORDINAL1:def 12;
A7: Indices DT=[:X,X:] by MATRIX_0:24;
then
A8: k in X by A5,ZFMISC_1:87;
then
A9: k+1 in X1 by A3,FINSEQ_1:60;
A10: Indices M=[:X1,X1:] by MATRIX_0:24;
A11: m in X by A5,A7,ZFMISC_1:87;
then
A12: m+1 in X1 by A3,FINSEQ_1:60;
per cases;
suppose
A13: m9<I & k9<j;
then
A14: D9*(k,m)=MT*(k,m) by A1,A2,A8,A11,Th13;
A15: [m,k] in Indices M by A8,A11,A4,A10,ZFMISC_1:87;
D*(m,k)=M*(m,k) by A1,A2,A8,A11,A13,Th13;
hence DT*(k,m)=D9*(k,m) by A6,A15,A14,MATRIX_0:def 6;
end;
suppose
A16: m9<I & k9>=j;
then
A17: D9*(k,m)=MT*(k+1,m) by A1,A2,A8,A11,Th13;
A18: [m,k+1] in Indices M by A11,A4,A9,A10,ZFMISC_1:87;
D*(m,k)=M*(m,k+1) by A1,A2,A8,A11,A16,Th13;
hence DT*(k,m)=D9*(k,m) by A6,A18,A17,MATRIX_0:def 6;
end;
suppose
A19: m9>=I & k9<j;
then
A20: D9*(k,m)=MT*(k,m+1) by A1,A2,A8,A11,Th13;
A21: [m+1,k] in Indices M by A8,A4,A12,A10,ZFMISC_1:87;
D*(m,k)=M*(m+1,k) by A1,A2,A8,A11,A19,Th13;
hence DT*(k,m)=D9*(k,m) by A6,A21,A20,MATRIX_0:def 6;
end;
suppose
A22: m9>=I & k9>=j;
then
A23: D9*(k,m)=MT*(k+1,m+1) by A1,A2,A8,A11,Th13;
A24: [m+1,k+1] in Indices M by A9,A12,A10,ZFMISC_1:87;
D*(m,k)=M*(m+1,k+1) by A1,A2,A8,A11,A22,Th13;
hence DT*(k,m)=D9*(k,m) by A6,A24,A23,MATRIX_0:def 6;
end;
end;
hence thesis by MATRIX_0:27;
end;
theorem Th15:
for f be FinSequence of K, i,j st i in Seg n & j in Seg n holds
Delete(M,i,j) = Delete(RLine(M,i,f),i,j)
proof
let f be FinSequence of K, i,j such that
A1: i in Seg n and
A2: j in Seg n;
A3: Delete(M,i,j) = Deleting(M,i,j) by A1,A2,Def1;
A4: Delete(RLine(M,i,f),i,j) = Deleting(RLine(M,i,f),i,j) by A1,A2,Def1;
reconsider f9=f as Element of (the carrier of K)* by FINSEQ_1:def 11;
reconsider I=i as Element of NAT by ORDINAL1:def 12;
per cases;
suppose
len f=width M;
then RLine(M,I,f)=Replace(M,i,f9) by MATRIX11:29;
hence thesis by A3,A4,COMPUT_1:3;
end;
suppose
len f<>width M;
hence thesis by MATRIX11:def 3;
end;
end;
definition
let c, n, m, D;
let M be Matrix of n,m,D;
let pD be FinSequence of D;
func ReplaceCol(M,c,pD) -> Matrix of n,m,D means
:Def2:
len it = len M &
width it = width M & for i,j st [i,j] in Indices M holds (j <> c implies it*(i,
j) = M*(i,j)) & (j = c implies it*(i,c) = pD.i) if len pD = len M otherwise it
= M;
consistency;
existence
proof
thus len pD=len M implies ex M1 be Matrix of n,m,D st len M1 = len M &
width M1 = width M & for i,j st [i,j] in Indices M holds (j <> c implies M1*(i,
j) = M*(i,j)) & (j = c implies M1*(i,c) = pD.i)
proof
reconsider M9=M as Matrix of len M,width M,D by MATRIX_0:51;
reconsider V = n, U = m as Element of NAT by ORDINAL1:def 12;
defpred P[set,set,set] means for i,j st i=$1 & j=$2 holds (j <>c implies
$3 = M*(i,j)) & (j = c implies $3 = pD.i);
assume
A1: len pD=len M;
A2: for i,j be Nat st [i,j] in [:Seg V, Seg U:] ex x being Element of D
st P[i,j,x]
proof
let i,j be Nat such that
A3: [i,j] in [:Seg V, Seg U:];
now
per cases;
case
A4: j=c;
A5: rng pD c= D by FINSEQ_1:def 4;
len M=n by MATRIX_0:def 2;
then i in Seg len pD by A1,A3,ZFMISC_1:87;
then i in dom pD by FINSEQ_1:def 3;
then
A6: pD.i in rng pD by FUNCT_1:def 3;
P[i,j,pD.i] by A4;
hence thesis by A6,A5;
end;
case
j<>c;
then P[i,j,M*(i,j)];
hence thesis;
end;
end;
hence thesis;
end;
consider M1 be Matrix of V,U,D such that
A7: for i,j be Nat st [i,j] in Indices M1 holds P[i,j,M1*(i,j)]
from MATRIX_0:sch 2(A2);
reconsider M1 as Matrix of n,m,D;
take M1;
A8: now
per cases;
suppose
A9: n=0;
then len M1=0 by MATRIX_0:def 2;
then
A10: width M1=0 by MATRIX_0:def 3;
len M=0 by A9,MATRIX_0:def 2;
hence len M = len M1 & width M1=width M by A9,A10,MATRIX_0:def 2
,def 3;
end;
suppose
A11: n > 0;
then
A12: width M=m by MATRIX_0:23;
len M=n by A11,MATRIX_0:23;
hence len M = len M1 & width M = width M1 by A11,A12,MATRIX_0:23;
end;
end;
Indices M9=Indices M1 by MATRIX_0:26;
hence thesis by A7,A8;
end;
thus thesis;
end;
uniqueness
proof
let M1,M2 be Matrix of n,m,D;
thus len pD=len M & (len M1 = len M & width M1 = width M & for i,j st [i,j
] in Indices M holds (j <> c implies M1*(i,j) = M*(i,j)) & (j = c implies M1*(i
,c) = pD.i))& (len M2 = len M & width M2 = width M & for i,j st [i,j] in
Indices M holds (j <> c implies M2*(i,j) = M*(i,j)) & (j = c implies M2*(i,c) =
pD.i)) implies M1=M2
proof
assume len pD=len M;
assume that
A13: len M1=len M and
A14: width M1=width M and
A15: for i,j st [i,j] in Indices M holds (j <> c implies M1*(i,j) =
M*(i, j))&(j = c implies M1*(i,c) = pD.i);
assume that
len M2=len M and
width M2=width M and
A16: for i,j st [i,j] in Indices M holds (j <> c implies M2*(i,j) =
M*(i, j))&(j = c implies M2*(i,c) = pD.i);
for i,j be Nat st [i,j] in Indices M1 holds M1*(i,j)=M2*(i,j)
proof
let i,j be Nat;
assume [i,j] in Indices M1;
then
A17: [i,j] in Indices M by A13,A14,MATRIX_4:55;
reconsider I=i,J=j as Element of NAT by ORDINAL1:def 12;
A18: J=c implies M1*(I,c)=pD.I by A15,A17;
A19: J<>c implies M2*(I,J)=M*(I,J) by A16,A17;
J<>c implies M1*(I,J)=M*(I,J) by A15,A17;
hence thesis by A16,A17,A18,A19;
end;
hence thesis by MATRIX_0:27;
end;
thus thesis;
end;
end;
notation
let c, n, m, D;
let M be Matrix of n,m,D;
let pD be FinSequence of D;
synonym RCol(M,c,pD) for ReplaceCol(M,c,pD);
end;
theorem
for i st i in Seg width AD holds (i = c & len pD = len AD implies Col(
RCol(AD,c,pD),i) = pD) & (i <> c implies Col(RCol(AD,c,pD),i) = Col(AD,i))
proof
let i such that
A1: i in Seg width AD;
set R=RCol(AD,c,pD);
set CR=Col(R,i);
thus i = c & len pD = len AD implies CR = pD
proof
assume that
A2: i = c and
A3: len pD = len AD;
A4: len R = len pD by A3,Def2;
A5: now
let J be Nat such that
A6: 1<=J and
A7: J<=len pD;
J in Seg len pD by A6,A7;
then
A8: J in dom R by A4,FINSEQ_1:def 3;
i in Seg width R by A1,A3,Def2;
then
A9: [J,c] in Indices R by A2,A8,ZFMISC_1:87;
A10: Indices R=Indices AD by MATRIX_0:26;
CR.J=R*(J,c) by A2,A8,MATRIX_0:def 8;
hence CR.J=pD.J by A3,A9,A10,Def2;
end;
len CR=len pD by A4,MATRIX_0:def 8;
hence thesis by A5;
end;
set CA=Col(AD,i);
A11: len AD=n by MATRIX_0:def 2;
A12: len R=n by MATRIX_0:def 2;
A13: len AD=len CA by MATRIX_0:def 8;
assume
A14: i <> c;
A15: now
let j be Nat such that
A16: 1 <=j and
A17: j <= len CA;
A18: j in Seg len AD by A13,A16,A17;
then
A19: j in dom AD by FINSEQ_1:def 3;
then
A20: CA.j=AD*(j,i) by MATRIX_0:def 8;
j in dom R by A11,A12,A18,FINSEQ_1:def 3;
then
A21: CR.j=R*(j,i) by MATRIX_0:def 8;
A22: [j,i] in Indices AD by A1,A19,ZFMISC_1:87;
per cases;
suppose
len pD=len AD;
hence CA.j=CR.j by A14,A20,A21,A22,Def2;
end;
suppose
len pD<>len AD;
hence CA.j=CR.j by Def2;
end;
end;
len CR=len R by MATRIX_0:def 8;
hence thesis by A11,A12,A13,A15;
end;
theorem
not c in Seg width AD implies RCol(AD,c,pD) = AD
proof
assume
A1: not c in Seg width AD;
set R=RCol(AD,c,pD);
per cases;
suppose
A2: len pD=len AD;
now
let i,j be Nat such that
A3: [i,j] in Indices AD;
j in Seg width AD by A3,ZFMISC_1:87;
hence R*(i,j) = AD*(i,j) by A1,A2,A3,Def2;
end;
hence thesis by MATRIX_0:27;
end;
suppose
len pD<>len AD;
hence thesis by Def2;
end;
end;
theorem
RCol(AD,c,Col(AD,c)) = AD
proof
set C=Col(AD,c);
set R=RCol(AD,c,C);
now
reconsider c as Element of NAT by ORDINAL1:def 12;
let i,j be Nat such that
A1: [i,j] in Indices AD;
A2: len C=len AD by MATRIX_0:def 8;
reconsider I=i,J=j as Element of NAT by ORDINAL1:def 12;
A3: i in dom AD by A1,ZFMISC_1:87;
now
per cases;
suppose
A4: c = j;
hence R*(i,j) = C.I by A1,A2,Def2
.= AD*(i,j) by A3,A4,MATRIX_0:def 8;
end;
suppose
c <> J;
hence R*(i,j)=AD*(i,j) by A1,A2,Def2;
end;
end;
hence R*(i,j)=AD*(i,j);
end;
hence thesis by MATRIX_0:27;
end;
theorem Th19:
for A be Matrix of n,m,D, A9 be Matrix of m,n,D st A9 = A@ & (m=
0 implies n=0) holds ReplaceCol(A,c,pD) = ReplaceLine(A9,c,pD)@
proof
let A be Matrix of n,m,D,A9 be Matrix of m,n,D such that
A1: A9=A@ and
A2: m=0 implies n=0;
set RC=ReplaceCol(A,c,pD);
set RL=ReplaceLine(A9,c,pD);
now
per cases;
suppose
A3: n=0;
then 0=len A by MATRIX_0:def 2;
then 0=width A by MATRIX_0:def 3
.=len A9 by A1,MATRIX_0:def 6;
then m=0 by MATRIX_0:def 2;
then len RL=0 by MATRIX_0:def 2;
then width RL=0 by MATRIX_0:def 3;
then len (RL@)=0 by MATRIX_0:def 6;
then
A4: RL@={};
len RC=0 by A3,MATRIX_0:def 2;
hence thesis by A4;
end;
suppose
A5: len pD <> len A & n>0;
then
A6: width A=m by MATRIX_0:23;
then
A7: width A9=len A by A1,A2,A5,MATRIX_0:54;
A8: len A=n by A5,MATRIX_0:23;
thus RC = A by A5,Def2
.= (A@)@ by A2,A5,A8,A6,MATRIX_0:57
.= RL@ by A1,A5,A7,MATRIX11:def 3;
end;
suppose
A9: len pD = len A & n>0;
then
A10: width RL=n by A2,MATRIX_0:23;
then
A11: len (RL@)=n by A9,MATRIX_0:54;
len RL=m by A2,A9,MATRIX_0:23;
then width (RL@)=m by A9,A10,MATRIX_0:54;
then reconsider RL9=RL@ as Matrix of n,m,D by A11,MATRIX_0:51;
A12: len A=n by A9,MATRIX_0:23;
A13: width A9=n by A2,A9,MATRIX_0:23;
now
A14: Indices RC=Indices A by MATRIX_0:26;
A15: Indices RL=Indices A9 by MATRIX_0:26;
let i,j be Nat such that
A16: [i,j] in Indices RC;
reconsider I=i,J=j as Element of NAT by ORDINAL1:def 12;
Indices RC=Indices RL9 by MATRIX_0:26;
then
A17: [j,i] in Indices RL by A16,MATRIX_0:def 6;
per cases;
suppose
A18: J=c;
hence RC*(i,j) = pD.I by A9,A16,A14,Def2
.= RL*(J,I) by A9,A12,A13,A17,A15,A18,MATRIX11:def 3
.= RL9*(i,j) by A17,MATRIX_0:def 6;
end;
suppose
A19: J<>c;
hence RC*(i,j) = A*(I,J) by A9,A16,A14,Def2
.= A9*(j,i) by A1,A16,A14,MATRIX_0:def 6
.= RL*(J,I) by A9,A12,A13,A17,A15,A19,MATRIX11:def 3
.= RL9*(i,j) by A17,MATRIX_0:def 6;
end;
end;
hence thesis by MATRIX_0:27;
end;
end;
hence thesis;
end;
begin :: Permutations
definition
let i,n;
let perm be Element of Permutations(n+1);
assume
A1: i in Seg (n+1);
func Rem(perm,i) -> Element of Permutations n means
:Def3:
for k st k in Seg
n holds (k<i implies (perm.k < perm.i implies it.k = perm.k )& (perm.k >= perm.
i implies it.k = perm.k-1) )& (k>=i implies (perm.(k+1) < perm.i implies it.k =
perm.(k+1) )& (perm.(k+1) >= perm.i implies it.k = perm.(k+1)-1));
existence
proof
set j=perm.i;
set P = Permutations n;
set p=perm;
set n1 = n+1;
reconsider N=n as Element of NAT by ORDINAL1:def 12;
reconsider p9=p as Permutation of Seg n1 by MATRIX_1:def 16;
A2: dom p9=Seg n1 by FUNCT_2:52;
defpred Q[object,object] means
for k st k in Seg n & $1=k holds (k<i implies (p.
k<j implies $2=p.k)&(p.k>=j implies $2=p.k-1))& (k>=i implies (p.(k+1)<j
implies $2=p.(k+1))&(p.(k+1)>=j implies $2=p.(k+1)-1));
A3: rng p9=Seg n1 by FUNCT_2:def 3;
then
A4: j in Seg n1 by A1,A2,FUNCT_1:def 3;
A5: for k9 be object st k9 in Seg n ex y being object st y in Seg n & Q[k9,y]
proof
let k9 be object;
assume k9 in Seg n;
then consider k being Nat such that
A6: k9=k and
A7: 1<=k and
A8: k <= n;
A9: k<n1 by A8,NAT_1:13;
then
A10: k in Seg n1 by A7;
then
A11: p.k in Seg n1 by A2,A3,FUNCT_1:def 3;
set k1=k+1;
A12: 1+0<=k+1 by NAT_1:13;
k+1<=n1 by A9,NAT_1:13;
then
A13: (k+1) in Seg n1 by A12;
then
A14: p.(k+1) in Seg n1 by A2,A3,FUNCT_1:def 3;
per cases;
suppose
A15: k < i & p.k<j;
j<=n1 by A4,FINSEQ_1:1;
then p.k < n1 by A15,XXREAL_0:2;
then
A16: p.k <=n by NAT_1:13;
A17: Q[k9,p.k] by A6,A15;
1<=p.k by A11,FINSEQ_1:1;
then p.k in Seg n by A16;
hence thesis by A17;
end;
suppose
A18: k<i & p.k>=j;
then p9.k<>p9.i by A1,A10,FUNCT_2:19;
then
A19: p.k > j by A18,XXREAL_0:1;
then reconsider pk1=p.k-1 as Element of NAT by NAT_1:20;
A20: Q[k9,pk1] by A6,A18;
A21: pk1<pk1+1 by NAT_1:13;
p.k <= n1 by A11,FINSEQ_1:1;
then pk1 <n1 by A21,XXREAL_0:2;
then
A22: pk1 <= n by NAT_1:13;
j>=1 by A4,FINSEQ_1:1;
then pk1+1 > 1 by A19,XXREAL_0:2;
then pk1 >= 1 by NAT_1:13;
then pk1 in Seg n by A22;
hence thesis by A20;
end;
suppose
A23: k>=i & p.k1<j;
j<=n1 by A4,FINSEQ_1:1;
then p.k1 < n1 by A23,XXREAL_0:2;
then
A24: p.k1 <=n by NAT_1:13;
A25: Q[k9,p.k1] by A6,A23;
1<=p.k1 by A14,FINSEQ_1:1;
then p.k1 in Seg n by A24;
hence thesis by A25;
end;
suppose
A26: k>=i & p.k1>=j;
then i<k1 by NAT_1:13;
then p9.k1<>p9.i by A1,A13,FUNCT_2:19;
then
A27: p.k1 > j by A26,XXREAL_0:1;
then reconsider pk1=p.k1-1 as Element of NAT by NAT_1:20;
A28: Q[k9,pk1] by A6,A26;
A29: pk1<pk1+1 by NAT_1:13;
p.k1 <= n1 by A14,FINSEQ_1:1;
then pk1 <n1 by A29,XXREAL_0:2;
then
A30: pk1 <= n by NAT_1:13;
j>=1 by A4,FINSEQ_1:1;
then pk1+1 > 1 by A27,XXREAL_0:2;
then pk1 >= 1 by NAT_1:13;
then pk1 in Seg n by A30;
hence thesis by A28;
end;
end;
consider q be Function of Seg n,Seg n such that
A31: for x being object st x in Seg n holds Q[x,q.x] from FUNCT_2:sch 1(A5);
for x1,x2 be object st x1 in dom q & x2 in dom q & q.x1 = q.x2
holds x1 = x2
proof
let x1,x2 be object such that
A32: x1 in dom q and
A33: x2 in dom q and
A34: q.x1 = q.x2;
A35: dom q=Seg n by FUNCT_2:52;
then consider k1 be Nat such that
A36: x1=k1 and
A37: 1<=k1 and
A38: k1 <=n by A32;
A39: 0+1<=k1+1 by NAT_1:13;
A40: k1 < n+1 by A38,NAT_1:13;
then
A41: k1 in Seg n1 by A37;
k1+1<=n+1 by A40,NAT_1:13;
then
A42: k1+1 in Seg n1 by A39;
consider k2 be Nat such that
A43: x2=k2 and
A44: 1<=k2 and
A45: k2 <=n by A33,A35;
A46: k2 < n+1 by A45,NAT_1:13;
then
A47: k2 in Seg n1 by A44;
A48: 0+1<=k2+1 by NAT_1:13;
k2+1<=n+1 by A46,NAT_1:13;
then
A49: k2+1 in Seg n1 by A48;
per cases;
suppose
A50: k1<i & p.k1<j;
then
A51: q.k1=p9.k1 by A31,A32,A36;
per cases;
suppose
k2<i & p.k2<j;
then p9.k2=p9.k1 by A31,A33,A34,A36,A43,A51;
hence thesis by A2,A36,A43,A41,A47,FUNCT_1:def 4;
end;
suppose
A52: k2<i & p.k2>=j;
then q.k2=p.k2-1 by A31,A33,A43;
then p.k1+1=p.k2 by A34,A36,A43,A51;
then p.k2 <= j by A50,NAT_1:13;
then p9.k2=p9.i by A52,XXREAL_0:1;
hence thesis by A1,A2,A47,A52,FUNCT_1:def 4;
end;
suppose
A53: k2>=i & p.(k2+1)<j;
then p9.k1=p9.(k2+1) by A31,A33,A34,A36,A43,A51;
then k1=k2+1 by A2,A41,A49,FUNCT_1:def 4;
hence thesis by A50,A53,NAT_1:13;
end;
suppose
A54: k2>=i & p.(k2+1)>=j;
then p.k1=p.(k2+1)-1 by A31,A33,A34,A36,A43,A51;
then p.k1+1=p.(k2+1);
then p.(k2+1)<=j by A50,NAT_1:13;
then p9.(k2+1) = p.i by A54,XXREAL_0:1;
then k2+1 = i by A1,A2,A49,FUNCT_1:def 4;
hence thesis by A54,NAT_1:13;
end;
end;
suppose
A55: k1<i & p.k1 >= j;
then
A56: q.k1=p.k1-1 by A31,A32,A36;
per cases;
suppose
A57: k2<i & p.k2<j;
then q.k2=p9.k2 by A31,A33,A43;
then p.k1 =p.k2+1 by A34,A36,A43,A56;
then p.k1 <= j by A57,NAT_1:13;
then p.k1=p.i by A55,XXREAL_0:1;
hence thesis by A1,A2,A41,A55,FUNCT_1:def 4;
end;
suppose
k2<i & p.k2>=j;
then p.k1-1=p.k2-1 by A31,A33,A34,A36,A43,A56;
hence thesis by A2,A36,A43,A41,A47,FUNCT_1:def 4;
end;
suppose
A58: k2>=i & p.(k2+1)<j;
then p.k1-1=p.(k2+1) by A31,A33,A34,A36,A43,A56;
then p.(k2+1)+1=p.k1;
then p.k1 <=j by A58,NAT_1:13;
then p9.k1=p9.i by A55,XXREAL_0:1;
hence thesis by A1,A2,A41,A55,FUNCT_1:def 4;
end;
suppose
A59: k2>=i & p.(k2+1)>=j;
then p.k1-1=p.(k2+1)-1 by A31,A33,A34,A36,A43,A56;
then k1=k2+1 by A2,A41,A49,FUNCT_1:def 4;
hence thesis by A55,A59,NAT_1:13;
end;
end;
suppose
A60: k1>=i & p.(k1+1)<j;
then
A61: q.k1=p.(k1+1) by A31,A32,A36;
per cases;
suppose
A62: k2<i & p.k2<j;
then p9.(k1+1)=p9.k2 by A31,A33,A34,A36,A43,A61;
then k1+1=k2 by A2,A47,A42,FUNCT_1:def 4;
hence thesis by A60,A62,NAT_1:13;
end;
suppose
A63: k2<i & p.k2>=j;
then p.(k1+1)=p.k2-1 by A31,A33,A34,A36,A43,A61;
then p.k2=p.(k1+1)+1;
then p.k2<=j by A60,NAT_1:13;
then p9.k2=p9.i by A63,XXREAL_0:1;
hence thesis by A1,A2,A47,A63,FUNCT_1:def 4;
end;
suppose
k2>=i & p.(k2+1)<j;
then q.k2=p.(k2+1) by A31,A33,A43;
then k1+1=k2+1 by A2,A34,A36,A43,A42,A49,A61,FUNCT_1:def 4;
hence thesis by A36,A43;
end;
suppose
A64: k2>=i & p.(k2+1)>=j;
then p.(k1+1)=p.(k2+1)-1 by A31,A33,A34,A36,A43,A61;
then p.(k2+1)=p.(k1+1)+1;
then p.(k2+1)<=j by A60,NAT_1:13;
then p9.(k2+1)=p9.i by A64,XXREAL_0:1;
then k2+1=i by A1,A2,A49,FUNCT_1:def 4;
hence thesis by A64,NAT_1:13;
end;
end;
suppose
A65: k1>=i & p.(k1+1)>=j;
then
A66: q.k1=p.(k1+1)-1 by A31,A32,A36;
per cases;
suppose
A67: k2<i & p.k2<j;
then p.(k1+1)-1=p.k2 by A31,A33,A34,A36,A43,A66;
then p.(k1+1)=p.k2+1;
then p.(k1+1)<=j by A67,NAT_1:13;
then p9.(k1+1)=p9.i by A65,XXREAL_0:1;
then k1+1=i by A1,A2,A42,FUNCT_1:def 4;
hence thesis by A65,NAT_1:13;
end;
suppose
A68: k2<i & p.k2>=j;
then p.(k1+1)-1=p.k2-1 by A31,A33,A34,A36,A43,A66;
then k1+1=k2 by A2,A47,A42,FUNCT_1:def 4;
hence thesis by A65,A68,NAT_1:13;
end;
suppose
A69: k2>=i & p.(k2+1)<j;
then p.(k1+1)-1=p.(k2+1) by A31,A33,A34,A36,A43,A66;
then p.(k1+1)=p.(k2+1)+1;
then p.(k1+1) <= j by A69,NAT_1:13;
then p9.(k1+1)=p9.i by A65,XXREAL_0:1;
then k1+1=i by A1,A2,A42,FUNCT_1:def 4;
hence thesis by A65,NAT_1:13;
end;
suppose
k2>=i & p.(k2+1)>=j;
then p.(k1+1)-1=p.(k2+1)-1 by A31,A33,A34,A36,A43,A66;
then k1+1=k2+1 by A2,A42,A49,FUNCT_1:def 4;
hence thesis by A36,A43;
end;
end;
end;
then
A70: q is one-to-one by FUNCT_1:def 4;
card finSeg N=card finSeg N;
then q is one-to-one onto by A70,FINSEQ_4:63;
then reconsider q as Element of P by MATRIX_1:def 16;
take q;
thus thesis by A31;
end;
uniqueness
proof
set p=perm;
let q1,q2 be Element of Permutations n such that
A71: for k st k in Seg n holds (k<i implies (p.k<p.i implies q1.k=p.k
)&(p.k>=p.i implies q1.k=p.k-1))& (k>=i implies (p.(k+1)<p.i implies q1.k=p.(k+
1))&(p.(k+1)>=p.i implies q1.k=p.(k+1)-1)) and
A72: for k st k in Seg n holds (k<i implies (p.k<p.i implies q2.k=p.k
)&(p.k>=p.i implies q2.k=p.k-1))& (k>=i implies (p.(k+1)<p.i implies q2.k=p.(k+
1))&(p.(k+1)>=p.i implies q2.k=p.(k+1)-1));
A73: q1 is Permutation of Seg n by MATRIX_1:def 16;
then
A74: dom q1=Seg n by FUNCT_2:52;
A75: now
let x be object such that
A76: x in dom q1;
consider k being Nat such that
A77: x=k and
1<=k and
k<=n by A74,A76;
set k1=k+1;
A78: p.k<p.i or p.k>=p.i;
A79: p.k1<p.i or p.k1>=p.i;
k<i or k>=i;
then p.k < p.i & q1.k = p.k & q2.k=p.k or p.k >= p.i & q1.k = p.k-1 &
q2.k=p.k-1 or p.k1 < p.i & q1.k = p.k1 & q2.k=p.k1 or p.k1 >= p.i & q1.k = p.k1
-1 & q2.k=p.k1-1 by A71,A72,A74,A76,A77,A78,A79;
hence q1.x=q2.x by A77;
end;
q2 is Permutation of Seg n by MATRIX_1:def 16;
then dom q2=Seg n by FUNCT_2:52;
hence thesis by A73,A75,FUNCT_1:2,FUNCT_2:52;
end;
end;
theorem Th20:
for i,j st i in Seg (n+1) & j in Seg(n+1) for P be set st P = { p1: p1
.i = j} ex Proj be Function of P,Permutations n st Proj is bijective & for
q1 st q1.i = j holds Proj.q1 = Rem(q1,i)
proof
let i,j such that
A1: i in Seg (n+1) and
A2: j in Seg(n+1);
set n1 = n+1;
reconsider N=n as Element of NAT by ORDINAL1:def 12;
set P1 = Permutations(N+1);
defpred F[object,object] means
for p be Element of P1 st $1=p & p.i=j holds $2=Rem(p,i);
let X be set such that
A3: X={p1:p1.i=j};
A4: for x being object st x in X
ex y being object st y in Permutations n & F[x,y]
proof
let x be object;
assume x in X;
then consider p be Element of P1 such that
A5: p=x and
p.i=j by A3;
take Rem(p,i);
thus thesis by A5;
end;
consider f be Function of X,Permutations n such that
A6: for x being object st x in X holds F[x,f.x] from FUNCT_2:sch 1(A4);
for x1,x2 be object st x1 in X & x2 in X & f.x1 = f.x2 holds x1 = x2
proof
let x1,x2 be object such that
A7: x1 in X and
A8: x2 in X and
A9: f.x1 = f.x2;
consider p1 be Element of P1 such that
A10: p1=x1 and
A11: p1.i=j by A3,A7;
set R1=Rem(p1,i);
A12: f.x1 =R1 by A6,A7,A10,A11;
consider p2 be Element of P1 such that
A13: p2=x2 and
A14: p2.i=j by A3,A8;
set R2=Rem(p2,i);
A15: f.x2 =R2 by A6,A8,A13,A14;
reconsider p19=p1,p29=p2 as Permutation of Seg n1 by MATRIX_1:def 16;
A16: dom p29=Seg n1 by FUNCT_2:52;
A17: dom p19=Seg n1 by FUNCT_2:52;
now
let x be object such that
A18: x in Seg n1;
consider k being Nat such that
A19: x=k and
A20: 1<=k and
A21: k<=n1 by A18;
per cases by XXREAL_0:1;
suppose
A22: k<i;
i<=n1 by A1,FINSEQ_1:1;
then k<n1 by A22,XXREAL_0:2;
then k<=n by NAT_1:13;
then
A23: k in Seg n by A20;
per cases;
suppose
p1.k<j & p2.k<j or p1.k>=j & p2.k>=j;
then R1.k=p1.k & R2.k=p2.k or R1.k=p1.k-1 & R2.k=p2.k-1 by A1,A11,A14
,A22,A23,Def3;
hence p1.x=p2.x by A9,A12,A15,A19;
end;
suppose
p1.k<j & p2.k>=j or p1.k>=j & p2.k<j;
then
R1.k=p1.k & R2.k=p2.k-1 & p1.k<j & p2.k>=j or R1.k=p1.k-1 & R2.
k=p2.k & p1.k>=j & p2.k<j by A1,A11,A14,A22,A23,Def3;
then
p1.k+1=p2.k & p1.k<j & p2.k>=j or p1.k=p2.k+1 & p1.k>=j & p2.k<
j by A9,A12,A15;
then p2.k<=j & p2.k>=j or p1.k>=j & p1.k<=j by NAT_1:13;
then p29.k=p29.i or p19.k=p19.i by A11,A14,XXREAL_0:1;
hence p1.x=p2.x by A1,A17,A16,A18,A19,A22,FUNCT_1:def 4;
end;
end;
suppose
k=i;
hence p1.x=p2.x by A11,A14,A19;
end;
suppose
A24: k>i;
then reconsider k1=k-1 as Element of NAT by NAT_1:20;
k1+1>i by A24;
then
A25: k1>=i by NAT_1:13;
k1+1 <= n1 by A21;
then k1 < n1 by NAT_1:13;
then
A26: k1<=n by NAT_1:13;
1<=i by A1,FINSEQ_1:1;
then 1<k1+1 by A24,XXREAL_0:2;
then 1<=k1 by NAT_1:13;
then
A27: k1 in Seg n by A26;
per cases;
suppose
p1.(k1+1)<j&p2.(k1+1)<j or p1.(k1+1)>=j&p2.(k1+1)>=j;
then R1.k1=p1.k & R2.k1=p2.k or R1.k1=p1.k-1 & R2.k1=p2.k-1 by A1,A11
,A14,A27,A25,Def3;
hence p1.x=p2.x by A9,A12,A15,A19;
end;
suppose
p1.(k1+1)<j&p2.(k1+1)>=j or p1.(k1+1)>=j&p2.(k1+1)<j;
then R1.k1=p1.k & R2.k1=p2.k-1 & p1.k<j & p2.k>=j or R1.k1=p1.k-1 &
R2.k1=p2.k & p1.k>=j & p2.k<j by A1,A11,A14,A27,A25,Def3;
then
p1.k+1=p2.k & p1.k<j & p2.k>=j or p1.k=p2.k+1 & p1.k>=j & p2.k<
j by A9,A12,A15;
then p2.k<=j & p2.k>=j or p1.k>=j & p1.k<=j by NAT_1:13;
then p29.k=p29.i or p19.k=p19.i by A11,A14,XXREAL_0:1;
hence p1.x=p2.x by A1,A17,A16,A18,A19,A24,FUNCT_1:def 4;
end;
end;
end;
hence thesis by A10,A13,A17,A16,FUNCT_1:2;
end;
then
A28: f is one-to-one by FUNCT_2:19;
set P = Permutations(N);
card X= N! by A1,A2,A3,Th7;
then reconsider P9=P,X9=X as finite set;
take f;
A30: card P9=n! by Th6;
card X9=n! by A1,A2,A3,Th7;
then f is onto one-to-one by A28,A30,FINSEQ_4:63;
hence f is bijective;
let p be Element of Permutations(n+1) such that
A31: p.i=j;
p in X by A3,A31;
hence thesis by A6,A31;
end;
theorem Th21:
for K being domRing
for a being Element of K
for i,j st i in Seg (n+1) & p1.i = j holds -(a,p1) = power(K).(-
1_K,i+j) * -(a,Rem(p1,i))
proof
let K be domRing;
let a be Element of K;
set n1=n+1;
let i,j such that
A1: i in Seg n1 and
A2: p1.i=j;
A3: p1 is Permutation of Seg n1 by MATRIX_1:def 16;
then
A4: rng p1=Seg n1 by FUNCT_2:def 3;
dom p1=Seg n1 by A3,FUNCT_2:52;
then
A5: j in Seg n1 by A1,A2,A4,FUNCT_1:def 3;
set R=Rem(p1,i);
per cases by NAT_1:23;
suppose
A6: n=0;
then R is even by Th11;
then
A7: -(a,R)=a by MATRIX_1:def 20;
A8: 1+1=2*1;
p1 is even by A6,Th11;
then
A9: -(a,p1)=a by MATRIX_1:def 20;
A10: j=1 by A5,A6,FINSEQ_1:2,TARSKI:def 1;
i=1 by A1,A6,FINSEQ_1:2,TARSKI:def 1;
then power(K).(-1_K,i+j)=1_K by A10,A8,HURWITZ:4;
hence thesis by A9,A7;
end;
suppose
A11: n=1;
then
A12: p1 is Permutation of Seg 2 by MATRIX_1:def 16;
per cases by A12,MATRIX_7:1;
suppose
A13: p1=<*1,2*>;
i=1 or i=2 by A1,A11,FINSEQ_1:2,TARSKI:def 2;
then i=1 & p1.i=1 or i=2 & p1.i=2 by A13;
then i+j=2*1 or i+j=2*2 by A2;
then
A14: power(K).(-1_K,i+j)=1_K by HURWITZ:4;
A15: len Permutations(2)=2 by MATRIX_1:9;
R is even by A11,Th11;
then
A16: -(a,R)=a by MATRIX_1:def 20;
id Seg 2 is even by MATRIX_1:16;
then -(a,p1)=a by A11,A13,A15,FINSEQ_2:52,MATRIX_1:def 20;
hence thesis by A14,A16;
end;
suppose
A17: p1=<*2,1*>;
len Permutations(2)=2 by MATRIX_1:9;
then -(a,p1)=-a by A11,A17,MATRIX_1:def 20,MATRIX_9:12;
then
A18: -(a,p1)=-1_K*a;
i=1 or i=2 by A1,A11,FINSEQ_1:2,TARSKI:def 2;
then i+j=2*1+1 by A2,A17;
then
A19: power(K).(-1_K,i+j)=-1_K by HURWITZ:4;
R is even by A11,Th11;
then -(a,R)=a by MATRIX_1:def 20;
hence thesis by A19,A18,VECTSP_1:8;
end;
end;
suppose
A20: n >= 2;
then reconsider n2=n-2 as Element of NAT by NAT_1:21;
per cases;
suppose
A21: not K is Fanoian;
A22: now
per cases by NAT_D:12;
suppose
i+j mod 2=0;
then consider t be Nat such that
A23: i+j = 2 * t + 0 and
0 < 2 by NAT_D:def 2;
t is Element of NAT by ORDINAL1:def 12;
hence power(K).(-1_K,i+j)=1_K by A23,HURWITZ:4;
end;
suppose
i+j mod 2=1;
then consider t be Nat such that
A24: i+j = 2 * t + 1 and
1 < 2 by NAT_D:def 2;
A25: 1_K=-1_K by A21,MATRIX11:22;
t is Element of NAT by ORDINAL1:def 12;
hence power(K).(-1_K,i+j)=1_K by A24,A25,HURWITZ:4;
end;
end;
A26: -(a,p1)=a or -(a,p1)=-a by MATRIX_1:def 20;
-1_K=1_K by A21,MATRIX11:22;
then
A27: -a*1_K=a*(1_K) by VECTSP_1:9;
-(a,R)=a or -(a,R)=-a by MATRIX_1:def 20;
then -(a,R)=a by A27;
hence thesis by A22,A26,A27;
end;
suppose
A29: K is Fanoian;
set mm=the multF of K;
reconsider n1=n2+1 as Element of NAT;
set P1=Permutations(n1+2);
reconsider Q1=p1 as Element of P1;
set SS1=2Set Seg (n1+2);
consider X be Element of Fin SS1 such that
A30: X = {{N,i} where N is Nat:{N,i} in SS1} and
A31: mm $$ (X,Part_sgn(Q1,K)) = power(K).(-1_K,i+j) by A1,A2,A29,Th9;
set PQ1=Part_sgn(Q1,K);
set SS2=2Set Seg (n2+2);
reconsider Q19=Q1 as Permutation of Seg (n1+2) by MATRIX_1:def 16;
set P2=Permutations(n2+2);
reconsider Q=R as Element of P2;
reconsider Q9=Q as Permutation of Seg (n2+2) by MATRIX_1:def 16;
set PQ=Part_sgn(Q,K);
SS1 in Fin SS1 by FINSUB_1:def 5; then
A32: In(SS1,Fin SS1)=SS1 by SUBSET_1:def 8;
reconsider SSX=SS1\X as Element of Fin SS1 by FINSUB_1:def 5;
A33: X\/SSX=SS1\/X by XBOOLE_1:39;
X c= SS1 by FINSUB_1:def 5;
then
A34: X\/SSX=SS1 by A33,XBOOLE_1:12;
consider f be Function of SS2,SS1 such that
A35: rng f=SS1\X and
A36: f is one-to-one and
A37: for k,m st k<m & {k,m} in SS2 holds (m < i & k < i implies f.{k
,m}={k,m}) & (m >= i & k < i implies f.{k,m}={k,m+1}) & (m >= i & k >= i
implies f.{k,m}={k+1,m+1}) by A1,A20,A30,Th10;
set Pf=PQ1*f;
A38: dom Pf=SS2 by FUNCT_2:def 1;
A39: dom Q19=Seg (n1+2) by FUNCT_2:52;
A40: now
n<=n+1 by NAT_1:11;
then
A41: Seg (n2+2) c= Seg (n1+2) by FINSEQ_1:5;
let x be object such that
A42: x in SS2;
consider k,m be Nat such that
A43: k in Seg (n2+2) and
A44: m in Seg (n2+2) and
A45: k < m and
A46: x={k,m} by A42,MATRIX11:1;
reconsider k,m as Element of NAT by ORDINAL1:def 12;
dom Q9=Seg (n2+2) by FUNCT_2:52;
then Q9.k<>Q.m by A43,A44,A45,FUNCT_1:def 4;
then
A47: Q.k>Q.m or Q.k<Q.m by XXREAL_0:1;
set m1=m+1;
set k1=k+1;
A48: (n2+2)+1=n1+2;
then
A49: k1 in Seg (n1+2) by A43,FINSEQ_1:60;
A50: m1 in Seg (n1+2) by A44,A48,FINSEQ_1:60;
per cases;
suppose
A51: k<i & m<i;
A52: Pf.x=PQ1.(f.x) by A38,A42,FUNCT_1:12;
A53: f.x=x by A37,A42,A45,A46,A51;
per cases;
suppose
Q1.k<j & Q1.m<j or Q1.k>=j & Q1.m>=j;
then Q.k=Q1.k&Q.m=Q1.m or Q.k=Q1.k-1&Q.m=Q1.m-1 by A1,A2,A43,A44
,A51,Def3;
then Q.k<Q.m & Q1.k<Q1.m or Q.k>Q.m & Q1.k>Q1.m by A47,XREAL_1:9;
then
PQ1.x=1_K & PQ.x=1_K or PQ1.x=-1_K & PQ.x=-1_K by A43,A44,A45,A46
,A41,MATRIX11:def 1;
hence Pf.x=PQ.x by A38,A42,A53,FUNCT_1:12;
end;
suppose
A54: Q1.k<j & Q1.m>=j;
then Q.m=Q1.m-1 by A1,A2,A44,A51,Def3;
then
A55: Q1.m=Q.m+1;
Q19.m<>j by A1,A2,A39,A44,A41,A51,FUNCT_1:def 4;
then Q1.m>j by A54,XXREAL_0:1;
then
A56: Q.m>=j by A55,NAT_1:13;
Q1.k<Q1.m by A54,XXREAL_0:2;
then
A57: PQ1.x=1_K by A43,A44,A45,A46,A41,MATRIX11:def 1;
Q1.k=Q.k by A1,A2,A43,A51,A54,Def3;
then Q.k<Q.m by A54,A56,XXREAL_0:2;
hence Pf.x=PQ.x by A43,A44,A45,A46,A53,A52,A57,MATRIX11:def 1;
end;
suppose
A58: Q1.k>=j & Q1.m<j;
then Q.k=Q1.k-1 by A1,A2,A43,A51,Def3;
then
A59: Q1.k=Q.k+1;
Q19.k<>j by A1,A2,A39,A43,A41,A51,FUNCT_1:def 4;
then Q1.k>j by A58,XXREAL_0:1;
then
A60: Q.k>=j by A59,NAT_1:13;
Q1.k>Q1.m by A58,XXREAL_0:2;
then
A61: PQ1.x=-1_K by A43,A44,A45,A46,A41,MATRIX11:def 1;
Q1.m=Q.m by A1,A2,A44,A51,A58,Def3;
then Q.k>Q.m by A58,A60,XXREAL_0:2;
hence Pf.x=PQ.x by A43,A44,A45,A46,A53,A52,A61,MATRIX11:def 1;
end;
end;
suppose
k>=i & m<i;
hence Pf.x=PQ.x by A45,XXREAL_0:2;
end;
suppose
A62: k<i & m>=i;
A63: Pf.x=PQ1.(f.{k,m}) by A38,A42,A46,FUNCT_1:12;
A64: f.{k,m}={k,m1} by A37,A42,A45,A46,A62;
per cases;
suppose
Q1.k<j & Q1.m1<j or Q1.k>=j & Q1.m1>=j;
then Q.k=Q1.k & Q.m=Q1.m1 or Q.k=Q1.k-1 & Q.m=Q1.m1-1 by A1,A2,A43
,A44,A62,Def3;
then
A65: Q.k<Q.m & Q1.k<Q1.m1 or Q.k>Q.m & Q1.k>Q1.m1 by A47,XREAL_1:9;
k < m1 by A45,NAT_1:13;
then PQ1.{k,m1}=1_K & PQ.x=1_K or PQ1.{k,m1}=-1_K & PQ.x=-1_K by
A43,A44,A45,A46,A41,A50,A65,MATRIX11:def 1;
hence Pf.x=PQ.x by A38,A42,A46,A64,FUNCT_1:12;
end;
suppose
A66: Q1.k<j & Q1.m1>=j;
m1>i by A62,NAT_1:13;
then Q19.m1<>j by A1,A2,A39,A50,FUNCT_1:def 4;
then
A67: Q1.m1>j by A66,XXREAL_0:1;
Q.m=Q1.m1-1 by A1,A2,A44,A62,A66,Def3;
then Q1.m1=Q.m+1;
then
A68: Q.m>=j by A67,NAT_1:13;
Q1.k=Q.k by A1,A2,A43,A62,A66,Def3;
then
A69: Q.k<Q.m by A66,A68,XXREAL_0:2;
A70: k<m1 by A45,NAT_1:13;
Q1.k<Q1.m1 by A66,XXREAL_0:2;
then PQ1.{k,m1}=1_K by A43,A41,A50,A70,MATRIX11:def 1;
hence Pf.x=PQ.x by A43,A44,A45,A46,A64,A63,A69,MATRIX11:def 1;
end;
suppose
A71: Q1.k>=j & Q1.m1<j;
then Q.k=Q1.k-1 by A1,A2,A43,A62,Def3;
then
A72: Q1.k=Q.k+1;
Q19.k<>j by A1,A2,A39,A43,A41,A62,FUNCT_1:def 4;
then Q1.k>j by A71,XXREAL_0:1;
then
A73: Q.k>=j by A72,NAT_1:13;
Q1.m1=Q.m by A1,A2,A44,A62,A71,Def3;
then
A74: Q.m<Q.k by A71,A73,XXREAL_0:2;
A75: k<m1 by A45,NAT_1:13;
Q1.k>Q1.m1 by A71,XXREAL_0:2;
then PQ1.{k,m1}=-1_K by A43,A41,A50,A75,MATRIX11:def 1;
hence Pf.x=PQ.x by A43,A44,A45,A46,A64,A63,A74,MATRIX11:def 1;
end;
end;
suppose
A76: k>=i & m>=i;
A77: Pf.x=PQ1.(f.{k,m}) by A38,A42,A46,FUNCT_1:12;
A78: k1<m1 by A45,XREAL_1:6;
A79: f.{k,m}={k+1,m+1} by A37,A42,A45,A46,A76;
per cases;
suppose
Q1.k1<j & Q1.m1<j or Q1.k1>=j & Q1.m1>=j;
then Q.k=Q1.k1&Q.m=Q1.m1 or Q.k=Q1.k1-1&Q.m=Q1.m1-1 by A1,A2,A43
,A44,A76,Def3;
then Q.k<Q.m & Q1.k1<Q1.m1 or Q.k>Q.m & Q1.k1>Q1.m1 by A47,
XREAL_1:9;
then PQ1.{k1,m1}=1_K & PQ.x=1_K or PQ1.{m1,k1}=-1_K&PQ.x=-1_K by
A43,A44,A45,A46,A49,A50,A78,MATRIX11:def 1;
hence Pf.x=PQ.x by A38,A42,A46,A79,FUNCT_1:12;
end;
suppose
A80: Q1.k1<j & Q1.m1>=j;
m1>i by A76,NAT_1:13;
then Q19.m1<>j by A1,A2,A39,A50,FUNCT_1:def 4;
then
A81: Q1.m1>j by A80,XXREAL_0:1;
Q.m=Q1.m1-1 by A1,A2,A44,A76,A80,Def3;
then Q1.m1=Q.m+1;
then
A82: Q.m>=j by A81,NAT_1:13;
Q1.k1<Q1.m1 by A80,XXREAL_0:2;
then
A83: PQ1.{k1,m1}=1_K by A49,A50,A78,MATRIX11:def 1;
Q1.k1=Q.k by A1,A2,A43,A76,A80,Def3;
then Q.k<Q.m by A80,A82,XXREAL_0:2;
hence Pf.x=PQ.x by A43,A44,A45,A46,A79,A77,A83,MATRIX11:def 1;
end;
suppose
A84: Q1.k1>=j & Q1.m1<j;
k1>i by A76,NAT_1:13;
then Q19.k1<>j by A1,A2,A39,A49,FUNCT_1:def 4;
then
A85: Q1.k1>j by A84,XXREAL_0:1;
Q.k=Q1.k1-1 by A1,A2,A43,A76,A84,Def3;
then Q1.k1=Q.k+1;
then
A86: Q.k>=j by A85,NAT_1:13;
Q1.k1>Q1.m1 by A84,XXREAL_0:2;
then
A87: PQ1.{k1,m1}=-1_K by A49,A50,A78,MATRIX11:def 1;
Q1.m1=Q.m by A1,A2,A44,A76,A84,Def3;
then Q.k>Q.m by A84,A86,XXREAL_0:2;
hence Pf.x=PQ.x by A43,A44,A45,A46,A79,A77,A87,MATRIX11:def 1;
end;
end;
end;
reconsider domf=dom f as Element of Fin SS2 by FINSUB_1:def 5;
A88: f.:domf=rng f by RELAT_1:113;
dom f=SS2 by FUNCT_2:def 1;
then
A89: domf=In(SS2,Fin SS2) by SUBSET_1:def 8;
dom PQ=SS2 by FUNCT_2:def 1;
then PQ=Pf by A38,A40,FUNCT_1:2;
then
A90: mm $$ (SSX,PQ1) = sgn(Q,K) by A35,A36,A89,A88,SETWOP_2:6;
X misses SSX by XBOOLE_1:79;
then sgn(Q1,K)=power(K).(-1_K,i+j)*sgn(Q,K) by A31,A90,A34,A32,SETWOP_2:4
;
hence -(a,p1) = power(K).(-1_K,i+j)*sgn(Q,K)*a by MATRIX11:26
.= power(K).(-1_K,i+j)*(sgn(Q,K)*a) by GROUP_1:def 3
.= power(K).(-1_K,i+j)*-(a,R) by MATRIX11:26;
end;
end;
end;
theorem Th22:
for K being domRing
for i,j st i in Seg (n+1) & p1.i = j for M be Matrix of n+1,K
for DM be Matrix of n,K st DM = Delete(M,i,j) holds (Path_product M).p1 = power
(K).(-1_K,i+j)*(M*(i,j))*(Path_product(DM)).Rem(p1,i)
proof
let K be domRing;
reconsider N=n as Element of NAT by ORDINAL1:def 12;
set n1 = N+1;
let i,j be Nat such that
A1: i in Seg(n+1) and
A2: p1.i=j;
set mm=the multF of K;
set R=Rem(p1,i);
let M be (Matrix of n+1,K),DM be (Matrix of n,K) such that
A3: DM=Delete(M,i,j);
set PR=Path_matrix(R,DM);
set Pp1=Path_matrix(p1,M);
len Pp1=n1 by MATRIX_3:def 7;
then dom Pp1=Seg n1 by FINSEQ_1:def 3;
then
A4: Pp1.i=M*(i,j) by A1,A2,MATRIX_3:def 7;
A5: now
per cases;
suppose
A6: N=0;
then
A7: len Pp1=1 by MATRIX_3:def 7;
Pp1.1=M*(i,j) by A1,A4,A6,FINSEQ_1:2,TARSKI:def 1;
then Pp1=<*M*(i,j)*> by A7,FINSEQ_1:40;
then
A8: mm $$ Pp1=M*(i,j) by FINSOP_1:11;
len PR=0 by A6,MATRIX_3:def 7;
then PR=<*>(the carrier of K);
then
A9: mm $$ PR = the_unity_wrt mm by FINSOP_1:10;
the_unity_wrt mm=1_K by FVSUM_1:5;
hence mm $$ Pp1=(M*(i,j))*(mm $$ PR) by A8,A9;
end;
suppose
A10: N>0;
len PR=n by MATRIX_3:def 7;
then consider f be sequence of the carrier of K such that
A11: f.1 = PR.1 and
A12: for k being Nat st 0<>k & k<n holds f.(k+1) = mm.(f.k,PR.(k+1)) and
A13: mm $$ PR=f.n by A10,FINSOP_1:def 1;
len Pp1=n1 by MATRIX_3:def 7;
then consider F be sequence of the carrier of K such that
A14: F.1 = Pp1.1 and
A15: for k being Nat st 0<>k & k<n1 holds F.(k+1) = mm.(F.k,Pp1.(k+1)) and
A16: mm $$ Pp1=F.n1 by FINSOP_1:def 1;
defpred P[Nat] means 1<=$1 & $1<i implies f.$1=F.$1;
A17: for k st k in Seg n holds (k<i implies PR.k=Pp1.k) & (k>=i implies
PR.k=Pp1.(k+1))
proof
len Pp1=n1 by MATRIX_3:def 7;
then
A18: dom Pp1=Seg n1 by FINSEQ_1:def 3;
len PR=n by MATRIX_3:def 7;
then
A19: dom PR=Seg n by FINSEQ_1:def 3;
reconsider p19=p1 as Permutation of Seg n1 by MATRIX_1:def 16;
reconsider R9=R as Permutation of Seg n by MATRIX_1:def 16;
let k such that
A20: k in Seg n;
reconsider k1=k+1 as Element of NAT;
A21: k1 in Seg n1 by A20,FINSEQ_1:60;
A22: rng p19=Seg n1 by FUNCT_2:def 3;
dom p19=Seg n1 by FUNCT_2:52;
then
A23: j in Seg n1 by A1,A2,A22,FUNCT_1:def 3;
A24: rng R9=Seg n by FUNCT_2:def 3;
dom R9=Seg n by FUNCT_2:52;
then
A25: R.k in Seg n by A20,A24,FUNCT_1:def 3;
then consider Rk be Nat such that
A26: Rk=R.k and
1<=Rk and
Rk<=n;
A27: n1-'1=n1-1 by XREAL_0:def 2;
n<=n1 by NAT_1:11;
then
A28: Seg n c= Seg n1 by FINSEQ_1:5;
thus k<i implies PR.k=Pp1.k
proof
assume
A29: k<i;
dom p19=Seg n1 by FUNCT_2:52;
then p19.k<>p19.i by A1,A20,A28,A29,FUNCT_1:def 4;
then p1.k<j or p1.k>j by A2,XXREAL_0:1;
then Rk=p1.k & p1.k<j or p1.k>j&Rk=p1.k-1 by A1,A2,A20,A26,A29,Def3;
then Rk=p1.k & p1.k<j or p1.k>j & p1.k=Rk+1;
then Rk=p1.k & p1.k<j or p1.k>j & Rk>=j & p1.k=Rk+1 by NAT_1:13;
then
DM*(k,Rk)=M*(k,Rk) & PR.k=DM*(k,Rk) & Pp1.k=M*(k,Rk) or PR.k=DM
*(k,Rk) & DM*(k,Rk)=M*(k,Rk+1) & Pp1.k=M*(k,Rk+1) by A1,A3,A20,A25,A23,A26,A28
,A27,A19,A18,A29,Th13,MATRIX_3:def 7;
hence thesis;
end;
A30: dom p19=Seg n1 by FUNCT_2:52;
assume
A31: k>=i;
then k1 >i by NAT_1:13;
then p19.k1<>p19.i by A1,A21,A30,FUNCT_1:def 4;
then p1.k1<j or p1.k1>j by A2,XXREAL_0:1;
then
Rk=p1.k1 & p1.k1<j or p1.k1>j&Rk=p1.k1-1 by A1,A2,A20,A26,A31,Def3;
then Rk=p1.k1 & p1.k1<j or p1.k1>j & p1.k1=Rk+1;
then Rk=p1.k1 & p1.k1<j or p1.k1>j & Rk>=j & p1.k1=Rk+1 by NAT_1:13;
then
DM*(k,Rk)=M*(k+1,Rk) & PR.k=DM*(k,Rk) & Pp1.k1=M*(k+1,Rk) or PR.k
=DM*(k,Rk) & DM*(k,Rk)=M*(k+1,Rk+1) & Pp1.k1=M*(k1,Rk+1) by A1,A3,A20,A25,A23
,A26,A27,A21,A19,A18,A31,Th13,MATRIX_3:def 7;
hence thesis;
end;
A32: for k st P[k] holds P[k+1]
proof
let k such that
A33: P[k];
reconsider e=k as Element of NAT by ORDINAL1:def 12;
assume that
A34: 1<=k+1 and
A35: k+1<i;
set k1 = e+1;
i<=n1 by A1,FINSEQ_1:1;
then k1<n1 by A35,XXREAL_0:2;
then k1<=n by NAT_1:13;
then
A36: k1 in Seg N by A34;
per cases by NAT_1:14;
suppose
k=0;
hence thesis by A14,A11,A17,A35,A36;
end;
suppose
A37: k>=1;
i<=n1 by A1,FINSEQ_1:1;
then
A38: k1<n1 by A35,XXREAL_0:2;
then k<n1 by NAT_1:13;
then
A39: F.k1=mm.(F.k,Pp1.k1) by A15,A37;
k1<=n by A38,NAT_1:13;
then
A40: k1 in Seg N by A34;
k<n by A38,XREAL_1:6;
then f.k1=mm.(f.k,PR.k1) by A12,A37;
hence thesis by A17,A33,A35,A37,A39,A40,NAT_1:13;
end;
end;
defpred Q[Nat] means i<=$1 & $1<=n1 implies ($1=1 implies F.($1)=M*(i,j)
) & ($1>1 implies for a being Element of K st a=f.($1-1)
holds F.$1=M*(i,j)*a);
A41: P[0];
A42: for k holds P[k] from NAT_1:sch 2(A41,A32);
A43: for k st Q[k] holds Q[k+1]
proof
let k such that
A44: Q[k];
set k1=k+1;
assume that
A45: i<=k1 and
A46: k1<=n1;
per cases;
suppose
A47: k=0;
1<=i by A1,FINSEQ_1:1;
hence thesis by A4,A14,A45,A47,XXREAL_0:1;
end;
suppose
A48: k>0;
hence k1=1 implies F.k1=M*(i,j);
assume k1>1;
let a be Element of K such that
A49: a=f.(k1-1);
A50: k<=n by A46,XREAL_1:6;
k>=1 by A48,NAT_1:14;
then
A51: k in Seg n by A50;
len PR=n by MATRIX_3:def 7;
then
A52: dom PR=Seg n by FINSEQ_1:def 3;
then
A53: PR.k=DM*(k,R.k) by A51,MATRIX_3:def 7;
k<n1 by A46,NAT_1:13;
then
A54: F.k1=mm.(F.k,Pp1.k1) by A15,A48;
per cases by A45,XXREAL_0:1;
suppose
A55: k1=i;
then k<i by NAT_1:13;
then F.k1=a*(M*(i,j)) by A4,A42,A48,A49,A54,A55,NAT_1:14;
hence thesis;
end;
suppose
A56: k1>i;
A57: k<n1 by A46,NAT_1:13;
A58: k>=i by A56,NAT_1:13;
i>=1 by A1,FINSEQ_1:1;
then
A59: k>=1 by A58,XXREAL_0:2;
per cases by A59,XXREAL_0:1;
suppose
k=1;
hence thesis by A11,A17,A44,A46,A49,A51,A54,A58,NAT_1:13;
end;
suppose
A60: k>1;
reconsider k9=k-1 as Element of NAT by A48,NAT_1:20;
reconsider fk9=f.k9 as Element of K;
k9+1<=n by A57,NAT_1:13;
then
A61: k9<n by NAT_1:13;
k9+1>0+1 by A60;
then
A62: a=mm.(fk9,PR.(k9+1)) by A12,A49,A61;
F.k=M*(i,j)*fk9 by A44,A46,A56,A60,NAT_1:13;
hence F.k1 = (M*(i,j)*fk9)*(DM*(k,R.k)) by A17,A51,A54,A53,A58
.= M*(i,j)*(fk9*(DM*(k,R.k)))by GROUP_1:def 3
.= M*(i,j)*a by A51,A52,A62,MATRIX_3:def 7;
end;
end;
end;
end;
A63: Q[0];
A64: for k holds Q[k] from NAT_1:sch 2(A63,A43);
A65: i<=n1 by A1,FINSEQ_1:1;
A66: n1-1=n;
n1>0+1 by A10,XREAL_1:6;
hence mm $$ Pp1=M*(i,j)*mm $$ PR by A16,A13,A64,A65,A66;
end;
end;
per cases;
suppose
A67: R is even;
thus (Path_product(M)).p1 = -(mm $$ Pp1,p1) by MATRIX_3:def 8
.= power(K).(-1_K,i+j)*-(mm $$ Pp1,R) by A1,A2,Th21
.= power(K).(-1_K,i+j)*(M*(i,j)*mm $$ PR) by A5,A67,MATRIX_1:def 20
.= power(K).(-1_K,i+j) * (M*(i,j))*mm $$ PR by GROUP_1:def 3
.= power(K).(-1_K,i+j) * (M*(i,j))* -(mm $$ PR,R) by A67,MATRIX_1:def 20
.= power(K).(-1_K,i+j)*(M*(i,j))*(Path_product(DM)).R by MATRIX_3:def 8;
end;
suppose
A68: R is odd;
thus (Path_product(M)).p1=-(mm $$ Pp1,p1) by MATRIX_3:def 8
.= power(K).(-1_K,i+j)*-(mm $$ Pp1,R) by A1,A2,Th21
.= power(K).(-1_K,i+j)*(-(M*(i,j)*mm $$ PR)) by A5,A68,MATRIX_1:def 20
.= power(K).(-1_K,i+j)*((M*(i,j)*(-(mm $$ PR)))) by VECTSP_1:8
.= power(K).(-1_K,i+j)*(M*(i,j))*(-(mm $$ PR)) by GROUP_1:def 3
.= power(K).(-1_K,i+j)*(M*(i,j))*-(mm $$ PR,R) by A68,MATRIX_1:def 20
.= power(K).(-1_K,i+j)*(M*(i,j))*(Path_product(DM)).R by MATRIX_3:def 8;
end;
end;
begin :: Minors & cofactors
definition
let i,j,n be Nat;
let K;
let M be Matrix of n,K;
func Minor(M,i,j) -> Element of K equals
Det Delete(M,i,j);
coherence;
end;
definition
let i,j,n be Nat;
let K;
let M be Matrix of n,K;
func Cofactor(M,i,j) -> Element of K equals
power(K).(-1_K,i+j)*Minor(M,i,j);
coherence;
end;
theorem Th23:
for K being domRing
for i,j st i in Seg n & j in Seg n for P be Element of Fin
Permutations n st P = {p:p.i = j} for M be Matrix of n,K holds (the addF of K)
$$ (P,Path_product(M)) = M*(i,j)*Cofactor(M,i,j)
proof
let K be domRing;
let i,j be Nat such that
A1: i in Seg n and
A2: j in Seg n;
n>0 by A1;
then reconsider n9=n-1 as Element of NAT by NAT_1:20;
set P=Permutations (n-'1);
set n91=n9+1;
set P1=Permutations n;
A3: n91-'1=n9+1-1 by XREAL_0:def 2;
set aa=the addF of K;
P in Fin P by FINSUB_1:def 5; then
A4: In(P,Fin P)=P by SUBSET_1:def 8;
let PP be Element of Fin P1 such that
A5: PP={p:p.i=j};
consider Proj be Function of PP,P such that
A6: Proj is bijective and
A7: for q be Element of Permutations n91 st q.i=j holds Proj.q = Rem(q,i
) by A1,A2,A5,A3,Th20;
let M be Matrix of n,K;
set DM=Delete(M,i,j);
set PathM=Path_product(M);
set PathDM=Path_product(DM);
set pm=power(K).(-1_K,i+j)*(M*(i,j));
defpred P[set] means for D be Element of Fin P1,ProjD be Element of Fin P st
D=$1 & ProjD=Proj.:D & D c= PP holds aa $$ (D,PathM) = pm * aa $$ (ProjD,PathDM
);
A8: for B9 be (Element of Fin P1), b be Element of P1 holds P[B9] & not b
in B9 implies P[B9 \/ {b}]
proof
let B9 be (Element of Fin P1), b be Element of P1 such that
A9: P[B9] and
A10: not b in B9;
A11: b in {b} by TARSKI:def 1;
A12: rng Proj=P by A6,FUNCT_2:def 3;
then Proj.:B9 c= P by RELAT_1:111;
then reconsider ProjB9=Proj.:B9 as Element of Fin P by FINSUB_1:def 5;
let D be Element of Fin P1,ProjD be Element of Fin P such that
A13: D=B9\/{b} and
A14: ProjD=Proj.:D and
A15: D c= PP;
A16: B9 c= D by A13,XBOOLE_1:7;
B9 c= D by A13,XBOOLE_1:7;
then
A17: B9 c= PP by A15;
{b}c=D by A13,XBOOLE_1:7;
then
A18: b in PP by A15,A11;
then consider Q1 be Element of P1 such that
A19: Q1=b and
A20: Q1.i=j by A5;
A21: dom Proj = PP by FUNCT_2:def 1;
then
A22: Im(Proj,b)={Proj.b} by A18,FUNCT_1:59;
reconsider Q=Proj.b as Element of P by A18,A21,A12,FUNCT_1:def 3;
A23: Proj.b in rng Proj by A18,A21,FUNCT_1:def 3;
reconsider Q19=Q1 as Element of Permutations (n9+1);
A24: Rem(Q19,i)=Q by A7,A19,A20;
then
A25: PathM.Q1=pm*PathDM.Q by A1,A3,A20,Th22;
A26: not Q in ProjB9
proof
assume Q in ProjB9;
then ex x being object st x in dom Proj & x in B9 & Proj.x=Q
by FUNCT_1:def 6;
hence thesis by A6,A10,A18,A21,FUNCT_1:def 4;
end;
per cases;
suppose
A27: B9={};
then
A28: aa $$ (D,PathM)=PathM.b by A13,SETWISEO:17;
aa $$ (ProjD,PathDM)=PathDM.(Proj.b) by A13,A14,A22,A23,A12,A27,
SETWISEO:17;
hence thesis by A1,A3,A19,A20,A24,A28,Th22;
end;
suppose
A29: B9<>{};
ProjD=ProjB9\/{Q} by A13,A14,A22,RELAT_1:120;
hence pm *aa $$ (ProjD,PathDM) = pm*(aa $$(ProjB9,PathDM)+PathDM.Q) by
A18,A17,A21,A26,A29,SETWOP_2:2
.= (pm * aa $$ (ProjB9,PathDM))+(pm * PathDM.Q) by VECTSP_1:def 2
.= aa.(aa $$ (B9,PathM),PathM.b) by A9,A15,A19,A16,A25,XBOOLE_1:1
.= aa $$ (D,PathM) by A10,A13,A29,SETWOP_2:2;
end;
end;
A30: P[{}.P1]
proof
let B be Element of Fin P1,ProjB be Element of Fin P such that
A31: B = {}.P1 and
A32: ProjB = Proj.:B and
B c= PP;
ProjB={}.P by A31,A32;
then
A33: aa $$ (ProjB,PathDM)=the_unity_wrt aa by FVSUM_1:8,SETWISEO:31;
A34: the_unity_wrt aa=0.K by FVSUM_1:7;
aa $$ (B,PathM)=the_unity_wrt aa by A31,FVSUM_1:8,SETWISEO:31;
hence thesis by A33,A34;
end;
A35: for B being Element of Fin P1 holds P[B] from SETWISEO:sch 2(A30,A8 );
A36: dom Proj=PP by FUNCT_2:def 1;
rng Proj=P by A6,FUNCT_2:def 3;
then Proj.:PP=In(P,Fin P) by A4,A36,RELAT_1:113;
hence aa $$ (PP,PathM) = M*(i,j) * power(K).(-1_K,i+j)* Det (Delete(M,i,j))
by A35
.= M*(i,j) * Cofactor(M,i,j) by GROUP_1:def 3;
end;
theorem Th24:
for i,j st i in Seg n & j in Seg n holds Minor(M,i,j) = Minor(M@ ,j,i)
proof
let i,j such that
A1: i in Seg n and
A2: j in Seg n;
thus Minor(M,i,j) = Det(Delete(M,i,j)@) by MATRIXR2:43
.= Minor(M@,j,i) by A1,A2,Th14;
end;
definition
let n,K;
let M be Matrix of n,K;
func Matrix_of_Cofactor(M) -> Matrix of n,K means
:Def6:
for i,j being Nat st [i,j] in Indices it holds it*(i,j) = Cofactor(M,i,j);
existence
proof
reconsider N=n as Element of NAT by ORDINAL1:def 12;
deffunc C(Nat,Nat)=Cofactor(M,$1,$2);
ex M being Matrix of N,N,K st for i,j being Nat st [i,j] in Indices M
holds M*(i,j) = C(i,j) from MATRIX_0:sch 1;
hence thesis;
end;
uniqueness
proof
let C1,C2 be Matrix of n,K such that
A1: for i,j being Nat st [i,j] in Indices C1 holds C1*(i,j) = Cofactor
(M,i,j) and
A2: for i,j being Nat st [i,j] in Indices C2 holds C2*(i,j) = Cofactor (M,i,j);
now
A3: Indices C1=Indices C2 by MATRIX_0:26;
let i,j be Nat such that
A4: [i,j] in Indices C1;
reconsider i9=i,j9=j as Element of NAT by ORDINAL1:def 12;
C1*(i,j) = Cofactor(M,i9,j9) by A1,A4;
hence C1*(i,j)=C2*(i,j) by A2,A4,A3;
end;
hence thesis by MATRIX_0:27;
end;
end;
begin :: Laplace expansion
definition
let n,i,K;
let M be Matrix of n,K;
::$N Laplace expansion
func LaplaceExpL(M,i) -> FinSequence of K means
:Def7:
len it = n & for j st j in dom it holds it.j = M*(i,j)*Cofactor(M,i,j);
existence
proof
reconsider N=n as Element of NAT by ORDINAL1:def 12;
deffunc L(Nat)=M*(i,$1)*Cofactor(M,i,$1);
consider LL be FinSequence such that
A1: len LL = N & for k being Nat st k in dom LL holds LL.k=L(k) from
FINSEQ_1:sch 2;
rng LL c= the carrier of K
proof
let x be object;
assume x in rng LL;
then consider y being object such that
A2: y in dom LL and
A3: LL.y=x by FUNCT_1:def 3;
dom LL=Seg n by A1,FINSEQ_1:def 3;
then consider k being Nat such that
A4: k=y and
1<=k and
k<=n by A2;
L(k) is Element of K;
then LL.k is Element of K by A1,A2,A4;
hence thesis by A3,A4;
end;
then reconsider LL as FinSequence of K by FINSEQ_1:def 4;
take LL;
thus len LL = n by A1;
thus thesis by A1;
end;
uniqueness
proof
let L1,L2 be FinSequence of K such that
A5: len L1=n and
A6: for j st j in dom L1 holds L1.j=M*(i,j)*Cofactor(M,i,j) and
A7: len L2=n and
A8: for j st j in dom L2 holds L2.j = M*(i,j)*Cofactor(M,i,j);
A9: dom L2=Seg n by A7,FINSEQ_1:def 3;
A10: dom L1=Seg n by A5,FINSEQ_1:def 3;
now
let k be Nat such that
A11: k in dom L1;
L1.k=M*(i,k)*Cofactor(M,i,k) by A6,A11;
hence L1.k=L2.k by A8,A10,A9,A11;
end;
hence thesis by A10,A9,FINSEQ_1:13;
end;
end;
definition
let n;
let j be Nat,K;
let M be Matrix of n,K;
func LaplaceExpC(M,j) -> FinSequence of K means
:Def8:
len it = n & for i st i in dom it holds it.i = M*(i,j)*Cofactor(M,i,j);
existence
proof
reconsider N=n as Element of NAT by ORDINAL1:def 12;
deffunc L(Nat)=M*($1,j)*Cofactor(M,$1,j);
consider LL be FinSequence such that
A1: len LL = N & for k being Nat st k in dom LL holds LL.k=L(k) from
FINSEQ_1:sch 2;
rng LL c= the carrier of K
proof
let x be object;
assume x in rng LL;
then consider y being object such that
A2: y in dom LL and
A3: LL.y=x by FUNCT_1:def 3;
dom LL=Seg n by A1,FINSEQ_1:def 3;
then consider k being Nat such that
A4: k=y and
1<=k and
k<=n by A2;
L(k) is Element of K;
then LL.k is Element of K by A1,A2,A4;
hence thesis by A3,A4;
end;
then reconsider LL as FinSequence of K by FINSEQ_1:def 4;
take LL;
thus len LL = n by A1;
let i;
assume i in dom LL;
hence thesis by A1;
end;
uniqueness
proof
let L1,L2 be FinSequence of K such that
A5: len L1=n and
A6: for i st i in dom L1 holds L1.i=M*(i,j)*Cofactor(M,i,j) and
A7: len L2=n and
A8: for i st i in dom L2 holds L2.i = M*(i,j)*Cofactor(M,i,j);
A9: dom L2=Seg n by A7,FINSEQ_1:def 3;
A10: dom L1=Seg n by A5,FINSEQ_1:def 3;
now
let k be Nat such that
A11: k in dom L1;
L1.k=M*(k,j)*Cofactor(M,k,j) by A6,A11;
hence L1.k=L2.k by A8,A10,A9,A11;
end;
hence thesis by A10,A9,FINSEQ_1:13;
end;
end;
theorem Th25:
for K being non degenerated domRing-like commutative Ring
for i be Nat, M be Matrix of n,K st i in Seg n holds Det M = Sum
LaplaceExpL(M,i)
proof
let K be non degenerated domRing-like commutative Ring;
reconsider N=n as Element of NAT by ORDINAL1:def 12;
set P=Permutations n;
set KK=the carrier of K;
set aa=the addF of K;
A1: aa is having_a_unity by FVSUM_1:8;
let i be Nat, M be Matrix of n,K such that
A2: i in Seg n;
reconsider X=finSeg N as non empty set by A2;
set Path=Path_product(M);
deffunc G(Element of Fin P)=aa $$ ($1,Path);
consider g be Function of Fin P,KK such that
A3: for x being Element of Fin P holds g.x = G(x) from FUNCT_2:sch 4;
A4: for A,B be Element of Fin P st A misses B holds aa.(g.A,g.B)=g.(A \/ B)
proof
let A,B be Element of Fin P such that
A5: A misses B;
A6: g.(A)=G(A) by A3;
A7: g.B=G(B) by A3;
g.(A \/ B)=G(A\/B) by A3;
hence thesis by A5,A6,A7,FVSUM_1:8,SETWOP_2:4;
end;
deffunc F(object) = {p:p.i=$1};
consider f be Function such that
A8: dom f = X &
for x being object st x in X holds f.x = F(x) from FUNCT_1:sch 3;
rng f c= Fin P
proof
let x be object;
assume x in rng f;
then consider y being object such that
A9: y in dom f and
A10: f.y=x by FUNCT_1:def 3;
A11: F(y) c= P
proof
let z be object;
assume z in F(y);
then ex p st p=z& p.i=y;
hence thesis;
end;
F(y) in Fin P by A11,FINSUB_1:def 5;
hence thesis by A8,A9,A10;
end;
then reconsider f as Function of X,Fin P by A8,FUNCT_2:2;
A12: g.In(P,Fin P)=Det M by A3;
set gf=g*f;
A13: dom gf=X by FUNCT_2:def 1;
then
A14: gf*(id X)=gf by RELAT_1:52;
A15: P c= union (f.:X)
proof
let x be object;
assume
A16: x in P;
then reconsider p=x as Permutation of X by MATRIX_1:def 16;
A17: x in F(p.i) by A16;
A18: rng p=X by FUNCT_2:def 3;
dom p=X by FUNCT_2:52;
then
A19: p.i in X by A2,A18,FUNCT_1:def 3;
then
A20: f.(p.i) in f.:X by A8,FUNCT_1:def 6;
f.(p.i)=F(p.i) by A8,A19;
hence thesis by A17,A20,TARSKI:def 4;
end;
set L=LaplaceExpL(M,i);
len L=n by Def7;
then
A21: dom L=Seg n by FINSEQ_1:def 3;
then
A22: dom id X=dom L;
reconsider X9=X as Element of Fin X by FINSUB_1:def 5;
P in Fin P by FINSUB_1:def 5; then
A23: In(P,Fin P)=P by SUBSET_1:def 8;
g.{}.Fin P=aa $$ ({}.P,Path) by A3;
then
A24: g.{}=the_unity_wrt aa by FVSUM_1:8,SETWISEO:31;
A25: now
let x,y such that
A26: x in X9 and
A27: y in X9 and
A28: f.x meets f.y;
consider z being object such that
A29: z in f.x and
A30: z in f.y by A28,XBOOLE_0:3;
f.y=F(y) by A8,A27;
then
A31: ex p st p=z& p.i=y by A30;
f.x=F(x) by A8,A26;
then ex p st p=z& p.i=x by A29;
hence x=y by A31;
end;
now
A32: rng f c= Fin P by RELAT_1:def 19;
let x be object such that
A33: x in dom gf;
consider k being Nat such that
A34: k=x and
1<=k and
k<=n by A13,A33;
f.k in rng f by A8,A33,A34,FUNCT_1:def 3;
then reconsider Fk=F(k) as Element of Fin P by A8,A33,A34,A32;
A35: f.k=Fk by A8,A33,A34;
gf.k=g.(f.k) by A8,A33,A34,FUNCT_1:13;
then
A36: gf.k=G(Fk) by A3,A35;
G(Fk)=M*(i,k)*Cofactor(M,i,k) by A2,A33,A34,Th23;
hence L.x=gf.x by A21,A33,A34,A36,Def7;
end;
then
A37: L=gf by A21,A13,FUNCT_1:2;
set Laa=[#](L,the_unity_wrt aa);
A38: rng id X=X9;
A39: Laa| (dom L)=L by SETWOP_2:21;
union (f.:X) c= P
proof
let x be object;
assume x in union (f.:X);
then consider y being set such that
A40: x in y and
A41: y in f.:X by TARSKI:def 4;
consider z be object such that
A42: z in dom f and
z in X and
A43: f.z=y by A41,FUNCT_1:def 6;
y=F(z) by A8,A42,A43;
then ex p st x=p & p.i=z by A40;
hence thesis;
end;
then P=union (f.:X) by A15,XBOOLE_0:def 10;
then
A44: aa $$ (f.:X9,g)= g.In(P,Fin P) by A25,A4,A1,A24,A23,Th12;
aa $$ (X9,g*f)=aa $$ (f.:X9,g) by A25,A4,A1,A24,Th12;
hence Det M = aa $$(findom L,Laa) by A22,A38,A39,A14,A37,A44,A12,SETWOP_2:5
.= Sum L by FVSUM_1:8,SETWOP_2:def 2;
end;
theorem Th26:
for i st i in Seg n holds LaplaceExpC(M,i) = LaplaceExpL(M@,i)
proof
let i such that
A1: i in Seg n;
set LL=LaplaceExpL(M@,i);
set LC=LaplaceExpC(M,i);
reconsider I=i as Element of NAT by ORDINAL1:def 12;
A2: len LL=n by Def7;
A3: len LC=n by Def8;
now
let k be Nat such that
A4: 1 <=k and
A5: k <= n;
A6: k in Seg n by A4,A5;
dom LC=Seg n by A3,FINSEQ_1:def 3;
then
A7: LC.k=M*(k,I)*Cofactor(M,k,I) by A6,Def8;
Indices M=[:Seg n,Seg n:] by MATRIX_0:24;
then
A8: [k,i] in Indices M by A1,A6,ZFMISC_1:87;
dom LL=Seg n by A2,FINSEQ_1:def 3;
then
A9: LL.k=M@*(I,k)*Cofactor(M@,I,k) by A6,Def7;
Cofactor(M,k,I)=Cofactor(M@,I,k) by A1,A6,Th24;
hence LC.k=LL.k by A8,A7,A9,MATRIX_0:def 6;
end;
hence thesis by A3,A2;
end;
theorem
for K be domRing
for j be Nat, M be Matrix of n,K st j in Seg n holds Det M = Sum
LaplaceExpC(M,j)
proof
let K be domRing;
let j be Nat, M be Matrix of n,K such that
A1: j in Seg n;
thus Det M = Det M@ by MATRIXR2:43
.= Sum LaplaceExpL(M@,j) by A1,Th25
.= Sum LaplaceExpC(M,j) by A1,Th26;
end;
theorem Th28:
for p,i st len f=n & i in Seg n holds mlt(Line(
Matrix_of_Cofactor M,i),f) = LaplaceExpL(RLine(M,i,f),i)
proof
let p,i such that
A1: len f=n and
A2: i in Seg n;
reconsider N=n as Element of NAT by ORDINAL1:def 12;
set KK=the carrier of K;
set C=Matrix_of_Cofactor M;
reconsider Tp=f,TL=Line(C,i) as Element of N-tuples_on KK by A1,FINSEQ_2:92
,MATRIX_0:24;
set R=RLine(M,i,f);
set LL=LaplaceExpL(R,i);
set MLT=mlt(TL,Tp);
A3: len LL=n by Def7;
A4: now
A5: dom LL=Seg n by A3,FINSEQ_1:def 3;
A6: n=width M by MATRIX_0:24;
let j be Nat such that
A7: 1<=j and
A8: j<=n;
A9: j in Seg n by A7,A8;
n=width C by MATRIX_0:24;
then
A10: Line(C,i).j=C*(i,j) by A9,MATRIX_0:def 7;
Indices M=[:Seg n,Seg n:] by MATRIX_0:24;
then [i,j] in Indices M by A2,A9,ZFMISC_1:87;
then
A11: R*(i,j)=f.j by A1,A6,MATRIX11:def 3;
Indices C=[:Seg n,Seg n:] by MATRIX_0:24;
then [i,j] in Indices C by A2,A9,ZFMISC_1:87;
then Line(C,i).j=Cofactor(M,i,j) by A10,Def6;
then
A12: MLT.j=Cofactor(M,i,j)*(R*(i,j)) by A9,A11,FVSUM_1:61;
Cofactor(M,i,j)=Cofactor(R,i,j) by A2,A9,Th15;
hence MLT.j=LL.j by A9,A5,A12,Def7;
end;
len MLT=n by CARD_1:def 7;
hence thesis by A3,A4;
end;
theorem Th29:
for K being domRing
for M being Matrix of n,K
st i in Seg n holds Line(M,j) "*" Col((Matrix_of_Cofactor M)@,i)
= Det RLine(M,i,Line(M,j))
proof
let K be domRing;
let M be Matrix of n,K;
assume
A1: i in Seg n;
set C=Matrix_of_Cofactor M;
len C=n by MATRIX_0:24;
then dom C=Seg n by FINSEQ_1:def 3;
then
A2: Line(C,i)=Col(C@,i) by A1,MATRIX_0:58;
width M=n by MATRIX_0:24;
then
A3: len Line(M,j)=n by MATRIX_0:def 7;
thus Det RLine(M,i,Line(M,j)) = Sum LaplaceExpL(RLine(M,i,Line(M,j)),i) by A1
,Th25
.= Sum mlt(Col(C@,i),Line(M,j)) by A1,A2,A3,Th28
.= Line(M,j) "*" Col(C@,i) by FVSUM_1:64;
end;
theorem Th30:
for K being domRing
for M being Matrix of n,K
st Det M is unital holds M * ((Det M)" * (Matrix_of_Cofactor M)@) = 1.(K,n)
proof
let K be domRing;
let M be Matrix of n,K;
set D=Det M;
set D9=D";
set C=Matrix_of_Cofactor M;
set DC=D9*(C@);
set MC=M*DC;
set ID=1.(K,n);
assume
A1: D is unital;
now
A2: Indices MC=Indices ID by MATRIX_0:26;
reconsider N=n as Element of NAT by ORDINAL1:def 12;
let i,j be Nat such that
A3: [i,j] in Indices MC;
reconsider COL=Col(C@,j),L=Line(M,i) as Element of N-tuples_on the carrier
of K by MATRIX_0:24;
reconsider i9=i,j9=j as Element of NAT by ORDINAL1:def 12;
A4: len DC=n by MATRIX_0:24;
A5: Indices MC=[:Seg n,Seg n:] by MATRIX_0:24;
then
A6: i in Seg n by A3,ZFMISC_1:87;
A7: j in Seg n by A3,A5,ZFMISC_1:87;
then
A8: 1<=j by FINSEQ_1:1;
width (C@)=n by MATRIX_0:24;
then j<=width (C@) by A7,FINSEQ_1:1;
then Col(DC,j)=D9*COL by A8,MATRIXR1:19;
then mlt(Line(M,i),Col(DC,j)) = D9* mlt(L,COL) by FVSUM_1:69;
then
A9: Line(M,i) "*" Col(DC,j) = D9*(Line(M,i)"*"Col(C@,j)) by FVSUM_1:73
.= D9* Det RLine(M,j9,Line(M,i9))by A7,Th29;
A10: width M=n by MATRIX_0:24;
then
A11: MC*(i,j)=D9* Det RLine(M,j,Line(M,i)) by A3,A4,A9,MATRIX_3:def 4;
per cases;
suppose
A12: i=j;
then
A13: RLine(M,j,Line(M,i))=M by MATRIX11:30;
A14: D*D9=1.K by A1, ALGSTR_0:def 30
.= 1_K;
ID*(i,j) = 1_K by A3,A2,A12,MATRIX_1:def 3;
hence ID*(i,j) = MC*(i,j) by A3,A10,A4,A9,A13,A14,MATRIX_3:def 4;
end;
suppose
A15: i<>j;
then
A16: ID*(i,j) = 0.K by A3,A2,MATRIX_1:def 3;
Det RLine(M,j9,Line(M,i9))=0.K by A6,A7,A15,MATRIX11:51;
hence ID*(i,j) = MC*(i,j) by A11,A16;
end;
end;
hence thesis by MATRIX_0:27;
end;
theorem Th31:
for f,i st len f=n & i in Seg n holds mlt(Col(Matrix_of_Cofactor
M,i),f) = LaplaceExpL(RLine(M@,i,f),i)
proof
let f,i such that
A1: len f=n and
A2: i in Seg n;
reconsider N=n as Element of NAT by ORDINAL1:def 12;
set KK=the carrier of K;
set C=Matrix_of_Cofactor M;
reconsider Tp=f,TC=Col(C,i) as Element of N-tuples_on KK by A1,FINSEQ_2:92
,MATRIX_0:24;
set R=RLine(M@,i,f);
set LL=LaplaceExpL(R,i);
set MCT=mlt(TC,Tp);
A3: len LL=n by Def7;
A4: now
A5: Indices M@=[:Seg n,Seg n:] by MATRIX_0:24;
A6: dom LL=Seg n by A3,FINSEQ_1:def 3;
A7: width (M@)=n by MATRIX_0:24;
let j be Nat such that
A8: 1<=j and
A9: j<=n;
A10: j in Seg n by A8,A9;
then Delete(M@,i,j)=Delete(M,j,i)@ by A2,Th14;
then
A11: Cofactor(M@,i,j)=Cofactor(M,j,i) by MATRIXR2:43;
Indices C=[:Seg n,Seg n:] by MATRIX_0:24;
then [j,i] in Indices C by A2,A10,ZFMISC_1:87;
then
A12: C*(j,i)=Cofactor(M,j,i) by Def6;
n=len C by MATRIX_0:24;
then dom C=Seg n by FINSEQ_1:def 3;
then
A13: Col(C,i).j=C*(j,i) by A10,MATRIX_0:def 8;
A14: Indices M=[:Seg n,Seg n:] by MATRIX_0:24;
then [i,j] in Indices M by A2,A10,ZFMISC_1:87;
then R*(i,j)=f.j by A1,A7,A14,A5,MATRIX11:def 3;
then
A15: MCT.j=Cofactor(M,j,i)*(R*(i,j)) by A10,A13,A12,FVSUM_1:61;
Cofactor(R,i,j)=Cofactor(M@,i,j) by A2,A10,Th15;
hence MCT.j=LL.j by A10,A11,A6,A15,Def7;
end;
len MCT=n by CARD_1:def 7;
hence thesis by A3,A4;
end;
theorem Th32:
for K be domRing
for M be Matrix of n,K
st i in Seg n & j in Seg n holds Line((Matrix_of_Cofactor M)@,i)
"*" Col(M,j) = Det RLine(M@,i,Line(M@,j))
proof
let K be domRing;
let M be Matrix of n,K;
assume that
A1: i in Seg n and
A2: j in Seg n;
set C=Matrix_of_Cofactor M;
set L=Line(M@,j);
A3: width C = n by MATRIX_0:24;
width (M@)=n by MATRIX_0:24;
then
A4: len L=n by MATRIX_0:def 7;
A5: width M=n by MATRIX_0:24;
thus Det RLine(M@,i,L) = Sum LaplaceExpL(RLine(M@,i,L),i) by A1,Th25
.= Sum mlt(Col(C,i),L) by A1,A4,Th31
.= Line(C@,i) "*" L by A1,A3,MATRIX_0:59
.= Line(C@,i) "*" Col(M,j) by A2,A5,MATRIX_0:59;
end;
theorem Th33:
for K be domRing
for M being Matrix of n,K
st Det M is unital holds ((Det M)" * (Matrix_of_Cofactor M)@) * M = 1.(K,n)
proof
let K be domRing;
let M be Matrix of n,K;
set D=Det M;
set D9=D";
set C=Matrix_of_Cofactor M;
set DC=D9*(C@);
set CM=DC*M;
set ID=1.(K,n);
assume
A1: D is unital;
now
A2: Indices CM=Indices ID by MATRIX_0:26;
reconsider N=n as Element of NAT by ORDINAL1:def 12;
let i,j be Nat such that
A3: [i,j] in Indices CM;
reconsider COL=Col(M,j),L=Line(C@,i) as Element of N-tuples_on the carrier
of K by MATRIX_0:24;
reconsider i9=i,j9=j as Element of NAT by ORDINAL1:def 12;
A4: len M=n by MATRIX_0:24;
A5: Indices CM=[:Seg n,Seg n:] by MATRIX_0:24;
then
A6: i in Seg n by A3,ZFMISC_1:87;
then
A7: 1<=i by FINSEQ_1:1;
A8: j in Seg n by A3,A5,ZFMISC_1:87;
len (C@)=n by MATRIX_0:24;
then i<=len (C@) by A6,FINSEQ_1:1;
then Line(DC,i)=D9*L by A7,MATRIXR1:20;
then mlt(Line(DC,i),Col(M,j)) = D9* mlt(L,COL) by FVSUM_1:69;
then
A9: Line(DC,i)"*"Col(M,j) = D9*(Line(C@,i)"*"Col(M,j)) by FVSUM_1:73
.= D9*Det RLine(M@,i9,Line(M@,j9))by A6,A8,Th32;
A10: width DC=n by MATRIX_0:24;
then
A11: CM*(i,j)=D9* Det RLine(M@,i,Line(M@,j)) by A3,A4,A9,MATRIX_3:def 4;
per cases;
suppose
A12: i=j;
then
A13: RLine(M@,i,Line(M@,j))=M@ by MATRIX11:30;
A14: D=Det M@ by MATRIXR2:43;
A15: D9*D=1_K by A1,ALGSTR_0:def 30;
ID*(i,j) = 1_K by A3,A2,A12,MATRIX_1:def 3;
hence ID*(i,j) = CM*(i,j) by A3,A10,A4,A9,A13,A15,A14,MATRIX_3:def 4;
end;
suppose
A16: i<>j;
then
A17: ID*(i,j) = 0.K by A3,A2,MATRIX_1:def 3;
Det RLine(M@,i9,Line(M@,j9))=0.K by A6,A8,A16,MATRIX11:51;
hence ID*(i,j) = CM*(i,j) by A11,A17;
end;
end;
hence thesis by MATRIX_0:27;
end;
theorem Th34:
for K be domRing
for M be Matrix of n,K
holds (M is invertible iff Det M is unital)
proof
let K be domRing;
let M be Matrix of n,K;
thus M is invertible implies Det M is unital
proof
reconsider N=n as Element of NAT by ORDINAL1:def 12;
assume M is invertible;
then consider M1 be Matrix of n,K such that
A1: M is_reverse_of M1 by MATRIX_6:def 3;
per cases by NAT_1:14;
suppose
N=0;
then Det M=1_K by MATRIXR2:41
.= 1.K;
hence thesis;
end;
suppose
A2: N>=1;
A3: M*M1=(1.(K,n)) by A1,MATRIX_6:def 2;
Det (1.(K,n))=1_K by A2,MATRIX_7:16;
then Det M*Det M1=1_K by A2,A3,MATRIX11:62
.= 1.K;
hence thesis by GCD_1:def 1,def 20;
end;
end;
set C=(Det M)" * (Matrix_of_Cofactor M)@;
assume
A4: Det M is unital;
then
A5: M*C=1.(K,n) by Th30;
C*M=1.(K,n) by A4,Th33;
then M is_reverse_of C by A5,MATRIX_6:def 2;
hence thesis by MATRIX_6:def 3;
end;
theorem Th35:
for K be domRing
for M be Matrix of n,K
st K is non degenerated & Det M is unital
holds M~ = (Det M)" * (Matrix_of_Cofactor M)@
proof
let K be domRing;
let M be Matrix of n,K;
set C=(Det M)" * (Matrix_of_Cofactor M)@;
assume
A0: K is non degenerated;
assume
A1: Det M is unital;
then
A2: M*C=1.(K,n) by Th30;
C*M=1.(K,n) by A1,Th33;
then
A3: M is_reverse_of C by A2,MATRIX_6:def 2;
M is invertible by A1,Th34;
hence thesis by A3,MATRIX_6:def 4;
end;
theorem
for K be domRing
for M be Matrix of n,K st M is invertible for i,j st [i,j] in Indices
(M~) holds M~*(i,j) = (Det M)" * power(K).(-1_K,i+j) * Minor(M,j,i)
proof
let K be domRing;
let M be Matrix of n,K;
A0: K is non degenerated;
assume M is invertible;
then
A1: Det M is unital by Th34;
set D=Det M;
set COF=Matrix_of_Cofactor M;
let i,j;
assume [i,j] in Indices (M~);
then
A2: [i,j] in Indices (COF@) by MATRIX_0:26;
then
A3: [j,i] in Indices COF by MATRIX_0:def 6;
thus M~*(i,j)=(D" * COF@)*(i,j) by A1,Th35
.=D"*((COF@)*(i,j)) by A2,MATRIX_3:def 5
.=D"*(COF*(j,i)) by A3,MATRIX_0:def 6
.=D"*Cofactor(M,j,i) by A3,Def6
.=D"*power(K).(-1_K,i+j) * Minor(M,j,i) by GROUP_1:def 3;
end;
theorem Th37:
for K be domRing
for A be Matrix of n,K st Det A is unital for x,b be Matrix of K st
len x = n & A * x = b holds x = A~ * b & for i,j st [i,j] in Indices x holds x*
(i,j) = (Det A)" * Det ReplaceCol(A,i,Col(b,j))
proof
let K be domRing;
let A be Matrix of n,K such that
A1: Det A is unital;
A is invertible by A1,Th34;
then A~ is_reverse_of A by MATRIX_6:def 4;
then
A2: A~*A=1.(K,n) by MATRIX_6:def 2;
set MC=Matrix_of_Cofactor A;
set D=Det A;
A3: width MC=n by MATRIX_0:24;
A4: len (MC@)=n by MATRIX_0:24;
A5: width (MC@)=n by MATRIX_0:24;
A6: width (A~)=n by MATRIX_0:24;
A7: width A=n by MATRIX_0:24;
let x,b be Matrix of K such that
A8: len x = n and
A9: A * x = b;
A10: len A=n by MATRIX_0:24;
then
A11: len b=n by A8,A9,A7,MATRIX_3:def 4;
x = 1.(K,n) * x by A8,MATRIXR2:68;
hence
A12: x=A~ * b by A8,A9,A6,A10,A7,A2,MATRIX_3:33;
let i,j such that
A13: [i,j] in Indices x;
A14: len Col(b,j)=n by A11,MATRIX_0:def 8;
Indices x=[:Seg n,Seg width x:] by A8,FINSEQ_1:def 3;
then
A15: i in Seg n by A13,ZFMISC_1:87;
then
A16: 1<=i by FINSEQ_1:1;
A17: i<= n by A15,FINSEQ_1:1;
thus x*(i,j) = Line(A~,i)"*"Col(b,j) by A6,A12,A13,A11,MATRIX_3:def 4
.= Line(D" * MC@,i)"*"Col(b,j) by A1,Th35
.= (D"*Line(MC@,i))"*"Col(b,j) by A4,A16,A17,MATRIXR1:20
.= Sum(D"*mlt(Line(MC@,i),Col(b,j))) by A5,A11,FVSUM_1:68
.= D"*(Line(MC@,i)"*"Col(b,j)) by FVSUM_1:73
.= D"*(Col(MC,i)"*"Col(b,j)) by A3,A15,MATRIX_0:59
.= D"*Sum(LaplaceExpL(RLine(A@,i,Col(b,j)),i)) by A15,A14,Th31
.= D"*Det RLine(A@,i,Col(b,j)) by A15,Th25
.= D"*Det (RLine(A@,i,Col(b,j))@) by MATRIXR2:43
.= D"*Det RCol(A,i,Col(b,j)) by Th19;
end;
theorem Th38:
for K be domRing
for A be Matrix of n,K st Det A is unital for x,b be Matrix of K st
width x = n & x * A = b holds x = b * A~ & for i,j st [i,j] in Indices x holds
x*(i,j) = (Det A)" * Det ReplaceLine(A,j,Line(b,i))
proof
let K be domRing;
let A be Matrix of n,K such that
A1: Det A is unital;
A is invertible by A1,Th34;
then A~ is_reverse_of A by MATRIX_6:def 4;
then
A2: A*A~=1.(K,n) by MATRIX_6:def 2;
A3: width A=n by MATRIX_0:24;
let x,b be Matrix of K such that
A4: width x = n and
A5: x * A = b;
A6: len A=n by MATRIX_0:24;
then
A7: width b=n by A4,A5,A3,MATRIX_3:def 4;
set MC=Matrix_of_Cofactor A;
set D=Det A;
A8: len (MC@)=n by MATRIX_0:24;
A9: width (MC@)=n by MATRIX_0:24;
len MC=n by MATRIX_0:24;
then
A10: Seg n=dom MC by FINSEQ_1:def 3;
A11: len (A~)=n by MATRIX_0:24;
x = x* 1.(K,n) by A4,MATRIXR2:67;
hence
A12: x= b * A~ by A4,A5,A11,A6,A3,A2,MATRIX_3:33;
let i,j such that
A13: [i,j] in Indices x;
A14: j in Seg n by A4,A13,ZFMISC_1:87;
then
A15: 1<=j by FINSEQ_1:1;
A16: len Line(b,i)=n by A7,MATRIX_0:def 7;
A17: j<= n by A14,FINSEQ_1:1;
thus x*(i,j) = Line(b,i)"*"Col(A~,j) by A11,A12,A13,A7,MATRIX_3:def 4
.= Line(b,i)"*"Col(D" * MC@,j) by A1,Th35
.= Line(b,i)"*"(D"*Col(MC@,j)) by A9,A15,A17,MATRIXR1:19
.= (D"*Col(MC@,j))"*"Line(b,i) by FVSUM_1:90
.= Sum(D"*mlt(Col(MC@,j),Line(b,i))) by A8,A7,FVSUM_1:69
.= D"*(Col(MC@,j)"*"Line(b,i)) by FVSUM_1:73
.= D"*(Line(MC,j)"*"Line(b,i)) by A14,A10,MATRIX_0:58
.= D"*Sum(LaplaceExpL(RLine(A,j,Line(b,i)),j)) by A14,A16,Th28
.= D"*Det RLine(A,j,Line(b,i)) by A14,Th25;
end;
begin :: Product by a vector
definition
let D be non empty set;
let f be FinSequence of D;
redefine func <*f*> -> Matrix of 1,len f,D; :: redefines <* (FINSEQ_1, definition)
coherence by MATRIX_0:11;
end;
definition
let K;
let M be Matrix of K;
let f be FinSequence of K;
func M * f -> Matrix of K equals
M * (<*f*>@);
coherence;
func f * M -> Matrix of K equals
<*f*> * M;
coherence;
end;
theorem
for K be domRing
for A be Matrix of n,K st Det A is unital for x,b be FinSequence of K st
len x = n & A * x = <*b*>@ holds <*x*>@ = A~ * b & for i st i in Seg n holds
x.i = (Det A)" * Det ReplaceCol(A,i,b)
proof
let K be domRing;
let A be Matrix of n,K such that
A1: Det A is unital;
let x,b be FinSequence of K such that
A2: len x = n and
A3: A * x = <*b*>@;
set X=<*x*>;
len X=1 by MATRIX_0:def 2;
then
A4: len x=width X by MATRIX_0:20;
then
A5: len (X@)=len x by MATRIX_0:def 6;
hence X@ = A~ * b by A1,A2,A3,Th37;
set B=<*b*>;
A6: 1 in Seg 1;
then
A7: Line(X,1)=X.1 by MATRIX_0:52;
len B=1 by MATRIX_0:def 2;
then
A8: 1 in dom B by A6,FINSEQ_1:def 3;
A9: Line(B,1)=B.1 by A6,MATRIX_0:52;
let i such that
A10: i in Seg n;
n>0 by A10;
then width (X@) = len X by A2,A4,MATRIX_0:54
.= 1 by MATRIX_0:def 2;
then Indices (X@)=[:Seg n,Seg 1:] by A2,A5,FINSEQ_1:def 3;
then
A11: [i,1] in Indices (X@) by A10,A6,ZFMISC_1:87;
then [1,i] in Indices X by MATRIX_0:def 6;
then (X@)*(i,1) = X*(1,i) by MATRIX_0:def 6
.= Line(X,1).i by A2,A4,A10,MATRIX_0:def 7
.= x.i by A7;
hence x.i = (Det A)" * Det ReplaceCol(A,i,Col(B@,1)) by A1,A2,A3,A5,A11,Th37
.= (Det A)" * Det ReplaceCol(A,i,Line(B,1)) by A8,MATRIX_0:58
.= (Det A)" * Det ReplaceCol(A,i,b) by A9;
end;
::$N Cramer's Rule
::$L https://en.wikipedia.org/wiki/Cramer's_rule Cramer's Rule
theorem
for K be domRing
for A be Matrix of n,K st Det A is unital for x,b be FinSequence of K st
len x = n & x * A = <*b*> holds <*x*> = b * A~ &
for i st i in Seg n holds x.i = (Det A)" * Det ReplaceLine(A,i,b)
proof
let K be domRing;
let A be Matrix of n,K such that
A1: Det A is unital;
let x,b be FinSequence of K such that
A2: len x = n and
A3: x * A = <*b*>;
set X=<*x*>;
A4: width X=len x by MATRIX_0:23;
hence X = b * A~ by A1,A2,A3,Th38;
A5: [:Seg 1,Seg n:]= Indices X by A2,MATRIX_0:23;
set B=<*b*>;
A6: 1 in Seg 1;
then
A7: Line(X,1)=X. 1 by MATRIX_0:52;
let i such that
A8: i in Seg n;
A9: [1,i] in [:Seg 1,Seg n:] by A8,A6,ZFMISC_1:87;
A10: Line(B,1)=B.1 by A6,MATRIX_0:52;
X*(1,i) = Line(X,1).i by A2,A4,A8,MATRIX_0:def 7
.= x.i by A7;
hence x.i = (Det A)" * Det ReplaceLine(A,i,Line(B,1)) by A1,A2,A3,A4,A9,A5
,Th38
.= (Det A)" * Det ReplaceLine(A,i,b) by A10;
end;
registration
let F be Field;
cluster -> unital for non zero Element of F;
coherence
proof
let a be non zero Element of F;
a <> 0.F;
then a * a" = 1.F by VECTSP_1:def 10;
then a divides 1.F by GCD_1:def 1;
hence a is unital by GCD_1:def 20;
end;
end;
:: Addenda: explicit Field versions of several frequently used theorems
theorem
for K being Field
for i be Nat, M be Matrix of n,K st i in Seg n holds Det M = Sum
LaplaceExpL(M,i) by Th25;
theorem
for K be Field
for M be Matrix of n,K
holds (M is invertible iff Det M is unital) by Th34;
theorem
for K be Field
for M be Matrix of n,K
holds (M is invertible iff Det M <> 0.K)
proof
let K be Field;
let M be Matrix of n,K;
hereby assume M is invertible; then
Det M is unital by Th34; then
Det M divides 1.K by GCD_1:def 20; then
consider y being Element of K such that
A1: 1.K = (Det M)*y by GCD_1:def 1;
Det M <> 0.K
proof
assume Det M = 0.K; then
1.K = (0.K) * y by A1;
hence thesis;
end;
hence Det M <> 0.K;
end;
assume Det M <> 0.K; then
(Det M) * (Det M)" = 1.K by VECTSP_1:def 10; then
Det M divides 1.K by GCD_1:def 1;
hence thesis by Th34,GCD_1:def 20;
end;