:: Basic Properties of Determinants of Square Matrices over a Field
:: by Karol P\c{a}k
::
:: Received March 21, 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, NAT_1, XBOOLE_0, VECTSP_1, SUBSET_1, FUNCT_2, FINSEQ_1,
FUNCT_1, ARYTM_3, SGRAPH1, XXREAL_0, TARSKI, CARD_1, FINSET_1, ORDINAL1,
RELAT_1, ALGSTR_0, SETWISEO, BINOP_1, STRUCT_0, GROUP_1, ARYTM_1,
FINSUB_1, INT_1, SUPINF_2, ABSVALUE, FINSEQ_2, CARD_3, ORDINAL4,
FINSOP_1, ABIAN, MATRIX_1, TREES_1, ZFMISC_1, INCSP_1, AFINSQ_1,
PARTFUN1, MATRIX_3, RLVECT_1, RVSUM_1, FVSUM_1, FUNCT_5, FUNCT_4,
MATRIX11, FUNCSDOM, VECTSP_2, INT_3, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, CARD_1,
XCMPLX_0, XXREAL_0, FINSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
FUNCT_4, FINSEQ_7, SGRAPH1, FINSEQ_1, BINOP_1, NAT_1, INT_1, STRUCT_0,
ALGSTR_0, NAT_D, RLVECT_1, GROUP_1, VECTSP_1, SETWISEO, SETWOP_2,
FINSEQ_2, FINSEQOP, FINSUB_1, VECTSP_2, FVSUM_1, FUNCT_5, FINSOP_1,
GROUP_4, MATRIX_0, MATRIX_1, MATRIX_3, MATRIX_6, INT_3;
constructors RELAT_2, WELLORD2, SETWISEO, XXREAL_0, NAT_1, NAT_D, INT_1,
FINSOP_1, SETWOP_2, FINSEQ_7, ALGSTR_1, GROUP_4, FVSUM_1, SGRAPH1,
MATRIX_6, MATRIX_1, MATRIX_7, RELSET_1, FUNCT_5, BINOP_1, VECTSP_2,
INT_3, BINOP_2, FINSEQOP, MATRIX_3;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1,
FUNCT_2, FINSET_1, FINSUB_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1,
STRUCT_0, GROUP_1, VECTSP_1, MATRIX_1, FVSUM_1, CARD_1, RELSET_1,
FINSEQ_2, FUNCT_4, MATRIX_6, INT_1, INT_3, FRAENKEL, SGRAPH1;
requirements ARITHM, NUMERALS, REAL, BOOLE, SUBSET;
definitions BINOP_1, TARSKI, XBOOLE_0, VECTSP_1;
equalities BINOP_1, FINSEQ_2, FINSEQ_1, MATRIX_0, MATRIX_3, FVSUM_1, RELAT_1,
ALGSTR_0, ORDINAL1, INT_3, STRUCT_0;
expansions BINOP_1, FINSEQ_1, TARSKI, XBOOLE_0, MATRIX_1, VECTSP_1;
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, FUNCOP_1,
FINSUB_1, FINSEQ_3, RLVECT_1, RELAT_1, FINSOP_1, XBOOLE_0, XBOOLE_1,
GROUP_1, MATRIX_3, FINSEQ_5, GROUP_4, XREAL_1, MATRIX_7, ORDINAL1,
MATRIX_4, CARD_1, CARD_2, MATRIX_9, STIRL2_1, REWRITE1, FINSEQ_7,
SGRAPH1, WELLORD2, FRAENKEL, FUNCT_5, FUNCT_4, NAT_D, XXREAL_0, PARTFUN1,
XTUPLE_0, VECTSP_2, BINOP_2, SUBSET_1, FINSEQ_4;
schemes FUNCT_2, NAT_1, FINSEQ_1, FINSEQ_2, MATRIX_0, BINOP_1, FUNCT_1,
SETWISEO;
begin :: The Sign of a Permutation
reserve x, y for object, X for set,
i, j, k, l, n, m for Nat,
D for non empty set,
K for commutative Ring,
a,b for Element of K,
perm, p, q for Element of Permutations(n),
Perm,P for Permutation of Seg n,
F for Function of Seg n,Seg n,
perm2, p2, q2, pq2 for Element of Permutations(n+2),
Perm2 for Permutation of Seg (n+2);
notation
let X be set;
synonym 2Set(X) for TWOELEMENTSETS(X);
end;
theorem Th1:
X in 2Set Seg n iff ex i,j st i in Seg n & j in Seg n & i < j & X = {i,j}
proof
thus X in 2Set Seg n implies ex i,j st i in Seg n & j in Seg n & i<j & X={i,
j}
proof
assume X in 2Set Seg n;
then consider x,y being object such that
A1: x in Seg n and
A2: y in Seg n and
A3: x<>y and
A4: X={x,y} by SGRAPH1:8;
reconsider x,y as Element of NAT by A1,A2;
x>y or y>x by A3,XXREAL_0:1;
hence thesis by A1,A2,A4;
end;
assume ex i,j st i in Seg n & j in Seg n & i<j & X={i,j};
then consider i,j such that
A5: i in Seg n and
A6: j in Seg n and
A7: i<j and
A8: X={i,j};
{i,j} c= Seg n by A5,A6,ZFMISC_1:32;
hence thesis by A5,A6,A7,A8,SGRAPH1:8;
end;
theorem Th2:
2Set Seg 0 = {} & 2Set Seg 1 = {} by FINSEQ_1:2;
theorem Th3:
for n st n >= 2 holds {1,2} in 2Set Seg n
proof
let n such that
A1: n>=2;
1<=n by A1,XXREAL_0:2;
then
A2: 1 in Seg n;
2 in Seg n by A1;
hence thesis by A2,Th1;
end;
registration
let n;
cluster 2Set Seg(n+2) -> non empty finite;
coherence
proof
n+2>=0+2 by XREAL_1:6;
hence thesis by Th3;
end;
end;
registration
let n, x;
let perm be Element of Permutations(n);
cluster perm.x -> natural;
coherence
proof
per cases;
suppose
A1: x in dom perm;
perm is Permutation of Seg n by MATRIX_1:def 16;
then
A2: rng perm=Seg n by FUNCT_2:def 3;
perm.x in rng perm by A1,FUNCT_1:def 3;
hence thesis by A2;
end;
suppose
not x in dom perm;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
registration
let K;
cluster the multF of K -> having_a_unity;
coherence;
cluster the multF of K -> associative;
coherence;
end;
::------------------------------------------::
:: The partial sign of a permutation ::
::------------------------------------------::
definition
let n,K;
let perm2 be Element of Permutations(n+2);
func Part_sgn(perm2,K) -> Function of 2Set Seg (n+2),the carrier of K means
:Def1:
for i,j be Nat st i in Seg (n+2)& j in Seg (n+2) & i < j
holds ( perm2.i < perm2.j implies it.{i,j}= 1_K ) & ( perm2.i > perm2.j implies
it.{i,j}=-1_K );
existence
proof
set n9=n+2;
defpred P[object,object] means
for i,j be Element of NAT st i in Seg n9 & j in
Seg n9 & i < j & $1={i,j} holds ( perm2.i < perm2.j implies $2=1_K) & ( perm2.i
> perm2.j implies $2=-1_K);
A1: for x being object st x in 2Set Seg n9
ex y being object st y in the carrier of K & P[x,y]
proof
let x be object;
assume x in 2Set Seg n9;
then consider i,j such that
A2: i in Seg n9 and
A3: j in Seg n9 and
A4: i<j and
A5: x={i,j} by Th1;
perm2 is Permutation of Seg n9 by MATRIX_1:def 16;
then
A6: perm2.i <> perm2.j by A2,A3,A4,FUNCT_2:19;
now
per cases by A6,XXREAL_0:1;
case
A7: perm2.i < perm2.j;
P[x,1_K]
proof
let i9,j9 be Element of NAT such that
i9 in Seg n9 and
j9 in Seg n9 and
A8: i9 < j9 and
A9: x={i9,j9};
i=i9 & j=j9 or i=j9 & j=i9 by A5,A9,ZFMISC_1:22;
hence thesis by A4,A7,A8;
end;
hence thesis;
end;
case
A10: perm2.i > perm2.j;
P[x,-1_K]
proof
let i9,j9 be Element of NAT such that
i9 in Seg n9 and
j9 in Seg n9 and
A11: i9 < j9 and
A12: x={i9,j9};
i=i9 & j=j9 or i=j9 & j=i9 by A5,A12,ZFMISC_1:22;
hence thesis by A4,A10,A11;
end;
hence thesis;
end;
end;
hence thesis;
end;
consider Path being Function of 2Set Seg n9,the carrier of K such that
A13: for x being object st x in 2Set Seg n9 holds P[x,Path.x]
from FUNCT_2:sch 1(A1
);
take Path;
let i,j be Nat such that
A14: i in Seg n9 and
A15: j in Seg n9 and
A16: i < j;
{i,j} in 2Set Seg n9 by A14,A15,A16,Th1;
hence thesis by A13,A14,A15,A16;
end;
uniqueness
proof
set n9=n+2;
let P1,P2 be Function of 2Set Seg n9,the carrier of K such that
A17: for i,j be Nat st i in Seg n9 & j in Seg n9 & i < j
holds ( perm2.i < perm2.j implies P1.{i,j}=1_K ) & ( perm2.i > perm2.j implies
P1.{i,j}=-1_K ) and
A18: for i,j be Nat st i in Seg n9 & j in Seg n9 & i < j
holds ( perm2.i < perm2.j implies P2.{i,j}=1_K ) & ( perm2.i > perm2.j implies
P2.{i,j}=-1_K );
for x being object st x in 2Set Seg n9 holds P1.x = P2.x
proof
let x be object;
assume x in 2Set Seg n9;
then consider i,j such that
A19: i in Seg n9 and
A20: j in Seg n9 and
A21: i < j and
A22: x={i,j} by Th1;
perm2 is Permutation of Seg n9 by MATRIX_1:def 16;
then
A23: perm2.i <> perm2.j by A19,A20,A21,FUNCT_2:19;
now
per cases by A23,XXREAL_0:1;
case
A24: perm2.i < perm2.j;
then P1.{i,j}=1_K by A17,A19,A20,A21;
hence thesis by A18,A19,A20,A21,A22,A24;
end;
case
A25: perm2.i > perm2.j;
then P1.{i,j}=-1_K by A17,A19,A20,A21;
hence thesis by A18,A19,A20,A21,A22,A25;
end;
end;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
end;
theorem Th4:
for X be Element of Fin 2Set Seg (n+2) st for x st x in X holds
Part_sgn(p2,K).x = 1_K holds (the multF of K) $$ (X,Part_sgn(p2,K)) = 1_K
proof
let X be Element of Fin 2Set Seg (n+2) such that
A1: for x st x in X holds Part_sgn(p2,K).x = 1_K;
set Path = Part_sgn(p2,K);
set 2S = 2Set Seg (n+2);
set KK = the carrier of K;
set mm = the multF of K;
consider G be Function of Fin 2S,KK such that
A2: mm $$ (X,Path) = G.X and
A3: for e being Element of KK st e is_a_unity_wrt mm holds G.{} = e and
A4: for x being Element of 2S holds G.{x} = Path.x and
A5: for B being Element of Fin 2S st B c= X & B <> {} for x being
Element of 2S st x in X \ B holds G.(B \/ {x}) = mm.(G.B,Path.x) by
SETWISEO:def 3;
defpred P[Nat] means for B be Element of Fin 2S st card B=$1 & B c= X holds
G.B=1_K;
A6: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A7: P[k];
set k1=k+1;
let B be Element of Fin 2S such that
A8: card B=k1 and
A9: B c= X;
now
per cases;
case
k=0;
then consider x being object such that
A10: B={x} by A8,CARD_2:42;
A11: x in B by A10,TARSKI:def 1;
B c= 2S by FINSUB_1:def 5;
then reconsider x as Element of 2S by A11;
G.B=Path.x by A4,A10;
hence thesis by A1,A9,A11;
end;
case
A12: k>0;
consider x being object such that
A13: x in B by A8,CARD_1:27,XBOOLE_0:def 1;
B c= 2S by FINSUB_1:def 5;
then reconsider x as Element of 2S by A13;
A14: Path.x=1_K by A1,A9,A13;
B c= 2S by FINSUB_1:def 5;
then B\{x} c= 2S;
then reconsider B9=B\{x} as Element of Fin 2S by FINSUB_1:def 5;
A15: not x in B9 by ZFMISC_1:56;
then
A16: x in X\B9 by A9,A13,XBOOLE_0:def 5;
A17: {x} \/ B9=B by A13,ZFMISC_1:116;
then
A18: k+1=card B9+1 by A8,A15,CARD_2:41;
then G.B9=1_K by A7,A9,XBOOLE_1:1;
then G.B=1_K * 1_K by A5,A9,A12,A17,A18,A16,A14,CARD_1:27,XBOOLE_1:1;
hence thesis;
end;
end;
hence thesis;
end;
A19: P[0]
proof
let B be Element of Fin 2S such that
A20: card B=0 and
B c= X;
B={} by A20;
hence thesis by A3,FVSUM_1:4;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A19,A6);
then P[card X];
hence thesis by A2;
end;
reserve s for Element of 2Set Seg (n+2);
theorem Th5:
Part_sgn(p2,K).s = 1_K or Part_sgn(p2,K).s = -1_K
proof
consider i,j such that
A1: i in Seg (n+2) and
A2: j in Seg (n+2) and
A3: i < j and
A4: s={i,j} by Th1;
p2 is Permutation of Seg (n+2) by MATRIX_1:def 16;
then p2.i <> p2.j by A1,A2,A3,FUNCT_2:19;
then p2.i > p2.j or p2.i < p2.j by XXREAL_0:1;
hence thesis by A1,A2,A3,A4,Def1;
end;
theorem Th6:
for i,j st i in Seg (n+2) & j in Seg (n+2) & i < j & p2.i = q2.i
& p2.j = q2.j holds Part_sgn(p2,K).{i,j} = Part_sgn(q2,K).{i,j}
proof
set n2=n+2;
let i,j such that
A1: i in Seg n2 and
A2: j in Seg n2 and
A3: i<j and
A4: p2.i=q2.i and
A5: p2.j=q2.j;
reconsider p29=p2 as Permutation of Seg n2 by MATRIX_1:def 16;
A6: p29.i<>p29.j by A1,A2,A3,FUNCT_2:19;
now
per cases by A6,XXREAL_0:1;
suppose
A7: p2.i < p2.j;
then Part_sgn(p2,K).{i,j}=1_K by A1,A2,A3,Def1;
hence thesis by A1,A2,A3,A4,A5,A7,Def1;
end;
suppose
A8: p2.i > p2.j;
then Part_sgn(p2,K).{i,j}=-1_K by A1,A2,A3,Def1;
hence thesis by A1,A2,A3,A4,A5,A8,Def1;
end;
end;
hence thesis;
end;
theorem Th7:
for X be Element of Fin 2Set Seg (n+2),p2,q2 for F be finite set
st F={s:s in X & Part_sgn(p2,K).s <> Part_sgn(q2,K).s} holds (card F mod 2 = 0
implies (the multF of K) $$ (X,Part_sgn(p2,K)) = (the multF of K) $$ (X,
Part_sgn(q2,K)) ) & (card F mod 2 = 1 implies (the multF of K) $$ (X,Part_sgn(
p2,K)) = -(the multF of K) $$ (X,Part_sgn(q2,K)) )
proof
let X be Element of Fin 2Set Seg (n+2);
let p2,q2;
let F be finite set such that
A1: F={s:s in X & Part_sgn(p2,K).s<>Part_sgn(q2,K).s};
set Pq=Part_sgn(q2,K);
set Pp=Part_sgn(p2,K);
set 2S=2Set Seg (n+2);
X c= 2S by FINSUB_1:def 5;
then X\F c= 2S;
then reconsider Y=X\F as Element of Fin 2S by FINSUB_1:def 5;
A2: F c= X
proof
let x be object;
assume x in F;
then ex s st x=s & s in X & Pp.s<>Pq.s by A1;
hence thesis;
end;
then
A3: F\/Y=X by XBOOLE_1:45;
X c= 2S by FINSUB_1:def 5;
then F c= 2S by A2;
then reconsider F9=F as Element of Fin 2S by FINSUB_1:def 5;
set KK=the carrier of K;
set mm=the multF of K;
consider Gp be Function of Fin 2S,KK such that
A4: mm $$ (F9,Pp) = Gp.F and
A5: for e be Element of KK st e is_a_unity_wrt mm holds Gp.{} = e and
A6: for x be Element of 2S holds Gp.{x} = Pp.x and
A7: for B be Element of Fin 2S st B c= F & B <> {} for x being Element
of 2S st x in F9 \ B holds Gp.(B\/{x})= mm.(Gp.B,Pp.x) by SETWISEO:def 3;
A8: Y c=2S by FINSUB_1:def 5;
consider Gq be Function of Fin 2S,KK such that
A9: mm $$ (F9,Pq) = Gq.F and
A10: for e be Element of KK st e is_a_unity_wrt mm holds Gq.{} = e and
A11: for x be Element of 2S holds Gq.{x} = Pq.x and
A12: for B be Element of Fin 2S st B c= F & B <> {} for x be Element of
2S st x in F \ B holds Gq.(B\/{x})= mm.(Gq.B,Pq.x) by SETWISEO:def 3;
defpred P[Nat] means for B be Element of Fin 2S st card B=$1 & B c= F holds
(card B mod 2=0 implies Gp.B=Gq.B) & (card B mod 2=1 implies Gp.B=-Gq.B);
A13: for s st s in F holds Pp.s = -Pq.s
proof
let s;
assume s in F;
then
A14: ex s9 be Element of 2S st s9=s & s9 in X & Pp.s9<>Pq.s9 by A1;
A15: Pq.s=1_K or Pq.s=-1_K by Th5;
Pp.s=1_K or Pp.s=-1_K by Th5;
then Pp.s+Pq.s=0.K by A14,A15,RLVECT_1:def 10;
hence thesis by VECTSP_1:16;
end;
A16: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A17: P[k];
set k1=k+1;
let B be Element of Fin 2S such that
A18: card B=k1 and
A19: B c= F;
now
per cases;
case
A20: k=0;
then consider x being object such that
A21: B={x} by A18,CARD_2:42;
A22: x in B by A21,TARSKI:def 1;
B c= 2S by FINSUB_1:def 5;
then reconsider x as Element of 2S by A22;
A23: Gq.B=Pq.x by A11,A21;
Gp.B=Pp.x by A6,A21;
hence thesis by A13,A18,A19,A20,A22,A23,NAT_D:14;
end;
case
A24: k>0;
consider x being object such that
A25: x in B by A18,CARD_1:27,XBOOLE_0:def 1;
B c= 2S by FINSUB_1:def 5;
then reconsider x as Element of 2S by A25;
B c= 2S by FINSUB_1:def 5;
then B\{x} c= 2S;
then reconsider B9=B\{x} as Element of Fin 2S by FINSUB_1:def 5;
A26: not x in B9 by ZFMISC_1:56;
then
A27: x in F\B9 by A19,A25,XBOOLE_0:def 5;
A28: B9 c= F by A19;
A29: {x} \/ B9=B by A25,ZFMISC_1:116;
then
A30: k+1=card B9+1 by A18,A26,CARD_2:41;
then
A31: Gq.B= mm.(Gq.B9,Pq.x) by A12,A19,A24,A29,A27,CARD_1:27,XBOOLE_1:1;
A32: Gp.B= mm.(Gp.B9,Pp.x) by A7,A19,A24,A29,A30,A27,CARD_1:27,XBOOLE_1:1;
now
per cases by NAT_D:12;
case
A33: k mod 2=0;
0<2-1;
then
A34: k1 mod 2 =0 +1 by A33,NAT_D:70;
A35: Gp.B=Gp.B9*(-Pq.x) by A13,A19,A25,A32;
Gq.B=Gp.B9*Pq.x by A17,A30,A28,A31,A33;
hence thesis by A18,A35,A34,VECTSP_1:8;
end;
case
A36: k mod 2=1;
A37: Pp.x=-Pq.x by A13,A19,A25;
Gp.B9=-Gq.B9 by A17,A30,A28,A36;
then
A38: Gp.B=(-Gq.B9)*(-Pq.x) by A7,A19,A24,A29,A30,A27,A37,CARD_1:27
,XBOOLE_1:1;
A39: 2-1=1;
Gq.B=Gq.B9*Pq.x by A12,A19,A24,A29,A30,A27,CARD_1:27,XBOOLE_1:1;
hence thesis by A18,A36,A38,A39,NAT_D:69,VECTSP_1:10;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
A40: P[0]
proof
let B be Element of Fin 2S such that
A41: card B=0 and
B c= F;
A42: 0=0 mod 2 by NAT_D:26;
A43: B={} by A41;
then Gp.B=1_K by A5,FVSUM_1:4;
hence thesis by A10,A43,A42,FVSUM_1:4;
end;
A44: for k be Nat holds P[k] from NAT_1:sch 2(A40,A16);
A45: Y misses F by XBOOLE_1:79;
then
A46: mm $$(X, Pp) = mm.(mm $$(Y,Pp),mm $$(F9,Pp)) by A3,SETWOP_2:4;
A47: mm $$(X, Pq) = mm.(mm $$(Y,Pq),mm $$(F9,Pq)) by A45,A3,SETWOP_2:4;
A48: dom Pp=2S by FUNCT_2:def 1;
then
A49: dom (Pp|Y)=Y by A8,RELAT_1:62;
dom Pq=2S by FUNCT_2:def 1;
then
A50: dom (Pq|Y)=Y by A8,RELAT_1:62;
for x being object st x in dom (Pp|Y) holds (Pp|Y).x=(Pq|Y).x
proof
let x be object such that
A51: x in dom (Pp|Y);
Y c= 2S by FINSUB_1:def 5;
then reconsider x9=x as Element of 2S by A49,A51;
A52: (Pp|Y).x9=Pp.x9 by A51,FUNCT_1:47;
A53: not x9 in F by A49,A51,XBOOLE_0:def 5;
assume
A54: (Pp|Y).x<>(Pq|Y).x;
(Pq|Y).x9=Pq.x9 by A49,A50,A51,FUNCT_1:47;
hence contradiction by A1,A49,A51,A54,A52,A53;
end;
then
A55: Pp|Y=Pq|Y by A48,A8,A50,FUNCT_1:2,RELAT_1:62;
then
A56: mm $$(Y,Pp) = mm $$(Y,Pq) by SETWOP_2:7;
now
per cases by NAT_D:12;
case
card F mod 2=0;
hence thesis by A4,A9,A44,A56,A46,A47;
end;
case
A57: card F mod 2=1;
A58: mm $$(X, Pq) = (mm $$(Y,Pp))*(mm $$(F9,Pq)) by A55,A47,SETWOP_2:7;
mm $$(X, Pp) = (mm $$(Y,Pp))*(-mm $$(F9,Pq)) by A4,A9,A44,A46,A57;
hence thesis by A57,A58,VECTSP_1:8;
end;
end;
hence thesis;
end;
theorem Th8:
for P be Permutation of Seg n st P is being_transposition for i,j
st i < j holds P.i = j iff i in dom P & j in dom P & P.i=j & P.j=i & for k st k
<> i & k <> j & k in dom P holds P.k = k
proof
let P;
assume P is being_transposition;
then consider i9,j9 be Nat such that
i9 in dom P and
j9 in dom P and
i9<>j9 and
A1: P.i9=j9 and
A2: P.j9=i9 and
A3: for k st k <>i9 & k<>j9 & k in dom P holds P.k=k;
let i,j such that
A4: i < j;
thus P.i=j implies (i in dom P & j in dom P & P.i=j & P.j=i & for k st k<>i
& k<>j & k in dom P holds P.k = k)
proof
A5: dom P=Seg n by FUNCT_2:52;
A6: rng P=Seg n by FUNCT_2:def 3;
assume
A7: P.i=j;
then
A8: i in dom P by A4,FUNCT_1:def 2;
then i=j9 or i=i9 by A4,A3,A7;
hence thesis by A1,A2,A3,A7,A8,A6,A5,FUNCT_1:def 3;
end;
thus thesis;
end;
theorem Th9:
for p2,q2,pq2,i,j st pq2 = p2*q2 & q2 is being_transposition & q2
.i = j & i < j for s st Part_sgn(p2,K).s <> Part_sgn(pq2,K).s holds i in s or j
in s
proof
set n2=n+2;
let p, q, pq be Element of Permutations(n2), i, j such that
A1: pq = p*q and
A2: q is being_transposition and
A3: q.i=j and
A4: i < j;
reconsider q9=q,pq9=pq as Permutation of Seg n2 by MATRIX_1:def 16;
let s be Element of 2Set Seg(n2) such that
A5: Part_sgn(p,K).s<>Part_sgn(pq,K).s;
A6: dom q9=Seg n2 by FUNCT_2:52;
A7: dom pq9=Seg n2 by FUNCT_2:52;
assume that
A8: not i in s and
A9: not j in s;
consider i9,j9 be Nat such that
A10: i9 in Seg n2 and
A11: j9 in Seg n2 and
A12: i9 < j9 and
A13: s={i9,j9} by Th1;
A14: j<>j9 by A13,A9,TARSKI:def 2;
A15: j<>i9 by A13,A9,TARSKI:def 2;
i<>j9 by A13,A8,TARSKI:def 2;
then q.j9=j9 by A2,A3,A4,A11,A14,A6,Th8;
then
A16: pq.j9=p.j9 by A1,A11,A7,FUNCT_1:12;
i<>i9 by A13,A8,TARSKI:def 2;
then q.i9=i9 by A2,A3,A4,A10,A15,A6,Th8;
then pq.i9=p.i9 by A1,A10,A7,FUNCT_1:12;
hence contradiction by A5,A10,A11,A12,A13,A16,Th6;
end;
Lm1: for i,j st i in Seg (n+2) & j in Seg (n+2) & i < j & 1_K<>-1_K holds (
Part_sgn(p2,K).{i,j}=1_K implies p2.i<p2.j)& (Part_sgn(p2,K).{i,j}=-1_K implies
p2.i>p2.j)
proof
set n2=n+2;
let i,j such that
A1: i in Seg n2 and
A2: j in Seg n2 and
A3: i < j and
A4: 1_K<>-1_K;
reconsider p9=p2 as Permutation of Seg n2 by MATRIX_1:def 16;
p9.i<>p9.j by A1,A2,A3,FUNCT_2:19;
then
A5: p2.i<p2.j or p2.i>p2.j by XXREAL_0:1;
thus Part_sgn(p2,K).{i,j}=1_K implies p2.i<p2.j
proof
p9.i<>p9.j by A1,A2,A3,FUNCT_2:19;
then
A6: p2.i<p2.j or p2.i>p2.j by XXREAL_0:1;
assume Part_sgn(p2,K).{i,j}=1_K;
hence thesis by A1,A2,A3,A4,A6,Def1;
end;
assume Part_sgn(p2,K).{i,j}=-1_K;
hence thesis by A1,A2,A3,A4,A5,Def1;
end;
theorem Th10:
for p2,q2,pq2,i,j,K st pq2 = p2*q2 & q2 is being_transposition &
q2.i = j & i < j & 1_K <> -1_K holds Part_sgn(p2,K).{i,j} <> Part_sgn(pq2,K).{i
,j} & for k st k in Seg(n+2) & i <> k & j <> k holds Part_sgn(p2,K).{i,k} <>
Part_sgn(pq2,K).{i,k} iff Part_sgn(p2,K).{j,k} <> Part_sgn(pq2,K).{j,k}
proof
set n2=n+2;
let p, q, pq be Element of Permutations(n2), i, j, K such that
A1: pq = p*q and
A2: q is being_transposition and
A3: q.i=j and
A4: i < j and
A5: 1_K <> -1_K;
A6: i in dom q by A2,A3,A4,Th8;
set P2=Part_sgn(pq,K);
set P1=Part_sgn(p,K);
reconsider p9=p,q9=q,pq9=pq as Permutation of Seg n2 by MATRIX_1:def 16;
A7: dom q9=Seg n2 by FUNCT_2:52;
A8: j in dom q by A2,A3,A4,Th8;
A9: dom pq9=Seg n2 by FUNCT_2:52;
then
A10: pq.i=p.j by A1,A3,A6,A7,FUNCT_1:12;
q.j=i by A2,A3,A4,Th8;
then
A11: pq.j=p.i by A1,A8,A9,A7,FUNCT_1:12;
dom p9=Seg n2 by FUNCT_2:52;
then
A12: p9.i<>p9.j by A4,A6,A8,A7,FUNCT_1:def 4;
now
per cases by A12,XXREAL_0:1;
suppose
A13: p.i < p.j;
then P1.{i,j}=1_K by A4,A6,A8,A7,Def1;
hence P1.{i,j}<>P2.{i,j} by A4,A5,A6,A8,A7,A10,A11,A13,Def1;
end;
suppose
A14: p.i > p.j;
then P1.{i,j}=-1_K by A4,A6,A8,A7,Def1;
hence P1.{i,j}<>P2.{i,j} by A4,A5,A6,A8,A7,A10,A11,A14,Def1;
end;
end;
hence P1.{i,j}<>P2.{i,j};
let k such that
A15: k in Seg n2 and
A16: i <> k and
A17: j <> k;
A18: q.k=k by A2,A3,A4,A7,A15,A16,A17,Th8;
A19: pq.k=p.(q.k) by A1,A9,A15,FUNCT_1:12;
i<k or k<i by A16,XXREAL_0:1;
then
A20: {i,k} in 2Set Seg n2 by A6,A7,A15,Th1;
A21: P1.{i,k} = P2.{i,k} implies P1.{j,k} = P2.{j,k}
proof
A22: j<k or k<j by A17,XXREAL_0:1;
A23: i<k or i>k by A16,XXREAL_0:1;
assume
A24: P1.{i,k} = P2.{i,k};
P1.{k,i}=1_K or P1.{k,i}=-1_K by A20,Th5;
then
pq.j<pq.k & p.j<p.k or pq.j>pq.k & p.j>p.k by A5,A6,A7,A10,A11,A15,A18,A19
,A24,A23,Lm1;
then P2.{j,k}=1_K & P1.{j,k}=1_K or P2.{j,k}=-1_K & P1.{j,k}=-1_K by A8,A7
,A15,A22,Def1;
hence thesis;
end;
j<k or k<j by A17,XXREAL_0:1;
then
A25: {j,k} in 2Set Seg n2 by A8,A7,A15,Th1;
P1.{j,k} = P2.{j,k} implies P1.{i,k} = P2.{i,k}
proof
A26: i<k or k<i by A16,XXREAL_0:1;
A27: j<k or j>k by A17,XXREAL_0:1;
assume
A28: P1.{j,k} = P2.{j,k};
P1.{k,j}=1_K or P1.{k,j}=-1_K by A25,Th5;
then
pq.i<pq.k & p.i<p.k or pq.i>pq.k & p.i>p.k by A5,A8,A7,A10,A11,A15,A18,A19
,A28,A27,Lm1;
then P2.{i,k}=1_K & P1.{i,k}=1_K or P2.{i,k}=-1_K & P1.{i,k}=-1_K by A6,A7
,A15,A26,Def1;
hence thesis;
end;
hence thesis by A21;
end;
::------------------------------------------::
:: The sign of a permutation ::
::------------------------------------------::
definition
let n,K;
let perm2 be Element of Permutations(n+2);
func sgn(perm2,K) -> Element of K equals
(the multF of K) $$ (In (2Set Seg (n+2),Fin 2Set Seg (n+2)),
Part_sgn(perm2,K));
coherence;
end;
theorem Th11:
sgn(p2,K) = 1_K or sgn(p2,K) = -1_K
proof
set KK=the carrier of K;
set n2=n+2;
set 2S=2Set Seg n2;
set mm=the multF of K;
set Path=Part_sgn(p2,K);
2S in Fin 2S by FINSUB_1:def 5; then
In(2S,Fin 2S)=2S by SUBSET_1:def 8;
then reconsider 2S9=2S as Element of Fin 2S;
consider G be Function of Fin 2S, KK such that
A2: mm $$(2S9,Path) = G.2S9 and
A3: for e be Element of KK st e is_a_unity_wrt mm holds G.{} = e and
A4: for s holds G.{s} = Path.s and
A5: for B be Element of Fin 2S st B c= 2S9 & B <> {} for s st s in 2S9 \
B holds G.(B \/ {s}) = mm.(G.B,Path.s) by SETWISEO:def 3;
defpred P[Nat] means for B be Element of Fin 2S st card B=$1 & B c= 2S holds
(G.B=1_K or G.B=-1_K);
A6: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A7: P[k];
set k1=k+1;
let B be Element of Fin 2S such that
A8: card B=k1 and
A9: B c= 2S;
now
per cases;
case
k=0;
then consider x being object such that
A10: B={x} by A8,CARD_2:42;
x in B by A10,TARSKI:def 1;
then reconsider x as Element of 2S by A9;
G.B=Path.x by A4,A10;
hence thesis by Th5;
end;
case
A11: k>0;
consider x being object such that
A12: x in B by A8,CARD_1:27,XBOOLE_0:def 1;
reconsider x as Element of 2S by A9,A12;
B\{x} c= 2S by A9;
then reconsider B9=B\{x} as Element of Fin 2S by FINSUB_1:def 5;
A13: not x in B9 by ZFMISC_1:56;
A14: {x}\/ B9=B by A12,ZFMISC_1:116;
then
A15: k+1=card B9+1 by A8,A13,CARD_2:41;
then
A16: G.B9=1_K or G.B9=-1_K by A7,A9,XBOOLE_1:1;
x in 2S\B9 by A13,XBOOLE_0:def 5;
then G.B=mm.(G.B9,Path.x) by A5,A9,A11,A14,A15,CARD_1:27,XBOOLE_1:1;
then G.B=1_K*1_K or G.B=1_K*(-1_K) or G.B=(-1_K)*1_K or G.B=(-1_K)*(-
1_K) by A16,Th5;
then G.B=1_K*1_K or G.B=1_K*(-1_K) by VECTSP_1:10;
hence thesis;
end;
end;
hence thesis;
end;
A17: P[0]
proof
let B be Element of Fin 2S such that
A18: card B=0 and
B c= 2S;
B={} by A18;
hence thesis by A3,FVSUM_1:4;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A17,A6);
then P[card 2S9];
hence thesis by A2;
end;
theorem Th12:
for Id be Element of Permutations(n+2) st Id = idseq (n+2) holds
sgn(Id,K) = 1_K
proof
set n2=n+2;
let Id be Element of Permutations n2 such that
A1: Id=idseq n2;
set Path=Part_sgn(Id,K);
set 2S=2Set Seg n2;
2S in Fin 2S by FINSUB_1:def 5; then
In (2S,Fin 2S)=2S by SUBSET_1:def 8;
then reconsider 2S9=2S as Element of Fin 2S;
now
let x;
assume x in 2S9;
then consider i,j such that
A3: i in Seg n2 and
A4: j in Seg n2 and
A5: i < j and
A6: x={i,j} by Th1;
A7: Id.j=j by A1,A4,FUNCT_1:18;
Id.i=i by A1,A3,FUNCT_1:18;
hence Path.x=1_K by A3,A4,A5,A6,A7,Def1;
end;
hence thesis by Th4;
end;
Lm2: X in 2Set Seg n & i in X implies i in Seg n & ex j st j in Seg n & i <> j
& X={i,j}
proof
assume that
A1: X in 2Set Seg n and
A2: i in X;
consider i9,j9 be Nat such that
A3: i9 in Seg n and
A4: j9 in Seg n and
A5: i9 < j9 and
A6: X={i9,j9} by A1,Th1;
now
per cases by A2,A6,TARSKI:def 2;
case
i=i9;
hence thesis by A3,A4,A5,A6;
end;
case
i=j9;
hence thesis by A3,A4,A5,A6;
end;
end;
hence thesis;
end;
theorem Th13:
for p2,q2,pq2 st pq2 = p2*q2 & q2 is being_transposition holds
sgn(pq2,K) = -sgn(p2,K)
proof
set n2=n+2;
set 2SS=2Set Seg n2;
let p, q, pq be Element of Permutations n2 such that
A1: pq = p*q and
A2: q is being_transposition;
2SS in Fin 2SS by FINSUB_1:def 5; then
In(2SS,Fin 2SS)=2SS by SUBSET_1:def 8;
then reconsider 2S=2SS as Element of Fin 2SS;
A4: for i,j st i < j & q.i=j holds sgn(pq,K)=-sgn(p,K)
proof
let i,j such that
A5: i < j and
A6: q.i=j;
now
per cases;
suppose
A7: 1_K=-1_K;
then sgn(pq,K)=-1_K by Th11;
hence thesis by A7,Th11;
end;
suppose
A8: 1_K<>-1_K;
set P2=Part_sgn(p,K);
set P1=Part_sgn(pq,K);
A9: P1.{i,j}<>P2.{i,j} by A1,A2,A5,A6,A8,Th10;
defpred P[object,object] means
ex D1 being set st D1 = $1 &
for k st k in D1 & k<>i holds (k<>j implies
$2={j,k}) &(k=j implies $2={i,j});
set D={s:s in 2S & Part_sgn(pq,K).s<>Part_sgn(p,K).s};
D c= 2S
proof
let x be object;
assume x in D;
then ex s st x=s & s in 2S & P1.s<>P2.s;
hence thesis;
end;
then reconsider D as finite set;
set D1={s:s in 2S & P1.s<>P2.s & i in s};
set D2={s:s in 2S & P1.s<>P2.s & j in s};
A10: D1 c= D
proof
let x be object;
assume x in D1;
then ex s st x=s & s in 2S & P1.s<>P2.s & i in s;
hence thesis;
end;
A11: D2 c= D
proof
let x be object;
assume x in D2;
then ex s st x=s & s in 2S & P1.s<>P2.s & j in s;
hence thesis;
end;
then reconsider D1,D2 as finite set by A10;
A12: j in dom q by A2,A5,A6,Th8;
A13: D c= D1\/D2
proof
let x be object;
assume x in D;
then consider s such that
A14: x=s and
s in 2S and
A15: P1.s<>P2.s;
i in s or j in s by A1,A2,A5,A6,A15,Th9;
then x in D1 or x in D2 by A14,A15;
hence thesis by XBOOLE_0:def 3;
end;
D1\/D2 c= D by A10,A11,XBOOLE_1:8;
then
A16: D1\/D2=D by A13;
A17: D1/\D2 c= {{i,j}}
proof
let x be object;
assume
A18: x in D1/\D2;
then x in D1 by XBOOLE_0:def 4;
then
A19: ex s1 be Element of 2SS st x=s1 & s1 in 2S & P1.s1<>P2. s1 & i in s1;
then consider i9,j9 be Nat such that
i9 in Seg n2 and
j9 in Seg n2 and
i9<j9 and
A20: {i9,j9}=x by Th1;
x in D2 by A18,XBOOLE_0:def 4;
then
ex s2 be Element of 2SS st x=s2 & s2 in 2S & P1.s2<>P2. s2 & j in s2;
then
A21: j=i9 or j=j9 by A20,TARSKI:def 2;
i=i9 or i=j9 by A19,A20,TARSKI:def 2;
hence thesis by A5,A20,A21,TARSKI:def 1;
end;
q is Permutation of Seg n2 by MATRIX_1:def 16;
then
A22: dom q=Seg n2 by FUNCT_2:52;
A23: i in dom q by A2,A5,A6,Th8;
then
A24: {i,j} in 2S by A5,A12,A22,Th1;
A25: i in {i,j} by TARSKI:def 2;
then {i,j} in D1 by A24,A9;
then card D1>0;
then reconsider c1=card D1-1 as Nat by NAT_1:20;
A26: j in {i,j} by TARSKI:def 2;
then
A27: {i,j} in D2 by A24,A9;
A28: for x being object st x in D1 ex y be object st y in D2 & P[x,y]
proof
let x be object;
assume x in D1;
then consider s such that
A29: x=s and
s in 2S and
A30: P1.s<>P2.s and
A31: i in s;
consider j9 be Nat such that
A32: j9 in Seg n2 and
A33: j9<>i and
A34: s={i,j9} by A31,Lm2;
now
per cases;
suppose
A35: j9=j;
take X={i,j};
thus X in D2 by A26,A24,A9;
reconsider xx=x as set by TARSKI:1;
take xx;
thus xx = x;
let k such that
A36: k in xx and
k<>i;
thus (k<>j implies X={j,k}) &(k=j implies X={i,j}) by A29,A34,A35
,A36,TARSKI:def 2;
end;
suppose
A37: j9<>j;
take X={j,j9};
j<j9 or j>j9 by A37,XXREAL_0:1;
then
A38: X in 2SS by A12,A22,A32,Th1;
A39: j in X by TARSKI:def 2;
P1.X<>P2.X by A1,A2,A5,A6,A8,A30,A32,A33,A34,A37,Th10;
hence X in D2 by A39,A38;
reconsider xx=x as set by TARSKI:1;
take xx;
thus xx = x;
let k such that
A40: k in xx and
A41: k<>i;
thus (k<>j implies X={j,k}) &(k=j implies X={i,j}) by A29,A34,A37
,A40,A41,TARSKI:def 2;
end;
end;
hence thesis;
end;
consider f be Function of D1,D2 such that
A42: for x being object st x in D1 holds P[x,f.x] from FUNCT_2:sch 1(A28);
A43: {i,j} in D2 by A26,A24,A9;
then
A44: dom f=D1 by FUNCT_2:def 1;
for y be object st y in D2 ex x being object st x in D1 & y = f.x
proof
let y be object;
assume y in D2;
then consider s such that
A45: s=y and
s in 2S and
A46: P1.s<>P2.s and
A47: j in s;
consider i1 be Nat such that
A48: i1 in Seg n2 and
A49: i1<>j and
A50: s={j,i1} by A47,Lm2;
now
per cases;
suppose
A51: i1=i;
A52: {i,j} in D1 by A25,A24,A9;
then P[s,f.s] by A42,A50,A51;
then f.s=y by A5,A26,A45,A50,A51;
hence thesis by A50,A51,A52;
end;
suppose
A53: i1<>i;
then i<i1 or i>i1 by XXREAL_0:1;
then
A54: {i,i1} in 2SS by A23,A22,A48,Th1;
A55: i in {i,i1} by TARSKI:def 2;
P1.{i,i1}<>P2.{i,i1} by A1,A2,A5,A6,A8,A46,A48,A49,A50,A53,Th10;
then
A56: {i,i1} in D1 by A54,A55;
A57: i1 in {i,i1} by TARSKI:def 2;
P[{i,i1},f.{i,i1}] by A42,A56;
then f.{i,i1}={j,i1} by A49,A53,A57;
hence thesis by A45,A50,A56;
end;
end;
hence thesis;
end;
then
A58: rng f=D2 by FUNCT_2:10;
for x1,x2 be object st x1 in D1 & x2 in D1 & f.x1 = f.x2 holds x1 = x2
proof
let x1,x2 be object such that
A59: x1 in D1 and
A60: x2 in D1 and
A61: f.x1 = f.x2;
consider s1 be Element of 2SS such that
A62: x1=s1 and
s1 in 2S and
P1.s1<>P2.s1 and
A63: i in s1 by A59;
consider j1 be Nat such that
j1 in Seg n2 and
A64: i<>j1 and
A65: {i,j1}=s1 by A63,Lm2;
consider s2 be Element of 2SS such that
A66: x2=s2 and
s2 in 2S and
P1.s2<>P2.s2 and
A67: i in s2 by A60;
consider j2 be Nat such that
j2 in Seg n2 and
A68: i<>j2 and
A69: {i,j2}=s2 by A67,Lm2;
A70: j2 in s2 by A69,TARSKI:def 2;
A71: j1 in s1 by A65,TARSKI:def 2;
now
per cases;
case
j=j1 & j=j2;
hence thesis by A62,A65,A66,A69;
end;
case
A72: j<>j1 & j=j2;
P[x2,f.x2] by A42,A60;
then
A73: f.x2={i,j} by A66,A68,A70,A72;
P[x1,f.x1] by A42,A59;
then f.x1={j,j1} by A62,A64,A71,A72;
hence thesis by A5,A61,A64,A67,A69,A72,A73,TARSKI:def 2;
end;
case
A74: j=j1 & j<>j2;
P[x2,f.x2] by A42,A60;
then
A75: f.x2={j,j2} by A66,A68,A70,A74;
P[x1,f.x1] by A42,A59;
then f.x1={i,j} by A62,A64,A71,A74;
hence thesis by A5,A61,A63,A65,A68,A74,A75,TARSKI:def 2;
end;
case
A76: j<>j1 & j<>j2;
P[x2,f.x2] by A42,A60;
then
A77: f.x2={j,j2} by A66,A68,A70,A76;
A78: j1 in {j,j1} by TARSKI:def 2;
P[x1,f.x1] by A42,A59;
then f.x1={j,j1} by A62,A64,A71,A76;
hence thesis by A61,A62,A65,A66,A69,A76,A77,A78,TARSKI:def 2;
end;
end;
hence thesis;
end;
then f is one-to-one by A43,FUNCT_2:19;
then D1,D2 are_equipotent by A58,A44,WELLORD2:def 4;
then
A79: card D1=card D2 by CARD_1:5;
{i,j} in D1 by A25,A24,A9;
then {i,j} in D1/\D2 by A27,XBOOLE_0:def 4;
then { {i,j}} c= D1/\D2 by ZFMISC_1:31;
then D1/\D2 ={{i,j}} by A17;
then card D=card D1+card D1-card{{i,j}} by A79,A16,CARD_2:45
.=(c1+1)+(c1+1)-1 by CARD_1:30
.=2*c1+1;
then card D mod 2=1 mod 2 by NAT_D:21;
hence thesis by Th7,NAT_D:14;
end;
end;
hence thesis;
end;
consider i,j such that
i in dom q and
j in dom q and
A80: i<>j and
A81: q.i=j and
A82: q.j=i and
for k st k <>i & k<>j & k in dom q holds q.k=k by A2;
i<j or j<i by A80,XXREAL_0:1;
hence thesis by A4,A81,A82;
end;
::------------------------------------------::
:: The sign of a transposition ::
::------------------------------------------::
theorem Th14:
for tr be Element of Permutations(n+2) st tr is
being_transposition holds sgn(tr,K) = -1_K
proof
set n2=n+2;
set S=Seg n2;
let tr be Element of Permutations(n2) such that
A1: tr is being_transposition;
reconsider Tr=tr as Permutation of S by MATRIX_1:def 16;
reconsider Id=idseq n2,IdTr=(id S)*Tr as Element of Permutations(n2) by
MATRIX_1:def 16;
rng Tr=S by FUNCT_2:def 3;
then IdTr=Tr by RELAT_1:54;
then sgn(tr,K) = -sgn(Id,K) by A1,Th13;
hence thesis by Th12;
end;
theorem Th15:
for P be FinSequence of Group_of_Perm(n+2), p2 be Element of
Permutations(n+2) st p2 = Product P & (for i st i in dom P ex trans be Element
of Permutations(n+2) st P.i = trans & trans is being_transposition) holds (len
P mod 2=0 implies sgn(p2,K) = 1_K) & (len P mod 2=1 implies sgn(p2,K) = -1_K)
proof
set n2=n+2;
set G=Group_of_Perm(n2);
defpred P[Nat] means for P be FinSequence of G,p2 st p2=Product P & len P=$1
& (for i st i in dom P ex trans be Element of Permutations(n2) st P.i=trans &
trans is being_transposition) holds (len P mod 2=0 implies sgn(p2,K)=1_K) & (
len P mod 2=1 implies sgn(p2,K)=-1_K);
A1: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A2: P[k];
set k1=k+1;
let P be FinSequence of G,p2 such that
A3: p2=Product P and
A4: len P=k1 and
A5: for i st i in dom P ex trans be Element of Permutations(n2) st P.
i=trans & trans is being_transposition;
consider x be object, Q be FinSequence such that
A6: P = <*x*>^Q and
A7: len P = len Q+1 by A4,RELAT_1:38,REWRITE1:5;
reconsider X=<*x*>,Q as FinSequence of G by A6,FINSEQ_1:36;
A8: for i st i in dom Q ex trans be Element of Permutations(n2) st Q.i=
trans & trans is being_transposition
proof
let i such that
A9: i in dom Q;
Q.i=P.(len X+i) by A6,A9,FINSEQ_1:def 7;
hence thesis by A5,A6,A9,FINSEQ_1:28;
end;
1+0<=k1 by XREAL_1:7;
then 1 in Seg k1;
then
A10: 1 in dom P by A4,FINSEQ_1:def 3;
P.1=x by A6,FINSEQ_1:41;
then consider tr be Element of Permutations(n2) such that
A11: x=tr and
A12: tr is being_transposition by A5,A10;
reconsider PQ=Product Q as Element of Permutations(n2) by MATRIX_1:def 17;
reconsider Tr=tr as Element of G by MATRIX_1:def 17;
A13: p2=Tr*Product Q by A3,A6,A11,GROUP_4:7
.=PQ*tr by MATRIX_1:def 17;
then
A14: sgn(p2,K)=-sgn(PQ,K) by A12,Th13;
now
per cases by NAT_D:12;
suppose
A15: len Q mod 2=0;
0<2-1;
then
A16: len P mod 2 =0 +1 by A7,A15,NAT_D:70;
sgn(PQ,K)=1_K by A2,A4,A7,A8,A15;
hence thesis by A12,A13,A16,Th13;
end;
suppose
A17: len Q mod 2=1;
A18: 2-1=1;
sgn(PQ,K)=-1_K by A2,A4,A7,A8,A17;
hence thesis by A7,A14,A17,A18,NAT_D:69,RLVECT_1:17;
end;
end;
hence thesis;
end;
A19: P[0]
proof
let P be FinSequence of G,p2 such that
A20: p2=Product P and
A21: len P=0 and
for i st i in dom P ex trans be Element of Permutations(n2) st P.i=
trans & trans is being_transposition;
P=<*>the carrier of G by A21;
then Product P=1_G by GROUP_4:8;
then Product P=idseq n2 by MATRIX_1:15;
hence thesis by A20,A21,Th12,NAT_D:26;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A19,A1);
hence thesis;
end;
theorem Th16:
for i,j,n st i < j & i in Seg n & j in Seg n ex tr be Element of
Permutations(n) st tr is being_transposition & tr.i = j
proof
let i,j,n such that
A1: i<j and
A2: i in Seg n and
A3: j in Seg n;
defpred P[object,object] means
for k st k in Seg n & k=$1 holds (k=i implies $2=j)
& (k=j implies $2=i) & (k<>i & k<>j implies $2=k);
A4: for x being object st x in Seg n ex y be object st y in Seg n & P[x,y]
proof
let x be object such that
A5: x in Seg n;
reconsider m=x as Nat by A5;
now
per cases;
suppose
m=i;
then P[x,j];
hence thesis by A3;
end;
suppose
m=j;
then P[x,i];
hence thesis by A2;
end;
suppose
m<>i & m<>j;
then P[x,x];
hence thesis by A5;
end;
end;
hence thesis;
end;
consider f be Function of Seg n,Seg n such that
A6: for x being object st x in Seg n holds P[x,f.x] from FUNCT_2:sch 1(A4);
for x1,x2 be object st x1 in Seg n & x2 in Seg n & f.x1 = f.x2 holds x1=x2
proof
let x1,x2 be object such that
A7: x1 in Seg n and
A8: x2 in Seg n and
A9: f.x1=f.x2;
reconsider k1=x1 as Nat by A7;
x1=i or x1=j or x1<>i & x1<>j;
then
A10: x1=i & f.x1=j or x1=j & f.x1=i or x1<>i & x1<>j & f.x1=k1 by A6,A7;
x2=i or x2=j or x2<>i & x2<>j;
hence thesis by A6,A8,A9,A10;
end;
then
A11: f is one-to-one by A2,FUNCT_2:19;
for y being object st y in Seg n ex x being object st x in Seg n & y = f.x
proof
let y being object such that
A12: y in Seg n;
reconsider k=y as Nat by A12;
k=i & f.j=i or k=j & f.i=j or k<>i & k<>j& f.k=k by A2,A3,A6,A12;
hence thesis by A2,A3,A12;
end;
then rng f=Seg n by FUNCT_2:10;
then f is onto by FUNCT_2:def 3;
then reconsider P=f as Element of Permutations(n) by A11,MATRIX_1:def 16;
A13: P.j=i by A3,A6;
dom P=Seg n by A2,FUNCT_2:def 1;
then
A14: for k st k <>i & k<>j & k in dom P holds P.k=k by A6;
take P;
A15: i in dom P by A2,FUNCT_2:def 1;
A16: j in dom P by A3,FUNCT_2:def 1;
P.i=j by A2,A6;
hence thesis by A1,A15,A16,A13,A14;
end;
theorem Th17:
for p be Element of Permutations(k+1) st p.(k+1) <> k+1 ex tr be
Element of Permutations(k+1) st tr is being_transposition & tr.(p.(k+1)) = k+1
& (tr*p).(k+1) = k+1
proof
set k1=k+1;
let p be Element of Permutations(k1) such that
A1: p.k1<>k1;
reconsider p9=p as Permutation of Seg k1 by MATRIX_1:def 16;
A2: dom p9=Seg k1 by FUNCT_2:52;
A3: rng p9=Seg k1 by FUNCT_2:def 3;
A4: k1 in Seg k1 by FINSEQ_1:3;
then
A5: p.k1 in Seg k1 by A2,A3,FUNCT_1:def 3;
then p.k1<=k1 by FINSEQ_1:1;
then p.k1 < k1 by A1,XXREAL_0:1;
then consider tr be Element of Permutations(k1) such that
A6: tr is being_transposition and
A7: tr.(p.k1)=k1 by A4,A5,Th16;
reconsider tr9=tr as Permutation of Seg k1 by MATRIX_1:def 16;
dom tr9=Seg k1 by FUNCT_2:52;
then dom (tr*p)= Seg k1 by A2,A3,RELAT_1:27;
then (tr*p).k1=tr.(p.k1) by FINSEQ_1:3,FUNCT_1:12;
hence thesis by A6,A7;
end;
theorem Th18:
for X,x st not x in X for p1 be Permutation of X\/{x} st p1.x =
x ex p be Permutation of X st p1|X = p
proof
let X,x such that
A1: not x in X;
let p1 be Permutation of X\/{x} such that
A2: p1.x=x;
A3: X c= X\/{x} by XBOOLE_1:7;
set pX=p1|X;
A4: dom p1=X\/{x} by FUNCT_2:52;
then
A5: dom pX=X by RELAT_1:62,XBOOLE_1:7;
A6: rng p1=X\/{x} by FUNCT_2:def 3;
then
A7: rng pX c= X\/{x} by RELAT_1:70;
A8: rng pX c= X
proof
let y be object such that
A9: y in rng pX;
consider x9 be object such that
A10: x9 in dom pX and
A11: pX.x9=y by A9,FUNCT_1:def 3;
assume
A12: not y in X;
y in rng pX by A10,A11,FUNCT_1:def 3;
then y in {x} by A7,A12,XBOOLE_0:def 3;
then
A13: y=x by TARSKI:def 1;
pX.x9=p1.x9 by A10,FUNCT_1:47;
hence thesis by A1,A2,A3,A4,A5,A7,A9,A10,A11,A13,FUNCT_1:def 4;
end;
X c= rng pX
proof
let y be object such that
A14: y in X;
consider x9 be object such that
A15: x9 in dom p1 and
A16: p1.x9=y by A3,A6,A14,FUNCT_1:def 3;
A17: x9 in X
proof
assume not x9 in X;
then x9 in {x} by A4,A15,XBOOLE_0:def 3;
hence thesis by A1,A2,A14,A16,TARSKI:def 1;
end;
then pX.x9=p1.x9 by A5,FUNCT_1:47;
hence thesis by A5,A16,A17,FUNCT_1:def 3;
end;
then
A18: rng pX=X by A8;
A19: pX is one-to-one by FUNCT_1:52;
reconsider pX as Function of X,X by A5,A18,FUNCT_2:1;
pX is onto by A18,FUNCT_2:def 3;
hence thesis by A19;
end;
theorem Th19:
for p,q be (Permutation of X),p1,q1 be Permutation of X\/{x} st
p1|X = p & q1|X = q & p1.x = x & q1.x = x holds (p1*q1) |X = p*q &
(p1*q1).x = x
proof
let p,q be Permutation of X,p1,q1 be Permutation of X\/{x} such that
A1: p1|X=p and
A2: q1|X=q and
A3: p1.x=x and
A4: q1.x=x;
set pq=p*q;
set pq1=p1*q1;
set X1=X\/{x};
A5: X c=X1 by XBOOLE_1:7;
A6: rng q=X by FUNCT_2:def 3;
A7: dom q=X by FUNCT_2:52;
dom pq1=X1 by FUNCT_2:52;
then
A8: dom (pq1|X)=X by RELAT_1:62,XBOOLE_1:7;
A9: dom pq =X by FUNCT_2:52;
A10: dom p=X by FUNCT_2:52;
for y be object st y in dom pq holds pq.y=(pq1|X).y
proof
let y be object such that
A11: y in dom pq;
A12: pq.y=p.(q.y) by A9,A11,FUNCT_2:15;
A13: pq1.y=(pq1|X).y by A9,A8,A11,FUNCT_1:47;
A14: q.y in rng q by A7,A9,A11,FUNCT_1:def 3;
A15: pq1.y=p1.(q1.y) by A5,A9,A11,FUNCT_2:15;
q1.y=q.y by A2,A7,A9,A11,FUNCT_1:47;
hence thesis by A1,A10,A6,A14,A13,A12,A15,FUNCT_1:47;
end;
hence pq1|X = pq by A8,FUNCT_1:2,FUNCT_2:52;
x in {x} by TARSKI:def 1;
then x in X1 by XBOOLE_0:def 3;
hence thesis by A3,A4,FUNCT_2:15;
end;
theorem Th20:
for tr be Element of Permutations(k) st
tr is being_transposition holds tr*tr = idseq k & tr = tr"
proof
set I=idseq k;
let tr be Element of Permutations(k);
assume tr is being_transposition;
then consider i,j such that
i in dom tr and
j in dom tr and
i<>j and
A1: tr.i=j and
A2: tr.j=i and
A3: for m st m <>i & m<>j & m in dom tr holds tr.m=m;
reconsider TR=tr as Permutation of Seg k by MATRIX_1:def 16;
set TT=TR*TR;
A4: dom TT=Seg k by FUNCT_2:52;
A5: dom TR=Seg k by FUNCT_2:52;
A6: for x being object st x in dom TT holds TT.x = I.x
proof
let x being object such that
A7: x in dom TT;
reconsider m=x as Nat by A4,A7;
now
per cases;
suppose
m=i or m=j;
hence TT.m=m by A1,A2,A7,FUNCT_1:12;
end;
suppose
m<>i & m<>j;
then tr.m=m by A3,A4,A5,A7;
hence TT.m=m by A7,FUNCT_1:12;
end;
end;
hence thesis by A4,A7,FUNCT_1:18;
end;
A8: dom I=Seg k;
hence tr*tr = idseq k by A6,FUNCT_1:2,FUNCT_2:52;
rng TR=Seg k by FUNCT_2:def 3;
hence thesis by A4,A8,A5,A6,FUNCT_1:2,42;
end;
::------------------------------------------::
:: A general theorem about ::
:: the representation of a permutation as ::
:: a product of transpositions ::
::------------------------------------------::
theorem Th21:
for perm ex P be FinSequence of Group_of_Perm(n) st perm=Product
P & for i st i in dom P ex trans be Element of Permutations(n) st P.i = trans &
trans is being_transposition
proof
defpred P[Nat] means for perm be Element of Permutations($1) ex P be
FinSequence of Group_of_Perm($1) st perm=Product P & for i st i in dom P ex
trans be Element of Permutations($1) st P.i=trans & trans is
being_transposition;
let perm be Element of Permutations(n);
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A2: P[k];
set k1=k+1;
let p be Element of Permutations(k1);
reconsider p9=p as Permutation of Seg k1 by MATRIX_1:def 16;
set Gk1=Group_of_Perm(k1);
A3: for p be Element of Permutations(k1) st p.k1=k1 ex P be FinSequence of
Group_of_Perm(k1) st p=Product P & for i st i in dom P ex trans be Element of
Permutations(k1) st P.i=trans & trans is being_transposition
proof
set Ik=idseq k;
set Ik1=idseq k1;
set Gk1=Group_of_Perm(k1);
set Gk=Group_of_Perm(k);
let p be Element of Permutations(k1) such that
A4: p.k1=k1;
set mG1=the multF of Gk1;
set mG=the multF of Gk;
reconsider p9=p as Permutation of Seg k1 by MATRIX_1:def 16;
A5: Seg k1=Seg k\/{k1} by FINSEQ_1:9;
then consider pk be Permutation of Seg k such that
A6: p9| (Seg k)=pk by A4,Th18,FINSEQ_3:8;
reconsider pk9=pk as Element of Permutations(k) by MATRIX_1:def 16;
consider P be FinSequence of Gk such that
A7: pk9=Product P and
A8: for i st i in dom P ex trans be Element of Permutations(k) st P
.i=trans & trans is being_transposition by A2;
A9: pk9=mG "**" P by A7,GROUP_4:def 2;
defpred PR[set,set] means for i be Nat, tr be Element of Permutations(k)
st i in dom P & P.i=tr & i=$1 ex newtr be Element of Permutations(k1) st newtr=
$2 & newtr is being_transposition & newtr.k1=k1 & tr=newtr| (Seg k);
A10: not k1 in Seg k by FINSEQ_3:8;
A11: for m be Nat st m in Seg (len P) ex x be Element of Gk1 st PR[m,x]
proof
let m be Nat;
assume m in Seg (len P);
then m in dom P by FINSEQ_1:def 3;
then consider tr be Element of Permutations(k) such that
A12: P.m=tr and
A13: tr is being_transposition by A8;
consider i9,j9 be Nat such that
A14: i9 in dom tr and
A15: j9 in dom tr and
A16: i9<>j9 and
A17: tr.i9=j9 and
A18: tr.j9=i9 and
A19: for k st k <>i9 & k<>j9 & k in dom tr holds tr.k=k by A13;
reconsider tr9=tr as Permutation of Seg k by MATRIX_1:def 16;
consider newt be Function of Seg k1,Seg k1 such that
A20: newt| (Seg k) = tr9 and
A21: newt.k1=k1 by A5,A10,STIRL2_1:57;
A22: newt.j9=tr.j9 by A20,A15,FUNCT_1:47;
A23: Seg k is empty implies Seg k is empty;
then
A24: newt is onto by A5,A20,A21,STIRL2_1:58;
newt is one-to-one by A5,A10,A23,A20,A21,STIRL2_1:58;
then reconsider NT=newt as Element of Permutations(k1) by A24,
MATRIX_1:def 16;
reconsider NT9=NT as Element of Gk1 by MATRIX_1:def 17;
take NT9;
let I be Nat, TR be Element of Permutations(k) such that
I in dom P and
A25: P.I=TR and
A26: I=m;
take NT;
A27: dom tr c= dom newt by A20,RELAT_1:60;
A28: for m st m <>i9 & m<>j9 & m in dom newt holds newt.m=m
proof
A29: dom tr9=Seg k by FUNCT_2:52;
let m such that
A30: m <>i9 and
A31: m<>j9 and
A32: m in dom newt;
dom newt=Seg k1 by FUNCT_2:52;
then m in Seg k or m in {k1} by A5,A32,XBOOLE_0:def 3;
then m in dom tr or m=k1 by A29,TARSKI:def 1;
then tr.m=newt.m&tr.m=m or newt.m=m by A20,A21,A19,A30,A31,FUNCT_1:47
;
hence thesis;
end;
newt.i9=tr.i9 by A20,A14,FUNCT_1:47;
hence thesis by A12,A20,A21,A25,A26,A14,A15,A16,A17,A18,A27,A22,A28;
end;
consider Pr be FinSequence of Gk1 such that
A33: dom Pr = Seg (len P) and
A34: for m be Nat st m in Seg (len P) holds PR[m,Pr.m] from FINSEQ_1
:sch 5(A11);
take Pr;
A35: Product Pr = mG1 "**" Pr by GROUP_4:def 2;
now
per cases;
suppose
A36: len Pr=0;
then
A37: Seg len Pr=0;
A38: Product Pr=the_unity_wrt mG1 by A35,A36,FINSOP_1:def 1;
the_unity_wrt mG1=1_Gk1 by GROUP_1:22;
then
A39: Product Pr=Ik1 by A38,MATRIX_1:15;
len P=0 by A33,A36,FINSEQ_1:def 3;
then
A40: pk9=the_unity_wrt mG by A9,FINSOP_1:def 1;
A41: dom p9=Seg k1 by FUNCT_2:52;
A42: the_unity_wrt mG=1_Gk by GROUP_1:22;
A43: for y being object st y in dom p holds p.y = Ik1.y
proof
let y being object such that
A44: y in dom p;
reconsider y9=y as Nat by A41,A44;
A45: Ik1.y9=y9 by A41,A44,FUNCT_1:18;
A46: dom pk=Seg k by FUNCT_2:52;
y in Seg k or y in {k1} by A5,A41,A44,XBOOLE_0:def 3;
then pk.y=p.y & Ik.y9=y9 or p.k1 =k1 & y=k1 by A4,A6,A46,FUNCT_1:18
,47,TARSKI:def 1;
hence thesis by A40,A42,A45,MATRIX_1:15;
end;
dom Ik1 = Seg k1;
hence thesis by A39,A41,A43,A37,FINSEQ_1:def 3,FUNCT_1:2;
end;
suppose
A47: len Pr>0;
consider fPr be sequence of Gk1 such that
A48: fPr.1=Pr.1 and
A49: for n be Nat st 0 <> n & n < len Pr holds fPr.(n
+ 1) = mG1.(fPr.n,Pr.(n + 1)) and
A50: Product Pr=fPr.(len Pr) by A35,A47,FINSOP_1:def 1;
len P>0 by A33,A47,FINSEQ_1:def 3;
then consider fP be sequence of Gk such that
A51: fP.1=P.1 and
A52: for n be Nat st 0 <> n & n < len P holds fP.(n +
1) = mG.(fP.n,P.(n + 1)) and
A53: pk=fP.(len P) by A9,FINSOP_1:def 1;
A54: len P=len Pr by A33,FINSEQ_1:def 3;
defpred N[Nat] means ($1>0 & $1<=len P) implies ex Prod1 be Element
of Permutations(k1), Prod be Element of Permutations(k) st Prod1=fPr.$1 & fP.$1
=Prod & Prod1| (Seg k)=Prod & Prod1.k1=k1;
A55: for m be Nat st N[m] holds N[m+1]
proof
let m be Nat such that
A56: N[m];
set m1=m+1;
assume that
m1>0 and
A57: m1<=len P;
m1+0>0;
then m1 >=1 by NAT_1:19;
then
A58: m1 in Seg len P by A57;
A59: dom P=Seg len P by FINSEQ_1:def 3;
then consider tr be Element of Permutations(k) such that
A60: P.m1=tr and
tr is being_transposition by A8,A58;
consider tr1 be Element of Permutations(k1) such that
A61: tr1=Pr.m1 and
tr1 is being_transposition and
A62: tr1.k1=k1 and
A63: tr=tr1| (Seg k) by A34,A58,A59,A60;
now
per cases;
suppose
m=0;
hence thesis by A51,A48,A60,A61,A62,A63;
end;
suppose
A64: m>0;
A65: m+0<m+1 by XREAL_1:6;
then consider
Q1 be Element of Permutations(k1), Q be Element of
Permutations(k) such that
A66: Q1=fPr.m and
A67: fP.m=Q and
A68: Q1| (Seg k)=Q and
A69: Q1.k1=k1 by A56,A57,A64,XXREAL_0:2;
reconsider Q,tr as Permutation of Seg k by MATRIX_1:def 16;
reconsider trQ=tr*Q as Element of Permutations(k) by
MATRIX_1:def 16;
A70: m<len P by A57,A65,XXREAL_0:2;
then
A71: fP.m1 = mG.(Q,tr) by A52,A60,A64,A67;
then
A72: fP.m1=trQ by MATRIX_1:def 17;
reconsider Q1,tr1 as Permutation of Seg k1 by MATRIX_1:def 16;
reconsider trQ1=tr1*Q1 as Element of Permutations(k1) by
MATRIX_1:def 16;
A73: trQ1| (Seg k)=trQ by A5,A62,A63,A68,A69,Th19;
len P=len Pr by A33,FINSEQ_1:def 3;
then fPr.m1 = mG1.(Q1,tr1) by A49,A61,A64,A66,A70;
then
A74: fPr.m1=trQ1 by MATRIX_1:def 17;
trQ1.k1=k1 by A5,A62,A63,A68,A69,A71,Th19;
hence thesis by A72,A74,A73;
end;
end;
hence thesis;
end;
A75: N[0];
for m be Nat holds N[m] from NAT_1:sch 2(A75,A55);
then consider
Prod1 be Element of Permutations(k1), Prod be Element of
Permutations(k) such that
A76: Prod1=fPr.(len P) and
A77: fP.(len P)=Prod and
A78: Prod1| (Seg k)=Prod and
A79: Prod1.k1=k1 by A47,A54;
reconsider Prod1 as Permutation of Seg k1 by MATRIX_1:def 16;
A80: dom p9=Seg k1 by FUNCT_2:52;
A81: for y being object st y in dom p holds p.y = Prod1.y
proof
let y be object;
assume y in dom p;
then
A82: y in Seg k or y in {k1} by A5,A80,XBOOLE_0:def 3;
dom pk=Seg k by FUNCT_2:52;
then Prod.y=p.y & Prod.y=Prod1.y or y=k1 & p.k1=Prod1.k1 by A4,A6
,A53,A77,A78,A79,A82,FUNCT_1:47,TARSKI:def 1;
hence thesis;
end;
dom Prod1 = Seg k1 by FUNCT_2:52;
hence p=Product Pr by A50,A54,A76,A80,A81,FUNCT_1:2;
thus for i st i in dom Pr ex trans be Element of Permutations(k1) st
Pr.i=trans & trans is being_transposition
proof
A83: Seg (len P)=dom P by FINSEQ_1:def 3;
let m such that
A84: m in dom Pr;
consider t be Element of Permutations(k) such that
A85: P.m=t and
t is being_transposition by A8,A33,A84,A83;
reconsider m9=m as Element of NAT by ORDINAL1:def 12;
ex T be Element of Permutations(k1) st T=Pr.m9 & T is
being_transposition & T.k1=k1 & t=T| Seg k by A33,A34,A84,A83,A85;
hence thesis;
end;
end;
end;
hence thesis;
end;
now
per cases;
suppose
p.k1=k1;
hence thesis by A3;
end;
suppose
A86: p.k1<>k1;
A87: rng p9=Seg k1 by FUNCT_2:def 3;
consider tr be Element of Permutations(k1) such that
A88: tr is being_transposition and
tr.(p.k1)=k1 and
A89: (tr*p).k1=k1 by A86,Th17;
reconsider tr9=tr as Permutation of Seg k1 by MATRIX_1:def 16;
reconsider trp=tr9*p9 as Element of Permutations(k1)
by MATRIX_1:def 16;
consider P be FinSequence of Gk1 such that
A90: trp=Product P and
A91: for i st i in dom P ex trans be Element of Permutations(k1)
st P.i=trans & trans is being_transposition by A3,A89;
reconsider TRP=trp as Element of Gk1 by MATRIX_1:def 17;
reconsider T=tr as Element of Gk1 by MATRIX_1:def 17;
take PT=P^<*T*>;
Product PT=TRP * T by A90,GROUP_4:6;
hence Product PT=tr*(tr*p) by MATRIX_1:def 17
.=(tr*tr)*p by RELAT_1:36
.=(idseq k1)*p by A88,Th20
.=p by A87,RELAT_1:54;
thus for m st m in dom PT ex trans be Element of Permutations(k1) st
PT.m=trans & trans is being_transposition
proof
set L=len P;
set L1=L+1;
A92: Seg L1=Seg L\/{L1} by FINSEQ_1:9;
len PT=len P + 1 by FINSEQ_2:16;
then
A93: dom PT=Seg L1 by FINSEQ_1:def 3;
let m such that
A94: m in dom PT;
now
per cases by A94,A93,A92,XBOOLE_0:def 3;
suppose
m in Seg L;
then
A95: m in dom P by FINSEQ_1:def 3;
then PT.m=P.m by FINSEQ_1:def 7;
hence thesis by A91,A95;
end;
suppose
m in {L1};
then m=L1 by TARSKI:def 1;
hence thesis by A88,FINSEQ_1:42;
end;
end;
hence thesis;
end;
end;
end;
hence thesis;
end;
A96: P[0]
proof
let perm be Element of Permutations(0);
take <*>the carrier of Group_of_Perm 0;
perm is Permutation of Seg 0 by MATRIX_1:def 16;
then perm=idseq 0;
then perm=1_Group_of_Perm(0) by MATRIX_1:15;
hence thesis by GROUP_4:8;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A96,A1);
hence thesis;
end;
th22:
K is non degenerated well-unital &
K is Fanoian implies 1_K <> -1_K
proof
assume A0: K is non degenerated well-unital;
assume
A1: K is Fanoian;
assume 1_K=-1_K;
then 1_K+1_K=0.K by RLVECT_1:def 10;
hence thesis by A0,A1;
end;
theorem Th22:
K is non degenerated well-unital domRing-like
implies
(K is Fanoian iff 1_K <> -1_K)
proof
assume A0: K is non degenerated well-unital domRing-like;
thus K is Fanoian implies 1_K <> -1_K
proof
assume
A1: K is Fanoian;
assume 1_K=-1_K;
then 1_K+1_K=0.K by RLVECT_1:def 10;
hence thesis by A0,A1;
end;
assume
A2: 1_K <> -1_K;
assume not K is Fanoian;
then consider a being Element of K such that
A3: a+a=0.K and
A4: a<>0.K;
a=a*1_K;
then 0.K=a*(1_K+1_K) by A3,VECTSP_1:def 7;
then 0.K=1_K+1_K by A0,A4,VECTSP_2:def 1;
hence thesis by A2,VECTSP_1:16;
end;
::------------------------------------------::
:: The relation between sign and parity ::
:: of permutations ::
::------------------------------------------::
theorem Th23:
K is Fanoian non degenerated implies
( perm2 is even iff sgn(perm2,K) = 1_K )&
( perm2 is odd iff sgn(perm2,K) = -1_K )
proof
assume A0: K is Fanoian non degenerated;
set n2=n+2;
A1: len Permutations n2 = n2 by MATRIX_1:9;
thus
A2: perm2 is even implies sgn(perm2,K) = 1_K by A1,Th15;
thus sgn(perm2,K)= 1_K implies perm2 is even
proof
assume
A3: sgn(perm2,K)= 1_K;
consider P be FinSequence of Group_of_Perm(n2) such that
A4: perm2=Product P and
A5: for i st i in dom P ex trans be Element of Permutations(n2) st P.i
=trans & trans is being_transposition by Th21;
assume perm2 is odd;
then len P mod 2 <> 0 by A1,A4,A5;
then len P mod 2 = 1 by NAT_D:12;
then sgn(perm2,K)=-1_K by A4,A5,Th15;
hence thesis by A0,A3,th22;
end;
hence thesis by A0,A2,Th11,th22;
end;
::------------------------------------------::
:: The sign of a composition of ::
:: permutations ::
::------------------------------------------::
theorem Th24:
for p2,q2,pq2 st pq2 = p2*q2 holds sgn(pq2,K) = sgn(p2,K)*sgn(q2 ,K)
proof
set n2=n+2;
let p, q, pq be Element of Permutations(n2) such that
A1: pq=p*q;
consider P2 be FinSequence of Group_of_Perm(n2) such that
A2: q=Product P2 and
A3: for i st i in dom P2 ex trans be Element of Permutations(n2) st P2.i
=trans & trans is being_transposition by Th21;
consider P1 be FinSequence of Group_of_Perm(n2) such that
A4: p=Product P1 and
A5: for i st i in dom P1 ex trans be Element of Permutations(n2) st P1.i
=trans & trans is being_transposition by Th21;
set PP=P2^P1;
A6: for i st i in dom PP ex trans be Element of Permutations(n2) st PP.i=
trans & trans is being_transposition
proof
let i such that
A7: i in dom PP;
now
per cases by A7,FINSEQ_1:25;
suppose
A8: i in dom P2;
then P2.i=PP.i by FINSEQ_1:def 7;
hence thesis by A3,A8;
end;
suppose
ex k be Nat st k in dom P1 & i=len P2 + k;
then consider k be Nat such that
A9: k in dom P1 and
A10: i=len P2 + k;
P1.k=PP.i by A9,A10,FINSEQ_1:def 7;
hence thesis by A5,A9;
end;
end;
hence thesis;
end;
A11: Product PP=(Product P2)*(Product P1) by GROUP_4:5
.=pq by A1,A4,A2,MATRIX_1:def 17;
now
per cases by NAT_D:12;
suppose
A12: len P1 mod 2=0 & len P2 mod 2=0;
len PP mod 2=(len P2+len P1) mod 2 by FINSEQ_1:22
.=(0+len P1+0) mod 2 by A12,NAT_D:22
.=0 by A12;
then
A13: sgn(pq,K)=1_K by A11,A6,Th15;
A14: sgn(q,K)=1_K by A2,A3,A12,Th15;
sgn(p,K)=1_K by A4,A5,A12,Th15;
hence thesis by A13,A14;
end;
suppose
A15: len P1 mod 2=1 & len P2 mod 2=0;
len PP mod 2=(len P2+len P1) mod 2 by FINSEQ_1:22
.=(0+len P1+0) mod 2 by A15,NAT_D:22
.=1 by A15;
then
A16: sgn(pq,K)=-1_K by A11,A6,Th15;
A17: sgn(q,K)=1_K by A2,A3,A15,Th15;
sgn(p,K)=-1_K by A4,A5,A15,Th15;
hence thesis by A16,A17;
end;
suppose
A18: len P1 mod 2=0 & len P2 mod 2=1;
len PP mod 2=(len P2+len P1) mod 2 by FINSEQ_1:22
.=(1+len P1) mod 2 by A18,NAT_D:22
.=(1+0) mod 2 by A18,NAT_D:22
.=1 by NAT_D:14;
then
A19: sgn(pq,K)=-1_K by A11,A6,Th15;
A20: sgn(q,K)=-1_K by A2,A3,A18,Th15;
sgn(p,K)=1_K by A4,A5,A18,Th15;
hence thesis by A19,A20;
end;
suppose
A21: len P1 mod 2=1 & len P2 mod 2=1;
len PP mod 2=(len P2+len P1) mod 2 by FINSEQ_1:22
.=(1+len P1) mod 2 by A21,NAT_D:22
.=(1+1) mod 2 by A21,NAT_D:22
.=0 by NAT_D:25;
then
A22: sgn(pq,K)=1_K by A11,A6,Th15;
A23: 1_K*1_K=1_K;
A24: sgn(q,K)=-1_K by A2,A3,A21,Th15;
sgn(p,K)=-1_K by A4,A5,A21,Th15;
hence thesis by A22,A24,A23,VECTSP_1:10;
end;
end;
hence thesis;
end;
Lm3: n<2 implies p is even & p=idseq n
proof
reconsider P=p as Permutation of Seg n by MATRIX_1:def 16;
assume
A1: n<2;
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;
registration
cluster Fanoian non degenerated well-unital domRing-like
commutative for Ring;
existence
proof
set K = INT.Ring;
take K;
K is Fanoian
proof
let a be Element of K;
assume A1: a + a = 0.K;
reconsider aa = a as Element of INT;
aa + aa = 0.K by A1,BINOP_2:def 20; then
2 * aa = 0; then
aa = 0; then
a = 0.K;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th25:
(p is even & q is even or p is odd & q is odd iff p*q is even)
proof
reconsider pq=p*q as Element of Permutations(n) by MATRIX_9:39;
now
per cases;
suppose
A1: n<2;
then pq is even by Lm3;
hence thesis by A1,Lm3;
end;
suppose
n>=2;
then reconsider n2=n-2 as Nat by NAT_1:21;
set K = the Fanoian non degenerated well-unital domRing-like
commutative Ring;
reconsider p9=p,q9=q,pq as Element of Permutations(n2+2);
thus p is even&q is even or p is odd&q is odd implies p*q is even
proof
assume p is even & q is even or p is odd & q is odd;
then sgn(p9,K)=1_K & sgn(q9,K)=1_K or sgn(p9,K)=-1_K & sgn(q9,K)=-1_K
by Th23;
then
A2: sgn(p9,K)*sgn(q9,K)=1_K *1_K by VECTSP_1:10;
sgn(pq,K)=1_K by A2,Th24;
hence thesis by Th23;
end;
thus p*q is even implies ( p is even&q is even or p is odd&q is odd )
proof
assume p*q is even;
then sgn(pq,K)=1_K by Th23;
then
A3: sgn(p9,K)*sgn(q9,K)=1_K by Th24;
assume
A4: not( p is even & q is even or p is odd & q is odd );
now
per cases by A4;
suppose
A5: p is even & q is odd;
then
A6: sgn(q9,K)=-1_K by Th23;
sgn(p9,K)=1_K by A5,Th23;
then sgn(p9,K)*sgn(q9,K)=-1_K by A6;
hence thesis by A3,Th22;
end;
suppose
A7: p is odd & q is even;
then
A8: sgn(q9,K)=1_K by Th23;
sgn(p9,K)=-1_K by A7,Th23;
then sgn(p9,K)*sgn(q9,K)=-1_K by A8;
hence thesis by A3,Th22;
end;
end;
hence thesis;
end;
end;
end;
hence thesis;
end;
theorem Th26:
-(a,perm2) = sgn(perm2,K)*a
proof
A1: len (Permutations (n + 2)) = n + 2 by MATRIX_1:9;
per cases;
suppose
A2: perm2 is even;
then sgn (perm2,K) = 1_K by A1,Th15;
hence sgn (perm2,K)*a = a
.= -(a,perm2) by A2,MATRIX_1:def 20;
end;
suppose A10: perm2 is odd;
consider P being FinSequence of Group_of_Perm (n + 2) such that
A11: perm2 = Product P & for i st i in dom P
ex trans be Element of Permutations(n+2) st P.i = trans &
trans is being_transposition by Th21;
for l being FinSequence of (Group_of_Perm (n + 2))
st perm2 = Product l
& (for i being Nat st i in dom l
ex q being Element of Permutations (n + 2)
st (l.i = q & q is being_transposition))
holds (len l) mod 2 = 1 by A1,A10,NAT_D:12;
then A13: (len P) mod 2 = 1 by A11;
A14: -(a,perm2) = -a by A10,MATRIX_1:def 20;
sgn(perm2,K) = -1_K by A13,A11,Th15;
hence sgn(perm2,K)*a = (-1_K) * a
.= -a by VECTSP_2:29
.= -(a,perm2) by A14;
end;
end;
theorem Th27:
for tr be Element of Permutations(n+2) st tr is
being_transposition holds tr is odd
proof
set K = the Fanoian Field;
let tr be Element of Permutations(n+2);
assume tr is being_transposition;
then sgn(tr,K)=-1_K by Th14;
hence thesis by Th23;
end;
registration
let n;
cluster odd for Permutation of Seg (n+2);
existence
proof
set n2=n+2;
A1: len Permutations n2=n2 by MATRIX_1:9;
n2>=2+0 by XREAL_1:6;
then {1,2} in 2Set Seg n2 by Th3;
then consider i,j such that
A2: i in Seg n2 and
A3: j in Seg n2 and
A4: i < j and
{1,2}={i,j} by Th1;
consider tr be Element of Permutations(n2) such that
A5: tr is being_transposition and
tr.i = j by A2,A3,A4,Th16;
tr is odd by A5,Th27;
hence thesis by A1;
end;
end;
begin :: The Determinant of a Linear Combination of Lines
reserve pD for FinSequence of D,
M for Matrix of n,m,D,
pK,qK for FinSequence of K,
A for Matrix of n,K;
definition
let l, n, m, D;
let M be Matrix of n,m,D;
let pD be FinSequence of D;
func ReplaceLine(M,l,pD) -> Matrix of n,m,D means
:Def3:
len it = len M &
width it = width M & for i,j st [i,j] in Indices M holds (i <> l implies it*(i,
j) = M*(i,j)) & (i = l implies it*(l,j) = pD.j) if len pD = width M otherwise
it = M;
consistency;
existence
proof
thus len pD=width 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 (i <> l implies M1*(i,
j) = M*(i,j)) & (i = l implies M1*(l,j) = pD.j)
proof
reconsider M9=M as Matrix of len M,width M,D by MATRIX_0:51;
reconsider n1=n,m1=m as Element of NAT by ORDINAL1:def 12;
defpred P[set,set,set] means for i,j st i=$1 & j=$2 holds (i <>l implies
$3 = M*(i,j)) & (i = l implies $3 = pD.j);
assume
A1: len pD=width M;
A2: for i,j st [i,j] in [:Seg n1, Seg m1:] ex x being Element of D st P[
i,j,x]
proof
let i,j such that
A3: [i,j] in [:Seg n1, Seg m1:];
now
per cases;
case
A4: i=l;
A5: rng pD c= D by FINSEQ_1:def 4;
n1<>0 by A3,ZFMISC_1:87;
then len pD=m by A1,MATRIX_0:23;
then j in Seg len pD by A3,ZFMISC_1:87;
then j in dom pD by FINSEQ_1:def 3;
then
A6: pD.j in rng pD by FUNCT_1:def 3;
P[i,j,pD.j] by A4;
hence thesis by A6,A5;
end;
case
i<>l;
then P[i,j,M*(i,j)];
hence thesis;
end;
end;
hence thesis;
end;
consider M1 be Matrix of n1,m1,D such that
A7: for i,j 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=width M & (len M1 = len M & width M1 = width M & for i,j st [i
,j] in Indices M holds (i <> l implies M1*(i,j) = M*(i,j)) & (i = l implies M1*
(l,j) = pD.j))& (len M2 = len M & width M2 = width M & for i,j st [i,j] in
Indices M holds (i <> l implies M2*(i,j) = M*(i,j)) & (i = l implies M2*(l,j) =
pD.j)) implies M1=M2
proof
assume len pD=width 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 (i <> l implies M1*(i,j) =
M*(i, j))&(i = l implies M1*(l,j) = pD.j);
assume that
len M2=len M and
width M2=width M and
A16: for i,j st [i,j] in Indices M holds (i <> l implies M2*(i,j) =
M*(i, j))&(i = l implies M2*(l,j) = pD.j);
for i,j st [i,j] in Indices M1 holds M1*(i,j)=M2*(i,j)
proof
let i,j;
assume [i,j] in Indices M1;
then
A17: [i,j] in Indices M by A13,A14,MATRIX_4:55;
then
A18: i=l implies M1*(l,j)=pD.j by A15;
A19: i<>l implies M2*(i,j)=M*(i,j) by A16,A17;
i<>l 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 l, n, m, D;
let M be Matrix of n,m,D;
let pD be FinSequence of D;
synonym RLine(M,l,pD) for ReplaceLine(M,l,pD);
end;
Lm4: for l,M,pD holds Indices M=Indices RLine(M,l,pD) & len M=len RLine(M,l,pD
) & width M=width RLine(M,l,pD)
proof
let l,M,pD;
now
per cases;
case
A1: len pD=width M;
then
A2: width M=width RLine(M,l,pD) by Def3;
len M=len ReplaceLine(M,l,pD) by A1,Def3;
hence thesis by A2,MATRIX_4:55;
end;
case
len pD<>width M;
hence thesis by Def3;
end;
end;
hence thesis;
end;
theorem Th28:
for l,M,pD,i st i in Seg n holds (i = l & len pD = width M
implies Line(RLine(M,l,pD),i) = pD) & (i <> l implies Line(RLine(M,l,pD),i) =
Line(M,i))
proof
let l,M,pD,i such that
A1: i in Seg n;
set R=RLine(M,l,pD);
set LR=Line(R,i);
thus i=l & len pD=width M implies LR=pD
proof
assume that
A2: i=l and
A3: len pD=width M;
A4: width R=len pD by A3,Def3;
A5: now
let j be Nat such that
A6: 1 <=j and
A7: j <= len pD;
A8: j in Seg width R by A4,A6,A7;
n=len R by MATRIX_0:def 2;
then i in dom R by A1,FINSEQ_1:def 3;
then
A9: [i,j] in Indices R by A8,ZFMISC_1:87;
A10: Indices R=Indices M by Lm4;
LR.j=R*(i,j) by A8,MATRIX_0:def 7;
hence LR.j=pD.j by A2,A3,A9,A10,Def3;
end;
len LR=len pD by A4,MATRIX_0:def 7;
hence thesis by A5;
end;
set LM=Line(M,i);
A11: width M=len LM by MATRIX_0:def 7;
A12: width M=width R by Lm4;
assume
A13: i<>l;
A14: now
let j be Nat such that
A15: 1 <=j and
A16: j <= len LM;
A17: j in Seg len LM by A15,A16;
then
A18: LM.j=M*(i,j) by A11,MATRIX_0:def 7;
i in Seg len M by A1,MATRIX_0:def 2;
then i in dom M by FINSEQ_1:def 3;
then
A19: [i,j] in Indices M by A11,A17,ZFMISC_1:87;
A20: LR.j=R*(i,j) by A12,A11,A17,MATRIX_0:def 7;
now
per cases;
case
len pD=width M;
hence LM.j=LR.j by A13,A18,A20,A19,Def3;
end;
case
len pD<>width M;
hence LM.j=LR.j by Def3;
end;
end;
hence LM.j=LR.j;
end;
len LR=width R by MATRIX_0:def 7;
hence thesis by A12,A11,A14;
end;
theorem
for M,pD st len pD=width M for p9 be Element of D* st pD = p9 holds
RLine(M,l,pD) = Replace(M,l,p9)
proof
let M,pD such that
A1: len pD=width M;
set RL=RLine(M,l,pD);
let p9 be Element of D* such that
A2: pD=p9;
set R=Replace(M,l,p9);
A3: len R=len M by FINSEQ_7:5;
A4: now
let i be Nat such that
A5: 1 <= i and
A6: i <=len R;
A7: i in Seg len R by A5,A6;
then
A8: i in dom R by FINSEQ_1:def 3;
A9: i in Seg n by A3,A7,MATRIX_0:def 2;
A10: i in dom M by A3,A7,FINSEQ_1:def 3;
now
per cases;
case
A11: i=l;
then
A12: Line(RL,i)=pD by A1,A9,Th28;
A13: R/.i=R.i by A8,PARTFUN1:def 6;
R/.i=p9 by A3,A5,A6,A11,FINSEQ_7:8;
hence R.i=RL.i by A2,A9,A13,A12,MATRIX_0:52;
end;
case
A14: i<>l;
then
A15: Line(M,i)=Line(RL,i) by A9,Th28;
A16: R.i=R/.i by A8,PARTFUN1:def 6;
A17: M.i=Line(M,i) by A9,MATRIX_0:52;
A18: M/.i=M.i by A10,PARTFUN1:def 6;
R/.i=M/.i by A3,A5,A6,A14,FINSEQ_7:10;
hence R.i=RL.i by A9,A16,A18,A17,A15,MATRIX_0:52;
end;
end;
hence R.i=RL.i;
end;
len M=len RL by Lm4;
hence thesis by A4,FINSEQ_1:14,FINSEQ_7:5;
end;
theorem Th30:
M = RLine(M,l,Line(M,l))
proof
set L=Line(M,l);
set RL=RLine(M,l,L);
A1: width M=len L by MATRIX_0:def 7;
A2: now
let i be Nat such that
A3: 1<= i and
A4: i <= len M;
A5: i in Seg len M by A3,A4;
A6: n=len M by MATRIX_0:def 2;
then
A7: RL.i=Line(RL,i) by A5,MATRIX_0:52;
A8: Line(M,i)=M.i by A5,A6,MATRIX_0:52;
now
per cases;
case
i=l;
hence RL.i=M.i by A1,A5,A6,A8,A7,Th28;
end;
case
i<>l;
hence RL.i=M.i by A5,A6,A8,A7,Th28;
end;
end;
hence RL.i=M.i;
end;
len M=len RL by Lm4;
hence thesis by A2;
end;
Lm5: for K being Ring,
pK being FinSequence of K
for a being Element of K holds len pK = len (a*pK)
proof
let K be Ring, pK be FinSequence of K;
let a be Element of K;
pK is Element of (len pK)-tuples_on the carrier of K by FINSEQ_2:92;
then (a*pK) is Element of (len pK)-tuples_on the carrier of K by FINSEQ_2:113
;
hence thesis by CARD_1:def 7;
end;
Lm6: for pK,qK st len pK=len qK holds len pK=len(pK+qK)
proof
let pK,qK be FinSequence of K;
assume len pK=len qK;
then
A1: qK is Element of (len pK)-tuples_on the carrier of K by FINSEQ_2:92;
pK is Element of (len pK)-tuples_on the carrier of K by FINSEQ_2:92;
then (pK+qK) is Element of (len pK)-tuples_on the carrier of K by A1,
FINSEQ_2:120;
hence thesis by CARD_1:def 7;
end;
theorem Th31:
for l,pK,qK,perm st l in Seg n & len pK = n & len qK = n for M
be Matrix of n,K holds (the multF of K) $$ Path_matrix(perm,RLine(M,l,a * pK +
b * qK)) = a * ((the multF of K) $$ Path_matrix(perm,RLine(M,l,pK))) + b * ((
the multF of K) $$ Path_matrix(perm,RLine(M,l,qK)))
proof
let l,pK,qK,perm such that
A1: l in Seg n and
A2: len pK = n and
A3: len qK = n;
Seg n <> {} by A1;
then
A4: n <> 0 ;
reconsider L=l as Element of NAT by ORDINAL1:def 12;
set mm=the multF of K;
let M be Matrix of n,K;
set Rpq=RLine(M,l,a*pK+b*qK);
set Ppq=Path_matrix(perm,Rpq);
A5: len Ppq=n by MATRIX_3:def 7;
then consider fpq be sequence of the carrier of K such that
A6: fpq.1 = Ppq.1 and
A7: for k be Nat st 0<>k & k<len Ppq holds fpq.(k+1)=mm.(fpq.
k,Ppq.(k+1)) and
A8: mm $$ Ppq=fpq.(len Ppq) by A4,FINSOP_1:def 1;
set Rq=RLine(M,l,qK);
set Pq=Path_matrix(perm,Rq);
A9: len Pq=n by MATRIX_3:def 7;
then consider fq be sequence of the carrier of K such that
A10: fq.1 = Pq.1 and
A11: for k be Nat st 0<>k & k<len Pq holds fq.(k+1)=mm.(fq.k,
Pq.(k+1)) and
A12: mm $$ Pq=fq.(len Pq) by A4,FINSOP_1:def 1;
set Rp=RLine(M,l,pK);
set Pp=Path_matrix(perm,Rp);
A13: len Pp=n by MATRIX_3:def 7;
then consider fp be sequence of the carrier of K such that
A14: fp.1 = Pp.1 and
A15: for k be Nat st 0<>k & k<len Pp holds fp.(k+1)=mm.(fp.k,
Pp.(k+1)) and
A16: mm $$ Pp=fp.(len Pp) by A4,FINSOP_1:def 1;
A17: n>=1 by A4,NAT_1:14;
defpred P[Nat] means (1 <= $1 & $1 < L) implies (fp.$1=fq.$1 & fpq.$1=fp.$1);
A18: for k be Element of NAT st k in Seg n holds (k<>L implies Ppq.k=Pp.k &
Pp.k=Pq.k)& (k=L implies ex Ppk,Pqk be Element of K st Ppk=Pp.k & Pqk=Pq.k &
Ppq.k=a*Ppk+b*Pqk)
proof
let k be Element of NAT such that
A19: k in Seg n;
A20: perm.k in Seg n by A19,MATRIX_7:14;
then reconsider pk=perm.k as Element of NAT;
A21: k in dom Pp by A13,A19,FINSEQ_1:def 3;
A22: k in dom Pq by A9,A19,FINSEQ_1:def 3;
[k,pk] in [:Seg n,Seg n:] by A19,A20,ZFMISC_1:87;
then
A23: [k,pk] in Indices M by MATRIX_0:24;
dom qK=Seg n by A3,FINSEQ_1:def 3;
then
A24: qK/.pk=qK.pk by A19,MATRIX_7:14,PARTFUN1:def 6;
dom pK=Seg n by A2,FINSEQ_1:def 3;
then pK/.pk=pK.pk by A19,MATRIX_7:14,PARTFUN1:def 6;
then reconsider ppk=pK.pk, qpk=qK.pk as Element of K by A24;
A25: len (b*qK)=n by A3,Lm5;
then dom (b*qK) =Seg n by FINSEQ_1:def 3;
then
A26: (b*qK).pk = b*qpk by A19,FVSUM_1:50,MATRIX_7:14;
A27: len (a*pK)=n by A2,Lm5;
then
A28: len (a*pK+b*qK)=n by A25,Lm6;
then
A29: dom (a*pK+b*qK)=Seg n by FINSEQ_1:def 3;
dom (a*pK) =Seg n by A27,FINSEQ_1:def 3;
then
A30: (a*pK).pk = a*ppk by A19,FVSUM_1:50,MATRIX_7:14;
A31: width M=n by MATRIX_0:24;
A32: k in dom Ppq by A5,A19,FINSEQ_1:def 3;
thus k<>L implies Ppq.k=Pp.k & Pp.k=Pq.k
proof
assume
A33: k<>L;
then
A34: Rq*(k,pk)=M*(k,pk) by A3,A23,A31,Def3;
Rp*(k,pk)=M*(k,pk) by A2,A23,A31,A33,Def3;
then
A35: Pp.k=M*(k,pk) by A21,MATRIX_3:def 7;
Rpq*(k,pk)=M*(k,pk) by A28,A23,A31,A33,Def3;
hence thesis by A32,A22,A34,A35,MATRIX_3:def 7;
end;
assume
A36: k=L;
then
A37: Rp*(k,pk)=pK.pk by A2,A23,A31,Def3;
A38: Rq*(k,pk)=qK.pk by A3,A23,A31,A36,Def3;
take ppk,qpk;
Rpq*(k,pk) = (a*pK+b*qK).pk by A28,A23,A31,A36,Def3;
then Rpq*(k,pk)=(a*ppk)+(b*qpk) by A19,A29,A30,A26,FVSUM_1:17,MATRIX_7:14;
hence thesis by A32,A21,A22,A37,A38,MATRIX_3:def 7;
end;
A39: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A40: P[k];
set k1=k+1;
assume that
A41: 1 <= k1 and
A42: k1 < L;
L<=n by A1,FINSEQ_1:1;
then
A43: k1 <= n by A42,XXREAL_0:2;
then
A44: k < n by NAT_1:13;
A45: k1 in Seg n by A41,A43;
now
per cases;
case
k=0;
hence thesis by A6,A14,A10,A18,A42,A45;
end;
case
A46: k>0;
then
A47: fp.k1=mm.(fp.k,Pp.k1) by A13,A15,A44;
A48: 0<k+0 by A46;
A49: fq.k1=mm.(fq.k,Pq.k1) by A9,A11,A44,A46;
fpq.k1=mm.(fpq.k,Ppq.k1) by A5,A7,A44,A46;
hence thesis by A18,A40,A42,A45,A48,A47,A49,NAT_1:13,19;
end;
end;
hence thesis;
end;
defpred Q[Nat] means (1<=$1 & L<=$1 & $1<=n) implies for k be Nat
st $1=k holds fpq.k=a*fp.k+b*fq.k;
A50: P[0];
A51: fpq.L=a*fp.L+b*fq.L
proof
consider PpL,PqL be Element of K such that
A52: PpL=Pp.L and
A53: PqL=Pq.L and
A54: Ppq.L=a*PpL+b*PqL by A1,A18;
A55: L>=1 by A1,FINSEQ_1:1;
now
per cases by A55,XXREAL_0:1;
case
A56: L>1;
then reconsider L1=L-1 as Element of NAT by NAT_1:20;
A57: L1+1>1+0 by A56;
A58: L1<L1+1 by NAT_1:19;
L <= n by A1,FINSEQ_1:1;
then
A59: L1 < n by A58,XXREAL_0:2;
then fp.L=fp.L1*PpL by A13,A15,A52,A57;
then
A60: fp.L1*(a*PpL)=a*fp.L by GROUP_1:def 3;
A61: for k be Nat holds P[k] from NAT_1:sch 2(A50,A39);
A62: 1<=L1 by A57,NAT_1:19;
then fp.L1=fq.L1 by A61,A58;
then fq.L=fp.L1*PqL by A9,A11,A53,A57,A59;
then
A63: fp.L1*(b*PqL)=b*fq.L by GROUP_1:def 3;
fpq.L1=fp.L1 by A61,A58,A62;
then fpq.L=fp.L1*(a*PpL+b*PqL ) by A5,A7,A54,A57,A59;
hence thesis by A60,A63,VECTSP_1:def 7;
end;
case
L=1;
hence thesis by A6,A14,A10,A52,A53,A54;
end;
end;
hence thesis;
end;
A64: for k be Nat st Q[k] holds Q[k+1]
proof
let k be Nat such that
A65: Q[k];
set k1=k+1;
assume that
A66: 1<=k1 and
A67: L<=k1 and
A68: k1<=n;
let k9 be Nat such that
A69: k9=k1;
now
per cases by A67,XXREAL_0:1;
case
k1=L;
hence thesis by A51,A69;
end;
case
A70: k1>L;
A71: k1 in Seg n by A66,A68;
then
A72: Ppq.k1=Pp.k1 by A18,A70;
k1 in dom Pp by A13,A71,FINSEQ_1:def 3;
then Pp/.k1=Pp.k1 by PARTFUN1:def 6;
then reconsider Ppk1=Pp.k1 as Element of K;
A73: k<n by A68,NAT_1:13;
A74: (b*fq.k)*Ppk1=b*(fq.k*Ppk1) by GROUP_1:def 3;
A75: (a*fp.k)*Ppk1=a*(fp.k*Ppk1) by GROUP_1:def 3;
A76: 1<=L by A1,FINSEQ_1:1;
A77: k>=L by A70,NAT_1:13;
then fpq.k=a*fp.k+b*fq.k by A65,A68,A76,NAT_1:13,XXREAL_0:2;
then
A78: fpq.k1=(a*fp.k+b*fq.k)*Ppk1 by A5,A7,A77,A73,A76,A72;
Pp.k1=Pq.k1 by A18,A70,A71;
then
A79: fq.k1=fq.k*Ppk1 by A9,A11,A77,A73,A76;
fp.k1=fp.k*Ppk1 by A13,A15,A77,A73,A76;
hence thesis by A69,A78,A79,A75,A74,VECTSP_1:def 7;
end;
end;
hence thesis;
end;
A80: L<=n by A1,FINSEQ_1:1;
A81: Q[0];
for k be Nat holds Q[k] from NAT_1:sch 2(A81,A64);
hence thesis by A17,A5,A13,A9,A8,A16,A12,A80;
end;
theorem Th32:
for l,pK,qK,perm st l in Seg n & len pK = n & len qK = n for M
be Matrix of n,K holds (Path_product(RLine(M,l,a*pK+b*qK))).perm = a*(
Path_product(RLine(M,l,pK))).perm + b*(Path_product(RLine(M,l,qK))).perm
proof
let l,pK,qK,perm such that
A1: l in Seg n and
A2: len pK = n and
A3: len qK = n;
set mm=the multF of K;
let M be Matrix of n,K;
set Rpq=RLine(M,l,a*pK+b*qK);
set Rp=RLine(M,l,pK);
set Rq=RLine(M,l,qK);
set Ppq=Path_matrix(perm,Rpq);
set Pathpq=Path_product(Rpq);
set Pp=Path_matrix(perm,Rp);
set Pathp=Path_product(Rp);
set Pq=Path_matrix(perm,Rq);
set Pathq=Path_product(Rq);
now
per cases;
case
A4: perm is even;
then mm $$ Ppq=-(mm $$ Ppq,perm) by MATRIX_1:def 20;
then
A5: Pathpq.perm=mm $$ Ppq by MATRIX_3:def 8;
mm $$ Pq=-(mm $$ Pq,perm) by A4,MATRIX_1:def 20;
then
A6: Pathq.perm=mm $$ Pq by MATRIX_3:def 8;
mm $$ Pp=-(mm $$ Pp,perm) by A4,MATRIX_1:def 20;
then Pathp.perm=mm $$ Pp by MATRIX_3:def 8;
hence thesis by A1,A2,A3,A6,A5,Th31;
end;
case
A7: perm is odd;
then -mm $$ Ppq=-(mm $$ Ppq,perm) by MATRIX_1:def 20;
then
A8: Pathpq.perm=-mm$$Ppq by MATRIX_3:def 8;
-mm $$ Pp=-(mm $$ Pp,perm) by A7,MATRIX_1:def 20;
then
A9: Pathp.perm=-mm$$Pp by MATRIX_3:def 8;
A10: -a*(mm $$ Pp)=a*(-mm $$ Pp) by VECTSP_1:8;
-mm $$ Pq=-(mm $$ Pq,perm) by A7,MATRIX_1:def 20;
then
A11: Pathq.perm=-mm$$Pq by MATRIX_3:def 8;
A12: -(a*(mm $$ Pp)+b*(mm $$ Pq))=-(a*(mm $$ Pp))-(b*(mm $$ Pq)) by
VECTSP_1:17;
mm $$ Ppq=a*(mm $$ Pp)+b*(mm $$ Pq) by A1,A2,A3,Th31;
hence thesis by A9,A11,A8,A10,A12,VECTSP_1:8;
end;
end;
hence thesis;
end;
::------------------------------------------::
:: The determinant of a linear ::
:: combination of lines ::
::------------------------------------------::
theorem Th33:
for l, pK, qK st l in Seg n & len pK = n & len qK = n for M be
Matrix of n,K holds Det(RLine(M,l,a*pK+b*qK)) = a*Det(RLine(M,l,pK)) + b*Det(
RLine(M,l,qK))
proof
let l, pK, qK such that
A1: l in Seg n and
A2: len pK = n and
A3: len qK = n;
set P=Permutations(n);
set KK=the carrier of K;
set aa=the addF of K;
let M be Matrix of n,K;
set Rpq=RLine(M,l,a*pK+b*qK);
set Rp=RLine(M,l,pK);
set Rq=RLine(M,l,qK);
set Pathpq=Path_product(Rpq);
set Pathp=Path_product(Rp);
set Pathq=Path_product(Rq);
set F=In (P,Fin P);
P in Fin P by FINSUB_1:def 5; then
A4: F=P by SUBSET_1:def 8;
then consider Gpq be Function of Fin P,KK such that
A5: Det Rpq = Gpq.F and
A6: for e being Element of KK st e is_a_unity_wrt aa holds Gpq.{} = e and
A7: for x being Element of P holds Gpq.{x} = Pathpq.x and
A8: for B9 being Element of Fin P st B9 c= F & B9 <> {} for x being
Element of P st x in F \ B9 holds Gpq.(B9 \/ {x}) = aa.(Gpq.B9,Pathpq.x) by
SETWISEO:def 3;
consider Gq be Function of Fin P,KK such that
A9: Det Rq = Gq.F and
A10: for e being Element of KK st e is_a_unity_wrt aa holds Gq.{} = e and
A11: for x being Element of P holds Gq.{x} = Pathq.x and
A12: for B9 being Element of Fin P st B9 c= F & B9 <> {} for x being
Element of P st x in F \ B9 holds Gq.(B9 \/ {x}) = aa.(Gq.B9,Pathq.x) by A4,
SETWISEO:def 3;
consider Gp be Function of Fin P,KK such that
A13: Det Rp = Gp.F and
A14: for e being Element of KK st e is_a_unity_wrt aa holds Gp.{} = e and
A15: for x being Element of P holds Gp.{x} = Pathp.x and
A16: for B9 being Element of Fin P st B9 c= F & B9 <> {} for x being
Element of P st x in F \ B9 holds Gp.(B9 \/ {x}) = aa.(Gp.B9,Pathp.x) by A4,
SETWISEO:def 3;
defpred P[Nat] means for B be Element of Fin P st card B=$1 holds Gpq.B=a*Gp
.B+b*Gq.B;
A17: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A18: P[k];
let B be Element of Fin P such that
A19: card B=k+1;
now
per cases;
case
k=0;
then consider x being object such that
A20: B={x} by A19,CARD_2:42;
A21: x in B by A20,TARSKI:def 1;
B c= P by FINSUB_1:def 5;
then reconsider x as Element of P by A21;
A22: Gp.B=Pathp.x by A15,A20;
A23: Gq.B=Pathq.x by A11,A20;
Gpq.B=Pathpq.x by A7,A20;
hence thesis by A1,A2,A3,A22,A23,Th32;
end;
case
A24: k>0;
consider x being object such that
A25: x in B by A19,CARD_1:27,XBOOLE_0:def 1;
B c= P by FINSUB_1:def 5;
then reconsider x as Element of P by A25;
B c= P by FINSUB_1:def 5;
then B\{x} c= P;
then reconsider B9=B\{x} as Element of Fin P by FINSUB_1:def 5;
A26: not x in B9 by ZFMISC_1:56;
then
A27: x in F\B9 by A4,XBOOLE_0:def 5;
A28: {x} \/ B9=B by A25,ZFMISC_1:116;
then
A29: k+1=card B9+1 by A19,A26,CARD_2:41;
then
A30: Gpq.B9=a*Gp.B9+b*Gq.B9 by A18;
A31: B9 c= F by A4,FINSUB_1:def 5;
then Gpq.B =aa.(Gpq.B9,Pathpq.x) by A8,A24,A28,A29,A27,CARD_1:27;
then
A32: Gpq.B =(a*Gp.B9+b*Gq.B9)+(a*Pathp.x+b*Pathq.x) by A1,A2,A3,A30,Th32
.=a*Gp.B9+(b*Gq.B9+(a*Pathp.x+b*Pathq.x)) by RLVECT_1:def 3
.=a*Gp.B9+(a*Pathp.x+(b*Gq.B9+b*Pathq.x)) by RLVECT_1:def 3
.=(a*Gp.B9+a*Pathp.x)+(b*Gq.B9+b*Pathq.x) by RLVECT_1:def 3
.=(a*(Gp.B9+Pathp.x))+(b*Gq.B9+b*Pathq.x) by VECTSP_1:def 7
.=(a*(aa.(Gp.B9,Pathp.x)))+(b*(Gq.B9+Pathq.x)) by VECTSP_1:def 7
.=(a*(aa.(Gp.B9,Pathp.x)))+(b*(aa.(Gq.B9,Pathq.x)));
Gp.B =aa.(Gp.B9,Pathp.x) by A16,A24,A28,A29,A27,A31,CARD_1:27;
hence thesis by A12,A24,A28,A29,A27,A31,A32,CARD_1:27;
end;
end;
hence thesis;
end;
A33: P[0]
proof
let B be Element of Fin P;
assume card B=0;
then
A34: B={};
then
A35: Gp.B=0.K by A14,FVSUM_1:6;
A36: Gq.B=0.K by A10,A34,FVSUM_1:6;
Gpq.B=0.K by A6,A34,FVSUM_1:6;
hence thesis by A35,A36,RLVECT_1:4;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A33,A17);
then P[card F];
hence thesis by A5,A13,A9;
end;
theorem Th34:
for K being commutative Ring,
pK being FinSequence of K,
a being Element of K,
A being Matrix of n, K holds
l in Seg n & len pK = n implies Det(RLine(A,l,a*pK)) = a*Det( RLine(A,l,pK))
proof
let K be commutative Ring,
pK be FinSequence of K,
a be Element of K,
A be Matrix of n,K;
assume that
A1: l in Seg n and
A2: len pK = n;
pK is Element of (len pK)-tuples_on the carrier of K by FINSEQ_2:92;
then
A3: a*pK+0.K*pK=(a+0.K)*pK by FVSUM_1:55;
a+0.K=a by RLVECT_1:4;
hence
Det(RLine(A,l,a*pK))=a*Det(RLine(A,l,pK))+0.K*Det(RLine(A,l,pK)) by A1,A2,A3
,Th33
.=a*Det(RLine(A,l,pK)) by RLVECT_1:4;
end;
theorem
l in Seg n implies Det(RLine(A,l,a*Line(A,l))) = a*Det(A)
proof
A1: len Line(A,l)=width A by MATRIX_0:def 7;
assume l in Seg n;
then Det(RLine(A,l,a*Line(A,l)))=a*Det(RLine(A,l,Line(A,l))) by A1,Th34,
MATRIX_0:24;
hence thesis by Th30;
end;
theorem Th36:
l in Seg n & len pK = n & len qK = n implies Det(RLine(A,l,pK+qK
)) = Det(RLine(A,l,pK)) + Det(RLine(A,l,qK))
proof
assume that
A1: l in Seg n and
A2: len pK=n and
A3: len qK=n;
pK is Element of (len pK)-tuples_on the carrier of K by FINSEQ_2:92;
then
A4: 1_K*pK=pK by FVSUM_1:57;
qK is Element of (len pK)-tuples_on the carrier of K by A2,A3,FINSEQ_2:92;
then 1_K*qK=qK by FVSUM_1:57;
hence Det(RLine(A,l,pK+qK))=1_K*Det(RLine(A,l,pK))+1_K*Det(RLine(A,l,qK)) by
A1,A2,A3,A4,Th33
.= Det(RLine(A,l,pK))+1_K*Det(RLine(A,l,qK))
.= Det(RLine(A,l,pK))+Det(RLine(A,l,qK));
end;
Lm7: for F,M holds M*F is Matrix of n,m,D
proof
let F,M;
A1: rng F c=Seg n by RELAT_1:def 19;
len M=n by MATRIX_0:def 2;
then
A2: dom M=Seg n by FINSEQ_1:def 3;
dom F=Seg n by FUNCT_2:52;
then
A3: dom(M*F)=Seg n by A1,A2,RELAT_1:27;
then reconsider Mp=M*F as FinSequence by FINSEQ_1:def 2;
A4: for x st x in rng Mp ex p be FinSequence of D st x = p & len p = m
proof
A5: rng M c= D* by FINSEQ_1:def 4;
let x such that
A6: x in rng Mp;
rng Mp c= rng M by RELAT_1:26;
then x in D* by A6,A5;
then reconsider p=x as FinSequence of D by FINSEQ_1:def 11;
take p;
p in rng M by A6,FUNCT_1:14;
hence thesis by MATRIX_0:def 2;
end;
then reconsider Mp as Matrix of D by MATRIX_0:9;
A7: n is Element of NAT by ORDINAL1:def 12;
len Mp = n & for p be FinSequence of D st p in rng Mp holds len p = m
proof
thus len Mp = n by A3,A7,FINSEQ_1:def 3;
let p be FinSequence of D;
assume p in rng Mp;
then ex q be FinSequence of D st p = q & len q = m by A4;
hence thesis;
end;
hence thesis by MATRIX_0:def 2;
end;
begin :: The Determinant of a Matrix with Permutated Lines
:: and with a Repeated Line
definition
let n, m, D;
let F be Function of Seg n,Seg n;
let M be Matrix of n,m,D;
redefine func M*F -> Matrix of n,m,D means :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
:Def4:
len it = len M & width it
= width M & for i,j,k st [i,j] in Indices M & F.i = k holds it*(i,j)= M*(k,j);
compatibility
proof
reconsider Mf=M*F as Matrix of n,m,D by Lm7;
let Mp be Matrix of n,m,D;
thus Mp=M*F implies len Mp = len M & width Mp = width M & for i,j,k st [i,
j] in Indices M & F.i = k holds Mp*(i,j)=M*(k,j)
proof
A1: rng F c= Seg n by RELAT_1:def 19;
assume
A2: Mp=M*F;
A3: len M=n by MATRIX_0:def 2;
A4: len Mp=n by MATRIX_0:def 2;
A5: now
per cases;
case
A6: n=0;
then width M=0 by A3,MATRIX_0:def 3;
hence width M=width Mp by A4,A6,MATRIX_0:def 3;
end;
case
A7: n>0;
then width M=m by A3,MATRIX_0:20;
hence width M=width Mp by A4,A7,MATRIX_0:20;
end;
end;
hence len Mp = len M & width Mp = width M by A3,MATRIX_0:def 2;
let i,j,k such that
A8: [i,j] in Indices M and
A9: F.i = k;
Indices M=[:Seg n,Seg width M:] by MATRIX_0:25;
then
A10: i in Seg n by A8,ZFMISC_1:87;
then
A11: Line(Mp,i)=Mp.i by MATRIX_0:52;
dom F =Seg n by FUNCT_2:52;
then
A12: F.i in rng F by A10,FUNCT_1:def 3;
len Mp=n by MATRIX_0:25;
then dom Mp=Seg n by FINSEQ_1:def 3;
then Mp.i=M.k by A2,A9,A10,FUNCT_1:12;
then
A13: Line(Mp,i)=Line(M,k) by A9,A12,A1,A11,MATRIX_0:52;
A14: j in Seg width M by A8,ZFMISC_1:87;
then Line(M,k).j=M*(k,j) by MATRIX_0:def 7;
hence thesis by A5,A14,A13,MATRIX_0:def 7;
end;
assume that
A15: len Mp = len M and
A16: width Mp = width M;
assume
A17: for i,j,k st [i,j] in Indices M &F.i=k holds Mp*(i,j)=M*(k,j);
for i,j st [i,j] in Indices Mp holds Mp*(i,j) = Mf*(i,j)
proof
A18: Indices Mp=Indices M by A15,A16,MATRIX_4:55;
let i,j such that
A19: [i,j] in Indices Mp;
Indices Mp=[:Seg n,Seg width M:] by A16,MATRIX_0:25;
then
A20: i in Seg n by A19,ZFMISC_1:87;
then
A21: Line(Mf,i)=Mf.i by MATRIX_0:52;
A22: rng F c= Seg n by RELAT_1:def 19;
dom F =Seg n by FUNCT_2:52;
then
A23: F.i in rng F by A20,FUNCT_1:def 3;
then F.i in Seg n by A22;
then reconsider k=F.i as Element of NAT;
len Mf=n by MATRIX_0:25;
then dom Mf=Seg n by FINSEQ_1:def 3;
then Mf.i=M.k by A20,FUNCT_1:12;
then
A24: Line(Mf,i)=Line(M,k) by A23,A22,A21,MATRIX_0:52;
A25: width M=len Line(M,k) by MATRIX_0:def 7;
A26: width Mf=len Line(Mf,i) by MATRIX_0:def 7;
A27: j in Seg width M by A16,A19,ZFMISC_1:87;
then Line(M,k).j=M*(k,j) by MATRIX_0:def 7;
then Mf*(i,j)=M*(k,j) by A27,A24,A25,A26,MATRIX_0:def 7;
hence thesis by A17,A19,A18;
end;
hence thesis by MATRIX_0:27;
end;
correctness by Lm7;
end;
theorem Th37:
Indices M = Indices (M*F) & for i,j st [i,j] in Indices M ex k
st F.i = k & [k,j] in Indices M & (M*F)*(i,j) = M*(k,j)
proof
set Mp=M*F;
A1: dom F=Seg n by FUNCT_2:52;
A2: width M=width Mp by Def4;
len M=len Mp by Def4;
hence Indices M=Indices Mp by A2,MATRIX_4:55;
let i,j such that
A3: [i,j] in Indices M;
Indices M=[:Seg n,Seg width M:] by MATRIX_0:25;
then i in Seg n by A3,ZFMISC_1:87;
then
A4: F.i in rng F by A1,FUNCT_1:def 3;
A5: rng F c= Seg n by RELAT_1:def 19;
then (F.i) in Seg n by A4;
then reconsider k=F.i as Element of NAT;
j in Seg width M by A3,ZFMISC_1:87;
then [k,j] in [:Seg n,Seg width M:] by A4,A5,ZFMISC_1:87;
then
A6: [k,j] in Indices M by MATRIX_0:25;
Mp*(i,j)=M*(k,j) by A3,Def4;
hence thesis by A6;
end;
theorem Th38:
for M be Matrix of n,m,D,F for k st k in Seg n holds Line(M*F,k) = M.(F.k)
proof
let M be Matrix of n,m,D,F;
let k such that
A1: k in Seg n;
len (M*F)=n by MATRIX_0:def 2;
then k in dom (M*F) by A1,FINSEQ_1:def 3;
then (M*F).k=M.(F.k) by FUNCT_1:12;
hence thesis by A1,MATRIX_0:52;
end;
theorem Th39:
M*(idseq n) = M
proof
reconsider I=idseq n as Permutation of Seg n;
A1: width (M*I) = width M by Def4;
A2: for i,j st [i,j] in Indices M holds M*(i,j) = (M*I)*(i,j)
proof
let i,j such that
A3: [i,j] in Indices M;
[i,j] in [:Seg n,Seg width M:] by A3,MATRIX_0:25;
then
A4: i in Seg n by ZFMISC_1:87;
ex k st I.i = k & [k,j] in Indices M & (M*I)*(i,j)=M*(k,j) by A3,Th37;
hence thesis by A4,FUNCT_1:17;
end;
len (M*I)=len M by Def4;
hence thesis by A1,A2,MATRIX_0:21;
end;
theorem Th40:
for p,Perm,q st q = p*Perm" holds Path_matrix(p,A*Perm) = (
Path_matrix(q,A))*Perm
proof
let p,Perm,q such that
A1: q=p*Perm";
reconsider perm=Perm as Element of Permutations(n) by MATRIX_1:def 16;
set Ap=A*Perm;
set P2= Path_matrix(q,A);
set P1=Path_matrix(p,A*Perm);
A2: dom perm=Seg n by FUNCT_2:52;
A3: p is Permutation of Seg n by MATRIX_1:def 16;
then
A4: dom p=Seg n by FUNCT_2:52;
A5: rng p=Seg n by A3,FUNCT_2:def 3;
A6: q is Permutation of Seg n by MATRIX_1:def 16;
then
A7: dom q=Seg n by FUNCT_2:52;
len P2=n by MATRIX_3:def 7;
then
A8: dom P2=Seg n by FINSEQ_1:def 3;
A9: rng perm=Seg n by FUNCT_2:def 3;
then
A10: dom (P2*perm)=Seg n by A2,A8,RELAT_1:27;
then reconsider P2p=P2*perm as FinSequence by FINSEQ_1:def 2;
A11: len P1=n by MATRIX_3:def 7;
A12: rng q=Seg n by A6,FUNCT_2:def 3;
A13: now
let k be Nat;
assume that
A14: 1<=k and
A15: k<=len P1;
A16: k in Seg n by A11,A14,A15;
then
A17: p.k in Seg n by A4,A5,FUNCT_1:3;
then reconsider pk=p.k as Element of NAT;
A18: k=(perm").(perm.k) by A2,A16,FUNCT_1:34;
[k,pk] in [:Seg n,Seg n:] by A16,A17,ZFMISC_1:87;
then [k,pk] in Indices A by MATRIX_0:24;
then consider permk be Nat such that
A19: perm.k = permk and
A20: [permk,pk] in Indices A and
A21: (Ap)*(k,pk)=A*(permk,pk) by Th37;
dom P2p=Seg n by A2,A9,A8,RELAT_1:27;
then
A22: P2p.k=P2.permk by A16,A19,FUNCT_1:12;
Indices A=[:Seg n,Seg n:] by MATRIX_0:24;
then
A23: permk in Seg n by A20,ZFMISC_1:87;
then q.permk in Seg n by A7,A12,FUNCT_1:3;
then reconsider qpermk=q.permk as Element of NAT;
A24: P2.permk=A*(permk,qpermk) by A8,A23,MATRIX_3:def 7;
A25: dom P1=Seg n by A11,FINSEQ_1:def 3;
q.permk=p.((perm").(perm.k)) by A1,A7,A19,A23,FUNCT_1:12;
hence P2p.k=P1.k by A16,A21,A24,A22,A18,A25,MATRIX_3:def 7;
end;
n is Element of NAT by ORDINAL1:def 12;
then len P2p=n by A10,FINSEQ_1:def 3;
hence thesis by A11,A13,FINSEQ_1:14;
end;
theorem Th41:
for p,Perm,q st q=p*Perm" holds (the multF of K) $$ (Path_matrix
(p,A*Perm)) = (the multF of K) $$ (Path_matrix(q,A))
proof
let p,Perm,q such that
A1: q=p*Perm";
set mm=the multF of K;
set P2= Path_matrix(q,A);
set P1=Path_matrix(p,A*Perm);
now
per cases;
case
A2: n=0;
then len P1=0 by MATRIX_3:def 7;
then
A3: mm $$ P1=the_unity_wrt mm by FINSOP_1:def 1;
len P2=0 by A2,MATRIX_3:def 7;
hence thesis by A3,FINSOP_1:def 1;
end;
case
n+0>0;
then
A4: n>=1 by NAT_1:19;
A5: len P2=n by MATRIX_3:def 7;
A6: Perm is Element of Permutations(n) by MATRIX_1:def 16;
P1 = P2*Perm by A1,Th40;
hence thesis by A4,A5,A6,MATRIX_7:33;
end;
end;
hence thesis;
end;
theorem Th42:
for p2,q2 st q2 = p2" holds sgn(p2,K) = sgn(q2,K)
proof
A1: n+1+1>=0+1 by XREAL_1:6;
let p2,q2;
assume q2=p2";
then
A2: -(1_K,p2)=-(1_K,q2) by A1,MATRIX_7:29;
A3: -(1_K,q2)=sgn(q2,K)*1_K by Th26;
-(1_K,p2)=sgn(p2,K)*1_K by Th26;
then sgn(p2,K)*1_K=sgn(q2,K) by A2,A3,VECTSP_1:def 4;
hence thesis;
end;
theorem Th43:
for M be (Matrix of n+2,K),perm2,Perm2 st perm2=Perm2 for p2,q2
st q2 = p2*Perm2" holds (Path_product(M)).q2 = sgn(perm2,K)*(Path_product(M*
Perm2)).p2
proof
let M be (Matrix of n+2,K),perm2,Perm2 such that
A1: perm2=Perm2;
set P=Permutations(n+2);
set mm=the multF of K;
let p2,q2 such that
A2: q2=p2*Perm2";
reconsider perm29=perm2" as Element of P by MATRIX_7:18;
set PM=mm $$ (Path_matrix(q2,M));
set PMp=mm $$ (Path_matrix(p2,M*Perm2));
sgn(q2,K)=sgn(p2,K)*sgn(perm29,K) by A1,A2,Th24
.=sgn(p2,K)*sgn(perm2,K) by Th42;
then -(PM,q2)=(sgn(perm2,K)*sgn(p2,K))*PM by Th26
.=sgn(perm2,K)*(sgn(p2,K)*PM) by GROUP_1:def 3
.=sgn(perm2,K)*(sgn(p2,K)*PMp) by A2,Th41
.=sgn(perm2,K)*-(PMp,p2) by Th26
.=sgn(perm2,K)*((Path_product(M*Perm2)).p2) by MATRIX_3:def 8;
hence thesis by MATRIX_3:def 8;
end;
theorem Th44:
for perm ex P be Permutation of Permutations(n) st for p be
Element of Permutations(n) holds P.p = p*perm
proof
let perm;
set P=Permutations(n);
defpred g[object,object] means
for p be Element of Permutations(n) st $1=p holds
$2=p*perm;
A1: card P=card P;
A2: for x being object st x in P ex y be object st y in P & g[x,y]
proof
let x be object;
assume x in P;
then reconsider p=x as Element of P;
reconsider pp=p*perm as Element of P by MATRIX_9:39;
take pp;
thus thesis;
end;
consider G be Function of P,P such that
A3: for x being object st x in P holds g[x,G.x] from FUNCT_2:sch 1(A2);
for x1,x2 be object st x1 in P & x2 in P & G.x1 = G.x2 holds x1 = x2
proof
let x1,x2 be object such that
A4: x1 in P and
A5: x2 in P and
A6: G.x1=G.x2;
reconsider p1=x1,p2=x2 as Element of P by A4,A5;
p2 is Permutation of Seg n by MATRIX_1:def 16;
then
A7: dom p2=Seg n by FUNCT_2:52;
A8: G.p2=p2*perm by A3;
A9: G.p1=p1*perm by A3;
perm is Permutation of Seg n by MATRIX_1:def 16;
then
A10: rng perm=Seg n by FUNCT_2:def 3;
p1 is Permutation of Seg n by MATRIX_1:def 16;
then dom p1=Seg n by FUNCT_2:52;
then p1=p1*(id rng perm) by A10,RELAT_1:52
.= p1*(perm*perm") by FUNCT_1:39
.= p2*perm*perm" by A6,A9,A8,RELAT_1:36
.= p2*(perm*perm") by RELAT_1:36
.=p2*(id rng perm) by FUNCT_1:39
.=p2 by A10,A7,RELAT_1:52;
hence thesis;
end;
then
A11: G is one-to-one by FUNCT_2:19;
G is onto by A11,A1,FINSEQ_4:63;
then reconsider G as Permutation of P by A11;
take G;
thus thesis by A3;
end;
theorem Th45:
for M be Matrix of n+2,n+2,K, perm2,Perm2 st perm2=Perm2 holds
Det(M*Perm2) = sgn(perm2,K)*Det(M)
proof
set n2=n+2;
let M be Matrix of n2,n2,K, perm2,Perm2 such that
A1: perm2=Perm2;
set PathM=Path_product(M);
set Mperm=M*Perm2;
set P=Permutations(n2);
set KK=the carrier of K;
set aa=the addF of K;
set PathMp=Path_product(Mperm);
set F=In(P,Fin P);
reconsider perm29=perm2" as Element of P by MATRIX_7:18;
P in Fin P by FINSUB_1:def 5; then
A2: F=P by SUBSET_1:def 8;
then consider GM be Function of Fin P,KK such that
A3: Det M = GM.F and
for e being Element of KK st e is_a_unity_wrt aa holds GM.{} = e and
A4: for x being Element of P holds GM.{x} = PathM.x and
A5: for B9 being Element of Fin P st B9 c= F & B9 <> {} for x being
Element of P st x in F \ B9 holds GM.(B9 \/ {x}) = aa.(GM.B9,PathM.x) by
SETWISEO:def 3;
consider PERM be Permutation of P such that
A6: for p be Element of P holds PERM.p=p*perm29 by Th44;
consider GMp be Function of Fin P,KK such that
A7: Det Mperm = GMp.F and
for e being Element of KK st e is_a_unity_wrt aa holds GMp.{} = e and
A8: for x being Element of P holds GMp.{x} = PathMp.x and
A9: for B9 being Element of Fin P st B9 c= F & B9 <> {} for x being
Element of P st x in F \ B9 holds GMp.(B9 \/ {x}) = aa.(GMp.B9,PathMp.x) by A2,
SETWISEO:def 3;
defpred P[Nat] means $1<>0 implies for B be Element of Fin P st card B=$1
holds sgn(perm2,K)*GMp.B=GM.(PERM.:B);
A10: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A11: P[k];
set k1=k+1;
assume k1<>0;
let B be Element of Fin P such that
A12: card B=k1;
per cases;
suppose
k=0;
then consider x being object such that
A13: B={x} by A12,CARD_2:42;
A14: x in B by A13,TARSKI:def 1;
B c= P by FINSUB_1:def 5;
then reconsider x as Element of P by A14;
A15: GM.{PERM.x}=PathM.(PERM.x) by A4;
A16: PERM.x=x*perm29 by A6;
A17: P=dom PERM by FUNCT_2:52;
GMp.{x}=PathMp.x by A8;
then sgn(perm2,K)* GMp.B = GM.{PERM.x} by A1,A13,A15,A16,Th43;
then sgn(perm2,K)* GMp.B = GM.(Im(PERM,x)) by A17,FUNCT_1:59;
hence thesis by A13;
end;
suppose
A18: k>0;
consider x being object such that
A19: x in B by A12,CARD_1:27,XBOOLE_0:def 1;
B c= P by FINSUB_1:def 5;
then reconsider x as Element of P by A19;
PERM.:(B\{x}) c= rng PERM by RELAT_1:111;
then
A20: PERM.:(B\{x}) c= P by FUNCT_2:def 3;
reconsider Px=PERM.x as Element of P;
A21: Px in {Px} by TARSKI:def 1;
dom PERM=P by FUNCT_2:52;
then
A22: Im(PERM,x)={Px} by FUNCT_1:59;
A23: B c= P by FINSUB_1:def 5;
then B\{x} c= P;
then reconsider
B9=B\{x},PeBx=PERM.:(B\{x}),PeB=PERM.:B as Element of Fin P
by A20,FINSUB_1:def 5;
A24: {x} \/ B9=B by A19,ZFMISC_1:116;
then
A25: PERM.:B=Im(PERM,x)\/PeBx by RELAT_1:120;
PERM.x=x*perm29 by A6;
then
A26: sgn(perm2,K)* PathMp.x = PathM.Px by A1,Th43;
A27: dom PERM=P by FUNCT_2:52;
B9 misses {x} by XBOOLE_1:79;
then B9/\{x}={};
then PERM.:{}={Px}/\PeBx by A22,FUNCT_1:62;
then not Px in PeBx by A21,XBOOLE_0:def 4;
then
A28: Px in F\PeBx by A2,XBOOLE_0:def 5;
A29: B9 c= P by FINSUB_1:def 5;
A30: not x in B9 by ZFMISC_1:56;
then
A31: x in F\B9 by A2,XBOOLE_0:def 5;
A32: k+1=card B9+1 by A12,A24,A30,CARD_2:41;
then ex y being object st y in B9 by A18,CARD_1:27,XBOOLE_0:def 1;
then GM.PeB = aa.(GM.PeBx,PathM.Px) by A2,A5,A20,A25,A22,A28,A29,A27;
then GM.PeB=(sgn(perm2,K)*GMp.B9)+(sgn(perm2,K)*PathMp.x)by A11,A18,A32
,A26
.=sgn(perm2,K)*(GMp.B9+PathMp.x) by VECTSP_1:def 7
.=sgn(perm2,K)*GMp.B by A2,A9,A18,A23,A24,A32,A31,CARD_1:27,XBOOLE_1:1;
hence thesis;
end;
end;
A33: P[0];
A34: for k be Nat holds P[k] from NAT_1:sch 2(A33,A10);
A35: rng PERM=P by FUNCT_2:def 3;
A36: dom PERM=P by FUNCT_2:52;
A37: PERM.:dom PERM=rng PERM by RELAT_1:113;
A38: (1_K)*(1_K)=(-1_K)*(-1_K) by VECTSP_1:10;
A39: sgn(perm2,K)=1_K or sgn(perm2,K)=-1_K by Th11;
card F<>0 by A2;
then sgn(perm2,K)*Det Mperm=Det M by A2,A3,A7,A34,A37,A36,A35;
hence sgn(perm2,K)*Det M = 1_K*Det Mperm by A39,A38,GROUP_1:def 3
.= Det Mperm;
end;
::------------------------------------------::
:: The determinant of a matrix with ::
:: permutated lines ::
::------------------------------------------::
theorem Th46:
for M be (Matrix of n,K),perm,Perm st perm = Perm holds Det(M*
Perm) = -(Det(M),perm)
proof
let M be (Matrix of n,K),perm,Perm such that
A1: Perm=perm;
per cases;
suppose
A2: n<2;
then perm=idseq n by Lm3;
then
A3: M*perm=M by Th39;
perm is even by A2,Lm3;
hence thesis by A1,A3,MATRIX_1:def 20;
end;
suppose
n>=2;
then reconsider n2=n-2 as Nat by NAT_1:21;
reconsider M9=M as Matrix of n2+2,K;
reconsider Perm2=Perm as Permutation of Seg(n2+2);
reconsider perm2=perm as Element of Permutations(n2+2);
Det(M9*Perm2) = sgn(perm2,K)*Det(M9) by A1,Th45;
hence thesis by Th26;
end;
end;
theorem Th47:
for PERM be Permutation of Permutations(n), perm st perm is odd
& for p holds PERM.p = p*perm holds PERM.:{p:p is even} = {q:q is odd}
proof
set P=Permutations(n);
let PERM be Permutation of P, perm such that
A1: perm is odd and
A2: for p holds PERM.p=p*perm;
set E={p:p is even};
set OD={q:q is odd};
for y being object holds y in OD iff
ex x being object st x in dom PERM & x in E & y = PERM.x
proof
let y be object;
thus y in OD implies
ex x being object st x in dom PERM & x in E & y = PERM.x
proof
reconsider perm9=perm" as Element of P by MATRIX_7:18;
A3: dom PERM=P by FUNCT_2:52;
n>=2 by A1,Lm3;
then
A4: n>=1 by XXREAL_0:2;
assume y in OD;
then consider q such that
A5: y=q and
A6: q is odd;
A7: q*(idseq n)=q by MATRIX_1:12;
perm9 is odd by A1,A4,MATRIX_7:28;
then
A8: q*perm9 is even by A6,Th25;
reconsider qp9=q*perm9 as Element of P by MATRIX_9:39;
take qp9;
A9: perm9*perm=idseq n by MATRIX_1:13;
PERM.qp9=qp9*perm by A2;
hence thesis by A5,A3,A9,A7,A8,RELAT_1:36;
end;
given x being object such that
x in dom PERM and
A10: x in E and
A11: y = PERM.x;
consider p such that
A12: p=x and
A13: p is even by A10;
reconsider pp=p*perm as Element of P by MATRIX_9:39;
A14: PERM.x=p*perm by A2,A12;
pp is odd by A1,A13,Th25;
hence thesis by A11,A14;
end;
hence thesis by FUNCT_1:def 6;
end;
Lm8: for n,i,j st i in Seg n & j in Seg n & i<j holds ex ODD,EVEN be finite
set st EVEN ={p:p is even} & ODD = {q:q is odd} & EVEN /\ ODD = {} & EVEN \/
ODD = Permutations(n) & ex PERM be Function of EVEN,ODD, perm st perm is
being_transposition & perm.i=j & dom PERM=EVEN & PERM is bijective & for p st p
in EVEN holds PERM.p=p*perm
proof
let n,i,j such that
A1: i in Seg n and
A2: j in Seg n and
A3: i<j;
set P=Permutations(n);
consider tr be Element of P such that
A4: tr is being_transposition and
A5: tr.i = j by A1,A2,A3,Th16;
{i,j} in 2Set Seg n by A1,A2,A3,Th1;
then reconsider n2=n-2 as Nat by Th2,NAT_1:21,23;
set ODD={q:q is odd};
set EVEN={p:p is even};
A6: EVEN c= P
proof
let x be object;
assume x in EVEN;
then ex p st p=x & p is even;
hence thesis;
end;
A7: ODD c= P
proof
let x be object;
assume x in ODD;
then ex q st q=x & q is odd;
hence thesis;
end;
then reconsider O=ODD,E=EVEN as finite set by A6;
take O,E;
thus E ={p:p is even} & O ={q:q is odd};
thus E /\ O = {}
proof
assume E /\ O <>{};
then consider x being object such that
A8: x in E/\O by XBOOLE_0:def 1;
x in O by A8,XBOOLE_0:def 4;
then
A9: ex q st q=x & q is odd;
x in E by A8,XBOOLE_0:def 4;
then ex p st p=x & p is even;
hence thesis by A9;
end;
thus E \/ O = P
proof
thus E \/ O c= P by A6,A7,XBOOLE_1:8;
let x be object;
assume x in P;
then reconsider p=x as Element of P;
p is even or p is odd;
then p in E or p in O;
hence thesis by XBOOLE_0:def 3;
end;
consider PE be Permutation of P such that
A10: for p holds PE.p=p*tr by Th44;
set PERM=PE|E;
tr is Element of Permutations(n2+2);
then PE.:E=O by A4,A10,Th27,Th47;
then
A11: rng PERM=O by RELAT_1:115;
A12: dom PE=P by FUNCT_2:52;
then
A13: dom PERM=E by A6,RELAT_1:62;
then reconsider PERM as Function of E,O by A11,FUNCT_2:1;
take PERM,tr;
PERM is one-to-one onto by A11,FUNCT_1:52,FUNCT_2:def 3;
hence tr is being_transposition & tr.i=j & dom PERM=E & PERM is bijective by
A4,A5,A6,A12,RELAT_1:62;
let p;
assume p in E;
then PERM.p=PE.p by A13,FUNCT_1:47;
hence thesis by A10;
end;
theorem
for n st n >= 2 ex ODD,EVEN be finite set st EVEN ={p:p is even} & ODD
= {q:q is odd} & EVEN /\ ODD = {} & EVEN \/ ODD =Permutations(n) & card EVEN =
card ODD
proof
let n such that
A1: n >= 2;
1 <= n by A1,XXREAL_0:2;
then
A2: 1 in Seg n;
2 in Seg n by A1;
then consider O,E be finite set such that
A3: E ={p:p is even} & O = {q:q is odd} and
A4: E /\ O = {} & E \/ O = Permutations(n) and
A5: ex P be Function of E,O, perm st perm is being_transposition & perm.
1=2 & dom P=E & P is bijective & for p st p in E holds P.p=p*perm by A2,Lm8;
consider P be Function of E,O, perm such that
perm is being_transposition and
perm.1=2 and
A6: dom P=E and
A7: P is bijective and
for p st p in E holds P.p=p*perm by A5;
rng P=O by A7,FUNCT_2:def 3;
then E,O are_equipotent by A6,A7,WELLORD2:def 4;
then card E=card O by CARD_1:5;
hence thesis by A3,A4;
end;
theorem Th49:
for i,j st i in Seg n & j in Seg n & i < j for M be (Matrix of n
,K) st Line(M,i) = Line(M,j) for p,q,tr be Element of Permutations(n) st q = p*
tr & tr is being_transposition & tr.i=j holds (Path_product M).q = - (
Path_product M).p
proof
let i,j such that
A1: i in Seg n and
A2: j in Seg n and
A3: i < j;
{i,j} in 2Set Seg n by A1,A2,A3,Th1;
then reconsider n2=n-2 as Nat by Th2,NAT_1:21,23;
let M be (Matrix of n,K) such that
A4: Line(M,i) = Line(M,j);
reconsider M9=M as Matrix of n2+2,K;
let p,q,tr be Element of Permutations(n) such that
A5: q = p*tr and
A6: tr is being_transposition and
A7: tr.i=j;
reconsider TR=tr as Permutation of Seg (n2+2) by MATRIX_1:def 16;
set Mt=M9*TR;
A8: for k be Nat st 1 <=k & k <= len M9 holds M9.k=Mt.k
proof
let k be Nat such that
A9: 1 <=k and
A10: k <= len M9;
A11: k in Seg (len M9) by A9,A10;
A12: Line(M,j)=M.j by A2,MATRIX_0:52;
A13: dom TR=Seg n by FUNCT_2:52;
A14: Line(M,i)=M.i by A1,MATRIX_0:52;
A15: len M9=n by MATRIX_0:def 2;
then
A16: Line(Mt,k)=M.(tr.k) by A11,Th38;
per cases;
suppose
k=i;
hence thesis by A1,A4,A7,A16,A14,A12,MATRIX_0:52;
end;
suppose
A17: k=j;
then
A18: M.k=M.i by A2,A4,A14,MATRIX_0:52;
Line(Mt,k)=M.i by A3,A6,A7,A16,A17,Th8;
hence thesis by A2,A17,A18,MATRIX_0:52;
end;
suppose
k<>i & k<>j;
then Line(Mt,k)=M.k by A3,A6,A7,A11,A15,A13,A16,Th8;
hence thesis by A11,A15,MATRIX_0:52;
end;
end;
len Mt=len M9 by Def4;
then
A19: Mt=M by A8;
reconsider Tr=tr,p2=p as Element of Permutations(n2+2);
A20: sgn(Tr,K)=-1_K by A6,Th14;
tr=tr" by A6,Th20;
hence (Path_product M).q = (-1_K)*((Path_product M9).p2)
by A5,A19,A20,Th43
.= -1_K*((Path_product M9).p2) by VECTSP_1:9
.= -(Path_product M).p;
end;
::------------------------------------------::
:: The determinant of a matrix with ::
:: a repeated line ::
::------------------------------------------::
theorem Th50:
for i,j st i in Seg n & j in Seg n & i < j for M be (Matrix of n
,K) st Line(M,i) = Line(M,j) holds Det(M) = 0.K
proof
let i,j such that
A1: i in Seg n and
A2: j in Seg n and
A3: i < j;
set P=Permutations(n);
consider Q,E be finite set such that
E ={p:p is even} & Q = {q:q is odd} and
A4: E /\ Q = {} & E \/ Q = P and
A5: ex P be Function of E,Q,tr be Element of Permutations n st tr is
being_transposition & tr.i=j & dom P=E & P is bijective & for p st p in E holds
P.p=p*tr by A1,A2,A3,Lm8;
A6: E c= P by A4,XBOOLE_1:7;
set KK=the carrier of K;
set aa=the addF of K;
let M be (Matrix of n,K) such that
A7: Line(M,i) = Line(M,j);
A8: Q c= P by A4,XBOOLE_1:7;
set PathM=Path_product(M);
consider PERM be Function of E,Q, tr be Element of Permutations n such that
A9: tr is being_transposition and
A10: tr.i=j and
A11: dom PERM = E and
A12: PERM is bijective and
A13: for p st p in E holds PERM.p=p*tr by A5;
reconsider E,Q as Element of Fin P by A6,A8,FINSUB_1:def 5;
aa is having_a_unity by FVSUM_1:8;
then consider GE be Function of Fin P,KK such that
A14: aa $$ (E,PathM) = GE.E and
A15: for e being Element of KK st e is_a_unity_wrt aa holds GE.{} = e and
A16: for x being Element of P holds GE.{x} = PathM.x and
A17: for B9 being Element of Fin P st B9 c= E & B9 <> {} for x being
Element of P st x in E \ B9 holds GE.(B9 \/ {x}) = aa.(GE.B9,PathM.x) by
SETWISEO:def 3;
A18: E misses Q by A4;
aa is having_a_unity by FVSUM_1:8;
then consider GQ be Function of Fin P,KK such that
A19: aa $$ (Q,PathM) = GQ.Q and
A20: for e being Element of KK st e is_a_unity_wrt aa holds GQ.{} = e and
A21: for x being Element of P holds GQ.{x} = PathM.x and
A22: for B9 being Element of Fin P st B9 c= Q & B9 <> {} for x being
Element of P st x in Q \ B9 holds GQ.(B9 \/ {x}) = aa.(GQ.B9,PathM.x) by
SETWISEO:def 3;
defpred P[Nat] means for B,PB be Element of Fin P st card B=$1 & B c= E &
PERM.:B=PB holds GE.B + GQ.PB = 0.K;
A23: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A24: P[k];
let B,PB be Element of Fin P such that
A25: card B=k+1 and
A26: B c=E and
A27: PERM.:B=PB;
now
per cases;
case
k=0;
then consider x being object such that
A28: B={x} by A25,CARD_2:42;
A29: x in B by A28,TARSKI:def 1;
B c= P by FINSUB_1:def 5;
then reconsider x as Element of P by A29;
x*tr is Element of P by MATRIX_9:39;
then reconsider Px=PERM.x as Element of P by A13,A26,A29;
A30: Im(PERM,x)={Px} by A11,A26,A29,FUNCT_1:59;
A31: GE.{x}=PathM.x by A16;
A32: GQ.{PERM.x}=PathM.(Px) by A21;
Px = x*tr by A13,A26,A29;
then -GE.B=GQ.PB by A1,A2,A3,A7,A9,A10,A27,A28,A31,A32,A30,Th49;
hence thesis by RLVECT_1:def 10;
end;
case
A33: k>0;
consider x being object such that
A34: x in B by A25,CARD_1:27,XBOOLE_0:def 1;
B c= P by FINSUB_1:def 5;
then reconsider x as Element of P by A34;
x*tr is Element of P by MATRIX_9:39;
then reconsider Px=PERM.x as Element of P by A13,A26,A34;
A35: Im(PERM,x)={Px} by A11,A26,A34,FUNCT_1:59;
Px=x*tr by A13,A26,A34;
then
A36: -PathM.x=PathM.Px by A1,A2,A3,A7,A9,A10,Th49;
A37: Q c= P by FINSUB_1:def 5;
B c= P by FINSUB_1:def 5;
then
A38: B\{x} c=P;
A39: rng PERM =Q by A12,FUNCT_2:def 3;
then
A40: Px in Q by A11,A26,A34,FUNCT_1:def 3;
PERM.:(B\{x}) c= rng PERM by RELAT_1:111;
then PERM.:(B\{x})c=P by A39,A37;
then reconsider
B9=B\{x},PeBx=PERM.:(B\{x}) as Element of Fin P
by A38,FINSUB_1:def 5;
A41: Px in {Px} by TARSKI:def 1;
A42: {x} \/ B9=B by A34,ZFMISC_1:116;
then
A43: PERM.:B=Im(PERM,x)\/PeBx by RELAT_1:120;
B9 misses {x} by XBOOLE_1:79;
then B9/\{x}={};
then PERM.:{}={Px}/\PeBx by A12,A35,FUNCT_1:62;
then not Px in PeBx by A41,XBOOLE_0:def 4;
then
A44: Px in Q\PeBx by A40,XBOOLE_0:def 5;
A45: not x in B9 by ZFMISC_1:56;
then
A46: x in E\B9 by A26,A34,XBOOLE_0:def 5;
A47: k+1=card B9+1 by A25,A42,A45,CARD_2:41;
then consider y being object such that
A48: y in B9 by A33,CARD_1:27,XBOOLE_0:def 1;
B\{x} c=E by A26;
then PERM.y in PeBx by A11,A48,FUNCT_1:def 6;
then GQ.PB = aa.(GQ.PeBx,PathM.Px) by A22,A27,A39,A43,A35,A44,
RELAT_1:111;
hence
GQ.PB+GE.B = (GQ.PeBx-PathM.x)+(GE.B9+PathM.x) by A17,A26,A33,A42,A47
,A46,A36,CARD_1:27,XBOOLE_1:1
.= GQ.PeBx+(-PathM.x+(GE.B9+PathM.x)) by RLVECT_1:def 3
.= GQ.PeBx+(GE.B9+(PathM.x-PathM.x)) by RLVECT_1:def 3
.= GQ.PeBx+(GE.B9+0.K) by RLVECT_1:def 10
.= (GQ.PeBx+GE.B9)+0.K by RLVECT_1:def 3
.= 0.K+0.K by A24,A26,A47,XBOOLE_1:1
.=0.K by RLVECT_1:4;
end;
end;
hence thesis;
end;
set F=In(P,Fin P);
P in Fin P by FINSUB_1:def 5; then
A49: P=F by SUBSET_1:def 8;
rng PERM=Q by A12,FUNCT_2:def 3;
then
A50: PERM.:E=Q by A11,RELAT_1:113;
A51: P[0]
proof
let B,PB be Element of Fin P such that
A52: card B=0 and
B c= E and
A53: PERM.:B=PB;
A54: B={} by A52;
then
A55: GE.B=0.K by A15,FVSUM_1:6;
PERM.:{}={};
then GQ.PB=0.K by A20,A53,A54,FVSUM_1:6;
hence thesis by A55,RLVECT_1:def 4;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A51,A23);
then P[card E];
then aa $$ (E,PathM)+aa $$ (Q,PathM)=0.K by A14,A19,A50;
hence thesis by A4,A18,A49,FVSUM_1:8,SETWOP_2:4;
end;
theorem Th51:
for i, j st i in Seg n & j in Seg n & i <> j holds Det RLine(A,i
,Line(A,j)) = 0.K
proof
let i, j such that
A1: i in Seg n and
A2: j in Seg n and
A3: i <> j;
A4: i<j or j<i by A3,XXREAL_0:1;
len Line(A,j) = width A by MATRIX_0:def 7;
then
A5: Line(RLine(A,i,Line(A,j)),i)=Line(A,j) by A1,Th28;
Line(RLine(A,i,Line(A,j)),j)=Line(A,j) by A2,A3,Th28;
hence thesis by A1,A2,A5,A4,Th50;
end;
theorem Th52:
for i, j st i in Seg n & j in Seg n & i <> j holds Det RLine(A,i
,a*Line(A,j)) = 0.K
proof
let i, j such that
A1: i in Seg n and
A2: j in Seg n and
A3: i <> j;
width A = n by MATRIX_0:24;
then len Line(A,j)=n by MATRIX_0:def 7;
hence Det(RLine(A,i,a*Line(A,j))) = a*Det(RLine(A,i,Line(A,j))) by A1,Th34
.= a*0.K by A1,A2,A3,Th51
.= 0.K;
end;
theorem
for i, j st i in Seg n & j in Seg n & i <> j holds Det A = Det RLine(A
,i,Line(A,i) + a*Line(A,j))
proof
let i, j such that
A1: i in Seg n and
A2: j in Seg n and
A3: i <> j;
A4: width A = n by MATRIX_0:24;
then
A5: len Line(A,j)=n by MATRIX_0:def 7;
A6: len Line(A,j)=len (a*Line(A,j)) by Lm5;
len Line(A,i)=n by A4,MATRIX_0:def 7;
hence Det RLine(A,i,Line(A,i)+a*Line(A,j))= Det(RLine(A,i,Line(A,i))) + Det(
RLine(A,i,a*Line(A,j))) by A1,A5,A6,Th36
.=Det(A)+Det(RLine(A,i,a*Line(A,j))) by Th30
.=Det(A)+0.K by A1,A2,A3,Th52
.=Det(A) by RLVECT_1:4;
end;
theorem Th54:
not F in Permutations(n) implies Det(A*F) = 0.K
proof
assume not F in Permutations(n);
then
A1: F is not onto or F is not one-to-one by MATRIX_1:def 16;
card Seg n=card Seg n;
then F is not one-to-one by A1,FINSEQ_4:63;
then consider x,y being object such that
A2: x in dom F and
A3: y in dom F and
A4: F.x = F.y and
A5: x<>y by FUNCT_1:def 4;
A6: dom F=Seg n by FUNCT_2:52;
then reconsider x,y as Nat by A2,A3;
Line(A*F,x)=A.(F.x) by A2,A6,Th38;
then
A7: Line(A*F,x)=Line(A*F,y) by A3,A4,A6,Th38;
x>y or y>x by A5,XXREAL_0:1;
hence thesis by A2,A3,A6,A7,Th50;
end;
begin :: The Determinant of a Product of Two Square Matrices
definition
let K be non empty addLoopStr;
func addFinS(K) -> BinOp of (the carrier of K)* means
:Def5:
for p1,p2 be Element of (the carrier of K)* holds it.(p1,p2)=p1+p2;
existence
proof
set KK= the carrier of K;
defpred ADD[set,set,set] means for p1,p2 be Element of KK* st $1=p1 & $2=
p2 holds $3=p1+p2;
A1: for x be Element of KK* for y be Element of KK* ex z be Element of KK*
st ADD[x,y,z]
proof
let x be Element of KK*;
let y be Element of KK*;
reconsider p1=x,p2=y as FinSequence of KK;
reconsider pp=p1+p2 as Element of KK* by FINSEQ_1:def 11;
take pp;
thus thesis;
end;
consider A be Function of [:KK*,KK*:],KK* such that
A2: for x be Element of KK* for y be Element of KK* holds ADD[x,y,A.(x
,y)] from BINOP_1:sch 3(A1);
take A;
thus thesis by A2;
end;
uniqueness
proof
set KK= the carrier of K;
let f1,f2 be Function of [:KK*,KK*:],KK* such that
A3: for p1,p2 be Element of KK* holds f1.(p1,p2)=p1+p2 and
A4: for p1,p2 be Element of KK* holds f2.(p1,p2)=p1+p2;
now
let p1 be Element of KK*;
let p2 be Element of KK*;
f1.(p1,p2)=p1+p2 by A3;
hence f1.(p1,p2) = f2.(p1,p2) by A4;
end;
hence thesis;
end;
end;
Lm9: for K be non empty addLoopStr for p1,p2 be Element of (the carrier of K)*
holds dom (p1+p2)=dom p1/\dom p2
proof
let K be non empty addLoopStr;
let p1,p2 be Element of (the carrier of K)*;
A1: rng p2 c= the carrier of K by FINSEQ_1:def 4;
rng p1 c= the carrier of K by FINSEQ_1:def 4;
then [:rng p1,rng p2:]c=[:the carrier of K,the carrier of K:]by A1,
ZFMISC_1:96;
then [:rng p1, rng p2:] c= dom (the addF of K) by FUNCT_2:def 1;
hence thesis by FUNCOP_1:69;
end;
registration
let K be Abelian non empty addLoopStr;
cluster addFinS(K) -> commutative;
coherence
proof
set KK= the carrier of K;
let p1,p2 be Element of KK*;
A1: rng p2 c= KK by FINSEQ_1:def 4;
A2: dom(p1+p2)=dom p1/\dom p2 by Lm9;
A3: dom(p2+p1)=dom p2/\dom p1 by Lm9;
A4: rng p1 c= KK by FINSEQ_1:def 4;
now
let k be Nat such that
A5: k in dom (p1+p2);
k in dom p2 by A2,A5,XBOOLE_0:def 4;
then
A6: p2.k in rng p2 by FUNCT_1:def 3;
k in dom p1 by A2,A5,XBOOLE_0:def 4;
then p1.k in rng p1 by FUNCT_1:def 3;
then reconsider p1k=p1.k,p2k=p2.k as Element of K by A4,A1,A6;
(p1+p2).k=p1k+p2k by A5,FVSUM_1:17;
hence (p1+p2).k=(p2+p1).k by A2,A3,A5,FVSUM_1:17;
end;
then
A7: p1+p2=p2+p1 by A3,Lm9,FINSEQ_1:13;
(addFinS(K)).(p1,p2)=p1+p2 by Def5;
hence thesis by A7,Def5;
end;
end;
registration
let K be add-associative non empty addLoopStr;
cluster addFinS(K) -> associative;
coherence
proof
set aK=addFinS(K);
set KK= the carrier of K;
let p1,p2,p3 be Element of KK*;
reconsider p12=p1+p2,p23=p2+p3 as Element of KK* by FINSEQ_1:def 11;
A1: rng p1 c=KK by FINSEQ_1:def 4;
A2: rng p2 c=KK by FINSEQ_1:def 4;
A3: rng p12 c=KK by FINSEQ_1:def 4;
A4: rng p3 c=KK by FINSEQ_1:def 4;
A5: rng p23 c=KK by FINSEQ_1:def 4;
A6: dom(p12)=dom p1/\dom p2 by Lm9;
A7: dom(p23)=dom p2/\dom p3 by Lm9;
A8: dom (p12+p3)=dom p12/\dom p3 by Lm9;
A9: dom (p1+p23)=dom p1/\dom p23 by Lm9;
then
A10: dom (p12+p3)=dom (p1+p23) by A6,A8,A7,XBOOLE_1:16;
now
let k be Nat such that
A11: k in dom (p12+p3);
A12: k in dom p12 by A8,A11,XBOOLE_0:def 4;
then
A13: p12.k in rng p12 by FUNCT_1:def 3;
k in dom p1 by A6,A12,XBOOLE_0:def 4;
then
A14: p1.k in rng p1 by FUNCT_1:def 3;
A15: k in dom p3 by A8,A11,XBOOLE_0:def 4;
then
A16: p3.k in rng p3 by FUNCT_1:def 3;
A17: k in dom p2 by A6,A12,XBOOLE_0:def 4;
then
A18: p2.k in rng p2 by FUNCT_1:def 3;
A19: k in dom p23 by A7,A15,A17,XBOOLE_0:def 4;
then p23.k in rng p23 by FUNCT_1:def 3;
then reconsider
p1k=p1.k, p12k=p12.k,p2k=p2.k,p23k=p23.k,p3k=p3.k as Element
of K by A1,A2,A4,A3,A5,A14,A13,A16,A18;
A20: (p12).k=p1k+p2k by A12,FVSUM_1:17;
A21: (p12+p3).k=p12k+p3k by A11,FVSUM_1:17;
A22: (p23).k=p2k+p3k by A19,FVSUM_1:17;
(p1+p23).k=p1k+p23k by A10,A11,FVSUM_1:17;
hence (p1+p23).k=(p12+p3).k by A20,A22,A21,RLVECT_1:def 3;
end;
then
A23: p1+p23 = p12+p3 by A6,A8,A7,A9,FINSEQ_1:13,XBOOLE_1:16;
thus aK.(p1,aK.(p2,p3)) = aK.(p1,p23) by Def5
.= p1+p23 by Def5
.= aK.(p12,p3) by A23,Def5
.= aK.(aK.(p1,p2),p3) by Def5;
end;
end;
theorem Th55:
for K being Ring
for A,B be Matrix of K st width A = len B & len B > 0 for i st i
in Seg len A ex P be FinSequence of (the carrier of K)* st len P = len B & Line
(A*B,i) = addFinS(K) "**" P & for j st j in Seg len B holds P.j = A*(i,j) *
Line(B,j)
proof
let K be Ring;
let A,B be Matrix of K such that
A1: width A = len B and
A2: len B > 0;
set aa=the addF of K;
set mm=the multF of K;
set a=addFinS(K);
set KK=the carrier of K;
reconsider m=len B,w=width B as Nat;
let i such that
A3: i in Seg len A;
deffunc F(Nat)=A*(i,$1) * Line(B,$1);
consider P be FinSequence such that
A4: len P = len B and
A5: for k be Nat st k in dom P holds P.k = F(k) from FINSEQ_1:sch 2;
A6: dom P = dom B by A4,FINSEQ_3:29
.= Seg len B by FINSEQ_1:def 3;
rng P c= KK*
proof
let y be object;
assume y in rng P;
then consider x being object such that
A7: x in dom P and
A8: y=P.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A7;
P.x=A*(i,x) * Line(B,x) by A5,A7;
hence thesis by A8,FINSEQ_1:def 11;
end;
then reconsider P as FinSequence of KK* by FINSEQ_1:def 4;
A9: m>=1 by A2,NAT_1:14;
then consider F be sequence of KK* such that
A10: F.1 = P.1 and
A11: for n be Nat st 0<>n & n<len P holds F.(n+1)=a.(F.n,P.(n
+1)) and
A12: a "**" P = F.(len P) by A4,FINSOP_1:def 1;
defpred P[Nat] means 1 <= $1 & $1 <= m implies for F1 be FinSequence of KK
st F.$1=F1 holds len F1=w & for j be Element of NAT st j in Seg w holds ex LC
be FinSequence of KK st LC = mlt(Line(A,i),Col(B,j)) | Seg $1 & aa"**"LC=F1.j;
A13: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A14: P[k];
set k1=k+1;
assume that
A15: 1 <= k1 and
A16: k1 <= m;
A17: k1 in Seg m by A15,A16;
let Fk1 be FinSequence of KK such that
A18: F.k1=Fk1;
per cases;
suppose
A19: k=0;
then
A20: P.1=A*(i,1) * Line(B,1) by A5,A6,A17;
A21: len Line(B,1) =w by MATRIX_0:def 7;
hence len Fk1= w by A10,A18,A19,A20,Lm5;
let j be Element of NAT such that
A22: j in Seg w;
len Fk1 =w by A10,A18,A19,A20,A21,Lm5;
then
A23: j in dom Fk1 by A22,FINSEQ_1:def 3;
Line(B,1).j=B*(1,j) by A22,MATRIX_0:def 7;
then
A24: Fk1.j=(A*(i,1)) * (B*(1,j)) by A10,A18,A19,A20,A23,FVSUM_1:50;
set C=Col(B,j);
set L=Line(A,i);
reconsider LC1=(mlt(L,C)) | (Seg k1),mLC=mlt(L,C) as FinSequence of KK
by FINSEQ_1:18;
A25: mm.:(L,C) is Element of m-tuples_on KK by A1,FINSEQ_2:120;
then len mLC=m by CARD_1:def 7;
then
A26: dom mLC=Seg m by FINSEQ_1:def 3;
Seg 1 = Seg m/\Seg 1 by A2,FINSEQ_1:7,NAT_1:14;
then
A27: dom LC1=Seg 1 by A19,A26,RELAT_1:61;
then
A28: len LC1=1 by FINSEQ_1:def 3;
1 in Seg 1;
then LC1.1=mLC.1 by A27,FUNCT_1:47;
then
A29: LC1=<*mLC.1*> by A28,FINSEQ_1:40;
take LC1;
A30: 1 in Seg m by A9;
len mLC=m by A25,CARD_1:def 7;
then
A31: 1 in dom mLC by A30,FINSEQ_1:def 3;
Seg m=dom B by FINSEQ_1:def 3;
then
A32: C.1=B*(1,j) by A30,MATRIX_0:def 8;
L.1=A*(i,1) by A1,A30,MATRIX_0:def 7;
then mLC.1=(A*(i,1)) * (B*(1,j)) by A32,A31,FVSUM_1:60;
hence thesis by A24,A29,FINSOP_1:11;
end;
suppose
A33: k>0;
dom P=Seg m by A4,FINSEQ_1:def 3;
then
A34: P.k1 in rng P by A17,FUNCT_1:def 3;
rng P c= KK* by FINSEQ_1:def 4;
then reconsider Pk1=P.k1,Fk=F.k as FinSequence of KK
by A34,FINSEQ_1:def 11;
reconsider Pk1,Fk as Element of KK* by FINSEQ_1:def 11;
A35: a.(Fk,Pk1)=Fk+Pk1 by Def5;
A36: k+0<k1 by XREAL_1:8;
then k < m by A16,XXREAL_0:2;
then
A37: Fk1=Fk+Pk1 by A4,A11,A18,A33,A35;
A38: len Line(B,k1)=w by MATRIX_0:def 7;
Pk1 = F(k1) by A5,A6,A17;
then len Pk1=w by A38,Lm5;
then
A39: dom Pk1=Seg w by FINSEQ_1:def 3;
A40: w in NAT by ORDINAL1:def 12;
A41: len Fk=w by A14,A16,A33,A36,NAT_1:14,XXREAL_0:2;
then dom Fk=Seg w by FINSEQ_1:def 3;
then
A42: dom (Fk+Pk1)=Seg w /\Seg w by A39,Lm9;
hence len Fk1=w by A37,A40,FINSEQ_1:def 3;
A43: rng Fk c= KK by FINSEQ_1:def 4;
set L=Line(A,i);
A44: Pk1 = F(k1) by A5,A6,A17;
let j be Element of NAT such that
A45: j in Seg w;
A46: Line(B,k1).j=B*(k1,j) by A45,MATRIX_0:def 7;
then Pk1.j=(A*(i,k1)) * (B*(k1,j)) by A39,A45,A44,FVSUM_1:50;
then reconsider Pk1j=Pk1.j as Element of KK;
set C=Col(B,j);
consider LC be FinSequence of KK such that
A47: LC = mlt(L,C) | (Seg k) and
A48: (the addF of K)"**"LC=Fk.j by A14,A16,A33,A36,A45,NAT_1:14,XXREAL_0:2;
reconsider LC1=mlt(L,C) | (Seg k1),mLC=mlt(L,C) as FinSequence of KK by
FINSEQ_1:18;
take LC1;
mm.:(L,C) is Element of m-tuples_on KK by A1,FINSEQ_2:120;
then len mLC=m by CARD_1:def 7;
then
A49: k1 in dom mLC by A17,FINSEQ_1:def 3;
A50: k1 in Seg m by A15,A16;
then
A51: L.k1=A*(i,k1) by A1,MATRIX_0:def 7;
Seg m=dom B by FINSEQ_1:def 3;
then C.k1=B*(k1,j) by A50,MATRIX_0:def 8;
then
A52: mLC.k1=(A*(i,k1))*(B*(k1,j)) by A51,A49,FVSUM_1:60;
LC1=LC^<*mLC.k1*> by A47,A49,FINSEQ_5:10;
then
A53: aa"**"LC1=aa.(Fk.j,(A*(i,k1)) * (B*(k1,j)))
by A48,A52,FINSOP_1:4,FVSUM_1:8;
j in dom Fk by A41,A45,FINSEQ_1:def 3;
then Fk.j in rng Fk by FUNCT_1:def 3;
then reconsider Fkj=Fk.j as Element of KK by A43;
Fk1.j=Fkj+Pk1j by A42,A37,A45,FVSUM_1:17;
hence thesis by A39,A45,A46,A44,A53,FVSUM_1:50;
end;
end;
set L=Line(A*B,i);
width (A*B)=w by A1,MATRIX_3:def 4;
then
A54: len L = w by MATRIX_0:def 7;
reconsider Fm=F.m as FinSequence of KK;
A55: P[0];
A56: for k be Nat holds P[k] from NAT_1:sch 2(A55,A13);
A57: for j be Nat st 1 <=j & j <= len L holds L.j=Fm.j
proof
set AB=A*B;
set LA=Line(A,i);
let j be Nat such that
A58: 1 <=j and
A59: j <= len L;
set CB=Col(B,j);
mm.:(LA,CB) is Element of m-tuples_on KK by A1,FINSEQ_2:120;
then len mlt(LA,CB)=m by CARD_1:def 7;
then
A60: dom mlt(LA,CB)=Seg m by FINSEQ_1:def 3;
A61: j in Seg w by A54,A58,A59;
then
ex LC be FinSequence of KK st LC = mlt(LA,CB) | (Seg m) & aa"**"LC=Fm
.j by A9,A56;
then
A62: Fm.j=LA "*" CB by A60;
A63: len AB=len A by A1,MATRIX_3:def 4;
A64: width AB=w by A1,MATRIX_3:def 4;
len A<>0 by A3;
then AB is Matrix of len A,w,K by A63,A64,MATRIX_0:20;
then Indices AB=[:Seg len A,Seg w:] by A64,MATRIX_0:25;
then [i,j] in Indices AB by A3,A61,ZFMISC_1:87;
then AB*(i,j)=LA "*" CB by A1,MATRIX_3:def 4;
hence thesis by A61,A62,A64,MATRIX_0:def 7;
end;
take P;
thus len P=len B by A4;
len Fm=w by A9,A56;
hence L=a "**" P by A4,A12,A54,A57;
let j;
assume j in Seg len B;
hence thesis by A5,A6;
end;
theorem Th56:
for A,B,C be (Matrix of n,K), i st i in Seg n ex P be
FinSequence of K st len P = n & Det RLine(C,i,Line(A*B,i)) = (the addF of K)
"**" P & for j st j in Seg n holds P.j = A*(i,j) * Det RLine(C,i,Line(B,j))
proof
let A,B,C be (Matrix of n,K), i such that
A1: i in Seg n;
Seg n <> {} by A1;
then
A2: n <> 0;
set a=addFinS(K);
A3: len B=n by MATRIX_0:24;
deffunc F(Nat)=A*(i,$1) * Det RLine(C,i,Line(B,$1));
set aa=the addF of K;
set KK=the carrier of K;
A4: len A=n by MATRIX_0:24;
consider D be FinSequence of KK such that
A5: len D = len A and
A6: for j be Nat st j in dom D holds D.j = F(j) from FINSEQ_2:sch 1;
A7: n<>0 by A1;
then len D >= 1 by A4,A5,NAT_1:14;
then consider Fd be sequence of KK such that
A8: Fd.1 = D.1 and
A9: for k be Nat st 0 <> k & k < n holds Fd.(k+1) = aa.(Fd.k,D.(k+1)) and
A10: aa"**"D = Fd.n by A4,A5,FINSOP_1:def 1;
A11: dom D = Seg len A by A5,FINSEQ_1:def 3;
width A=n by MATRIX_0:24;
then consider P be FinSequence of KK* such that
A12: len P = n and
A13: Line(A*B,i) = a "**" P and
A14: for j st j in Seg len B holds P.j = A*(i,j) * Line(B,j) by A1,A7,A3,A4
,Th55;
len P >= 1 by A12,A2,NAT_1:14;
then consider Fp be sequence of KK* such that
A15: Fp.1 = P.1 and
A16: for k be Nat st 0 <> k & k < n holds Fp.(k+1) = a.(Fp.k,P.(k+1)) and
A17: Line(A*B,i) = Fp.n by A12,A13,FINSOP_1:def 1;
defpred P[Nat] means 1 <= $1 & $1<= n implies for pK
being FinSequence of K st pK=Fp.$1 holds len
pK=n & Fd.$1=Det RLine(C,i,pK);
A18: width B=n by MATRIX_0:24;
A19: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A20: P[k];
set k1=k+1;
set A9=A*(i,k1);
set L=Line(B,k1);
assume that
A21: 1 <= k1 and
A22: k1 <= n;
A23: k1 in Seg n by A21,A22;
let Fpk1 be FinSequence of KK such that
A24: Fpk1=Fp.k1;
per cases;
suppose
A25: k=0;
A26: P.k1=A9*L by A3,A14,A23;
A27: len L = n by A18,MATRIX_0:def 7;
D.k1=F(1) by A4,A6,A11,A23,A25;
hence thesis by A1,A15,A8,A24,A25,A26,A27,Lm5,Th34;
end;
suppose
A28: k>0;
k1 in dom P by A12,A23,FINSEQ_1:def 3;
then
A29: P.k1 in rng P by FUNCT_1:def 3;
rng P c= KK* by FINSEQ_1:def 4;
then reconsider Pk1=P.k1,Fpk=Fp.k as Element of KK*
by A29,FINSEQ_1:def 11;
A30: k+0<k1 by XREAL_1:8;
then
A31: Fd.k=Det RLine(C,i,Fpk) by A20,A22,A28,NAT_1:14,XXREAL_0:2;
A32: len Fpk=n by A20,A22,A28,A30,NAT_1:14,XXREAL_0:2;
A33: k<n by A22,A30,XXREAL_0:2;
then
A34: Fd.k1 = aa.(Fd.k,D.k1) by A9,A28;
A35: P.k1=A9 * L by A3,A14,A23;
Fpk1 = a.(Fpk,Pk1) by A16,A24,A28,A33;
then
A36: Fpk1=Fpk+(A9*L) by A35,Def5;
A37: len L=n by A18,MATRIX_0:def 7;
then
A38: len (A9*L)=n by Lm5;
Det RLine(C,i,A9*L)=A9* Det RLine(C,i,L) by A1,A37,Th34;
then
Det RLine(C,i,Fpk1)=Det RLine(C,i,Fpk) + A9*Det RLine(C,i,L) by A1,A32
,A36,A38,Th36;
hence thesis by A4,A6,A11,A23,A31,A34,A32,A36,A38,Lm6;
end;
end;
take D;
thus len D=n by A5,MATRIX_0:24;
A39: P[0];
for k be Nat holds P[k] from NAT_1:sch 2(A39,A19);
then P[len P];
hence thesis by A4,A12,A6,A11,A17,A10,A2,NAT_1:14;
end;
theorem Th57:
for X being set,Y being non empty set, x st not x in X ex BIJECT
be Function of [:Funcs(X,Y),Y:],Funcs(X\/{x},Y) st BIJECT is bijective & for f
be Function of X,Y,F be Function of X\/{x},Y st F|X=f holds BIJECT.(f,F.x)=F
proof
let X be set, Y be non empty set, x such that
A1: not x in X;
set Xx=X\/{x};
set FXY=Funcs(X,Y);
set FXxY=Funcs(Xx,Y);
defpred P[set,set] means for f be Function of X,Y,F be Function of Xx,Y, y
be set st [f,y]=$1 & F.x=y & F|X=f holds F=$2;
A2: for x be Element of [:FXY,Y:] ex y be Element of FXxY st P[x,y]
proof
let x9 be Element of [:FXY,Y:];
consider f,y be object such that
A3: f in FXY and
A4: y in Y and
A5: x9=[f,y] by ZFMISC_1:def 2;
reconsider f as Function of X,Y by A3,FUNCT_2:66;
Y\/{y}=Y by A4,ZFMISC_1:40;
then consider F be Function of X\/{x},Y such that
A6: F|X = f and
A7: F.x=y by A1,STIRL2_1:57;
reconsider F9=F as Element of FXxY by FUNCT_2:8;
take F9;
let g be Function of X,Y,G be Function of Xx,Y, y9 be set such that
A8: [g,y9]=x9 and
A9: G.x=y9 and
A10: G|X=g;
now
let xx be object;
assume xx in Xx;
then
A11: xx in X or xx in {x} by XBOOLE_0:def 3;
A12: dom f=X by FUNCT_2:def 1;
dom g= X by FUNCT_2:def 1;
then G.xx=g.xx & F.xx=f.xx or xx = x by A6,A10,A11,A12,FUNCT_1:47
,TARSKI:def 1;
hence G.xx=F.xx by A5,A7,A8,A9,XTUPLE_0:1;
end;
hence thesis by FUNCT_2:12;
end;
consider H be Function of [:FXY,Y:],FXxY such that
A13: for x be Element of [:FXY,Y:] holds P[x,H.x] from FUNCT_2:sch 3(A2);
A14: now
let x1,x2 be object such that
A15: x1 in [:FXY,Y:] and
A16: x2 in [:FXY,Y:] and
A17: H.x1 = H.x2;
consider f2,y2 be object such that
A18: f2 in FXY and
A19: y2 in Y and
A20: x2=[f2,y2] by A16,ZFMISC_1:def 2;
consider f1,y1 be object such that
A21: f1 in FXY and
A22: y1 in Y and
A23: x1=[f1,y1] by A15,ZFMISC_1:def 2;
reconsider f1,f2 as Function of X,Y by A21,A18,FUNCT_2:66;
Y\/{y2}=Y by A19,ZFMISC_1:40;
then consider F2 be Function of X\/{x},Y such that
A24: F2|X = f2 and
A25: F2.x=y2 by A1,STIRL2_1:57;
A26: H.x2=F2 by A13,A16,A20,A24,A25;
Y\/{y1}=Y by A22,ZFMISC_1:40;
then consider F1 be Function of X\/{x},Y such that
A27: F1|X = f1 and
A28: F1.x=y1 by A1,STIRL2_1:57;
H.x1=F1 by A13,A15,A23,A27,A28;
hence x1=x2 by A17,A23,A20,A27,A28,A24,A25,A26;
end;
take H;
x in {x} by TARSKI:def 1;
then
A29: x in Xx by XBOOLE_0:def 3;
A30: FXxY c= rng H
proof
let f9 be object;
assume f9 in FXxY;
then reconsider f=f9 as Function of Xx,Y by FUNCT_2:66;
dom f=Xx by FUNCT_2:def 1;
then
A31: dom (f|X)=X by RELAT_1:62,XBOOLE_1:7;
rng (f|X) c= Y by RELAT_1:def 19;
then reconsider fX=f|X as Function of X,Y by A31,FUNCT_2:2;
A32: fX in FXY by FUNCT_2:8;
x in {x} by TARSKI:def 1;
then
A33: x in Xx by XBOOLE_0:def 3;
Xx=dom f by FUNCT_2:def 1;
then
A34: f.x in rng f by A33,FUNCT_1:def 3;
rng f c= Y by RELAT_1:def 19;
then
A35: [fX,f.x] in [:FXY,Y:] by A34,A32,ZFMISC_1:87;
[:FXY,Y:]=dom H by FUNCT_2:def 1;
then H.[fX,f.x] in rng H by A35,FUNCT_1:def 3;
hence thesis by A13,A35;
end;
rng H c= FXxY by RELAT_1:def 19;
then FXxY = rng H by A30;
then H is one-to-one onto by A14,FUNCT_2:19,def 3;
hence H is bijective;
let f be Function of X,Y,F be Function of X\/{x},Y such that
A36: F|X=f;
Xx=dom F by FUNCT_2:def 1;
then
A37: F.x in rng F by A29,FUNCT_1:def 3;
A38: f in FXY by FUNCT_2:8;
rng F c= Y by RELAT_1:def 19;
then [f,F.x] in [:FXY,Y:] by A37,A38,ZFMISC_1:87;
hence thesis by A13,A36;
end;
theorem Th58:
for X being finite set, Y being non empty finite set, x st not x
in X for F being BinOp of D st F is having_a_unity & F is commutative & F is
associative for f being Function of Funcs(X,Y),D for g being Function of Funcs(
X\/{x},Y),D st for H be Function of X,Y, SF be Element of Fin Funcs(X\/{x},Y)
st SF={h where h is Function of X\/{x},Y: h|X = H} holds F $$ (SF,g)=f.H holds
F $$ (In(Funcs(X,Y),Fin Funcs(X,Y)),f) =
F $$ (In(Funcs(X\/{x},Y),Fin Funcs(X\/{x},Y)),g)
proof
let X be finite set,Y be non empty finite set, x such that
A1: not x in X;
set Xx=X\/{x};
set FXY=Funcs(X,Y);
set FXxY=Funcs(Xx,Y);
consider B be Function of [:FXY,Y:],FXxY such that
A2: B is bijective and
A3: for f be Function of X,Y,F be Function of Xx,Y st F|X=f holds B.(f,F
.x)=F by A1,Th57;
dom B=[:FXY,Y:] by FUNCT_2:def 1;
then reconsider domB=dom B as Element of Fin [:FXY,Y:] by FINSUB_1:def 5;
reconsider FXY9=FXY as Element of Fin FXY by FINSUB_1:def 5;
FXxY in Fin FXxY by FINSUB_1:def 5; then
A5: In(FXxY,Fin FXxY)=FXxY by SUBSET_1:def 8;
reconsider Y9=Y as Element of Fin Y by FINSUB_1:def 5;
let F be BinOp of D such that
A6: F is having_a_unity and
A7: F is commutative and
A8: F is associative;
let f be Function of FXY,D;
let g be Function of FXxY,D such that
A9: for H be Function of X,Y, SF be Element of Fin FXxY st SF={h where h
is Function of Xx,Y: h|X = H} holds F $$ (SF,g)=f.H;
reconsider gB=g*B as Function of [:FXY,Y:],D;
for z be Element of FXY holds f.z=F$$(Y9,(curry (gB)).z)
proof
let z be Element of FXY;
reconsider Z=z as Function of X,Y;
set SF={h where h is Function of Xx,Y: h|X = Z};
deffunc Q(object) = [z,$1];
consider q be Function such that
A10: dom q = Y &
for x being object st x in Y holds q.x = Q(x) from FUNCT_1:sch 3;
A11: {z} c= FXY by ZFMISC_1:31;
then [:{Z},Y:] c= [:FXY,Y:] by ZFMISC_1:95;
then reconsider ZY=[:{Z},Y:]as Element of Fin [:FXY,Y:] by FINSUB_1:def 5;
for x9 be object holds x9 in ZY iff x9 in q.:(Y)
proof
let x9 be object;
thus x9 in ZY implies x9 in q.:(Y)
proof
assume x9 in ZY;
then consider z9,y9 be object such that
A12: z9 in {Z} and
A13: y9 in Y and
A14: x9=[z9,y9] by ZFMISC_1:def 2;
A15: z=z9 by A12,TARSKI:def 1;
q.y9=[z,y9] by A10,A13;
hence thesis by A10,A13,A14,A15,FUNCT_1:def 6;
end;
assume x9 in q.:Y;
then consider y9 be object such that
A16: y9 in dom q and
A17: y9 in Y and
A18: x9 = q.y9 by FUNCT_1:def 6;
x9=[z,y9] by A10,A16,A18;
hence thesis by A17,ZFMISC_1:105;
end;
then
A19: q.:Y=ZY by TARSKI:2;
then
A20: rng q=ZY by A10,RELAT_1:113;
now
let x1,x2 be object such that
A21: x1 in dom q and
A22: x2 in dom q and
A23: q.x1=q.x2;
A24: q.x2=[z,x2] by A10,A22;
[z,x1]=q.x1 by A10,A21;
hence x1=x2 by A23,A24,XTUPLE_0:1;
end;
then
A25: q is one-to-one by FUNCT_1:def 4;
ZY c= [:FXY,Y:] by A11,ZFMISC_1:95;
then reconsider q as Function of Y,[:FXY,Y:] by A10,A20,FUNCT_2:2;
reconsider gBq=gB*q as Function of Y,D;
dom gB=[:FXY,Y:] by FUNCT_2:def 1;
then consider C be Function such that
A26: (curry (gB)).z =C and
dom C=Y and
rng C c= rng gB and
A27: for y9 be object st y9 in Y holds C.y9=gB.(z,y9) by FUNCT_5:29;
reconsider C as Function of Y,D by A26;
now
let x9 be object such that
A28: x9 in Y;
A29: q.x9=[z,x9] by A10,A28;
C.x9=gB.(z,x9) by A27,A28;
hence C.x9 = gBq.x9 by A28,A29,FUNCT_2:15;
end;
then
A30: C=gBq by FUNCT_2:12;
A31: B.:ZY c= SF
proof
let b be object;
assume b in B.:ZY;
then consider zy be object such that
zy in dom B and
A32: zy in ZY and
A33: b=B.zy by FUNCT_1:def 6;
consider z9,y9 be object such that
A34: z9 in {Z} and
A35: y9 in Y and
A36: zy = [z9,y9] by A32,ZFMISC_1:def 2;
Y\/{y9}=Y by A35,ZFMISC_1:40;
then consider F1 be Function of Xx,Y such that
A37: F1|X = Z and
A38: F1.x=y9 by A1,STIRL2_1:57;
z9=Z by A34,TARSKI:def 1;
then B.(z9,y9)=F1 by A3,A37,A38;
hence thesis by A33,A36,A37;
end;
A39: SF c= B.:ZY
proof
x in {x} by TARSKI:def 1;
then
A40: x in Xx by XBOOLE_0:def 3;
let sf be object;
assume sf in SF;
then consider h be Function of Xx,Y such that
A41: h=sf and
A42: h|X = Z;
A43: [:FXY,Y:]=dom B by FUNCT_2:def 1;
dom h =Xx by FUNCT_2:def 1;
then
A44: h.x in rng h by A40,FUNCT_1:def 3;
A45: rng h c= Y by RELAT_1:def 19;
then
A46: [z,h.x] in [:FXY,Y:] by A44,ZFMISC_1:87;
z in {Z} by TARSKI:def 1;
then [z,h.x] in ZY by A44,A45,ZFMISC_1:87;
then B.(z,h.x) in B.:ZY by A46,A43,FUNCT_1:def 6;
hence thesis by A3,A41,A42;
end;
then reconsider SF as Element of Fin FXxY by A31,XBOOLE_0:def 10;
B.:ZY = SF by A31,A39;
then
A47: F $$(B.:ZY,g)=f.Z by A9;
F $$(B.:ZY,g)=F $$(ZY,gB) by A7,A8,A2,SETWOP_2:6;
hence thesis by A7,A8,A47,A25,A19,A26,A30,SETWOP_2:6;
end;
then F$$([:FXY9,Y9:],gB)=F$$(FXY9,f) by A6,A7,A8,MATRIX_3:30;
then
A48: F$$(domB,gB)=F$$(FXY9,f) by FUNCT_2:def 1;
A49: rng B=FXxY by A2,FUNCT_2:def 3;
F $$(B.:domB,g)=F $$ (domB, g*B) by A7,A8,A2,SETWOP_2:6;
then F $$(In(FXxY,Fin FXxY),g)=F $$ (domB, g*B) by A49,A5,RELAT_1:113;
hence thesis by A48;
end;
theorem Th59:
for A,B be Matrix of n,m,D, i st i <= n & 0 < n for F be
Function of Seg i, Seg n ex M be Matrix of n,m,D st
M = A +* ((B*(idseq n+*F)) | Seg i) &
for j holds (j in Seg i implies M.j = B.(F.j)) & (not j in Seg i
implies M.j = A.j)
proof
let A,B be Matrix of n,m,D, i such that
A1: i<= n and
A2: 0<n;
set I=idseq n;
let F be Function of Seg i,Seg n;
set IF=I+*F;
A3: dom I=Seg n;
A4: rng I=Seg n;
rng F c= Seg n by RELAT_1:def 19;
then rng F\/Seg n=Seg n by XBOOLE_1:12;
then
A5: rng IF c=Seg n by A4,FUNCT_4:17;
A6: Seg i c= Seg n by A1,FINSEQ_1:5;
then
A7: Seg i\/Seg n=Seg n by XBOOLE_1:12;
A8: dom F=Seg i by A2,FUNCT_2:def 1;
then dom F c= Seg n by A1,FINSEQ_1:5;
then dom F\/Seg n =Seg n by XBOOLE_1:12;
then dom IF=Seg n by A3,FUNCT_4:def 1;
then reconsider IF as Function of Seg n,Seg n by A5,FUNCT_2:2;
reconsider BIF=B*IF as Matrix of n,m,D;
set BIFi=BIF|Seg i;
set M=A+* BIFi;
A9: len B=n by A2,MATRIX_0:23;
len BIF=len B by Def4;
then dom BIF=Seg n by A9,FINSEQ_1:def 3;
then
A10: dom BIFi=Seg i by A6,RELAT_1:62;
len A=n by A2,MATRIX_0:23;
then dom A=Seg n by FINSEQ_1:def 3;
then
A11: dom M=Seg i \/Seg n by A10,FUNCT_4:def 1;
then reconsider M as FinSequence by A7,FINSEQ_1:def 2;
A12: for j holds (j in Seg i implies M.j = B.(F.j) )&( not j in Seg i
implies M.j = A.j )
proof
let j;
thus j in Seg i implies M.j = B.(F.j)
proof
A13: Seg i c= Seg n by A1,FINSEQ_1:5;
assume
A14: j in Seg i;
then
A15: BIFi.j=BIF.j by A10,FUNCT_1:47;
IF.j=F.j by A8,A14,FUNCT_4:13;
then
A16: Line(BIF,j)=B.(F.j) by A14,A13,Th38;
Line(BIF,j)=BIF.j by A14,A13,MATRIX_0:52;
hence thesis by A10,A14,A16,A15,FUNCT_4:13;
end;
assume not j in Seg i;
hence thesis by A10,FUNCT_4:11;
end;
A17: for x st x in rng M ex p be FinSequence of D st x = p & len p = m
proof
let x;
assume x in rng M;
then consider k be object such that
A18: k in dom M and
A19: M.k=x by FUNCT_1:def 3;
reconsider k as Nat by A18;
per cases;
suppose
A20: k in Seg i;
A21: rng F c= Seg n by RELAT_1:def 19;
A22: F.k in rng F by A8,A20,FUNCT_1:def 3;
then reconsider Fk=F.k as Element of NAT by A21,TARSKI:def 3;
take L=Line(B,Fk);
A23: len L=width B by MATRIX_0:def 7;
B.(F.k)=L by A22,A21,MATRIX_0:52;
hence thesis by A2,A12,A19,A20,A23,MATRIX_0:23;
end;
suppose
A24: not k in Seg i;
take L=Line(A,k);
A25: len L=width A by MATRIX_0:def 7;
M.k=A.k by A12,A24;
hence thesis by A2,A11,A7,A18,A19,A25,MATRIX_0:23,52;
end;
end;
then reconsider M as Matrix of D by MATRIX_0:9;
n is Element of NAT by ORDINAL1:def 12;
then
A26: len M=n by A11,A7,FINSEQ_1:def 3;
now
let p be FinSequence of D;
assume p in rng M;
then ex q be FinSequence of D st p = q & len q = m by A17;
hence len p=m;
end;
then reconsider M as Matrix of n,m,D by A26,MATRIX_0:def 2;
take M;
thus thesis by A12;
end;
Lm10:
for K being Ring
for A,B be Matrix of n,n,K, i st i <= n & 0 < n ex P be Function of
Funcs(Seg i,Seg n),the carrier of K st for F be Function of Seg i,Seg n for M
be Matrix of n,n,K st M = A*B +* ((B*(idseq n +* F)) | Seg i) & for j holds (j
in Seg i implies M.j=B.(F.j))& (not j in Seg i implies M.j=(A*B).j) ex Path be
FinSequence of K st len Path=i & (for Fj,j be Nat st j in Seg i & Fj=F.j holds
Path.j=A*(j,Fj)) & P.F= (the multF of K) $$ Path * Det M
proof
let K be Ring;
let A,B be Matrix of n,n,K, i such that
A1: i <= n and
A2: 0 < n;
set KK=the carrier of K;
set I=idseq n;
set Sn=Seg n;
set Si=Seg i;
set mm=the multF of K;
set FF=Funcs(Si,Sn);
reconsider Sn as non empty set by A2;
set AB=A*B;
reconsider AB as Matrix of n,K;
defpred PP[object,object] means
for F be Function of Seg i,Seg n st F=$1 for M be
Matrix of n,n,K st M = A*B +* ((B*(I +* F)) | Si) & for j holds(j in Si implies
M.j=B.(F.j))& (not j in Si implies M.j=(A*B).j) ex Path be FinSequence of K st
len Path=i & (for Fj,j be Nat st j in Si & Fj=F.j holds Path.j=A*(j,Fj)) & $2=
mm $$ Path * Det M;
ex f be Function st dom f = Si & rng f c= Sn by FUNCT_1:8;
then reconsider FF as non empty set;
A3: for x be Element of FF ex y be Element of KK st PP[x,y]
proof
let x be Element of FF;
reconsider F=x as Function of Si,Sn by FUNCT_2:66;
defpred Path[object,object] means
for Fj,j be Nat st j =$1 & Fj=F.j holds $2=A*(j,Fj);
A4: i is Element of NAT by ORDINAL1:def 12;
A5: for x9 be object st x9 in Si ex y being object st y in KK & Path[x9,y]
proof
let x9 be object such that
A6: x9 in Si;
reconsider i=x9 as Nat by A6;
A7: rng F c= Seg n by RELAT_1:def 19;
Si=dom F by FUNCT_2:def 1;
then F.i in rng F by A6,FUNCT_1:def 3;
then F.i in Sn by A7;
then reconsider Fi=F.i as Nat;
take A*(i,Fi);
thus thesis;
end;
consider path be Function of Si,KK such that
A8: for x being object st x in Si holds Path[x,path.x] from FUNCT_2:sch 1(A5);
dom path=Si by FUNCT_2:def 1;
then reconsider p=path as FinSequence by FINSEQ_1:def 2;
rng path c= KK by RELAT_1:def 19;
then reconsider p as FinSequence of K by FINSEQ_1:def 4;
consider M be Matrix of n,K such that
M = AB +* ((B*(I +* F)) | Si) and
A9: for j holds (j in Si implies M.j=B.(F.j))& (not j in Si implies M.
j=(AB).j) by A1,A2,Th59;
take (mm $$ p)*Det M;
let F9 be Function of Si,Seg n such that
A10: F9=x;
let M9 be Matrix of n,n,K such that
M9 = A*B +* ((B*(I +* F9)) | Si) and
A11: for j holds (j in Seg i implies M9.j=B.(F9.j))& (not j in Seg i
implies M9.j=(A*B).j);
take p;
dom path=Si by FUNCT_2:def 1;
hence len p=i & for Fj,j be Nat st j in Si & Fj=F9.j holds p.j=A*(j,Fj) by
A8,A10,A4,FINSEQ_1:def 3;
A12: len M9=n by MATRIX_0:24;
A13: now
let k be Nat such that
1 <=k and
k <= len M;
per cases;
suppose
A14: k in Si;
then M.k=B.(F.k) by A9;
hence M.k=M9.k by A10,A11,A14;
end;
suppose
A15: not k in Si;
then M.k=AB.k by A9;
hence M.k=M9.k by A11,A15;
end;
end;
len M=n by MATRIX_0:24;
hence thesis by A12,A13,FINSEQ_1:14;
end;
consider P be Function of FF,KK such that
A16: for x be Element of FF holds PP[x,P.x] from FUNCT_2:sch 3(A3);
reconsider P as Function of Funcs(Si,Seg n),KK;
take P;
let F be Function of Si,Seg n;
reconsider F9=F as Function of Si,Sn;
let M be Matrix of n,K such that
A17: M = A*B +* ((B*(I +* F)) | Si) and
A18: for j holds (j in Si implies M.j=B.(F.j))& (not j in Si implies M.j
=(A*B).j);
F9 in FF by FUNCT_2:8;
hence thesis by A16,A17,A18;
end;
theorem Th60:
for A,B be Matrix of n,K st 0 < n ex P be Function of Funcs(Seg
n,Seg n),the carrier of K st ( for F be Function of Seg n,Seg n ex Path be
FinSequence of K st len Path = n & (for Fj,j be Nat st j in Seg n & Fj = F.j
holds Path.j = A*(j,Fj))& P.F= (the multF of K) $$ Path * Det (B*F) ) & Det(A*B
) = (the addF of K) $$ (In(Funcs(Seg n,Seg n),Fin Funcs(Seg n,Seg n)),P)
proof
let A,B be Matrix of n,K such that
A1: 0 < n;
set AB=A*B;
set aa=the addF of K;
set I=idseq n;
set mm= the multF of K;
set KK=the carrier of K;
defpred FF[Function,Nat] means for F be Function of Seg $2,Seg n for M be
Matrix of n,n,K st M = A*B +* ((B*(I +* F)) | Seg $2) & for j holds
(j in Seg $2
implies M.j=B.(F.j))& (not j in Seg $2 implies M.j=(A*B).j) ex Path be
FinSequence of K st len Path=$2 & (for Fj,j be Nat st j in Seg $2 & Fj=F.j
holds Path.j=A*(j,Fj)) & $1.F= mm $$ Path * Det M;
defpred P[Nat] means $1<=n implies for FUNC be non empty set st FUNC=Funcs(
Seg $1,Seg n) ex P be Function of FUNC,KK st FF[P,$1] & Det(AB) = aa $$ (
In(FUNC,Fin FUNC),P);
A2: for k be Nat st P[k] holds P[k+1]
proof
set Y=Seg n;
let k be Nat such that
A3: P[k];
set X=Seg k;
reconsider FUNC=Funcs(Seg k,Seg n) as non empty set by A1;
set k1=k+1;
assume
A4: k1 <= n;
set Xx=Seg k\/{k1};
let FUNC1 be non empty set such that
A5: FUNC1=Funcs(Seg k1,Seg n);
consider P1 be Function of FUNC1,KK such that
A6: FF[P1,k1] by A4,A5,Lm10;
reconsider FUNC19=Funcs(Xx,Y) as non empty set by A5,FINSEQ_1:9;
A7: FUNC1=Funcs(Xx,Y) by A5,FINSEQ_1:9;
then reconsider P19=P1 as Function of FUNC19,KK;
A8: k+0<=k1 by XREAL_1:8;
then consider P be Function of FUNC,KK such that
A9: FF[P,k] and
A10: Det(AB) = aa $$ (In(FUNC,Fin FUNC),P) by A3,A4,XXREAL_0:2;
A11: not k1 in X by FINSEQ_3:8;
A12: for H be Function of X,Y, SF be Element of Fin FUNC19 st SF={h where
h is Function of Xx,Y: h|X=H} holds aa $$ (SF,P19)=P.H
proof
reconsider YY=Y as non empty set by A1;
let H be Function of X,Y, SF be Element of Fin FUNC19 such that
A13: SF={h where h is Function of Xx,Y: h|X=H};
defpred Q[object,object] means
for h be Function of Xx,Y st h|X=H & h.k1=$1
holds h=$2;
A14: for y being object st y in YY ex f9 be object st f9 in SF & Q[y,f9]
proof
let y be object;
assume y in YY;
then Y\/{y}=Y by ZFMISC_1:40;
then consider q be Function of Xx,Y such that
A15: q|X=H and
A16: q.k1=y by A11,STIRL2_1:57;
take q;
thus q in SF by A13,A15;
let h be Function of Xx,Y such that
A17: h|X=H and
A18: h.k1=y;
now
let x be object;
assume x in Xx;
then
A19: x in X or x in {k1} by XBOOLE_0:def 3;
dom H=X by A1,FUNCT_2:def 1;
then q.x=H.x & h.x=H.x or x=k1 by A15,A17,A19,FUNCT_1:47,TARSKI:def 1
;
hence h.x = q.x by A16,A18;
end;
hence thesis by FUNCT_2:12;
end;
consider QQ be Function of YY,SF such that
A20: for y being object st y in YY holds Q[y,QQ.y] from FUNCT_2:sch 1(A14);
A21: SF c= rng QQ
proof
let y be object;
k1 in {k1} by TARSKI:def 1;
then
A22: k1 in Xx by XBOOLE_0:def 3;
assume
A23: y in SF;
then consider h be Function of Xx,Y such that
A24: y=h and
A25: h|X=H by A13;
dom h=Xx by A1,FUNCT_2:def 1;
then
A26: h.k1 in rng h by A22,FUNCT_1:def 3;
A27: rng h c= Y by RELAT_1:def 19;
dom QQ=YY by A23,FUNCT_2:def 1;
then QQ.(h.k1) in rng QQ by A26,A27,FUNCT_1:def 3;
hence thesis by A20,A24,A25,A26,A27;
end;
rng QQ c= SF by RELAT_1:def 19;
then
A28: rng QQ=SF by A21;
Y\/{n}=Y by A1,FINSEQ_1:3,ZFMISC_1:40;
then consider h be Function of Xx,Y such that
A29: h|X=H and
h.k1=n by A11,STIRL2_1:57;
A30: SF c= FUNC19 by FINSUB_1:def 5;
k<=n by A4,A8,XXREAL_0:2;
then consider Mh be Matrix of n,K such that
A31: Mh = AB +* ((B*(I +* H)) | Seg k) and
A32: for j holds (j in Seg k implies Mh.j=B.(H.j))& (not j in Seg k
implies Mh.j=AB.j) by A1,Th59;
consider Path be FinSequence of K such that
A33: len Path=k and
A34: for Hj,j be Nat st j in Seg k & Hj=H.j holds Path.j=A*(j,Hj) and
A35: P.H= mm $$ Path * Det Mh by A9,A31,A32;
A36: Mh.k1=AB.k1 by A11,A32;
h in SF by A13,A29;
then reconsider QQ as Function of YY,FUNC19 by A28,A30,FUNCT_2:6;
A37: dom (P19*QQ)=Y by FUNCT_2:def 1;
A38: QQ.:dom QQ= SF by A28,RELAT_1:113;
1+0<=k1 by XREAL_1:7;
then
A39: k1 in Seg n by A4;
then
A40: AB.k1=Line(AB,k1) by MATRIX_0:52;
Mh.k1=Line(Mh,k1) by A39,MATRIX_0:52;
then Mh=RLine(Mh,k1,Line(AB,k1)) by A36,A40,Th30;
then consider SUM1 be FinSequence of KK such that
A41: len SUM1 = n and
A42: Det Mh = aa"**" SUM1 and
A43: for j st j in Y holds SUM1.j= A*(k1,j)*Det RLine(Mh,k1,Line(B,j
)) by A39,Th56;
A44: dom id Y=Y;
set PA=mm "**" Path;
set PS=PA*SUM1;
len PS=n by A41,Lm5;
then
A45: dom PS=Y by FINSEQ_1:def 3;
set PSaa=[#](PS,the_unity_wrt aa);
A46: for j be Nat st j in Y holds (P19*QQ).j=PA*(A*(k1,j))* Det RLine(Mh
,k1,Line(B,j))
proof
A47: width B=n by MATRIX_0:24;
A48: len Mh=n by MATRIX_0:24;
A49: dom (P19*QQ)=Y by FUNCT_2:def 1;
A50: width Mh=n by MATRIX_0:24;
let j be Nat such that
A51: j in Y;
Y\/{j}=Y by A51,ZFMISC_1:40;
then consider hj be Function of Xx,Y such that
A52: hj|X=H and
A53: hj.k1=j by A11,STIRL2_1:57;
set L=Line(B,j);
set R=RLine(Mh,k1,L);
Xx=Seg k1 by FINSEQ_1:9;
then reconsider hj9=hj as Function of Seg k1,Y;
consider Mhj be Matrix of n,K such that
A54: Mhj = AB +* ((B*(I +* hj9)) | Seg k1) and
A55: for i holds (i in Seg k1 implies Mhj.i=B.(hj9.i))& (not i in
Seg k1 implies Mhj.i=AB.i) by A4,Th59;
A56: len Mhj=n by MATRIX_0:24;
A57: len L=width B by MATRIX_0:def 7;
A58: now
A59: k+0 < k1 by XREAL_1:8;
let i be Nat such that
A60: 1 <=i and
A61: i <= len Mhj;
A62: i in Seg n by A56,A60,A61;
per cases;
suppose
A63: i <=k;
then i<=k1 by A59,XXREAL_0:2;
then
A64: i in Seg k1 by A60;
A65: Line(R,i)=R.i by A62,MATRIX_0:52;
A66: i in X by A60,A63;
then
A67: Mh.i=B.(H.i) by A32;
dom H=X by A56,A60,A61,FUNCT_2:def 1;
then
A68: H.i=hj.i by A52,A66,FUNCT_1:47;
A69: Line(Mh,i)=Mh.i by A62,MATRIX_0:52;
Line(R,i)=Line(Mh,i) by A62,A59,A63,Th28;
hence Mhj.i=R.i by A55,A65,A69,A67,A68,A64;
end;
suppose
A70: i>k & i<=k1;
A71: k1 in Seg k1 by FINSEQ_1:4;
A72: L=B.j by A51,MATRIX_0:52;
A73: R.i=Line(R,i) by A62,MATRIX_0:52;
A74: i=k1 by A70,NAT_1:9;
then L=Line(R,i) by A57,A47,A50,A62,Th28;
hence Mhj.i=R.i by A53,A55,A74,A71,A73,A72;
end;
suppose
A75: i>k & i>k1;
then not i in Seg k1 by FINSEQ_1:1;
then
A76: Mhj.i=AB.i by A55;
A77: Line(R,i)=R.i by A62,MATRIX_0:52;
A78: not i in X by A75,FINSEQ_1:1;
A79: Line(Mh,i)=Mh.i by A62,MATRIX_0:52;
Line(R,i)=Line(Mh,i) by A62,A75,Th28;
hence Mhj.i=R.i by A32,A77,A79,A78,A76;
end;
end;
len R=len Mh by Lm4;
then R=Mhj by A48,A56,A58;
then consider Pathj be FinSequence of K such that
A80: len Pathj=k1 and
A81: for m,j be Nat st j in Seg k1 & m=hj.j holds Pathj.j=A*(j,m) and
A82: P1.hj= (mm "**" Pathj) * Det R by A6,A54,A55;
A83: Pathj.k1=A*(k1,j) by A53,A81,FINSEQ_1:4;
A84: now
A85: rng H c= Y by RELAT_1:def 19;
A86: X=dom H by A51,FUNCT_2:def 1;
let i be Nat such that
A87: 1 <=i and
A88: i <= len Path;
A89: (Pathj|k).i=Pathj.i by A33,A88,FINSEQ_3:112;
A90: i in X by A33,A87,A88;
then H.i in rng H by A86,FUNCT_1:def 3;
then H.i in Y by A85;
then reconsider Hi=H.i as Nat;
i<=k1 by A8,A33,A88,XXREAL_0:2;
then
A91: i in Seg k1 by A87;
i in X by A33,A87,A88;
then
A92: Path.i=A*(i,Hi) by A34;
H.i=hj.i by A52,A90,A86,FUNCT_1:47;
hence Path.i=(Pathj|X).i by A81,A91,A92,A89;
end;
len (Pathj|k)=k by A8,A80,FINSEQ_1:59;
then Pathj=Path^<*Pathj.k1*> by A33,A80,A84,FINSEQ_1:14,FINSEQ_3:55;
then
A93: mm "**" Pathj = PA*(A*(k1,j)) by A83,FINSOP_1:4;
QQ.j=hj by A20,A51,A52,A53;
hence thesis by A51,A82,A49,A93,FUNCT_1:12;
end;
now
let y being object such that
A94: y in dom PS;
reconsider j=y as Nat by A94;
SUM1.j = A*(k1,j)*Det RLine(Mh,k1,Line(B,j)) by A43,A45,A94;
hence PS.y =PA*(A*(k1,j)*Det RLine(Mh,k1,Line(B,j))) by A94,FVSUM_1:50
.=PA*(A*(k1,j))*Det RLine(Mh,k1,Line(B,j)) by GROUP_1:def 3
.=(P19*QQ).y by A46,A45,A94;
end;
then PS=P19*QQ by A37,A45,FUNCT_1:2;
then
A95: PSaa| (dom PS)=(P19*QQ) by SETWOP_2:21;
now
let x1,x2 be object such that
A96: x1 in Y and
A97: x2 in Y and
A98: QQ.x1 = QQ.x2;
Y\/{x2}=Y by A97,ZFMISC_1:40;
then
A99: ex h2 be Function of Xx,Y st h2|X=H & h2.k1=x2 by A11,STIRL2_1:57;
Y\/{x1}=Y by A96,ZFMISC_1:40;
then consider h1 be Function of Xx,Y such that
A100: h1|X=H and
A101: h1.k1=x1 by A11,STIRL2_1:57;
QQ.x1=h1 by A20,A96,A100,A101;
hence x1=x2 by A20,A97,A98,A101,A99;
end;
then
A102: QQ is one-to-one by FUNCT_2:19;
reconsider Y9=Y as Element of Fin YY by FINSUB_1:def 5;
A103: dom QQ=Y9 by FUNCT_2:def 1;
A104: rng id Y =Y;
(P19*QQ)*(id Y)=P19*QQ by A37,RELAT_1:52;
then aa $$ (Y9,P19*QQ) = aa $$(findom PS,PSaa) by A45,A44,A104,A95,
SETWOP_2:5
.= Sum(PS) by FVSUM_1:8,SETWOP_2:def 2
.= PA*Sum(SUM1) by FVSUM_1:73
.= P.H by A35,A42;
hence thesis by A102,A38,A103,SETWOP_2:6;
end;
aa is having_a_unity by FVSUM_1:8;
then Det AB=aa $$(In(FUNC19,Fin FUNC19),P19) by A1,A10,A11,A12,Th58;
hence thesis by A6,A7;
end;
set FUN=Funcs(Seg n,Seg n);
A105: P[0]
proof
reconsider E={} as Function of Seg 0,Seg n by XBOOLE_1:2;
assume 0<=n;
A106: the_unity_wrt mm=1_K by GROUP_1:22;
let FUNC be non empty set such that
A107: FUNC=Funcs(Seg 0,Seg n);
consider P be Function of FUNC,KK such that
A108: FF[P,0] by A1,A107,Lm10;
A109: FUNC={E} by A107,FUNCT_5:57;
then
A110: E in FUNC by TARSKI:def 1;
FUNC is finite by A109; then
FUNC in Fin FUNC by FINSUB_1:def 5; then
In(FUNC,Fin FUNC)={E} by A109,SUBSET_1:def 8;
then
A111: aa $$ (In(FUNC,Fin FUNC),P)=P.E by A110,SETWISEO:17;
consider M be Matrix of n,K such that
A112: M = AB +* ((B*(I +* E)) | (Seg 0 qua set)) and
A113: for j holds (j in Seg 0 implies M.j=B.(E.j))& (not j in Seg 0
implies M.j=AB.j)by A1,Th59;
A114: M=AB +* {} by A112;
consider Path be FinSequence of K such that
A115: len Path=0 and
for Fj,j be Nat st j in Seg 0 & Fj=E.j holds Path.j=A*(j,Fj) and
A116: P.E= mm $$ Path * Det M by A108,A112,A113;
Path=<*>KK by A115;
then mm "**" Path= 1_K by A106,FINSOP_1:10;
then P.E=Det AB by A116,A114;
hence thesis by A108,A111;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A105,A2);
then consider P be Function of FUN,KK such that
A117: FF[P,n] and
A118: Det(AB) = aa $$ (In(FUN,Fin FUN),P);
take P;
thus for F be Function of Seg n,Seg n ex Path be FinSequence of K st len
Path=n & (for Fj,j be Nat st j in Seg n & Fj=F.j holds Path.j=A*(j,Fj)) & P.F=
(the multF of K) $$ Path * Det (B*F)
proof
len AB=n by MATRIX_0:24;
then
A119: dom AB=Seg n by FINSEQ_1:def 3;
let F be Function of Seg n,Seg n;
A120: dom I=Seg n;
dom F=Seg n by FUNCT_2:52;
then
A121: I+*F=F by A120,FUNCT_4:19;
A122: len B=n by MATRIX_0:24;
len (B*F)=len B by Def4;
then
A123: dom (B*F)=Seg n by A122,FINSEQ_1:def 3;
consider M be Matrix of n,K such that
A124: M = AB +* ((B*(I +* F)) | Seg n) and
A125: for j holds (j in Seg n implies M.j=B.(F.j))& (not j in Seg n
implies M.j=AB.j)by A1,Th59;
M=B*F by A124,A121,A123,A119,FUNCT_4:19;
hence thesis by A117,A124,A125;
end;
thus thesis by A118;
end;
theorem Th61:
for A,B be Matrix of n,K st 0 < n ex P be Function of
Permutations n,the carrier of K st Det(A*B) = (the addF of K) $$
(In(Permutations n,Fin Permutations n),P) &
for perm be Element of Permutations n holds P.perm= (the
multF of K) $$ Path_matrix(perm,A) * -(Det B,perm)
proof
let A,B be Matrix of n,K such that
A1: 0 < n;
set P=Permutations n;
A2: dom id P=P;
set KK=the carrier of K;
set mm=the multF of K;
set aa=the addF of K;
set AB=A*B;
set X=Seg n;
set F=Funcs(X,X);
consider SUM1 be Function of F,KK such that
A3: for F be Function of X,X ex Path be FinSequence of K st len Path=n &
(for Fj,j be Nat st j in Seg n & Fj=F.j holds Path.j=A*(j,Fj)) & SUM1.F= mm $$
Path * Det (B*F) and
A4: Det(AB)=aa $$ (In(F,Fin F),SUM1) by A1,Th60;
reconsider FP=F\P as Element of Fin F by FINSUB_1:def 5;
A6: P c= F
proof
let x be object;
assume x in P;
then reconsider p=x as Permutation of X by MATRIX_1:def 16;
p is Element of F by FUNCT_2:9;
hence thesis;
end;
then reconsider P9=P as Element of Fin F by FINSUB_1:def 5;
P in Fin P by FINSUB_1:def 5; then
A7: P=In (P,Fin P) by SUBSET_1:def 8;
F in Fin F by FINSUB_1:def 5; then
A8: In (F,Fin F)=F by SUBSET_1:def 8;
A9: now
per cases;
suppose
FP={};
then F c= P by XBOOLE_1:37;
hence Det(AB)=aa $$ (P9,SUM1) by A4,A8,A6,XBOOLE_0:def 10;
end;
suppose
A10: FP<>{};
A11: 0.K = the_unity_wrt aa by FVSUM_1:7;
A12: SUM1.:FP c= {0.K}
proof
let s be object;
assume s in SUM1.:FP;
then consider x being object such that
x in dom SUM1 and
A13: x in FP and
A14: s = SUM1.x by FUNCT_1:def 6;
reconsider f=x as Function of X,X by A13,FUNCT_2:66;
not f in P by A13,XBOOLE_0:def 5;
then
A15: Det(B*f)=0.K by Th54;
ex Path be FinSequence of K st len Path=n &( for Fj,j be Nat st
j in Seg n & Fj=f.j holds Path.j=A*(j,Fj))& SUM1.f= (mm $$ Path) * Det ( B*f)
by A3;
then SUM1.f=0.K by A15;
hence thesis by A14,TARSKI:def 1;
end;
dom SUM1=F by FUNCT_2:def 1;
then SUM1.:FP={0.K} by A10,A12,ZFMISC_1:33;
then
A16: aa $$ (FP,SUM1)=0.K by A11,FVSUM_1:8,SETWOP_2:8;
A17: FP misses P by XBOOLE_1:79;
A18: FP\/P=F\/P by XBOOLE_1:39;
F\/P=F by A6,XBOOLE_1:12;
hence Det(AB) = aa $$ (P9,SUM1)+0.K by A4,A8,A16,A17,A18,FVSUM_1:8
,SETWOP_2:4
.= aa $$ (P9,SUM1) by RLVECT_1:4;
end;
end;
dom SUM1=F by FUNCT_2:def 1;
then
A19: dom (SUM1|P)=P by A6,RELAT_1:62;
rng (SUM1|P) c= KK by RELAT_1:def 19;
then reconsider SP=SUM1|P as Function of P,KK by A19,FUNCT_2:2;
take SP;
A20: rng id P=P;
SP*id P=SP by A19,RELAT_1:52;
hence Det(AB)=aa $$ (In(P,Fin P),SP) by A9,A2,A20,A7,SETWOP_2:5;
let perm be Element of P;
reconsider Perm=perm as Permutation of X by MATRIX_1:def 16;
SUM1.Perm=SP.Perm by A19,FUNCT_1:47;
then consider Path be FinSequence of K such that
A21: len Path=n and
A22: for Fj,j be Nat st j in Seg n & Fj=Perm.j holds Path.j=A*(j,Fj) and
A23: SP.Perm= mm $$ Path * Det (B*Perm) by A3;
set PM=Path_matrix(perm,A);
A24: len PM=n by MATRIX_3:def 7;
now
A25: X=dom Perm by FUNCT_2:52;
let i be Nat such that
A26: 1 <= i and
A27: i <= len Path;
A28: i in X by A21,A26,A27;
i in X by A21,A26,A27;
then
A29: Perm.i in rng Perm by A25,FUNCT_1:def 3;
rng Perm c= X by RELAT_1:def 19;
then Perm.i in X by A29;
then reconsider Pi=Perm.i as Element of NAT;
dom PM=X by A24,FINSEQ_1:def 3;
then PM.i=A*(i,Pi) by A28,MATRIX_3:def 7;
hence Path.i=PM.i by A22,A28;
end;
then Path=PM by A21,A24;
hence thesis by A23,Th46;
end;
::------------------------------------------::
:: Determinant of a product of ::
:: two square matrices ::
::------------------------------------------::
theorem
for A,B be Matrix of n,K st 0 < n holds Det (A * B) = Det A * Det B
proof
let A,B be Matrix of n,K such that
A1: 0 < n;
set P=Permutations n;
set KK=the carrier of K;
set mm=the multF of K;
set aa=the addF of K;
set AB = A * B;
consider SUM1 be Function of P,KK such that
A2: Det(AB) = aa $$ (In(P,Fin P),SUM1) and
A3: for perm be Element of Permutations n holds SUM1.perm = mm $$
Path_matrix(perm,A) * -(Det B,perm) by A1,Th61;
set Path=Path_product(A);
set F=In(P,Fin P);
P in Fin P by FINSUB_1:def 5; then
A4: F=P by SUBSET_1:def 8;
then consider Ga be Function of Fin P,KK such that
A5: Det A = Ga.F and
A6: for e being Element of KK st e is_a_unity_wrt aa holds Ga.{} = e and
A7: for x being Element of P holds Ga.{x} = Path.x and
A8: for B9 being Element of Fin P st B9 c= F & B9 <> {} for x being
Element of P st x in F \ B9 holds Ga.(B9 \/ {x}) = aa.(Ga.B9,Path.x) by
SETWISEO:def 3;
A9: Ga.{}=0.K by A6,FVSUM_1:6;
consider Gs be Function of Fin P,KK such that
A10: Det(AB) = Gs.F and
A11: for e being Element of KK st e is_a_unity_wrt aa holds Gs.{} = e and
A12: for x being Element of P holds Gs.{x} = SUM1.x and
A13: for B9 being Element of Fin P st B9 c= F & B9 <> {} for x being
Element of P st x in F \ B9 holds Gs.(B9 \/ {x}) = aa.(Gs.B9,SUM1.x)
by A2,A4,SETWISEO:def 3;
defpred S[set] means for B9 be Element of Fin P st B9=$1 holds Gs.B9=(Ga.B9)
*Det B;
A14: for B9 be (Element of Fin P), b be Element of P holds S[B9] & not b in
B9 implies S[B9 \/ {b}]
proof
let B9 be (Element of Fin P), b be Element of P;
assume that
A15: S[B9] and
A16: not b in B9;
set mA=mm $$ Path_matrix(b,A);
let Bb be Element of Fin P such that
A17: Bb=B9\/{b};
A18: now
per cases;
suppose
A19: b is even;
then
A20: -(mA,b)=mA by MATRIX_1:def 20;
-(Det B,b)=Det B by A19,MATRIX_1:def 20;
hence SUM1.b = -(mA,b)*Det B by A3,A20
.= Path.b*Det B by MATRIX_3:def 8;
end;
suppose
A21: b is odd;
then
A22: -(mA,b)=-mA by MATRIX_1:def 20;
-(Det B,b)=-Det B by A21,MATRIX_1:def 20;
then -(-(mA,b)*(Det B)) = (-mA)*(-(Det B,b)) by A22,VECTSP_1:9
.= -(mA*-(Det B,b)) by VECTSP_1:9;
then (mA*-(Det B,b))--(mA,b)*(Det B)=0.K by VECTSP_1:16;
then
A23: -(mA,b)*(Det B)=mA*-(Det B,b) by VECTSP_1:19;
-(mA,b)=Path.b by MATRIX_3:def 8;
hence SUM1.b=Path.b*Det B by A3,A23;
end;
end;
per cases;
suppose
A24: B9={};
then Ga.Bb = Path.b by A7,A17;
hence thesis by A12,A17,A18,A24;
end;
suppose
A25: B9<>{};
A26: B9 c= P by FINSUB_1:def 5;
A27: b in F\B9 by A4,A16,XBOOLE_0:def 5;
then Gs.Bb = aa.(Gs.B9,SUM1.b) by A4,A13,A17,A25,A26;
then
A28: Gs.Bb=((Ga.B9)*Det B)+(Path.b*Det B) by A15,A18;
Ga.Bb=Ga.B9+Path.b by A4,A8,A17,A25,A27,A26;
hence thesis by A28,VECTSP_1:def 7;
end;
end;
Gs.{}=0.K by A11,FVSUM_1:6;
then
A29: S[{}.P] by A9;
for B be Element of Fin P holds S[B] from SETWISEO:sch 2(A29,A14);
hence thesis by A10,A5;
end;