:: Determinant of Some Matrices of Field Elements
:: by Yatsuka Nakamura
::
:: Received January 4, 2006
:: Copyright (c) 2006-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, NAT_1, FUNCT_2, FINSEQ_1, RELAT_1, FUNCT_1, TARSKI,
FINSEQ_2, XBOOLE_0, SUBSET_1, XXREAL_0, ARYTM_3, JORDAN3, ORDINAL4,
ARYTM_1, CARD_1, STRUCT_0, INT_1, CARD_3, GROUP_1, VECTSP_1, MATRIX_1,
MATRIX_3, ALGSTR_0, SETWISEO, FINSUB_1, BINOP_1, FINSOP_1, ABIAN,
TREES_1, SUPINF_2, FUNCOP_1, MESFUNC1, ZFMISC_1, QC_LANG1, PARTFUN1,
FINSEQ_5, CLASSES1, RFINSEQ, FUNCSDOM, MATRIX_7, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XXREAL_0, ORDINAL1, NAT_1,
NAT_D, RELAT_1, FUNCT_1, BINOP_1, ZFMISC_1, CARD_1, NUMBERS, VECTSP_1,
FUNCT_2, FUNCOP_1, SETWISEO, PARTFUN1, GROUP_4, FINSUB_1, NEWTON,
FINSOP_1, SETWOP_2, FINSEQ_1, FINSEQ_2, STRUCT_0, ALGSTR_0, MATRIX_1,
MATRIX_3, FINSEQ_6, MATRIX_0, CLASSES1, RFINSEQ, FINSEQ_5, GROUP_1;
constructors SETWISEO, REAL_1, NAT_1, NAT_D, FINSOP_1, NEWTON, RFINSEQ,
FINSEQ_5, ALGSTR_1, GROUP_4, MATRIX_3, FINSEQ_6, CLASSES1, RELSET_1,
BINOP_1, MATRIX_1;
registrations SUBSET_1, FUNCT_1, ORDINAL1, PARTFUN1, FUNCT_2, FINSUB_1,
XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, GROUP_1, VECTSP_1,
MATRIX_1, FVSUM_1, FINSET_1, CARD_1, RELSET_1, FINSEQ_2, MATRIX_0;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions TARSKI, MATRIX_1;
equalities XBOOLE_0, BINOP_1, FINSEQ_1, MATRIX_0, FINSEQ_2, GROUP_4, ALGSTR_0,
RELAT_1;
expansions TARSKI, XBOOLE_0, FINSEQ_1, MATRIX_1;
theorems BINOP_1, RLVECT_1, MATRIX_3, MATRIX_0, GROUP_1, FUNCT_1, FINSEQ_1,
NAT_1, FINSEQ_2, TARSKI, FINSOP_1, FVSUM_1, SETWISEO, FUNCT_2, XBOOLE_0,
GROUP_4, ENUMSET1, ZFMISC_1, FINSEQ_6, XREAL_1, FINSEQ_5, INTEGRA2,
FUNCOP_1, FINSUB_1, XBOOLE_1, RELAT_1, SUBSET_1, RFINSEQ, FINSEQ_3,
XXREAL_0, ORDINAL1, NAT_D, PARTFUN1, XREAL_0, CLASSES1, CARD_1, MATRIX_1;
schemes NAT_1, FUNCT_2, FINSEQ_1;
begin
reserve k,n,i,j for Nat;
theorem Th1:
for f being Permutation of Seg 2 holds f=<*1,2*> or f=<*2,1*>
proof
let f be Permutation of Seg 2;
A1: rng f = Seg 2 by FUNCT_2:def 3;
2 in {1,2} by TARSKI:def 2;
then
A2: f.2 in Seg 2 by A1,FINSEQ_1:2,FUNCT_2:4;
A3: dom f=Seg 2 by FUNCT_2:52;
then reconsider p=f as FinSequence by FINSEQ_1:def 2;
A4: len p= 2 by A3,FINSEQ_1:def 3;
A5: 1 in dom f & 2 in dom f by A3;
1 in {1,2} by TARSKI:def 2;
then
A6: f.1 in Seg 2 by A1,FINSEQ_1:2,FUNCT_2:4;
now
per cases by A6,A2,FINSEQ_1:2,TARSKI:def 2;
case
f.1=1 & f.2=1;
hence contradiction by A5,FUNCT_1:def 4;
end;
case
f.1=1 & f.2=2;
hence thesis by A4,FINSEQ_1:44;
end;
case
f.1=2 & f.2=1;
hence thesis by A4,FINSEQ_1:44;
end;
case
f.1=2 & f.2=2;
hence contradiction by A5,FUNCT_1:def 4;
end;
end;
hence thesis;
end;
theorem Th2:
for f being FinSequence st f=<*1,2*> or f=<*2,1*> holds f is
Permutation of Seg 2
proof
let f be FinSequence;
assume
A1: f=<*1,2*> or f=<*2,1*>;
len (<*1,2*>)=2 & len (<*2,1*>)=2 by FINSEQ_1:44;
then
A2: dom f =Seg 2 by A1,FINSEQ_1:def 3;
rng f c= Seg 2
proof
let y be object;
assume y in rng f;
then ex x being object st x in dom f & y=f.x by FUNCT_1:def 3;
then y=f.1 or y=f.2 by A2,FINSEQ_1:2,TARSKI:def 2;
then y=1 or y=2 or (y=2 or y=1) by A1;
hence thesis;
end;
then reconsider g=f as Function of Seg 2,Seg 2 by A2,FUNCT_2:2;
now
per cases by A1;
case
A3: f=<*1,2*>;
for x1,x2 being object st x1 in dom f & x2 in dom f & f.x1=f.x2
holds x1=x2
proof
let x1,x2 be object;
assume that
A4: x1 in dom f & x2 in dom f and
A5: f.x1=f.x2;
now
per cases by A2,A4,FINSEQ_1:2,TARSKI:def 2;
case
x1=1 & x2=1;
hence thesis;
end;
case
A6: x1=1 & x2=2;
thus contradiction by A3,A5,A6;
end;
case
A7: x1=2 & x2=1;
thus contradiction by A3,A5,A7;
end;
case
x1=2 & x2=2;
hence thesis;
end;
end;
hence thesis;
end;
then
A8: f is one-to-one by FUNCT_1:def 4;
now
let x be object;
assume x in rng f;
then consider z being object such that
A9: z in dom f and
A10: f.z=x by FUNCT_1:def 3;
len f=2 by A3,FINSEQ_1:44;
then dom f=Seg 2 by FINSEQ_1:def 3;
then z=1 or z=2 by A9,FINSEQ_1:2,TARSKI:def 2;
then x =1 or x=2 by A3,A10;
hence x in Seg 2;
end;
then
A11: rng f c= Seg 2;
Seg 2 c= rng f
proof
let z be object;
assume z in Seg 2;
then z=1 or z=2 by FINSEQ_1:2,TARSKI:def 2;
then
A12: z=f.1 or z=f.2 by A3;
1 in dom f & 2 in dom f by A2;
hence thesis by A12,FUNCT_1:def 3;
end;
then rng f = Seg 2 by A11;
then g is onto by FUNCT_2:def 3;
hence thesis by A8;
end;
case
A13: f=<*2,1*>;
for x1,x2 being object st x1 in dom f & x2 in dom f & f.x1=f.x2
holds x1=x2
proof
let x1,x2 be object;
assume that
A14: x1 in dom f & x2 in dom f and
A15: f.x1=f.x2;
now
per cases by A2,A14,FINSEQ_1:2,TARSKI:def 2;
case
x1=1 & x2=1;
hence thesis;
end;
case
A16: x1=1 & x2=2;
thus contradiction by A13,A15,A16;
end;
case
A17: x1=2 & x2=1;
thus contradiction by A13,A15,A17;
end;
case
x1=2 & x2=2;
hence thesis;
end;
end;
hence thesis;
end;
then
A18: f is one-to-one by FUNCT_1:def 4;
now
let x be object;
assume x in rng f;
then consider z being object such that
A19: z in dom f and
A20: f.z=x by FUNCT_1:def 3;
len f=2 by A13,FINSEQ_1:44;
then dom f=Seg 2 by FINSEQ_1:def 3;
then z=1 or z=2 by A19,FINSEQ_1:2,TARSKI:def 2;
then x =2 or x=1 by A13,A20;
hence x in Seg 2;
end;
then
A21: rng f c= Seg 2;
Seg 2 c= rng f
proof
let z be object;
assume z in Seg 2;
then z=1 or z=2 by FINSEQ_1:2,TARSKI:def 2;
then
A22: z=f.2 or z=f.1 by A13;
2 in dom f & 1 in dom f by A2;
hence thesis by A22,FUNCT_1:def 3;
end;
then rng f = Seg 2 by A21;
then g is onto by FUNCT_2:def 3;
hence thesis by A18;
end;
end;
hence thesis;
end;
theorem Th3:
Permutations(2)={<*1,2*>,<*2,1*>}
proof
now
let x be object;
assume
A1: x in {idseq 2,<*2,1*>};
now
per cases by A1,TARSKI:def 2;
case
x=idseq 2;
hence x in Permutations(2) by MATRIX_1:def 16;
end;
case
A2: x=<*2,1*>;
<*2,1*> is Permutation of Seg 2 by Th2;
hence x in Permutations(2) by A2,MATRIX_1:def 16;
end;
end;
hence x in Permutations(2);
end;
then
A3: {idseq 2,<*2,1*>} c=Permutations(2);
now
let p be object;
assume p in Permutations(2);
then reconsider q=p as Permutation of Seg 2 by MATRIX_1:def 16;
q=<*1,2*> or q=<*2,1*> by Th1;
hence p in {idseq 2,<*2,1*>} by FINSEQ_2:52,TARSKI:def 2;
end;
then Permutations(2) c={idseq 2,<*2,1*>};
hence thesis by A3,FINSEQ_2:52;
end;
theorem Th4:
for p being Permutation of Seg 2 st p is being_transposition
holds p = <*2,1*>
proof
let p be Permutation of Seg 2;
assume
A1: p is being_transposition;
now
set p0=<*1,2*>;
assume
A2: p=<*1,2*>;
consider i,j being Nat such that
A3: i in dom p and
A4: j in dom p & i<>j and
A5: p.i=j and
p.j=i and
for k being Nat st k <>i & k<>j & k in dom p holds p.k=k by A1;
len p0=2 by FINSEQ_1:44;
then
A6: dom p ={1,2} by A2,FINSEQ_1:2,def 3;
then
A7: i=1 or i=2 by A3,TARSKI:def 2;
now
per cases by A4,A6,A7,TARSKI:def 2;
case
i=1 & j=2;
hence contradiction by A2,A5;
end;
case
i=2 & j=1;
hence contradiction by A2,A5;
end;
end;
hence contradiction;
end;
hence thesis by Th1;
end;
theorem Th5:
for D being non empty set, f being FinSequence of D, k2 being
Nat st 1<=k2 & k2< len f holds f = mid(f,1,k2)^mid(f,k2+1,len f)
proof
let D be non empty set, f be FinSequence of D, k2 be Nat;
assume
A1: 1<=k2 & k2< len f;
then mid(f,1,len f) = mid(f,1,k2)^mid(f,k2+1,len f) by INTEGRA2:4;
hence thesis by A1,FINSEQ_6:120,XXREAL_0:2;
end;
theorem Th6:
for D being non empty set, f being FinSequence of D st 2<= len f
holds f = (f|(len f-'2))^mid(f,len f-'1,len f)
proof
let D be non empty set, f be FinSequence of D;
assume
A1: 2<= len f;
then
A2: len f-'2=len f-2 by XREAL_1:233;
then
A3: len f-'2+1=len f-1-1+1 .=len f-'1 by A1,XREAL_1:233,XXREAL_0:2;
now
per cases;
case
len f-'2>0;
then
A4: 0+1<=len f-'2 by NAT_1:13;
len f<len f+1 by NAT_1:13;
then len f<len f+1+1 by NAT_1:13;
then len f -2<len f+2-2 by XREAL_1:14;
then f=mid(f,1,len f-'2)^mid(f,len f-'2+1,len f) by A2,A4,Th5;
hence thesis by A3,A4,FINSEQ_6:116;
end;
case
A5: len f-'2=0;
then
A6: mid(f,len f-'2+1,len f)=f by A1,FINSEQ_6:120,XXREAL_0:2;
A7: f|0 is empty;
len f-'2+1=(len f)-2+1 by A1,XREAL_1:233
.=len f-1
.=len f-'1 by A1,XREAL_1:233,XXREAL_0:2;
hence thesis by A5,A6,A7,FINSEQ_1:34;
end;
end;
hence thesis;
end;
theorem Th7:
for D being non empty set, f being FinSequence of D st 1<= len f
holds f = (f|(len f-'1))^mid(f,len f,len f)
proof
let D be non empty set, f be FinSequence of D;
assume
A1: 1<= len f;
then
A2: len f-'1=len f-1 by XREAL_1:233;
now
per cases;
case
len f-'1>0;
then
A3: 0+1<=len f-'1 by NAT_1:13;
len f<len f+1 by NAT_1:13;
then len f -1<len f+1-1 by XREAL_1:14;
then f=mid(f,1,len f-'1)^mid(f,len f-'1+1,len f) by A2,A3,Th5;
hence thesis by A2,A3,FINSEQ_6:116;
end;
case
A4: len f-'1=0;
A5: f|0 is empty;
mid(f,len f-'1+1,len f)=f by A1,A4,FINSEQ_6:120;
hence thesis by A2,A4,A5,FINSEQ_1:34;
end;
end;
hence thesis;
end;
Lm1: <*1,2*> <> <*2,1*> by FINSEQ_1:77;
theorem Th8:
for a being Element of Group_of_Perm 2 st (ex q being Element of
Permutations 2 st q=a & q is being_transposition) holds a = <*2,1*>
proof
let a be Element of Group_of_Perm 2;
given q being Element of Permutations 2 such that
A1: q=a and
A2: q is being_transposition;
the carrier of Group_of_Perm 2 = Permutations 2 by MATRIX_1:def 17;
then reconsider b=a as Permutation of Seg 2 by MATRIX_1:def 16;
ex i,j being Nat st i in dom q & j in dom q & i<>j & q. i=j & q.j=i & for
k being Nat st k <>i & k<>j & k in dom q holds q.k=k by A2;
then b is being_transposition by A1;
hence thesis by Th4;
end;
theorem
for n being Nat,a,b being Element of Group_of_Perm n, pa,pb
being Element of Permutations n st a=pa & b=pb holds a*b=pb*pa by
MATRIX_1:def 17;
theorem Th10:
for a,b being Element of Group_of_Perm 2 st (ex p being Element
of Permutations 2 st p=a & p is being_transposition)& (ex q being Element of
Permutations 2 st q=b & q is being_transposition) holds a*b = <*1,2*>
proof
let a,b be Element of Group_of_Perm 2;
assume that
A1: ex p being Element of Permutations 2 st p=a & p is being_transposition and
A2: ex q being Element of Permutations 2 st q=b & q is being_transposition;
consider p being Element of Permutations 2 such that
A3: p=a and
A4: p is being_transposition by A1;
the carrier of Group_of_Perm 2 =Permutations 2 by MATRIX_1:def 17;
then
A5: a*b = <*1,2*> or a*b = <*2,1*> by Th3,TARSKI:def 2;
reconsider p2=p as FinSequence by A3,A4,Th8;
A6: a= <*2,1*> by A1,Th8;
then len p2=2 by A3,FINSEQ_1:44;
then 1 in Seg len p2;
then
A7: 1 in dom p2 by FINSEQ_1:def 3;
consider q being Element of Permutations 2 such that
A8: q=b and
A9: q is being_transposition by A2;
reconsider q2=q as FinSequence by A8,A9,Th8;
b= <*2,1*> by A2,Th8;
then
A10: q2.2=1 by A8;
A11: a*b=q*p by A3,A8,MATRIX_1:def 17;
p2.1=2 by A6,A3;
then (q*p).1=1 by A10,A7,FUNCT_1:13;
hence thesis by A5,A11;
end;
theorem Th11:
for l being FinSequence of Group_of_Perm 2 st (len l) mod 2=0 &
(for i st i in dom l holds (ex q being Element of Permutations 2 st l.i=q & q
is being_transposition)) holds Product l = <*1,2*>
proof
defpred P[Nat] means for f being FinSequence of Group_of_Perm 2
st len f=2*$1 & (for i st i in dom f holds (ex q being Element of Permutations
2 st f.i=q & q is being_transposition)) holds Product f = <*1,2*>;
let l be FinSequence of Group_of_Perm 2;
assume that
A1: (len l)mod 2=0 and
A2: for i st i in dom l holds ex q being Element of Permutations 2 st l.
i=q & q is being_transposition;
( ex t being Nat st len l = 2 * t + 0 & 0 < 2 ) or 0 = 0 & 2 = 0 by A1,
NAT_D:def 2;
then consider t being Nat such that
A3: len l = 2 * t;
A4: for s being Nat st P[s] holds P[s+1]
proof
let s be Nat;
assume
A5: P[s];
for f being FinSequence of Group_of_Perm 2 st len f=2*(s+1) & (for i
st i in dom f holds (ex q being Element of Permutations 2 st f.i=q & q is
being_transposition)) holds Product f = <*1,2*>
proof
let f be FinSequence of Group_of_Perm 2;
assume that
A6: len f=2*(s+1) and
A7: for i st i in dom f holds ex q being Element of Permutations 2
st f .i=q & q is being_transposition;
A8: len f = 2*s+2 by A6;
then
A9: 2 <= len f by NAT_1:11;
then
A10: len f-'1=len f-1 by XREAL_1:233,XXREAL_0:2;
A11: len f-(len f-'1)+1=len f-(len f-1)+1 by A9,XREAL_1:233,XXREAL_0:2
.=2;
set g=mid(f,len f-'1,len f);
A12: len f-'1<= len f by NAT_D:35;
A13: 1 <= len f by A9,XXREAL_0:2;
then len f in Seg len f;
then len f in dom f by FINSEQ_1:def 3;
then
A14: ex q being Element of Permutations 2 st f.(len f)=q & q is
being_transposition by A7;
reconsider pw2=Product mid(g,len g,len g) as Element of Group_of_Perm 2;
reconsider pw1=Product (g|(len g-'1)) as Element of Group_of_Perm 2;
A15: 1+(len f-'1)-'1=1+(len f-'1)-1 by NAT_1:11,XREAL_1:233
.=len f-'1;
A16: 1+1-1<=len f-1 by A9,XREAL_1:13;
then
A17: 1<=len f-'1 by A9,XREAL_1:233,XXREAL_0:2;
then
A18: len (mid(f,len f-'1,len f)) = len f-'(len f-'1)+1 by A13,A12,FINSEQ_6:118
.=len f-(len f-'1)+1 by NAT_D:35,XREAL_1:233
.=len f-(len f-1)+1 by A9,XREAL_1:233,XXREAL_0:2
.=2;
then len g-'1=len g-1 by XREAL_1:233;
then
A19: (g|(len g-'1)).1=g.1 by A18,FINSEQ_3:112
.=f.(len f-'1) by A16,A12,A11,A15,FINSEQ_6:122;
A20: for i st i in dom (f|(len f-'2)) holds ex q being Element of
Permutations 2 st (f|(len f-'2)).i=q & q is being_transposition
proof
let i;
assume i in dom (f|(len f-'2));
then
A21: i in Seg len (f|(len f-'2)) by FINSEQ_1:def 3;
then
A22: 1<= i by FINSEQ_1:1;
A23: i<= len (f|(len f-'2)) by A21,FINSEQ_1:1;
len (f|(len f-'2)) <= len f by FINSEQ_5:16;
then i<=len f by A23,XXREAL_0:2;
then i in dom f by A22,FINSEQ_3:25;
then
A24: ex q being Element of Permutations 2 st f.i=q & q is
being_transposition by A7;
len (f|(len f-'2))=len f-'2 by FINSEQ_1:59,NAT_D:35;
hence thesis by A23,A24,FINSEQ_3:112;
end;
len (f|(len f-'2))=len f-'2 by FINSEQ_1:59,NAT_D:35
.= 2*s by A8,NAT_D:34;
then Product (f|(len f-'2))=<*1,2*> by A5,A20;
then
A25: 1_Group_of_Perm 2=(Product (f|(len f-'2))) by FINSEQ_2:52,MATRIX_1:15;
f = (f|(len f-'2))^mid(f,len f-'1,len f) by A8,Th6,NAT_1:11;
then
A26: Product f = (Product (f|(len f-'2)))*(Product (mid(f,len f-'1,len f
))) by GROUP_4:5
.= (Product (mid(f,len f-'1,len f))) by A25,GROUP_1:def 4;
2<=2+(len f-'1) by NAT_1:11;
then
A27: 2+(len f-'1)-'1=2+(len f-'1)-1 by XREAL_1:233,XXREAL_0:2
.=len f by A10;
A28: len f-(len f-'1)+1=len f-(len f-1)+1 by A9,XREAL_1:233,XXREAL_0:2
.= 1+1;
A29: 1+ len g-'1=1+len g-1 by NAT_1:11,XREAL_1:233;
A30: len (g|(len g-'1)) = len g-'1 by FINSEQ_1:59,NAT_D:35
.= len g-1 by A18,XREAL_1:233
.=1 by A18;
then 1 in Seg len (g|(len g-'1));
then 1 in dom (g|(len g-'1)) by FINSEQ_1:def 3;
then
rng (g|(len g-'1)) c= the carrier of Group_of_Perm 2 & (g|(len g-'1
)).1 in rng (g|(len g-'1)) by FINSEQ_1:def 4,FUNCT_1:def 3;
then reconsider r=(g|(len g-'1)).1 as Element of Group_of_Perm 2;
A31: pw1 = Product (<* r *>) by A30,FINSEQ_1:40
.=f.(len f-'1) by A19,FINSOP_1:11;
1<=len g-len g+1;
then
A32: (mid(g,len g,len g)).1=g.(1+len g-'1) by A18,FINSEQ_6:122
.=f.(len f) by A16,A12,A18,A28,A29,A27,FINSEQ_6:122;
A33: len mid(g,len g,len g)=len g-'len g+1 by A18,FINSEQ_6:118
.= 0+1 by XREAL_1:232
.=1;
then 1 in Seg len (mid(g,len g,len g));
then 1 in dom (mid(g,len g,len g)) by FINSEQ_1:def 3;
then
rng (mid(g,len g,len g)) c= the carrier of Group_of_Perm 2 & (mid(g
,len g, len g)).1 in rng (mid(g,len g,len g)) by FINSEQ_1:def 4,FUNCT_1:def 3;
then reconsider s=(mid(g,len g,len g)).1 as Element of Group_of_Perm 2;
A34: pw2 = Product (<* s *>) by A33,FINSEQ_1:40
.=f.len f by A32,FINSOP_1:11;
len f-'1 in Seg len f by A17,A12;
then len f-'1 in dom f by FINSEQ_1:def 3;
then
A35: ex q being Element of Permutations 2 st f.(len f-'1)=q & q is
being_transposition by A7;
g= (g|(len g-'1))^mid(g,len g,len g) by A18,Th7;
then Product g=(Product ((g|(len g-'1))))*(Product mid(g,len g,len g))
by GROUP_4:5
.= <*1,2*> by A35,A14,A31,A34,Th10;
hence thesis by A26;
end;
hence thesis;
end;
for f being FinSequence of Group_of_Perm 2 st len f=2*0 & (for i st i in
dom f holds (ex q being Element of Permutations 2 st f.i=q & q is
being_transposition)) holds Product f = <*1,2*>
proof
set G=Group_of_Perm 2;
let f be FinSequence of Group_of_Perm 2;
assume that
A36: len f=2*0 and
for i st i in dom f holds ex q being Element of Permutations 2 st f. i
=q & q is being_transposition;
A37: 1_G= <*1,2*> by FINSEQ_2:52,MATRIX_1:15;
f=<*> (the carrier of G) by A36;
hence thesis by A37,GROUP_4:8;
end;
then
A38: P[0];
A39: for s being Nat holds P[s] from NAT_1:sch 2(A38,A4);
reconsider t as Nat;
len l = 2 * t by A3;
hence thesis by A2,A39;
end;
theorem
for K being Field, M being Matrix of 2,K holds Det M = (M*(1,1))*(M*(2
,2))-(M*(1,2))*(M*(2,1))
proof
reconsider s1=<*1,2*>, s2=<*2,1*> as Permutation of Seg 2 by Th2;
let K be Field, M be Matrix of 2,K;
A1: now
A2: s1.1=1;
assume s1=s2;
hence contradiction by A2,FINSEQ_1:44;
end;
set D0={s1,s2};
reconsider l0=<*>D0 as FinSequence of Group_of_Perm(2) by Th3,MATRIX_1:def 17
;
set X=Permutations 2;
reconsider p1 = s1, p2 = s2 as Element of Permutations(2) by MATRIX_1:def 16;
set Y=the carrier of K;
set f=Path_product M;
set F=the addF of K;
set di=(the multF of K) $$ (Path_matrix(p1,M));
set B=In (Permutations 2,Fin Permutations 2);
Permutations 2 in Fin Permutations 2 by FINSUB_1:def 5; then
A3: B=Permutations 2 by SUBSET_1:def 8;
Det M=(the addF of K) $$ (In(Permutations 2,Fin Permutations 2)
,Path_product M) by MATRIX_3:def 9;
then consider G being Function of Fin X, Y such that
A4: Det M = G.B and
for e being Element of Y st e is_a_unity_wrt F holds G.{} = e and
A5: for x being Element of X holds G.{x} = f.x and
A6: for B9 being Element of Fin X st B9 c= B & B9 <> {} for x being
Element of X st x in B \ B9 holds G.(B9 \/ {x}) = F.(G.B9,f.x) by A3,
SETWISEO:def 3;
A7: G.{p1} = f.p1 by A5;
A8: G.B = (the addF of K).(f.p1,f.p2)
proof
reconsider B9={.p1.} as Element of Fin X;
A9: B9 c= B
proof
let y be object;
assume y in B9;
then y=p1 by TARSKI:def 1;
hence thesis by A3;
end;
B\B9 ={s2} by A1,A3,Th3,ZFMISC_1:17;
then s2 in B\B9 by TARSKI:def 1;
then G.(B9 \/ {p2}) = F.(G.B9,f.p2) by A6,A9;
hence thesis by A3,A7,Th3,ENUMSET1:1;
end;
set dj=(the multF of K) $$ (Path_matrix(p2,M));
A10: p1.2 = 2;
A11: p2.2 = 1;
A12: len Path_matrix(p1,M) = 2 by MATRIX_3:def 7;
then consider f3 being sequence of the carrier of K such that
A13: f3.1 = (Path_matrix(p1,M)).1 and
A14: for n being Nat st 0 <> n & n < 2 holds f3.(n + 1) = (
the multF of K).(f3.n,(Path_matrix(p1,M)).(n + 1)) and
A15: di = f3.2 by FINSOP_1:def 1;
A16: 1 in Seg 2;
then
A17: 1 in dom Path_matrix(p1,M) by A12,FINSEQ_1:def 3;
A18: 2 in Seg 2;
then 2 in dom Path_matrix(p1,M) by A12,FINSEQ_1:def 3;
then
A19: p1.1 = 1 & Path_matrix(p1,M).2=M*(2,2) by A10,MATRIX_3:def 7;
A20: len Path_matrix(p2,M) = 2 by MATRIX_3:def 7;
then consider f4 being sequence of the carrier of K such that
A21: f4.1 = (Path_matrix(p2,M)).1 and
A22: for n being Nat st 0 <> n & n < 2 holds f4.(n + 1) = (
the multF of K).(f4.n,(Path_matrix(p2,M)).(n + 1)) and
A23: dj = f4.2 by FINSOP_1:def 1;
A24: 1 in dom Path_matrix(p2,M) by A20,A16,FINSEQ_1:def 3;
2 in dom Path_matrix(p2,M) by A20,A18,FINSEQ_1:def 3;
then
A25: p2.1 = 2 & Path_matrix(p2,M).2=M*(2,1) by A11,MATRIX_3:def 7;
A26: f4.(1+1)=(the multF of K).(f4.1,(Path_matrix(p2,M)).(1+1)) by A22
.=(M*(1,2))*(M*(2,1)) by A24,A25,A21,MATRIX_3:def 7;
A27: len Permutations 2 = 2 by MATRIX_1:9;
not ex l be FinSequence of Group_of_Perm 2 st (len l)mod 2=0 & s2=
Product l & for i st i in dom l ex q being Element of Permutations 2 st l.i=q &
q is being_transposition by Lm1,Th11;
then f.p2 = -((the multF of K) "**" (Path_matrix(p2,M)),p2) & p2 is odd by
A27,MATRIX_3:def 8;
then
A28: f.p2 = - dj by MATRIX_1:def 20;
A29: Product l0=Product <*> (the carrier of Group_of_Perm 2)
.= 1_(Group_of_Perm(2)) by GROUP_4:8
.= p1 by FINSEQ_2:52,MATRIX_1:15;
A30: 0 mod 2=0 by NAT_D:26;
ex l be FinSequence of Group_of_Perm 2 st (len l)mod 2=0 & s1=Product l
& for i st i in dom l ex q being Element of Permutations 2 st l.i=q & q is
being_transposition
proof
take l0;
thus (len l0)mod 2=0 & s1=Product l0 by A30,A29;
let i;
thus thesis;
end;
then
A31: f.p1 = -((the multF of K) "**" (Path_matrix(p1,M)),p1) & p1 is even by A27
,MATRIX_3:def 8;
f3.(1+1)=(the multF of K).(f3.1,(Path_matrix(p1,M)).(1+1)) by A14
.=(M*(1,1))*(M*(2,2)) by A17,A19,A13,MATRIX_3:def 7;
hence thesis by A4,A8,A15,A23,A26,A31,A28,MATRIX_1:def 20;
end;
theorem Th13:
for K being Ring, n,m being Nat holds
len (0.(K,n,m))=n & dom (0.(K,n,m))=Seg n
proof
let K be Ring, n,m be Nat;
len (n |-> (m |-> 0.K))=n by CARD_1:def 7;
hence len (0.(K,n,m)) =n by MATRIX_3:def 1;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th14:
for K being Ring, n being Nat, p being Element of Permutations n
for i being Nat st i in Seg n holds p.i in Seg n
proof
let K be Ring, n be Nat, p be Element of Permutations(n),i be Nat;
p is Permutation of Seg n by MATRIX_1:def 16;
hence thesis by FUNCT_2:5;
end;
theorem
for K being Ring, n being Nat st n>=1 holds Det (0.(K,n,n)
) = 0.K
proof
let K be Ring, n be Nat;
set B=In(Permutations n,Fin Permutations n);
set f=Path_product(0.(K,n,n));
set F=the addF of K;
set Y=the carrier of K;
set X=Permutations n;
reconsider G0= Fin X --> 0.K as Function of Fin X, Y;
A1: G0.B=0.K by FUNCOP_1:7;
A2: for e being Element of Y st e is_a_unity_wrt F holds G0.({}) = e
proof
let e be Element of Y;
0.K is_a_unity_wrt F by FVSUM_1:6;
then
A3: F.(0.K,e)=e by BINOP_1:3;
assume e is_a_unity_wrt F;
then F.(0.K,e)=0.K by BINOP_1:3;
hence thesis by A3,FINSUB_1:7,FUNCOP_1:7;
end;
assume
A4: n>=1;
A5: for x being object st x in dom (Path_product(0.(K,n,n))) holds (
Path_product(0.(K,n,n))).x=(Permutations(n) --> 0.K).x
proof
let x be object;
assume x in dom (Path_product(0.(K,n,n)));
for p being Element of Permutations(n) holds (Permutations(n) --> 0.K)
.p = -((the multF of K) $$ Path_matrix(p,(0.(K,n,n))),p)
proof
defpred P[Nat] means (the multF of K) $$ ( ($1+1) |-> 0.K)=0.
K;
let p be Element of Permutations(n);
A6: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
A7: (k+1+1) |-> 0.K = ((k+1) |-> 0.K) ^ <* 0.K *> by FINSEQ_2:60;
assume P[k];
then (the multF of K) $$ ( (k+1+1) |-> 0.K) = (0.K)*(0.K) by A7,
FINSOP_1:4
.= 0.K;
hence thesis;
end;
(1 |-> 0.K)= <* 0.K *> by FINSEQ_2:59;
then
A8: P[0] by FINSOP_1:11;
A9: for k being Nat holds P[k] from NAT_1:sch 2(A8,A6);
A10: now
per cases;
case
p is even;
hence -(0.K,p)=(0.K) by MATRIX_1:def 20;
end;
case
not p is even;
then -(0.K,p)= -(0.K) by MATRIX_1:def 20
.=0.K by RLVECT_1:12;
hence -(0.K,p)=(0.K);
end;
end;
A11: for i,j st i in dom (n |-> 0.K) & j=p.i holds (n |-> 0.K).i=(0.(K,n,
n))*(i,j)
proof
let i,j;
assume that
A12: i in dom (n |-> 0.K) and
A13: j=p.i;
A14: i in Seg n by A12,FUNCOP_1:13;
then j in Seg n by A13,Th14;
then
A15: j in Seg width (0.(K,n,n)) by A4,MATRIX_0:23;
i in dom (0.(K,n,n)) by A14,Th13;
then
A16: [i,j] in Indices (0.(K,n,n)) by A15,ZFMISC_1:def 2;
(n |-> 0.K).i=0.K by A14,FUNCOP_1:7;
hence thesis by A16,MATRIX_3:1;
end;
len (n |-> 0.K)=n by CARD_1:def 7;
then
A17: Path_matrix(p,(0.(K,n,n)))=(n |-> 0.K) by A11,MATRIX_3:def 7;
n-'1=n-1 by A4,XREAL_1:233;
then
A18: n-'1+1=n;
(Permutations(n) --> 0.K).p = 0.K by FUNCOP_1:7;
hence thesis by A17,A9,A18,A10;
end;
hence thesis by MATRIX_3:def 8;
end;
dom (Permutations(n) --> 0.K)=Permutations(n) by FUNCOP_1:13;
then dom (Path_product(0.(K,n,n)))=dom (Permutations(n) --> 0.K) by
FUNCT_2:def 1;
then
A19: Path_product(0.(K,n,n))=Permutations(n) --> 0.K by A5,FUNCT_1:2;
A20: for x being Element of X holds G0.({x}) = f.x
proof
let x be Element of X;
G0.({.x.})=0.K by FUNCOP_1:7;
hence thesis by A19,FUNCOP_1:7;
end;
A21: for B9 being Element of Fin X st B9 c= B & B9 <> {} for x being Element
of X st x in B\B9 holds G0.(B9 \/ {x}) = F.(G0.B9,f.x)
proof
let B9 be Element of Fin X;
assume that
B9 c= B and
B9 <> {};
thus for x being Element of X st x in B\B9 holds G0.(B9 \/ {x}) = F.(G0.B9
,f.x)
proof
let x be Element of X;
assume x in B\B9;
A22: G0.(B9 \/ {.x.})=0.K & G0.B9=0.K by FUNCOP_1:7;
f.x= 0.K & 0.K is_a_unity_wrt F by A19,FUNCOP_1:7,FVSUM_1:6;
hence thesis by A22,BINOP_1:3;
end;
end;
X in Fin X by FINSUB_1:def 5; then
B = X by SUBSET_1:def 8; then
B <> {} or F is having_a_unity;
then
(the addF of K) $$ (In(Permutations(n),Fin Permutations n),
Path_product(0.(K,n,n)))=
0.K by A1,A2,A20,A21,SETWISEO:def 3;
hence thesis by MATRIX_3:def 9;
end;
definition
let x be object; let y be set; let a,b be object;
func IFIN(x,y,a,b) -> object equals
:Def1:
a if x in y otherwise b;
correctness;
end;
theorem
for K being Ring, n being Nat st n>=1 holds Det (1.(K,n)) = 1_K
proof
let K be Ring, n be Nat;
assume
A1: n>=1;
deffunc F2(object) = IFEQ(idseq n,$1,1_K,0.K);
set X=Permutations(n);
set Y=the carrier of K;
A2: for x being object st x in X holds F2(x) in Y;
ex f2 being Function of X,Y st
for x being object st x in X holds f2.x =
F2(x) from FUNCT_2:sch 2(A2);
then consider f2 being Function of X,Y such that
A3: for x being object st x in X holds f2.x = F2(x);
A4: id (Seg n) is even by MATRIX_1:16;
A5: for x being object st x in dom (Path_product(1.(K,n)))
holds (Path_product(1.(K,n))).x=f2.x
proof
let x be object;
assume x in dom (Path_product(1.(K,n)));
for p being Element of Permutations(n) holds f2.p = -((the multF of K
) $$ Path_matrix(p,(1.(K,n))),p)
proof
defpred P[Nat] means (the multF of K) $$ ( ($1+1) |-> 1_K)=
1_K;
let p be Element of Permutations(n);
A6: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
A7: (k+1+1) |-> 1_K = ((k+1) |-> 1_K) ^ <* 1_K *> by FINSEQ_2:60;
assume P[k];
then (the multF of K) $$ ( (k+1+1) |-> 1_K) = (1_K)*(1_K) by A7,
FINSOP_1:4
.= 1_K;
hence thesis;
end;
A8: now
per cases;
case
p is even;
hence -(0.K,p)=(0.K) by MATRIX_1:def 20;
end;
case
not p is even;
then -(0.K,p)= -(0.K) by MATRIX_1:def 20
.=0.K by RLVECT_1:12;
hence -(0.K,p)=0.K;
end;
end;
n-'1=n-1 by A1,XREAL_1:233;
then
A9: n-'1+1=n;
(1 |-> 1_K)= <* 1_K *> by FINSEQ_2:59;
then
A10: P[0] by FINSOP_1:11;
for k being Nat holds P[k] from NAT_1:sch 2(A10,A6);
then
A11: len (n |-> 1_K)=n & (the multF of K) $$ (n |-> 1_K)=1_K by A9,
CARD_1:def 7;
now
per cases;
case
A12: p=idseq n;
A13: for i,j st i in dom (n |-> 1_K) & j=p.i holds (n |-> 1_K).i=(1.
(K,n))*(i,j)
proof
A14: Indices (1.(K,n))=[: Seg n,Seg n:] by A1,MATRIX_0:23;
let i,j;
assume that
A15: i in dom (n |-> 1_K) and
A16: j=p.i;
A17: i in Seg n by A15,FUNCOP_1:13;
then j in Seg n by A16,Th14;
then
A18: [i,j] in Indices (1.(K,n)) by A17,A14,ZFMISC_1:def 2;
(n |-> 1_K).i=1_K & p.i=i by A12,A17,FUNCOP_1:7,FUNCT_1:17;
hence thesis by A16,A18,MATRIX_1:def 3;
end;
len Permutations n = n by MATRIX_1:9;
then
A19: -((the multF of K) $$ Path_matrix(p,(1.(K,n))),p) = (the multF
of K) $$ Path_matrix(p,(1.(K,n))) by A4,A12,MATRIX_1:def 20;
f2.p=F2(p) by A3
.= 1_K by A12,FUNCOP_1:def 8;
hence thesis by A11,A19,A13,MATRIX_3:def 7;
end;
case
A20: p<>idseq n;
reconsider A=NAT as non empty set;
defpred P3[Nat] means $1 < n implies ex p3 being
FinSequence of K st len p3=$1+1 & p3.1=(Path_matrix(p,(1.(K,n)))).1 & (for n3
being Nat st 0 <> n3 & n3 < $1+1 & n3<n holds p3.(n3 + 1) = (the
multF of K). (p3.n3,(Path_matrix(p,(1.(K,n)))).(n3 + 1)));
A21: rng ((Path_matrix(p,(1.(K,n))))) c= the carrier of K by
FINSEQ_1:def 4;
A22: len (Path_matrix(p,(1.(K,n))))=n by MATRIX_3:def 7;
then 1 in Seg len (Path_matrix(p,(1.(K,n)))) by A1;
then 1 in dom (Path_matrix(p,(1.(K,n)))) by FINSEQ_1:def 3;
then
(Path_matrix(p,(1.(K,n)))).1 in rng ((Path_matrix(p,( 1.(K,n) )
))) by FUNCT_1:def 3;
then reconsider d=(Path_matrix(p,(1.(K,n)))).1 as Element of K by A21
;
reconsider q3=<* d *> as FinSequence of K;
A23: for n3 being Nat st 0 <> n3 & n3 < 0+1 & n3< n holds
q3.(n3 + 1) = (the multF of K). (q3.n3,(Path_matrix(p,(1.(K,n)))).(n3 + 1)) by
NAT_1:13;
A24: dom p = Seg len Permutations n by FUNCT_2:52;
then
A25: dom p = Seg n by MATRIX_1:9;
then dom p = dom idseq n by RELAT_1:45;
then consider i0 being object such that
A26: i0 in dom p and
A27: p.i0 <> (idseq n).i0 by A20,FUNCT_1:2;
reconsider i0 as Element of NAT by A24,A26;
A28: p.i0<>i0 by A25,A26,A27,FUNCT_1:18;
A29: for k being Nat st P3[k] holds P3[k+1]
proof
let k be Nat;
assume
A30: P3[k];
now
per cases;
case
A31: k+1<n;
then consider p3 being FinSequence of K such that
A32: len p3=k+1 and
A33: p3.1=(Path_matrix(p,(1.(K,n)))).1 and
A34: for n3 being Nat st 0 <> n3 & n3 < k+1 &
n3<n holds p3.( n3 + 1) = (the multF of K). (p3.n3,(Path_matrix(p,(1.(K,n)))).(
n3 + 1)) by A30,NAT_1:12;
defpred P6[object,object] means
($1 in Seg (k+1) implies $2=p3.$1)&
(not $1 in Seg (k+1) implies $2=0.K);
A35: for x being object st x in NAT ex y being object st y in the
carrier of K & P6[x,y]
proof
let x be object;
assume x in NAT;
now
per cases;
case
A36: x in Seg (k+1);
then reconsider nx=x as Nat;
nx in dom p3 by A32,A36,FINSEQ_1:def 3;
then
A37: p3.nx in rng p3 by FUNCT_1:def 3;
rng p3 c= the carrier of K by FINSEQ_1:def 4;
then reconsider s=p3.nx as Element of K by A37;
x in Seg (k+1) implies s=p3.x;
hence thesis by A36;
end;
case
not x in Seg (k+1);
hence thesis;
end;
end;
hence thesis;
end;
ex f6 being sequence of the carrier of K st
for x being object st x in NAT holds P6[x,f6.x] from FUNCT_2:sch 1(A35);
then consider
f6 being sequence of the carrier of K such that
A38: for x being object st x in NAT holds P6[x,f6.x];
1<=k+1+1 & k+1+1 <=n by A31,NAT_1:12,13;
then k+1+1 in Seg len (Path_matrix(p,(1.(K,n)))) by A22;
then k+1+1 in dom (Path_matrix(p,(1.(K,n)))) by FINSEQ_1:def 3;
then rng ((Path_matrix(p,(1.(K,n))))) c= the carrier of K & (
Path_matrix(p,(1.(K, n)))).(k + 1+1) in rng (Path_matrix(p,(1.(K,n)))) by
FINSEQ_1:def 4,FUNCT_1:def 3;
then [f6.(k+1),(Path_matrix(p,(1.(K,n)))).(k + 1+1)] in [:the
carrier of K, the carrier of K:] by ZFMISC_1:def 2;
then reconsider
e=(the multF of K). (f6.(k+1),(Path_matrix(p,(1.(K,
n)))).(k + 1+1)) as Element of K by FUNCT_2:5;
reconsider q3=p3^<* e *> as FinSequence of K;
A39: len q3=(len p3) + len (<*e*>) by FINSEQ_1:22
.=k+1+1 by A32,FINSEQ_1:40;
A40: for n3 being Nat st 0 <> n3 & n3 < k+1+1 & n3<
n holds q3.(n3 + 1) = (the multF of K). (q3.n3,(Path_matrix(p,(1.(K,n)))).(n3 +
1))
proof
let n3 be Nat;
assume that
A41: 0 <> n3 and
A42: n3 < k+1+1 and
A43: n3<n;
now
per cases;
case
A44: n3<k+1;
then 1<=n3+1 & n3+1<=k+1 by NAT_1:12,13;
then n3+1 in Seg len p3 by A32;
then n3+1 in dom p3 by FINSEQ_1:def 3;
then
A45: p3.(n3+1)=q3.(n3+1) by FINSEQ_1:def 7;
0+1<=n3 by A41,NAT_1:13;
then n3 in Seg len p3 by A32,A44;
then
A46: n3 in dom p3 by FINSEQ_1:def 3;
p3.(n3 + 1) = (the multF of K) . (p3.n3,(
Path_matrix(p,(1.(K,n)))).(n3 + 1)) by A34,A41,A43,A44;
hence thesis by A45,A46,FINSEQ_1:def 7;
end;
case
A47: n3>=k+1;
A48: n3+1<=k+1+1 by A42,NAT_1:13;
A49: n3+1>k+1 by A47,NAT_1:13;
then n3+1>=k+1+1 by NAT_1:13;
then
A50: n3+1=k+1+1 by A48,XXREAL_0:1;
1<=k+1 by NAT_1:12;
then
A51: k+1 in Seg (k+1);
then k+1 in dom p3 by A32,FINSEQ_1:def 3;
then
A52: q3.(k+1)=p3.(k+1) by FINSEQ_1:def 7;
(q3).(n3+1) = (<*e*>).(n3+1 - (k+1)) by A32,A39,A49,A48,
FINSEQ_1:24
.= e by A50;
hence thesis by A38,A50,A51,A52;
end;
end;
hence thesis;
end;
1<=k+1 by NAT_1:12;
then 1 in Seg len p3 by A32;
then 1 in dom p3 by FINSEQ_1:def 3;
then q3.1=(Path_matrix(p,(1.(K,n)))).1 by A33,FINSEQ_1:def 7;
hence thesis by A39,A40;
end;
case
k+1>=n;
hence thesis;
end;
end;
hence thesis;
end;
n<n+1 by NAT_1:13;
then
A53: n-1<n+1-1 by XREAL_1:14;
A54: f2.p=F2(p) by A3
.= 0.K by A20,FUNCOP_1:def 8;
A55: n-1=n-'1 by A1,XREAL_1:233;
len q3=1 & q3.1=(Path_matrix(p,(1.(K,n)))).1 by FINSEQ_1:40;
then
A56: P3[0] by A23;
for k being Nat holds P3[k] from NAT_1:sch 2(A56,
A29);
then consider p3 being FinSequence of K such that
A57: len p3=n-'1+1 and
A58: p3.1=(Path_matrix(p,(1.(K,n)))).1 and
A59: for n3 being Nat st 0 <> n3 & n3 < n-'1+1 & n3<
n holds p3.(n3 + 1) = (the multF of K). (p3.n3,(Path_matrix(p,(1.(K,n)))).(n3 +
1)) by A55,A53;
defpred P[set,set] means ($1 in Seg n implies $2=p3.$1)& (not $1 in
Seg n implies $2=0.K);
A60: for x3 being Element of A ex y3 being Element of K st P[x3,y3]
proof
let x3 be Element of A;
now
per cases;
case
A61: x3 in Seg n;
then x3 in dom p3 by A55,A57,FINSEQ_1:def 3;
then rng p3 c= the carrier of K & p3.x3 in rng p3 by
FINSEQ_1:def 4,FUNCT_1:def 3;
hence thesis by A61;
end;
case
not x3 in Seg n;
hence thesis;
end;
end;
hence thesis;
end;
ex f4 being Function of A,the carrier of K st for x2 being
Element of A holds P[x2,f4.x2] from FUNCT_2:sch 3(A60);
then consider f4 being sequence of the carrier of K such that
A62: for x4 being Element of NAT holds (x4 in Seg n implies f4.
x4=p3.x4)& (not x4 in Seg n implies f4.x4=0.K);
p is Permutation of Seg n by MATRIX_1:def 16;
then
A63: p.i0 in Seg n by A25,A26,FUNCT_2:5;
then reconsider j0=p.i0 as Element of NAT;
Indices (1.(K,n))=[: Seg n,Seg n:] by A1,MATRIX_0:23;
then
A64: [i0,j0] in Indices (1.(K,n)) by A25,A26,A63,ZFMISC_1:def 2;
i0 <= n by A25,A26,FINSEQ_1:1;
then
A65: n-'i0 =n-i0 by XREAL_1:233;
i0 in dom (Path_matrix(p,(1.(K,n)))) by A25,A26,A22,FINSEQ_1:def 3;
then
A66: (Path_matrix(p,(1.(K,n)))).i0=(1.(K,n))*(i0,j0) by MATRIX_3:def 7;
defpred P5[Nat] means f4.(i0+$1)=0.K;
A67: 0<i0 by A24,A26,FINSEQ_1:1;
A68: for k being Nat st P5[k] holds P5[k+1]
proof
let k be Nat;
A69: 1<=1+(i0+k) by NAT_1:12;
assume
A70: P5[k];
now
per cases;
case
A71: i0+k+1<=n;
1<=1+(i0+k) by NAT_1:12;
then i0+k+1 in Seg len (Path_matrix(p,(1.(K,n)))) by A22,A71;
then i0+k+1 in dom (Path_matrix(p,(1.(K,n)))) by FINSEQ_1:def 3
;
then
A72: (Path_matrix(p,(1.(K,n)))).(i0+k+1) in rng (Path_matrix(
p,(1.(K,n)))) by FUNCT_1:def 3;
rng (Path_matrix(p,(1.(K,n)))) c= the carrier of K by
FINSEQ_1:def 4;
then reconsider
b=(Path_matrix(p,(1.(K,n)))).(i0+k+1) as Element of
K by A72;
A73: i0+k<n by A71,NAT_1:13;
0+1<=i0+k by A67,NAT_1:13;
then
A74: i0+k in Seg n by A73;
i0+k+1 in Seg n by A69,A71;
then f4.(i0+k+1)=p3.(i0+k+1) by A62
.=(the multF of K). (p3.(i0+k),(Path_matrix(p,(1.(K,n)))).
(i0+k+1)) by A55,A59,A67,A73
.= (0.K)*(b) by A62,A70,A74
.= 0.K;
hence thesis;
end;
case
i0+k+1>n;
then not i0+(k+1) in Seg n by FINSEQ_1:1;
hence thesis by A62;
end;
end;
hence thesis;
end;
1 in Seg n by A1;
then
A75: f4.1=(Path_matrix(p,(1.(K,n)))).1 by A58,A62;
A76: for n3 being Nat st 0 <> n3 & n3 < len (Path_matrix
(p,(1.(K,n)))) holds f4.(n3 + 1) = (the multF of K). (f4.n3,(Path_matrix(p,(1.(
K,n)))).(n3 + 1))
proof
let n3 be Nat;
assume that
A77: 0 <> n3 and
A78: n3 < len (Path_matrix(p,(1.(K,n))));
A79: n3+1<=len (Path_matrix(p,(1.(K,n)))) by A78,NAT_1:13;
A80: 0+1<=n3 by A77,NAT_1:13;
then
A81: n3 in Seg n by A22,A78;
1<n3+1 by A80,NAT_1:13;
then n3+1 in Seg n by A22,A79;
then
A82: f4.(n3+1)=p3.(n3+1) by A62;
p3.(n3 + 1) = (the multF of K). (p3.n3,(Path_matrix(p,(1.(K,
n)))).(n3 + 1)) by A22,A55,A59,A77,A78;
hence thesis by A62,A82,A81;
end;
A83: 1 <= i0 by A24,A26,FINSEQ_1:1;
now
per cases;
case
i0<=1;
then i0=1 by A83,XXREAL_0:1;
hence P5[0] by A28,A66,A64,A75,MATRIX_1:def 3;
end;
case
A84: i0>1;
reconsider a=f4.(i0-'1) as Element of K;
i0<i0+1 by NAT_1:13;
then
A85: i0-1<i0+1-1 by XREAL_1:14;
i0 <= n by A25,A26,FINSEQ_1:1;
then
A86: i0-1<len (Path_matrix(p,(1.(K,n)))) by A22,A85,XXREAL_0:2;
i0-'1=i0-1 by A84,XREAL_1:233;
then
A87: i0-'1+1=i0;
i0-1> 1-1 by A84,XREAL_1:14;
then f4.(i0) = (the multF of K). (f4.(i0-'1),(Path_matrix(p,(1.
(K,n)))).(i0)) by A76,A86,A87
.= a*(0.K) by A28,A66,A64,MATRIX_1:def 3
.= 0.K;
hence P5[0];
end;
end;
then
A88: P5[0];
for k being Nat holds P5[k] from NAT_1:sch 2(A88,
A68);
then P5[n-'i0];
then f4.(i0+(n-'i0))=0.K;
hence thesis by A1,A8,A54,A22,A75,A76,A65,FINSOP_1:2;
end;
end;
hence thesis;
end;
hence thesis by MATRIX_3:def 8;
end;
deffunc F3(set) = IFIN(idseq n,$1,1_K,0.K);
:: dla rodzin zbir? ??? !!!
set F=(the addF of K);
set f=Path_product(1.(K,n));
set B=In(Permutations(n),Fin Permutations n);
A89: for x being set st x in Fin X holds F3(x) in Y
proof
let x be set;
assume x in Fin X;
now
per cases;
case
idseq n in x;
then F3(x)=1_K by Def1;
hence thesis;
end;
case
not idseq n in x;
then F3(x)=0.K by Def1;
hence thesis;
end;
end;
hence thesis;
end;
ex f2 being Function of Fin X,Y st
for x being set st x in Fin X holds
f2.x = F3(x) from FUNCT_2:sch 11(A89);
then consider G0 being Function of Fin X,Y such that
A90: for x being set st x in Fin X holds G0.x = F3(x);
dom (f2)=Permutations(n) by FUNCT_2:def 1;
then
A91: dom (Path_product(1.(K,n)))=dom f2 by FUNCT_2:def 1;
then
A92: Path_product(1.(K,n))=f2 by A5,FUNCT_1:2;
A93: for B9 being Element of Fin X st B9 c= B & B9 <> {} for x being
Element of X st x in B\B9 holds G0.(B9 \/ {x}) = F.(G0.B9,f.x)
proof
let B9 be Element of Fin X;
assume that
B9 c= B and
B9 <> {};
thus for x being Element of X st x in B\B9 holds G0.(B9 \/ {x}) = F.(G0.B9
,f.x)
proof
let x be Element of X;
assume
A94: x in B\B9;
A95: now
assume
A96: not idseq n in B9 \/ {x};
thus G0.(B9 \/ {x})=IFIN(idseq n,B9 \/ {.x.},1_K,0.K) by A90
.=0.K by A96,Def1;
end;
A97: 0.K is_a_unity_wrt F by FVSUM_1:6;
A98: now
assume
A99: not idseq n in B9;
thus G0.(B9)=IFIN(idseq n,B9,1_K,0.K) by A90
.=0.K by A99,Def1;
end;
A100: now
assume
A101: not idseq n in B9 \/ {x};
then not idseq n in {x} by XBOOLE_0:def 3;
then
A102: not idseq n=x by TARSKI:def 1;
f.x=F2(x) by A3,A92
.=0.K by A102,FUNCOP_1:def 8;
hence F.(G0.B9,f.x)=0.K by A98,A97,A101,BINOP_1:3,XBOOLE_0:def 3;
end;
A103: now
assume
A104: idseq n in B9;
thus G0.(B9)=IFIN(idseq n,B9,1_K,0.K) by A90
.=1_K by A104,Def1;
end;
A105: now
assume idseq n in B9 \/ {x};
then
A106: idseq n in B9 or idseq n in {x} by XBOOLE_0:def 3;
now
per cases by A106,TARSKI:def 1;
case
A107: idseq n in B9;
A108: not x in B9 by A94,XBOOLE_0:def 5;
f.x=F2(x) by A3,A92
.=0.K by A107,A108,FUNCOP_1:def 8;
hence F.(G0.B9,f.x)=1_K by A103,A97,A107,BINOP_1:3;
end;
case
A109: idseq n=x;
f.x=F2(x) by A3,A92
.=1_K by A109,FUNCOP_1:def 8;
hence F.(G0.B9,f.x)=1_K by A94,A98,A97,A109,BINOP_1:3
,XBOOLE_0:def 5;
end;
end;
hence F.(G0.B9,f.x)=1_K;
end;
now
assume
A110: idseq n in B9 \/ {x};
thus G0.(B9 \/ {x})=IFIN(idseq n,B9 \/ {.x.},1_K,0.K) by A90
.=1_K by A110,Def1;
end;
hence thesis by A95,A105,A100;
end;
end;
A111: for x being Element of X holds G0.({x}) = f.x
proof
let x be Element of X;
now
per cases;
case
A112: x=idseq n;
then idseq n in {x} by TARSKI:def 1;
then
A113: IFIN(idseq n,{x},1_K,0.K)=1_K by Def1;
f2.x=F2(x) by A3
.=1_K by A112,FUNCOP_1:def 8;
hence G0.({.x.})=f2.x by A90,A113;
end;
case
A114: x <> idseq n;
then not idseq n in {x} by TARSKI:def 1;
then
A115: IFIN(idseq n,{x},1_K,0.K)=0.K by Def1;
f2.x=F2(x) by A3
.=0.K by A114,FUNCOP_1:def 8;
hence G0.({.x.})=f2.x by A90,A115;
end;
end;
hence thesis by A91,A5,FUNCT_1:2;
end;
A116: for e being Element of Y st e is_a_unity_wrt F holds G0.({}) = e
proof
let e be Element of Y;
assume e is_a_unity_wrt F;
then
A117: F.(0.K,e)=0.K by BINOP_1:3;
0.K is_a_unity_wrt F by FVSUM_1:6;
then
A118: F.(0.K,e)=e by BINOP_1:3;
IFIN(idseq n,{},1_K,0.K)=0.K by Def1;
hence thesis by A90,A117,A118,FINSUB_1:7;
end;
A119: now
assume
A120: idseq n in B;
thus G0.(B)=IFIN(idseq n,B,1_K,0.K) by A90
.=1_K by A120,Def1;
end;
S: (idseq n) is Element of Group_of_Perm(n) by MATRIX_1:11;
Permutations n in Fin Permutations n by FINSUB_1:def 5;
then B=Permutations(n) & (idseq n) in the carrier of Group_of_Perm(n) by S,
SUBSET_1:def 8;
then (the addF of K) $$ (In(Permutations n,Fin Permutations n),
Path_product(1.(K,n)))=
1_K by A119,A116,A111,A93,MATRIX_1:def 17,SETWISEO:def 3;
hence thesis by MATRIX_3:def 9;
end;
definition
let n be Nat, K be Field, M be Matrix of n,K;
redefine attr M is diagonal means :: redefines diagonal (MATRIX_1, definition)
for i,j being Nat st i in Seg n & j in Seg n & i <> j holds M*(i,j) = 0.K;
compatibility
proof
hereby
assume
A1: M is diagonal;
let i, j be Nat;
assume that
A2: i in Seg n & j in Seg n and
A3: i <> j;
[i,j] in [:Seg n, Seg n:] by A2,ZFMISC_1:def 2;
then [i,j] in Indices M by MATRIX_0:24;
hence M*(i,j) = 0.K by A1,A3;
end;
assume
A4: for i,j being Nat st i in Seg n & j in Seg n & i <> j
holds M*(i,j) = 0.K;
let i,j be Nat;
assume that
A5: [i,j] in Indices M and
A6: M*(i,j) <> 0.K;
[i,j] in [:Seg n, Seg n:] by A5,MATRIX_0:24;
then i in Seg n & j in Seg n by ZFMISC_1:87;
hence thesis by A4,A6;
end;
end;
theorem
for K being Field, n being Nat, A being Matrix of n,K st n
>=1 & A is diagonal holds Det A = (the multF of K) $$ (diagonal_of_Matrix A)
proof
let K be Field, n be Nat, A be Matrix of n,K;
assume that
A1: n>=1 and
A2: A is diagonal;
set k1=(the multF of K)$$(diagonal_of_Matrix A);
set X=Permutations n;
set Y=the carrier of K;
reconsider p0=idseq n as Permutation of Seg n;
A3: len (diagonal_of_Matrix A)=n by MATRIX_3:def 10;
deffunc F2(object) = IFEQ(idseq n,$1,k1,0.K);
A4: for x being object st x in X holds F2(x) in Y;
ex f2 being Function of X,Y st for x being object st x in X holds f2.x =
F2(x) from FUNCT_2:sch 2(A4);
then consider f2 being Function of X,Y such that
A5: for x being object st x in X holds f2.x = F2(x);
A6: p0 is even by MATRIX_1:16;
A7: for x being object st x in dom (Path_product A)
holds (Path_product A).x= f2.x
proof
let x be object;
assume x in dom Path_product A;
for p being Element of Permutations n holds f2.p = -((the multF of K)
$$ Path_matrix(p,A),p)
proof
let p be Element of Permutations n;
A8: now
per cases;
suppose
p is even;
hence -(0.K,p)=(0.K) by MATRIX_1:def 20;
end;
suppose
p is odd;
then -(0.K,p)= -(0.K) by MATRIX_1:def 20
.=0.K by RLVECT_1:12;
hence -(0.K,p)=0.K;
end;
end;
now
per cases;
case
A9: p=idseq n;
A10: for i,j st i in dom ((diagonal_of_Matrix A)) & j=p.i holds (
diagonal_of_Matrix A) .i=(A)*(i,j)
proof
let i,j;
assume that
A11: i in dom ((diagonal_of_Matrix A)) and
A12: j=p.i;
A13: i in Seg n by A3,A11,FINSEQ_1:def 3;
then p.i=i by A9,FUNCT_1:17;
hence thesis by A12,A13,MATRIX_3:def 10;
end;
len Permutations n = n by MATRIX_1:9;
then
A14: -((the multF of K) $$ Path_matrix(p,A),p) = (the multF of K) $$
Path_matrix(p,(A)) by A6,A9,MATRIX_1:def 20;
f2.p=F2(p) by A5
.= k1 by A9,FUNCOP_1:def 8;
hence thesis by A3,A14,A10,MATRIX_3:def 7;
end;
case
A15: p<>idseq n;
reconsider Ab=NAT as non empty set;
defpred P3[Nat] means $1 < n implies ex p3 being
FinSequence of K st len p3=$1+1 & p3.1=(Path_matrix(p,A)).1 & (for n3 being
Nat st 0 <> n3 & n3 < $1+1 & n3<n holds p3.(n3 + 1) = (the multF of
K). (p3.n3,(Path_matrix(p,A)).(n3 + 1)));
A16: rng ((Path_matrix(p,A))) c= the carrier of K by FINSEQ_1:def 4;
A17: len (Path_matrix(p,A))=n by MATRIX_3:def 7;
then 1 in Seg len (Path_matrix(p,A)) by A1;
then 1 in dom (Path_matrix(p,A)) by FINSEQ_1:def 3;
then (Path_matrix(p,A)).1 in rng ((Path_matrix(p,A))) by
FUNCT_1:def 3;
then reconsider d=(Path_matrix(p,A)).1 as Element of K by A16;
reconsider q3=<* d *> as FinSequence of K;
A18: for n3 being Nat st 0 <> n3 & n3 < 0+1 & n3< n holds
q3.(n3 + 1) = (the multF of K). (q3.n3,(Path_matrix(p,A)).(n3 + 1)) by NAT_1:13
;
A19: for k being Nat st P3[k] holds P3[k+1]
proof
let k be Nat;
assume
A20: P3[k];
now
per cases;
case
A21: k+1<n;
then consider p3 being FinSequence of K such that
A22: len p3=k+1 and
A23: p3.1=(Path_matrix(p,A)).1 and
A24: for n3 being Nat st 0 <> n3 & n3 < k+1 &
n3<n holds p3.( n3 + 1) = (the multF of K). (p3.n3,(Path_matrix(p,A)).(n3 + 1))
by A20,NAT_1:12;
defpred P6[object,object] means
($1 in Seg (k+1) implies $2=p3.$1)&
(not $1 in Seg (k+1) implies $2=0.K);
A25: for x being object st x in NAT
ex y being object st y in the carrier of K & P6[x,y]
proof
let x be object;
assume x in NAT;
now
per cases;
case
A26: x in Seg (k+1);
then reconsider nx=x as Nat;
nx in dom p3 by A22,A26,FINSEQ_1:def 3;
then
A27: p3.nx in rng p3 by FUNCT_1:def 3;
rng p3 c= the carrier of K by FINSEQ_1:def 4;
then reconsider s=p3.nx as Element of K by A27;
x in Seg (k+1) implies s=p3.x;
hence thesis by A26;
end;
case
not x in Seg (k+1);
hence thesis;
end;
end;
hence thesis;
end;
ex f6 being sequence of the carrier of K st for x
being object st x in NAT holds P6[x,f6.x] from FUNCT_2:sch 1(A25);
then consider
f6 being sequence of the carrier of K such that
A28: for x being object st x in NAT holds P6[x,f6.x];
1<=k+1+1 & k+1+1 <=n by A21,NAT_1:12,13;
then k+1+1 in Seg len (Path_matrix(p,A)) by A17;
then k+1+1 in dom (Path_matrix(p,A)) by FINSEQ_1:def 3;
then rng ((Path_matrix(p,A))) c= the carrier of K & (
Path_matrix(p,A)).(k + 1+1) in rng (Path_matrix(p,A)) by FINSEQ_1:def 4
,FUNCT_1:def 3;
then [f6.(k+1),(Path_matrix(p,A)).(k + 1+1)] in [:the carrier
of K, the carrier of K:] by ZFMISC_1:def 2;
then reconsider
e=(the multF of K). (f6.(k+1),(Path_matrix(p,A)).(k
+ 1+1)) as Element of K by FUNCT_2:5;
reconsider q3=p3^<* e *> as FinSequence of K;
A29: len q3=(len p3) + len (<*e*>) by FINSEQ_1:22
.=k+1+1 by A22,FINSEQ_1:40;
A30: for n3 being Nat st 0 <> n3 & n3 < k+1+1 & n3<
n holds q3.(n3 + 1) = (the multF of K). (q3.n3,(Path_matrix(p,(A))).(n3 + 1))
proof
let n3 be Nat;
assume that
A31: 0 <> n3 and
A32: n3 < k+1+1 and
A33: n3<n;
now
per cases;
case
A34: n3<k+1;
then 1<=n3+1 & n3+1<=k+1 by NAT_1:12,13;
then n3+1 in Seg len p3 by A22;
then n3+1 in dom p3 by FINSEQ_1:def 3;
then
A35: p3.(n3+1)=q3.(n3+1) by FINSEQ_1:def 7;
0+1<=n3 by A31,NAT_1:13;
then n3 in Seg len p3 by A22,A34;
then
A36: n3 in dom p3 by FINSEQ_1:def 3;
p3.(n3 + 1) = (the multF of K) . (p3.n3,(
Path_matrix(p,(A))).(n3 + 1)) by A24,A31,A33,A34;
hence thesis by A35,A36,FINSEQ_1:def 7;
end;
case
A37: n3>=k+1;
A38: n3+1<=k+1+1 by A32,NAT_1:13;
A39: n3+1>k+1 by A37,NAT_1:13;
then n3+1>=k+1+1 by NAT_1:13;
then
A40: n3+1=k+1+1 by A38,XXREAL_0:1;
1<=k+1 by NAT_1:12;
then
A41: k+1 in Seg (k+1);
then k+1 in dom p3 by A22,FINSEQ_1:def 3;
then
A42: q3.(k+1)=p3.(k+1) by FINSEQ_1:def 7;
(q3).(n3+1) = (<*e*>).(n3+1 - (k+1)) by A22,A29,A39,A38,
FINSEQ_1:24
.= e by A40;
hence thesis by A28,A40,A41,A42;
end;
end;
hence thesis;
end;
1<=k+1 by NAT_1:12;
then 1 in Seg len p3 by A22;
then 1 in dom p3 by FINSEQ_1:def 3;
then q3.1=(Path_matrix(p,(A))).1 by A23,FINSEQ_1:def 7;
hence thesis by A29,A30;
end;
case
k+1>=n;
hence thesis;
end;
end;
hence thesis;
end;
A43: f2.p=F2(p) by A5
.= 0.K by A15,FUNCOP_1:def 8;
n<n+1 by NAT_1:13;
then
A44: n-1<n+1-1 by XREAL_1:14;
A45: dom p = Seg len Permutations n by FUNCT_2:52;
then
A46: dom p = Seg n by MATRIX_1:9;
then dom p = dom idseq n by RELAT_1:45;
then consider i0 being object such that
A47: i0 in dom p and
A48: p.i0 <> (idseq n).i0 by A15,FUNCT_1:2;
A49: i0 in Seg n by A45,A47,MATRIX_1:9;
reconsider i0 as Nat by A45,A47;
A50: p.i0<>i0 by A46,A47,A48,FUNCT_1:18;
p is Permutation of Seg n by MATRIX_1:def 16;
then
A51: p.i0 in Seg n by A46,A47,FUNCT_2:5;
then reconsider j0=p.i0 as Nat;
A52: n-1=n-'1 by A1,XREAL_1:233;
len q3=1 & q3.1=(Path_matrix(p,A)).1 by FINSEQ_1:40;
then
A53: P3[0] by A18;
for k being Nat holds P3[k] from NAT_1:sch 2(A53,
A19);
then consider p3 being FinSequence of K such that
A54: len p3=n-'1+1 and
A55: p3.1=(Path_matrix(p,A)).1 and
A56: for n3 being Nat st 0 <> n3 & n3 < n-'1+1 & n3<
n holds p3.(n3 + 1) = (the multF of K). (p3.n3,(Path_matrix(p,(A))).(n3 + 1))
by A52,A44;
defpred P[set,set] means ($1 in Seg n implies $2=p3.$1)& (not $1 in
Seg n implies $2=0.K);
A57: for x3 being Element of Ab ex y3 being Element of K st P[x3,y3 ]
proof
let x3 be Element of Ab;
now
per cases;
case
A58: x3 in Seg n;
then x3 in dom p3 by A52,A54,FINSEQ_1:def 3;
then rng p3 c= the carrier of K & p3.x3 in rng p3 by
FINSEQ_1:def 4,FUNCT_1:def 3;
hence thesis by A58;
end;
case
not x3 in Seg n;
hence thesis;
end;
end;
hence thesis;
end;
ex f4 being Function of Ab,the carrier of K st for x2 being
Element of Ab holds P[x2,f4.x2] from FUNCT_2:sch 3(A57);
then consider f4 being sequence of the carrier of K such that
A59: for x4 being Element of NAT holds (x4 in Seg n implies f4.
x4=p3.x4)& (not x4 in Seg n implies f4.x4=0.K);
A60: for n3 being Nat st 0 <> n3 & n3 < len (Path_matrix(p,A))
holds f4.(n3 + 1) = (the multF of K). (f4.n3,(Path_matrix(p,A)).(n3 + 1))
proof
let n3 be Nat;
assume that
A61: 0 <> n3 and
A62: n3 < len (Path_matrix(p,A));
A63: n3+1<=len (Path_matrix(p,A)) by A62,NAT_1:13;
A64: 0+1<=n3 by A61,NAT_1:13;
then
A65: n3 in Seg n by A17,A62;
1<n3+1 by A64,NAT_1:13;
then n3+1 in Seg n by A17,A63;
then
A66: f4.(n3+1)=p3.(n3+1) by A59;
p3.(n3 + 1) = (the multF of K). (p3.n3,(Path_matrix(p,A)).(
n3 + 1)) by A17,A52,A56,A61,A62;
hence thesis by A59,A66,A65;
end;
A67: i0<=n by A46,A47,FINSEQ_1:1;
then
A68: n-'i0 =n-i0 by XREAL_1:233;
i0 in dom (Path_matrix(p,A)) by A49,A17,FINSEQ_1:def 3;
then
A69: (Path_matrix(p,A)).i0=(A)*(i0,j0) by MATRIX_3:def 7;
defpred P5[Nat] means f4.(i0+$1)=0.K;
A70: 0<i0 by A45,A47,FINSEQ_1:1;
A71: for k being Nat st P5[k] holds P5[k+1]
proof
let k be Nat;
A72: 1<=1+(i0+k) by NAT_1:12;
assume
A73: P5[k];
now
per cases;
case
A74: i0+k+1<=n;
1<=1+(i0+k) by NAT_1:12;
then i0+k+1 in Seg len (Path_matrix(p,A)) by A17,A74;
then i0+k+1 in dom (Path_matrix(p,A)) by FINSEQ_1:def 3;
then
A75: (Path_matrix(p,A)).(i0+k+1) in rng (Path_matrix(p,A)) by
FUNCT_1:def 3;
rng (Path_matrix(p,A)) c= the carrier of K by FINSEQ_1:def 4;
then reconsider
b=(Path_matrix(p,A)).(i0+k+1) as Element of K by A75;
i0<=i0+k by NAT_1:12;
then
A76: 0<i0+k by A45,A47,FINSEQ_1:1;
A77: i0+k<n by A74,NAT_1:13;
0+1<=i0+k by A70,NAT_1:13;
then
A78: i0+k in Seg n by A77;
i0+k+1 in Seg n by A72,A74;
then f4.(i0+k+1)=p3.(i0+k+1) by A59
.=(the multF of K). (p3.(i0+k),(Path_matrix(p,A)).(i0+k+1)
) by A52,A56,A77,A76
.= (0.K)*b by A59,A73,A78
.= 0.K;
hence thesis;
end;
case
i0+k+1>n;
then not i0+(k+1) in Seg n by FINSEQ_1:1;
hence thesis by A59;
end;
end;
hence thesis;
end;
1 in Seg n by A1;
then
A79: f4.1=(Path_matrix(p,A)).1 by A55,A59;
A80: 1<=i0 by A45,A47,FINSEQ_1:1;
now
per cases;
case
i0<=1;
then i0=1 by A80,XXREAL_0:1;
hence P5[0] by A2,A49,A50,A51,A69,A79;
end;
case
A81: i0>1;
reconsider a=f4.(i0-'1) as Element of K;
i0<i0+1 by NAT_1:13;
then i0-1<i0+1-1 by XREAL_1:14;
then
A82: i0-1<len (Path_matrix(p,A)) by A67,A17,XXREAL_0:2;
i0-'1=i0-1 by A81,XREAL_1:233;
then
A83: i0-'1+1=i0;
i0-1> 1-1 by A81,XREAL_1:14;
then f4.i0 = (the multF of K). (f4.(i0-'1),(Path_matrix(p,A)).
i0) by A60,A82,A83
.= a*(0.K) by A2,A49,A50,A51,A69
.= 0.K;
hence P5[0];
end;
end;
then
A84: P5[0];
for k being Nat holds P5[k] from NAT_1:sch 2(A84,
A71);
then P5[n-'i0];
hence thesis by A1,A8,A43,A17,A79,A60,A68,FINSOP_1:2;
end;
end;
hence thesis;
end;
hence thesis by MATRIX_3:def 8;
end;
deffunc F3(set) = IFIN(idseq n,$1,k1,0.K);
set F=the addF of K;
set f=Path_product(A);
set B=In(Permutations(n),Fin Permutations n);
A85: for x being set st x in Fin X holds F3(x) in Y
proof
let x be set;
assume x in Fin X;
per cases;
suppose
idseq n in x;
then F3(x)=k1 by Def1;
hence thesis;
end;
suppose
not idseq n in x;
then F3(x)=0.K by Def1;
hence thesis;
end;
end;
ex f2 being Function of Fin X,Y st
for x being set st x in Fin X holds
f2.x = F3(x) from FUNCT_2:sch 11(A85);
then consider G0 being Function of Fin X,Y such that
A86: for x being set st x in Fin X holds G0.x = F3(x);
dom (f2)=Permutations(n) by FUNCT_2:def 1;
then
A87: dom (Path_product A)=dom f2 by FUNCT_2:def 1;
then
A88: Path_product(A)=f2 by A7,FUNCT_1:2;
A89: for B9 being Element of Fin X st B9 c= B & B9 <> {} for x being
Element of X st x in B\B9 holds G0.(B9 \/ {x}) = F.(G0.B9,f.x)
proof
let B9 be Element of Fin X;
assume that
B9 c= B and
B9 <> {};
thus for x being Element of X st x in B\B9 holds G0.(B9 \/ {x}) = F.(G0.B9
,f.x)
proof
let x be Element of X;
assume
A90: x in B\B9;
A91: now
assume
A92: not idseq n in B9 \/ {x};
thus G0.(B9 \/ {x})=IFIN(idseq n,B9 \/ {.x.},k1,0.K) by A86
.=0.K by A92,Def1;
end;
A93: 0.K is_a_unity_wrt F by FVSUM_1:6;
A94: now
assume
A95: not idseq n in B9;
thus G0.(B9)=IFIN(idseq n,B9,k1,0.K) by A86
.=0.K by A95,Def1;
end;
A96: now
assume
A97: not idseq n in B9 \/ {x};
then not idseq n in {x} by XBOOLE_0:def 3;
then
A98: not idseq n=x by TARSKI:def 1;
f.x=F2(x) by A5,A88
.=0.K by A98,FUNCOP_1:def 8;
hence F.(G0.B9,f.x)=0.K by A94,A93,A97,BINOP_1:3,XBOOLE_0:def 3;
end;
A99: now
assume
A100: idseq n in B9;
thus G0.(B9)=IFIN(idseq n,B9,k1,0.K) by A86
.=k1 by A100,Def1;
end;
A101: now
assume idseq n in B9 \/ {x};
then
A102: idseq n in B9 or idseq n in {x} by XBOOLE_0:def 3;
now
per cases by A102,TARSKI:def 1;
case
A103: idseq n in B9;
A104: not x in B9 by A90,XBOOLE_0:def 5;
f.x=F2(x) by A5,A88
.=0.K by A103,A104,FUNCOP_1:def 8;
hence F.(G0.B9,f.x)=k1 by A99,A93,A103,BINOP_1:3;
end;
case
A105: idseq n=x;
f.x=F2(x) by A5,A88
.=k1 by A105,FUNCOP_1:def 8;
hence F.(G0.B9,f.x)=k1 by A90,A94,A93,A105,BINOP_1:3,XBOOLE_0:def 5
;
end;
end;
hence F.(G0.B9,f.x)=k1;
end;
now
assume
A106: idseq n in B9 \/ {x};
thus G0.(B9 \/ {x})=IFIN(idseq n,B9 \/ {.x.},k1,0.K) by A86
.=k1 by A106,Def1;
end;
hence thesis by A91,A101,A96;
end;
end;
A107: for x being Element of X holds G0.({x}) = f.x
proof
let x be Element of X;
now
per cases;
case
A108: x=idseq n;
then idseq n in {x} by TARSKI:def 1;
then
A109: IFIN(idseq n,{x},k1,0.K)=k1 by Def1;
f2.x=F2(x) by A5
.=k1 by A108,FUNCOP_1:def 8;
hence G0.({.x.})=f2.x by A86,A109;
end;
case
A110: x <> idseq n;
then not idseq n in {x} by TARSKI:def 1;
then
A111: IFIN(idseq n,{x},k1,0.K)=0.K by Def1;
f2.x=F2(x) by A5
.=0.K by A110,FUNCOP_1:def 8;
hence G0.({.x.})=f2.x by A86,A111;
end;
end;
hence thesis by A87,A7,FUNCT_1:2;
end;
A112: for e being Element of Y st e is_a_unity_wrt F holds G0.({}) = e
proof
let e be Element of Y;
assume e is_a_unity_wrt F;
then
A113: F.(0.K,e)=0.K by BINOP_1:3;
0.K is_a_unity_wrt F by FVSUM_1:6;
then
A114: F.(0.K,e)=e by BINOP_1:3;
IFIN(idseq n,{},k1,0.K)=0.K by Def1;
hence thesis by A86,A113,A114,FINSUB_1:7;
end;
A115: now
assume
A116: idseq n in B;
thus G0.(B)=IFIN(idseq n,B,k1,0.K) by A86
.=(the multF of K)$$ (diagonal_of_Matrix A) by A116,Def1;
end;
S: (idseq n) is Element of Group_of_Perm(n) by MATRIX_1:11;
Permutations n in Fin Permutations n by FINSUB_1:def 5;
then B=Permutations(n) & (idseq n) in the carrier of Group_of_Perm(n) by S,
SUBSET_1:def 8;
then (the addF of K) $$ (In(Permutations(n),Fin Permutations n),
Path_product(A))= (the
multF of K)$$ (diagonal_of_Matrix A) by A115,A112,A107,A89,MATRIX_1:def 17
,SETWISEO:def 3;
hence thesis by MATRIX_3:def 9;
end;
theorem Th18:
for p being Element of Permutations(n) holds p" is Element of Permutations(n)
proof
let p be Element of Permutations(n);
p" is Element of Group_of_Perm(n) by MATRIX_1:14;
hence thesis by MATRIX_1:def 17;
end;
definition
let n;
let p be Element of Permutations(n);
redefine func p" -> Element of Permutations(n); :: redefines " (FUNCT_1, definition)
coherence by Th18;
end;
::$CT
theorem
for G being Group, f1,f2 being FinSequence of G
holds (Product (f1^f2))" = (Product f2)" * (Product f1)"
proof
let G be Group,f1,f2 be FinSequence of G;
thus (Product (f1^f2))" = ((Product f1) * (Product f2))" by GROUP_4:5
.= (Product f2)" * (Product f1)" by GROUP_1:17;
end;
definition
let G be Group, f be FinSequence of G;
::$CD
func f" -> FinSequence of G means
:Def3:
len it = len f &
for i being Nat st i in dom f holds it/.i = (f/.i)";
existence
proof
deffunc F(Nat) = (f/.$1)";
ex p being FinSequence st len p = len f & for k being Nat st k in dom
p holds p.k=F(k) from FINSEQ_1:sch 2;
then consider p being FinSequence such that
A1: len p = len f and
A2: for k being Nat st k in dom p holds p.k=F(k);
rng p c= the carrier of G
proof
let y be object;
assume y in rng p;
then consider x being object such that
A3: x in dom p and
A4: y=p.x by FUNCT_1:def 3;
reconsider k=x as Nat by A3;
p.k=(f/.k)" by A2,A3;
hence thesis by A4;
end;
then reconsider q=p as FinSequence of G by FINSEQ_1:def 4;
A5: dom p = dom f by A1,FINSEQ_3:29;
for i being Nat st i in dom f holds q/.i=(f/.i)"
proof
let i be Nat;
assume
A6: i in dom f;
hence q/.i=p.i by A5,PARTFUN1:def 6
.=(f/.i)" by A2,A5,A6;
end;
hence thesis by A1;
end;
uniqueness
proof
thus for g1,g2 being FinSequence of G st (len g1=len f & for i being
Nat st i in dom f holds g1/.i=(f/.i)")& (len g2=len f & for j being
Nat st j in dom f holds g2/.j=(f/.j)") holds g1=g2
proof
let g1,g2 be FinSequence of G;
assume that
A7: len g1=len f and
A8: for i being Nat st i in dom f holds g1/.i=(f /.i)" and
A9: len g2=len f and
A10: for j being Nat st j in dom f holds g2/. j=(f/.j)";
A11: dom g1 = dom f by A7,FINSEQ_3:29;
for k being Nat st 1<= k & k<= len g1 holds g1.k=g2.k
proof
let k be Nat;
assume
A12: 1<= k & k<= len g1;
k in Seg len g2 by A7,A9,A12;
then k in dom g2 by FINSEQ_1:def 3;
then
A13: g2.k=g2/.k by PARTFUN1:def 6;
k in Seg len g1 by A12;
then
A14: k in dom g1 by FINSEQ_1:def 3;
then g1.k=g1/.k & g1/.k=(f/.k)" by A8,A11,PARTFUN1:def 6;
hence thesis by A10,A11,A14,A13;
end;
hence thesis by A7,A9;
end;
end;
end;
theorem Th20:
for G being Group holds (<*>(the carrier of G))"=<*>(the carrier of G)
proof
let G be Group;
len (<*>(the carrier of G))=0;
then len ((<*>(the carrier of G))" qua FinSequence of G)=0 by Def3;
hence thesis;
end;
theorem Th21:
for G being Group, f,g being FinSequence of G holds (f^g)"=(f")^ (g")
proof
let G be Group, f,g be FinSequence of G;
A1: len ((f^g)")=len (f^g) by Def3
.= len f+len g by FINSEQ_1:22;
A2: len f+len g=len (f") +len g by Def3
.=len (f") + len (g") by Def3
.= len ((f")^(g")) by FINSEQ_1:22;
A3: len ((f^g)")=len (f^g) by Def3;
for i being Nat st 1<=i & i<= len ((f^g)") holds ((f^g)").i=((f")^(g")). i
proof
let i be Nat;
assume that
A4: 1<=i and
A5: i<= len ((f^g)");
now
per cases;
case
len f>0;
A6: len (f")=len f by Def3;
len ((f^g)")=len (f^g) by Def3;
then
A7: dom ((f^g)")=dom (f^g) by FINSEQ_3:29;
i in Seg len ((f^g)") by A4,A5;
then
A8: i in dom ((f^g)") by FINSEQ_1:def 3;
then
A9: ((f^g)") .i=(((f^g)"))/.i by PARTFUN1:def 6
.= ((f^g)/.i)" by A7,A8,Def3;
A10: len (g")=len g by Def3;
now
per cases;
case
i<=len f;
then
A11: i in Seg len f by A4;
then
A12: i in dom f by FINSEQ_1:def 3;
A13: i in dom (f") by A6,A11,FINSEQ_1:def 3;
(f^g)/.i=(f^g).i by A7,A8,PARTFUN1:def 6
.=f.i by A12,FINSEQ_1:def 7
.=f/.i by A12,PARTFUN1:def 6;
then ((f^g)/.i)" =(f")/.i by A12,Def3
.=(f").i by A13,PARTFUN1:def 6;
hence thesis by A9,A13,FINSEQ_1:def 7;
end;
case
A14: i>len f;
then 1+len f<=i by NAT_1:13;
then
A15: 1+len f -len f<=i-len f by XREAL_1:9;
A16: i-'len f=i-len f by A14,XREAL_1:233;
i-len f <= len g+len f -len f by A1,A5,XREAL_1:9;
then
A17: i-'len f in Seg len g by A16,A15;
then
A18: i-'len f in dom g by FINSEQ_1:def 3;
A19: i-'len f in dom (g") by A10,A17,FINSEQ_1:def 3;
(f^g)/.i=(f^g).i by A7,A8,PARTFUN1:def 6
.=g.(i-len (f)) by A3,A5,A14,FINSEQ_1:24
.=g/.(i-'len f) by A16,A18,PARTFUN1:def 6;
then ((f^g)/.i)" =(g")/.(i-'len f) by A18,Def3
.=(g").(i-len (f")) by A6,A16,A19,PARTFUN1:def 6;
hence thesis by A1,A2,A5,A6,A9,A14,FINSEQ_1:24;
end;
end;
hence thesis;
end;
case
len f<=0;
then f={};
then ((f^g)")=g" & f"=<*>(the carrier of G) by Th20,FINSEQ_1:34;
hence thesis by FINSEQ_1:34;
end;
end;
hence thesis;
end;
hence thesis by A1,A2;
end;
theorem Th22:
for G being Group,a being Element of G holds (<*a*>)" =<* a" *>
proof
let G be Group,a be Element of G;
A1: len ((<*a*>)")=len (<* a *>) by Def3
.=1 by FINSEQ_1:39
.=len (<* a" *>) by FINSEQ_1:39;
for i being Nat st 1<=i & i<= len <*a" *> holds ((<*a*>)").i=(<* a" *>). i
proof
let i be Nat;
assume
A2: 1<=i & i<= len <*a" *>;
A3: len <*a" *>=1 by FINSEQ_1:39;
then
A4: i=1 by A2,XXREAL_0:1;
len (<* a *>) =1 by FINSEQ_1:39;
then i in Seg len (<*a*>) by A2,A3;
then
A5: i in dom (<*a*>) by FINSEQ_1:def 3;
i in Seg len ((<*a*>)") by A1,A2;
then i in dom ((<*a*>)") by FINSEQ_1:def 3;
then
A6: ((<*a*>)").i=((<*a*>)")/.i by PARTFUN1:def 6
.= ((<* a *>)/.i)" by A5,Def3;
(<* a *>)/.i= ((<* a *>).i) by A5,PARTFUN1:def 6
.= a by A4;
hence thesis by A4,A6;
end;
hence thesis by A1;
end;
theorem Th23:
for G being Group, f being FinSequence of G holds Product (f^( Rev f)")=1_G
proof
let G be Group,f be FinSequence of G;
defpred P[Nat] means for g being FinSequence of G st len g <=$1
holds Product (g^(Rev g)")=1_G;
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A2: P[k];
for g being FinSequence of G st len g <= k+1 holds Product (g^(Rev g)
")=1_G
proof
let g be FinSequence of G;
assume
A3: len g <= k+1;
now
per cases by A3,XXREAL_0:1;
case
len g<k+1;
then len g<=k by NAT_1:13;
hence thesis by A2;
end;
case
A4: len g=k+1;
reconsider h=g|k as FinSequence of G;
k< len g by A4,NAT_1:13;
then
A5: len h=k by FINSEQ_1:59;
A6: Product (<* g/.(k+1) *> ^ (<* g/.(k + 1) *>)") =Product (<* g/.
(k+1) *>) * Product ((<* g/.(k + 1) *>)") by GROUP_4:5
.=(g/.(k+1))*Product ((<* g/.(k + 1) *>)") by FINSOP_1:11
.=(g/.(k+1))*Product ((<* (g/.(k + 1))" *>)) by Th22
.=(g/.(k+1))*(g/.(k + 1))" by FINSOP_1:11
.=1_G by GROUP_1:def 5;
A7: g=h^<* g/.(k+1) *> by A4,FINSEQ_5:21;
then Rev g=<* g/.(k+1) *> ^ (Rev h) by FINSEQ_5:63;
then (Rev g)"=(<* g/.(k + 1) *>)" ^ (Rev h)" by Th21;
then
g^(Rev g)"=h^ (<* g/.(k+1) *> ^ ((<* g/.(k + 1) *>)" ^ (Rev h)"
)) by A7,FINSEQ_1:32
.=h^ (<* g/.(k+1) *> ^ (<* g/.(k + 1) *>)" ^ (Rev h)") by
FINSEQ_1:32;
then
Product (g^(Rev g)") =Product (h) * Product (<* g/.(k+1) *> ^ (
<* g/.(k + 1) *>)" ^ (Rev h)") by GROUP_4:5
.=Product (h) * (Product (<* g/.(k+1) *> ^ (<* g/.(k + 1) *>)" )
* Product ((Rev h)")) by GROUP_4:5
.=Product (h) * Product ((Rev h)") by A6,GROUP_1:def 4
.=Product (h^((Rev h)")) by GROUP_4:5;
hence thesis by A2,A5;
end;
end;
hence thesis;
end;
hence thesis;
end;
for g being FinSequence of G st len g <= 0 holds Product (g^(Rev g)")= 1_G
proof
let g be FinSequence of G;
assume len g <= 0;
then
A8: g=<*>(the carrier of G);
then Rev g=<*>(the carrier of G) by FINSEQ_5:79;
then (Rev g)" = <*>(the carrier of G) by Th20;
then g^(Rev g)"=<*>(the carrier of G) by A8,FINSEQ_1:34;
hence thesis by GROUP_4:8;
end;
then
A9: P[0];
for j being Nat holds P[j] from NAT_1:sch 2(A9,A1);
then P[len f];
hence thesis;
end;
theorem Th24:
for G being Group,f being FinSequence of G holds Product ((Rev f )" ^f)=1_G
proof
let G be Group,f be FinSequence of G;
A1: len f=len Rev f by FINSEQ_5:def 3;
A2: len Rev ((Rev f)")=len ((Rev ((Rev f)"))") by Def3;
then
A3: dom Rev ((Rev f)")=dom ((Rev ((Rev f)"))") by FINSEQ_3:29;
A4: len ((Rev f)") = len Rev ((Rev f)") by FINSEQ_5:def 3;
A5: len Rev f = len ((Rev f)") by Def3;
then
A6: dom Rev f = dom ((Rev f)") by FINSEQ_3:29;
for i being Nat st 1<= i & i <= len f holds f.i = ((Rev ((Rev f)") )").i
proof
let i be Nat;
assume that
A7: 1<= i and
A8: i <= len f;
len f-i+1=len f-'i+1 by A8,XREAL_1:233;
then reconsider j=len f-i+1 as Nat;
A9: i+j=len f+1;
A10: i in Seg len f by A7,A8;
then
A11: i in dom ((Rev ((Rev f)"))") by A1,A5,A4,A2,FINSEQ_1:def 3;
i-1>=0 by A7,XREAL_1:48;
then len f +0 <=len f+(i-1) by XREAL_1:7;
then
A12: len f-(i-1)<=len f+(i-1)-(i-1) by XREAL_1:13;
len f-i=len f-'i by A8,XREAL_1:233;
then len f-i+1>=0+1 by XREAL_1:6;
then j in Seg len f by A12;
then
A13: j in dom ((Rev f)") by A1,A5,FINSEQ_1:def 3;
A14: j+i=len f+1;
A15: i in dom f by A10,FINSEQ_1:def 3;
then f.i=f/.i by PARTFUN1:def 6
.= (Rev f)/.j by A15,A9,FINSEQ_5:66
.= ((Rev f)/.j)""
.= (((Rev f)")/.j)" by A6,A13,Def3
.= ((Rev ((Rev f)"))/.i)" by A1,A5,A13,A14,FINSEQ_5:66
.= ((Rev ((Rev f)"))")/.i by A3,A11,Def3
.=((Rev ((Rev f)"))").i by A11,PARTFUN1:def 6;
hence thesis;
end;
then (Rev ((Rev f)") )"=f by A1,A5,A4,A2;
hence thesis by Th23;
end;
theorem Th25:
for G being Group,f being FinSequence of G holds (Product f)" =
Product ((Rev f)")
proof
let G be Group,f be FinSequence of G;
Product(f ^ (Rev f)")=1_G by Th23;
then
A1: (Product f) * Product ((Rev f)") = 1_G by GROUP_4:5;
Product((Rev f)" ^ f)=1_G by Th24;
then Product ((Rev f)") * (Product f) = 1_G by GROUP_4:5;
hence thesis by A1,GROUP_1:5;
end;
theorem Th26:
for ITP being Element of Permutations(n), ITG being Element of
Group_of_Perm(n) st ITG=ITP & n>=1 holds ITP"=ITG"
proof
let ITP be Element of Permutations(n), ITG be Element of Group_of_Perm(n);
assume that
A1: ITG=ITP and
A2: n>=1;
reconsider qf=ITP as Function of Seg n,Seg n by MATRIX_1:def 16;
dom qf=Seg n by A2,FUNCT_2:def 1;
then
A3: ITP"*ITP=id Seg n by FUNCT_1:39;
ITP is Permutation of Seg n by MATRIX_1:def 16;
then rng qf = Seg n by FUNCT_2:def 3;
then
A4: ITP*ITP"=id Seg n by FUNCT_1:39;
reconsider pf=ITP" as Element of Group_of_Perm n by MATRIX_1:def 17;
A5: idseq n=1_Group_of_Perm n & ITG*pf=(the multF of (Group_of_Perm(n))).(
ITG,pf ) by MATRIX_1:15;
A6: pf*ITG=(the multF of (Group_of_Perm(n))).(pf,ITG);
(the multF of (Group_of_Perm n)).(ITG,pf)=(ITP")*ITP & (the multF of (
Group_of_Perm n)).(pf,ITG)=ITP*(ITP") by A1,MATRIX_1:def 17;
hence thesis by A3,A4,A5,A6,GROUP_1:def 5;
end;
Lm2: for n being Nat, IT being Element of Permutations(n) st IT is
even & n>=1 holds IT" is even
proof
let n be Nat, IT be Element of Permutations(n);
assume that
A1: IT is even and
A2: n>=1;
reconsider ITP=IT as Element of Permutations n;
reconsider ITG=ITP as Element of Group_of_Perm n by MATRIX_1:def 17;
A3: len Permutations n=n by MATRIX_1:9;
then consider l being FinSequence of Group_of_Perm n such that
A4: (len l)mod 2=0 and
A5: IT=Product l and
A6: for i st i in dom l ex q being Element of Permutations n st l.i=q &
q is being_transposition by A1;
set m=len l;
reconsider lv=(Rev l)" as FinSequence of Group_of_Perm n;
A7: len l =len Rev l by FINSEQ_5:def 3;
then
A8: len l=len lv by Def3;
A9: for i st i in dom lv ex q2 being Element of Permutations(n) st lv.i=q2
& q2 is being_transposition
proof
let i;
reconsider ii=i as Nat;
assume
A10: i in dom lv;
then
A11: i in dom Rev l by A7,A8,FINSEQ_3:29;
A12: i in Seg len lv by A10,FINSEQ_1:def 3;
then 1<=i by FINSEQ_1:1;
then m+1<=m+i by XREAL_1:7;
then
A13: m+1-i<=m+i-i by XREAL_1:9;
i<=m by A8,A12,FINSEQ_1:1;
then
A14: m-i>=0 by XREAL_1:48;
then m-i+1=m-'i+1 by XREAL_0:def 2;
then reconsider j=len l-i+1 as Nat;
m-i+1>=0+1 by A14,XREAL_1:7;
then j in Seg len l by A13;
then
A15: j in dom l by FINSEQ_1:def 3;
then consider q being Element of Permutations n such that
A16: l.j=q and
A17: q is being_transposition by A6;
lv.i=lv/.i by A10,PARTFUN1:def 6;
then reconsider qq=lv.i as Element of Permutations(n) by MATRIX_1:def 17;
reconsider qqf=qq as Function of Seg n,Seg n by MATRIX_1:def 16;
A18: i+j=len l+1;
reconsider qf=q as Function of Seg n,Seg n by MATRIX_1:def 16;
consider i1,j1 being Nat such that
A19: i1 in dom q & j1 in dom q & i1<>j1 & q.i1=j1 & q.j1=i1 and
A20: for k being Nat st k <>i1 & k<>j1 & k in dom q holds q.k=k by A17;
A21: dom qf=Seg n & dom qqf=Seg n by A2,FUNCT_2:def 1;
A22: qq=(Rev l)"/.i by A10,PARTFUN1:def 6
.=((Rev l)/.ii)" by A11,Def3
.=(l/.j)" by A18,A15,FINSEQ_5:66
.=q" by A2,A15,A16,Th26,PARTFUN1:def 6;
A23: for k being Nat st k <>j1 & k<>i1 & k in dom qq holds qq.k =k
proof
let k be Nat;
assume that
A24: k <>j1 & k<>i1 and
A25: k in dom qq;
q.k=k by A20,A21,A24,A25;
hence thesis by A21,A22,A25,FUNCT_1:32;
end;
A26: qq=(Rev l)"/.i by A10,PARTFUN1:def 6
.=((Rev l)/.ii)" by A11,Def3
.=(l/.j)" by A18,A15,FINSEQ_5:66
.=q" by A2,A15,A16,Th26,PARTFUN1:def 6;
ex i,j st i in dom qq & j in dom qq & i<>j & qq.i=j & qq.j=i & for k
st k <>i & k<>j & k in dom qq holds qq.k=k
proof
take i=i1,j=j1;
thus i in dom qq & j in dom qq & i<>j & qq.i=j & qq.j=i by A19,A21,A26,
FUNCT_1:32;
let k;
thus thesis by A23;
end;
then qq is being_transposition;
hence thesis;
end;
ITG"=ITP" by A2,Th26;
then IT"=Product lv by A5,Th25;
hence thesis by A3,A4,A8,A9;
end;
theorem Th27:
for n being Nat, IT being Element of Permutations(n)
st n>=1 holds IT is even iff IT" is even
proof
let n be Nat, IT be Element of Permutations(n);
assume
A1: n>=1;
hence IT is even implies IT" is even by Lm2;
now
assume IT" is even;
then IT"" is even by A1,Lm2;
hence IT is even by FUNCT_1:43;
end;
hence thesis;
end;
theorem Th28:
for n being Nat,K being commutative Ring, p being Element of
Permutations(n), x being Element of K st n>=1 holds -(x,p) = -(x,p")
proof
let n be Nat,K be commutative Ring, p be Element of Permutations(n), x be
Element of K;
assume
A1: n>=1;
reconsider pf=p as Permutation of Seg n by MATRIX_1:def 16;
A2: len ((Permutations(n)))=n by MATRIX_1:9;
per cases;
suppose
p is even;
then -(x,p) = x & pf" is even by A1,A2,Th27,MATRIX_1:def 20;
hence thesis by A2,MATRIX_1:def 20;
end;
suppose
not p is even;
then -(x,p) = -x & not p" is even by A1,Th27,MATRIX_1:def 20;
hence thesis by MATRIX_1:def 20;
end;
end;
theorem
for K being commutative Ring,
f1,f2 being FinSequence of K holds (the multF
of K) $$ (f1^f2) = ((the multF of K)$$f1)*((the multF of K)$$f2)
by FINSOP_1:5;
theorem Th30:
for K being commutative Ring,R1,R2 be FinSequence of K st R1,R2
are_fiberwise_equipotent holds (the multF of K)$$ R1 = (the multF of K)$$ R2
proof
let K be commutative Ring;
defpred P[Nat] means for f,g be FinSequence of K st f,g
are_fiberwise_equipotent & len f = $1 holds (the multF of K)$$ f = (the multF
of K)$$ g;
let R1,R2 be FinSequence of K;
assume
A1: R1,R2 are_fiberwise_equipotent;
A2: len R1 = len R1;
A3: for n st P[n] holds P[n+1]
proof
let n;
assume
A4: P[n];
reconsider n1=n as Nat;
let f,g be FinSequence of K;
assume that
A5: f,g are_fiberwise_equipotent and
A6: len f = n+1;
A7: rng f c= the carrier of K by FINSEQ_1:def 4;
0+1<=n+1 by NAT_1:13;
then
A8: n+1 in dom f by A6,FINSEQ_3:25;
then f.(n+1) in rng f by FUNCT_1:def 3;
then reconsider a = f.(n+1) as Element of K by A7;
rng f = rng g by A5,CLASSES1:75;
then a in rng g by A8,FUNCT_1:def 3;
then consider m be Nat such that
A9: m in dom g and
A10: g.m = a by FINSEQ_2:10;
A11: g = (g|m)^(g/^m) by RFINSEQ:8;
set gg = g/^m, gm = g|m;
A12: 1<=m by A9,FINSEQ_3:25;
then max(0,m-1) = m-1 by FINSEQ_2:4;
then reconsider m1 = m-1 as Nat by FINSEQ_2:5;
m in Seg m by A12;
then
A13: gm.m = a by A9,A10,RFINSEQ:6;
A14: m = m1+1;
then m1<=m by NAT_1:11;
then
A15: Seg m1 c= Seg m by FINSEQ_1:5;
m<=len g by A9,FINSEQ_3:25;
then len gm = m by FINSEQ_1:59;
then
A16: gm = (gm|m1)^<*a*> by A14,A13,RFINSEQ:7;
set fn = f|n1;
A17: f = fn ^ <*a*> by A6,RFINSEQ:7;
A18: gm|m1 = g|((Seg m)/\(Seg m1)) by RELAT_1:71
.= g|m1 by A15,XBOOLE_1:28;
now
let x be object;
card Coim(f,x) = card Coim(g,x) by A5,CLASSES1:def 10;
then card(fn"{x})+card(<*a*>"{x}) = card(((g|m1)^<*a*>^(g/^m))"{x}) by
A11,A16,A18,A17,FINSEQ_3:57
.= card(((g|m1)^<*a*>)"{x})+card((g/^m)"{x}) by FINSEQ_3:57
.= card((g|m1)"{x})+card(<*a*>"{x})+card((g/^m)"{x}) by FINSEQ_3:57
.= card((g|m1)"{x})+card((g/^m)"{x})+card(<*a*>"{x})
.= card(((g|m1)^(g/^m))"{x})+card(<*a*>"{x}) by FINSEQ_3:57;
hence card Coim(fn,x) = card Coim((g|m1)^(g/^m),x);
end;
then
A19: fn, (g|m1)^(g/^m) are_fiberwise_equipotent by CLASSES1:def 10;
len fn = n by A6,FINSEQ_1:59,NAT_1:11;
then (the multF of K)$$ fn = (the multF of K)$$((g|m1)^gg) by A4,A19;
hence
(the multF of K)$$ f = (the multF of K)$$((g|m1)^gg)*(the multF of K)
$$ <*a*> by A17,FINSOP_1:5
.= (the multF of K)$$(g|m1)*(the multF of K)$$ gg*(the multF of K)$$
<*a*> by FINSOP_1:5
.= (the multF of K)$$(g|m1)*(the multF of K)$$ <*a*>*(the multF of K)
$$ gg by GROUP_1:def 3
.= (the multF of K)$$ gm*(the multF of K)$$ gg by A16,A18,FINSOP_1:5
.= (the multF of K)$$ g by A11,FINSOP_1:5;
end;
A20: P[0]
proof
let f,g be FinSequence of K;
assume f,g are_fiberwise_equipotent & len f = 0;
then
A21: len g = 0 & f = <*>(the carrier of K) by RFINSEQ:3;
then g = <*>(the carrier of K);
hence thesis by A21;
end;
for n holds P[n] from NAT_1:sch 2(A20,A3);
hence thesis by A1,A2;
end;
theorem Th31:
for n being Nat, K being commutative Ring, p being Element of
Permutations(n), f,g being FinSequence of K st len f=n & g=f*p holds f,g
are_fiberwise_equipotent
proof
let n be Nat, K be commutative Ring,
p be Element of Permutations(n), f,g be
FinSequence of K;
assume that
A1: len f=n and
A2: g=f*p;
reconsider fp=p as Function of Seg n,Seg n by MATRIX_1:def 16;
A3: p is Permutation of Seg n by MATRIX_1:def 16;
then
A4: rng p=Seg n by FUNCT_2:def 3;
rng fp = Seg n by A3,FUNCT_2:def 3;
then rng p c= dom f by A1,FINSEQ_1:def 3;
then
A5: dom (f*p)=dom fp by RELAT_1:27;
dom f=Seg n by A1,FINSEQ_1:def 3;
hence thesis by A2,A5,A4,CLASSES1:77;
end;
theorem
for n being Nat, K being commutative Ring, p being Element of
Permutations(n), f,g being FinSequence of K st n>=1 & len f=n & g=f*p holds (
the multF of K) $$ f = (the multF of K) $$ g by Th30,Th31;
theorem Th33:
for n being Nat, K being Ring, p being Element of
Permutations(n), f being FinSequence of K st n>=1 & len f=n holds f*p is
FinSequence of K
proof
let n be Nat, K be Ring, p be Element of Permutations(n), f be
FinSequence of K;
assume that
A1: n>=1 and
A2: len f=n;
reconsider q=p as Function of Seg n,Seg n by MATRIX_1:def 16;
p is bijective Function of Seg n,Seg n by MATRIX_1:def 16;
then rng q = Seg n by FUNCT_2:def 3;
then rng p c= dom f by A2,FINSEQ_1:def 3;
then dom (f*p)=dom q by RELAT_1:27
.=Seg n by A1,FUNCT_2:def 1;
then reconsider h=f*p as FinSequence by FINSEQ_1:def 2;
rng h c= rng f & rng f c= the carrier of K by FINSEQ_1:def 4,RELAT_1:26;
then rng h c= the carrier of K;
hence thesis by FINSEQ_1:def 4;
end;
theorem Th34:
for n being Nat, K being commutative Ring, p being Element of
Permutations(n), A being Matrix of n,K st n>=1 holds Path_matrix(p",A@) = (
Path_matrix(p,A))*p"
proof
let n be Nat, K be commutative Ring,p be Element of Permutations(n), A be
Matrix of n,K;
set f=(Path_matrix(p,A));
reconsider fp=p" as Function of Seg n,Seg n by MATRIX_1:def 16;
reconsider fp0=p as Function of Seg n,Seg n by MATRIX_1:def 16;
assume
A1: n>=1;
then
A2: dom fp =Seg n by FUNCT_2:def 1;
A3: len (Path_matrix(p,A))=n by MATRIX_3:def 7;
then reconsider m=(Path_matrix(p,A))*p" as FinSequence of K by A1,Th33;
p" is Permutation of Seg n by MATRIX_1:def 16;
then
A4: rng fp = Seg n by FUNCT_2:def 3;
then rng (p") c= dom f by A3,FINSEQ_1:def 3;
then
A5: dom (f*p")=dom fp by RELAT_1:27;
A6: p is Permutation of Seg n by MATRIX_1:def 16;
A7: for i,j st i in dom (m) & j=(p").i holds m.i=(A@)*(i,j)
proof
let i,j;
assume that
A8: i in dom (m) and
A9: j=(p").i;
A10: j in Seg n by A4,A5,A8,A9,FUNCT_1:def 3;
then
A11: j in dom f by A3,FINSEQ_1:def 3;
rng fp0 = Seg n by A6,FUNCT_2:def 3;
then i=p.j by A5,A2,A8,A9,FUNCT_1:32;
then
A12: (Path_matrix(p,A)).j=A*(j,i) by A11,MATRIX_3:def 7;
A13: dom A=Seg len A by FINSEQ_1:def 3
.= Seg n by MATRIX_0:def 2;
len A=n by MATRIX_0:def 2;
then i in Seg width A by A1,A5,A2,A8,MATRIX_0:20;
then
A14: [j,i] in Indices A by A10,A13,ZFMISC_1:def 2;
((Path_matrix(p,A))*p").i=(Path_matrix(p,A)).((p").i) by A5,A8,FUNCT_1:13;
hence thesis by A9,A12,A14,MATRIX_0:def 6;
end;
n in NAT by ORDINAL1:def 12;
then len m=n by A5,A2,FINSEQ_1:def 3;
hence thesis by A7,MATRIX_3:def 7;
end;
theorem Th35:
for n being Nat, K being commutative Ring, p being Element of
Permutations(n), A being Matrix of n,K st n>=1 holds (Path_product(A@)).(p") =
(Path_product(A)).p
proof
let n be Nat, K be commutative Ring,
p be Element of Permutations n, A be
Matrix of n,K;
assume
A1: n>=1;
A2: len (Path_matrix(p,A))=n by MATRIX_3:def 7;
then reconsider g=Path_matrix(p,A)*(p") as FinSequence of K by A1,Th33;
(Path_product(A@)).(p") = -((the multF of K) $$ Path_matrix(p",A@),p")
by MATRIX_3:def 8
.= -((the multF of K) $$ g,p") by A1,Th34
.= -((the multF of K) $$ g,p) by A1,Th28
.= -((the multF of K) $$ (Path_matrix(p,A)),p) by A2,Th30,Th31;
hence thesis by MATRIX_3:def 8;
end;
theorem
for n being Nat, K being commutative Ring, A being Matrix of n,K st n
>=1 holds Det (A) = Det (A@)
proof
let n be Nat, K be commutative Ring, A be Matrix of n,K;
set f=Path_product(A);
set f2=Path_product(A@);
set F=(the addF of K);
set Y=the carrier of K;
set X=Permutations(n);
set B=In(X,Fin X);
set I=(the addF of K) $$ (B,Path_product(A@));
A1: Det A = (the addF of K) $$ (B,Path_product A) by MATRIX_3:def 9;
X in Fin X by FINSUB_1:def 5; then
A2: B=Permutations(n) by SUBSET_1:def 8;
A3: {p" where p is Permutation of Seg n : p in B} c= B
proof
let z be object;
assume z in {p" where p is Permutation of Seg n : p in B};
then ex p being Permutation of Seg n st z=p" & p in B;
hence thesis by A2,MATRIX_1:def 16;
end;
A4: B c= {p" where p is Permutation of Seg n : p in B}
proof
let z be object;
assume z in B;
then reconsider q2=z as Permutation of Seg n by A2,MATRIX_1:def 16;
set q3=q2";
q3"=q2 & q3 in B by A2,FUNCT_1:43,MATRIX_1:def 16;
hence thesis;
end;
X in Fin X by FINSUB_1:def 5; then
A5: B <> {} or F is having_a_unity by SUBSET_1:def 8;
then consider G0 being Function of Fin X, Y such that
A6: I = G0.B and
A7: for e being Element of Y st e is_a_unity_wrt F holds G0.{} = e and
A8: for x being Element of X holds G0.{x} = f2.x and
A9: for B9 being Element of Fin X st B9 c= B & B9 <> {} for x being
Element of X st x in B \ B9 holds G0.(B9 \/ {x}) = F.(G0.B9,f2.x) by
SETWISEO:def 3;
deffunc F8(set) = G0.{p" where p is Permutation of Seg n : p in $1};
A10: for x2 being set st x2 in Fin X holds F8(x2) in Y
proof
let x2 be set;
assume x2 in Fin X;
{p" where p is Permutation of Seg n : p in x2} c= X
proof
let r be object;
assume r in {p" where p is Permutation of Seg n : p in x2};
then ex p being Permutation of Seg n st r=p" & p in x2;
hence thesis by MATRIX_1:def 16;
end;
then {p" where p is Permutation of Seg n : p in x2} is Element of Fin X
by FINSUB_1:17;
hence thesis by FUNCT_2:5;
end;
consider G1 being Function of Fin X,Y such that
A11: for x5 being set st x5 in Fin X holds G1.x5 = F8(x5) from FUNCT_2:
sch 11(A10);
assume
A12: n>=1;
A13: for x being Element of X holds G1.{x} = f.x
proof
let x be Element of X;
reconsider B4={.x.} as Element of Fin X;
reconsider q=x as Permutation of Seg n by MATRIX_1:def 16;
A14: q" is Element of X by MATRIX_1:def 16;
A15: {p" where p is Permutation of Seg n : p in B4} c= {q"}
proof
let z be object;
assume z in {p" where p is Permutation of Seg n : p in B4};
then consider p being Permutation of Seg n such that
A16: z=p" and
A17: p in B4;
p=x by A17,TARSKI:def 1;
hence thesis by A16,TARSKI:def 1;
end;
{q"} c= {p" where p is Permutation of Seg n : p in B4}
proof
let z be object;
assume z in {q"};
then q in B4 & z=q" by TARSKI:def 1;
hence thesis;
end;
then {p" where p is Permutation of Seg n : p in B4}={q"} by A15;
then G1.B4=G0.{q"} by A11
.=f2.(q") by A8,A14
.=(Path_product A).q by A12,Th35;
hence thesis;
end;
A18: for B9 being Element of Fin X st B9 c= B & B9 <> {} for x being Element
of X st x in B \ B9 holds G1.(B9 \/ {x}) = F.(G1.B9,f.x)
proof
let B9 be Element of Fin X;
assume that
A19: B9 c= B and
A20: B9 <> {};
thus for x being Element of X st x in B \ B9 holds G1.(B9 \/ {x}) = F.(G1.
B9,f.x)
proof
{p" where p is Permutation of Seg n : p in B9} c= X
proof
let v be object;
assume v in {p" where p is Permutation of Seg n : p in B9};
then ex p being Permutation of Seg n st p"=v & p in B9;
hence thesis by MATRIX_1:def 16;
end;
then reconsider
B2={p" where p is Permutation of Seg n : p in B9} as Element
of Fin X by FINSUB_1:17;
set d = the Element of B9;
let x be Element of X;
reconsider px=x as Permutation of Seg n by MATRIX_1:def 16;
reconsider y=px" as Element of X by MATRIX_1:def 16;
A21: B2 \/ {y} c={p" where p is Permutation of Seg n : p in B9 \/ {x}}
proof
let z be object;
assume z in B2 \/ {y};
then
A22: z in B2 or z in {y} by XBOOLE_0:def 3;
now
per cases by A22,TARSKI:def 1;
case
z in B2;
then consider p being Permutation of Seg n such that
A23: z=p" and
A24: p in B9;
p in B9 \/ {x} by A24,XBOOLE_0:def 3;
hence thesis by A23;
end;
case
A25: z=y;
px in {x} by TARSKI:def 1;
then px in B9 \/ {x} by XBOOLE_0:def 3;
hence thesis by A25;
end;
end;
hence thesis;
end;
A26: B2 c= B
proof
let u be object;
assume u in B2;
then ex p being Permutation of Seg n st p"=u & p in B9;
hence thesis by A2,MATRIX_1:def 16;
end;
assume x in B \ B9;
then
A27: not x in B9 by XBOOLE_0:def 5;
now
assume y in B2;
then consider pp being Permutation of Seg n such that
A28: y=pp" and
A29: pp in B9;
px=(pp")" by A28,FUNCT_1:43;
hence contradiction by A27,A29,FUNCT_1:43;
end;
then
A30: y in B\B2 by A2,XBOOLE_0:def 5;
d in B by A19,A20;
then reconsider pd=d as Permutation of Seg n by A2,MATRIX_1:def 16;
A31: pd" in B2 by A20;
A32: G1.(B9 \/ {.x.})= G0.{p" where p is Permutation of Seg n : p in B9
\/ {x}} & G0.B2=G1.B9 by A11;
{p" where p is Permutation of Seg n : p in B9 \/ {x}} c= B2 \/ {y}
proof
let z be object;
assume z in {p" where p is Permutation of Seg n : p in B9 \/ {x}};
then consider p being Permutation of Seg n such that
A33: z=p" and
A34: p in B9 \/ {x};
now
per cases by A34,XBOOLE_0:def 3;
case
p in B9;
hence z in B2 or z in {y} by A33;
end;
case
p in {x};
then p=x by TARSKI:def 1;
hence z in B2 or z in {y} by A33,TARSKI:def 1;
end;
end;
hence thesis by XBOOLE_0:def 3;
end;
then
B2 \/ {y} ={p" where p is Permutation of Seg n : p in B9 \/ {x}} by A21;
then
G0.{p" where p is Permutation of Seg n : p in B9 \/ {x}} = F.(G0.B2
,f2.y) by A9,A26,A31,A30;
hence thesis by A12,A32,Th35;
end;
end;
A35: for e being Element of Y st e is_a_unity_wrt F holds G1.{} = e
proof
{} is Subset of X by SUBSET_1:1;
then reconsider B3={} as Element of Fin X by FINSUB_1:17;
let e be Element of Y;
{p" where p is Permutation of Seg n : p in B3} c= {}
proof
let s be object;
assume s in {p" where p is Permutation of Seg n : p in B3};
then ex p being Permutation of Seg n st s=p" & p in B3;
hence thesis;
end;
then
A36: {p" where p is Permutation of Seg n : p in B3}= {};
assume e is_a_unity_wrt F;
then G0.{p" where p is Permutation of Seg n : p in B3}=e by A7,A36;
hence thesis by A11;
end;
G1.B =G0.{p" where p is Permutation of Seg n : p in B} by A11;
then I=G1.B by A6,A3,A4,XBOOLE_0:def 10;
then
(the addF of K) $$ (In(Permutations n,Fin Permutations n),
Path_product A) =(the addF
of K) $$ (In(Permutations n,Fin Permutations n),
Path_product(A@)) by A5,A35,A13,A18,SETWISEO:def 3;
hence thesis by A1,MATRIX_3:def 9;
end;