:: On the Permanent of a Matrix
:: by Ewa Romanowicz and Adam Grabowski
::
:: Received January 4, 2006
:: Copyright (c) 2006-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, VECTSP_1, FINSUB_1, TARSKI, XBOOLE_0, SUBSET_1,
FINSEQ_2, FINSET_1, FINSEQ_1, FUNCT_1, RELAT_1, FINSEQ_5, FUNCT_2,
CARD_1, MATRIX_1, STRUCT_0, ALGSTR_0, SETWISEO, MATRIX_3, CALCUL_2,
XXREAL_0, SUPINF_2, FUNCOP_1, BINOP_1, ARYTM_3, ORDINAL4, TREES_1,
ZFMISC_1, ARYTM_1, CARD_3, ABIAN, INT_1, PARTFUN1, GROUP_1, FUNCT_7,
MATRIX_9;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
NAT_1, NAT_D, ENUMSET1, FINSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
FINSEQ_1, FUNCOP_1, FINSEQ_2, BINOP_1, STRUCT_0, ALGSTR_0, GROUP_1,
VECTSP_1, SETWISEO, GROUP_4, SETWOP_2, FINSUB_1, MATRIX_0, FINSEQ_4,
FINSEQ_5, MATRIX_1, MATRIX_3, XXREAL_0;
constructors BINOP_1, SETWISEO, NAT_1, NAT_D, FINSEQ_4, FINSOP_1, FINSEQ_5,
ALGSTR_1, GROUP_4, MATRIX_7, RELSET_1, MATRIX_3;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, PARTFUN1, FUNCT_2,
FINSET_1, FINSUB_1, XXREAL_0, XREAL_0, FINSEQ_1, FINSEQ_5, FINSEQ_6,
STRUCT_0, GROUP_1, VECTSP_1, MATRIX_1, FVSUM_1, RELSET_1, FINSEQ_2,
CARD_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities FINSEQ_2, FINSEQ_1, ALGSTR_0;
theorems FINSEQ_1, FINSEQ_2, TARSKI, FUNCT_2, NAT_1, BINOP_1, FUNCT_1,
SETWISEO, 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,
MATRIX_3, FINSEQ_5, ENUMSET1, FINSEQ_6, GROUP_4, XREAL_1, MATRIX_7,
XXREAL_0, ORDINAL1, NAT_D, PARTFUN1, CARD_1, SUBSET_1;
schemes FUNCT_2, FINSET_1, NAT_1;
begin :: Preliminaries
reserve x for set,
i,j,k,n for Nat,
K for Field;
theorem Th1:
for a, A being set st a in A holds {a} in Fin A
proof
let a, A be set;
assume a in A;
then {a} c= A by ZFMISC_1:31;
hence thesis by FINSUB_1:def 5;
end;
registration
let n be Nat;
cluster non empty for Element of Fin Permutations n;
existence
proof
idseq n in Permutations n by MATRIX_1:def 16;
then {idseq n} in Fin Permutations n by Th1;
hence thesis;
end;
end;
scheme
NonEmptyFiniteX { n() -> Element of NAT, A() -> non empty Element of Fin
Permutations n(), P[set] } : P[A()]
provided
A1: for x being Element of Permutations n() st x in A() holds P[{x}] and
A2: for x being Element of Permutations n(), B being non empty Element
of Fin Permutations n() st x in A() & B c= A() & not x in B & P[B] holds P[B \/
{x}]
proof
defpred Q[set] means $1 is empty or P[$1];
A3: for x,B being set st x in A() & B c= A() & Q[B] holds Q[B \/ {x}]
proof
let x,B be set;
assume that
A4: x in A() and
A5: B c= A() and
A6: Q[B];
A7: A() c= Permutations n() by FINSUB_1:def 5;
then reconsider x as Element of Permutations n() by A4;
A8: B c= Permutations n() by A5,A7,XBOOLE_1:1;
per cases;
suppose
A9: x in B;
then reconsider
B as non empty Element of Fin Permutations n() by A8,FINSUB_1:def 5;
{x} c= B by A9,ZFMISC_1:31;
hence thesis by A6,XBOOLE_1:12;
end;
suppose
A10: B is non empty & not x in B;
then reconsider
B as non empty Element of Fin Permutations n() by A8,FINSUB_1:def 5;
P[B \/ {x}] by A2,A4,A5,A6,A10;
hence thesis;
end;
suppose
B is empty;
then P[B \/ {x}] by A1,A4;
hence thesis;
end;
end;
A11: Q[{}];
A12: A() is finite;
Q[A()] from FINSET_1:sch 2(A12,A11,A3);
hence thesis;
end;
Lm1: <*1,2*> <> <*2,1*> by FINSEQ_1:77;
Lm2: <*2,1*> in Permutations 2 by MATRIX_7:3,TARSKI:def 2;
registration
let n;
cluster one-to-one FinSequence-like for Function of Seg n, Seg n;
existence
proof
take f = id Seg n;
dom f = Seg n by RELAT_1:45;
hence thesis by FINSEQ_1:def 2;
end;
end;
registration
let n;
cluster id Seg n -> FinSequence-like;
coherence
proof
dom id Seg n = Seg n by RELAT_1:45;
hence thesis by FINSEQ_1:def 2;
end;
end;
theorem Th2:
(Rev idseq 2).1 = 2 & (Rev idseq 2).2 = 1
proof
reconsider f = idseq 2 as one-to-one FinSequence-like Function of Seg 2, Seg
2;
f.1 = (Rev f).len f by FINSEQ_5:62;
then
A1: (idseq 2).1 = (Rev idseq 2).2 by CARD_1:def 7;
f.(len f) = (Rev f).1 by FINSEQ_5:62;
then
A2: f.2 = (Rev f).1 by CARD_1:def 7;
A3: dom Rev f = dom f by FINSEQ_5:57;
then
A4: dom Rev f = Seg 2 by RELAT_1:45;
then 1 in dom f & 2 in dom f by A3;
hence thesis by A1,A2,A3,A4,FUNCT_1:18;
end;
theorem Th3:
for f being one-to-one Function st dom f = Seg 2 & rng f = Seg 2
holds f = id Seg 2 or f = Rev id Seg 2
proof
let f be one-to-one Function;
A1: dom idseq 2 = Seg 2 by RELAT_1:45;
assume that
A2: dom f = Seg 2 and
A3: rng f = Seg 2;
A4: 1 in dom f by A2;
then f.1 in rng f by FUNCT_1:3;
then
A5: f.1 = 1 or f.1 = 2 by A3,FINSEQ_1:2,TARSKI:def 2;
A6: 2 in dom f by A2;
then f.2 in rng f by FUNCT_1:3;
then
A7: f.2 = 2 or f.2 = 1 by A3,FINSEQ_1:2,TARSKI:def 2;
per cases by A4,A5,A6,A7,FUNCT_1:def 4;
suppose
A8: f.1 = 1 & f.2 = 2;
for x being object st x in Seg 2 holds f.x = x
proof
let x be object;
assume x in Seg 2;
then x = 1 or x = 2 by FINSEQ_1:2,TARSKI:def 2;
hence thesis by A8;
end;
hence thesis by A2,FUNCT_1:17;
end;
suppose
A9: f.1 = 2 & f.2 = 1;
A10: for x being object st x in Seg 2 holds f.x = (Rev id Seg 2).x
proof
let x be object;
assume x in Seg 2;
then x = 1 or x = 2 by FINSEQ_1:2,TARSKI:def 2;
hence thesis by A9,Th2;
end;
dom f = dom Rev id Seg 2 by A1,A2,FINSEQ_5:57;
hence thesis by A2,A10,FUNCT_1:2;
end;
end;
begin :: Permutations
theorem Th4:
Rev idseq n in Permutations n
proof
reconsider f = idseq n as one-to-one FinSequence-like Function of Seg n, Seg
n;
dom f = dom Rev f by FINSEQ_5:57;
then
A1: dom Rev f = Seg n by RELAT_1:45;
A2: rng idseq n = Seg n by FUNCT_2:def 3;
then rng Rev f c= Seg n by FINSEQ_5:57;
then reconsider
g = Rev f as FinSequence-like Function of Seg n, Seg n by A1,FUNCT_2:2;
rng f = rng Rev f by FINSEQ_5:57;
then g is onto by A2,FUNCT_2:def 3;
hence thesis by MATRIX_1:def 16;
end;
theorem Th5:
for f being FinSequence st n <> 0 & f in Permutations n holds Rev
f in Permutations n
proof
let f be FinSequence;
assume that
A1: n <> 0 and
A2: f in Permutations n;
A3: f is Permutation of Seg n by A2,MATRIX_1:def 16;
dom f = dom Rev f by FINSEQ_5:57;
then
A4: dom Rev f = Seg n by A1,A3,FUNCT_2:def 1;
A5: rng f = rng Rev f by FINSEQ_5:57;
then rng Rev f = Seg n by A3,FUNCT_2:def 3;
then reconsider g = Rev f as FinSequence-like Function of Seg n,Seg n by A4,
FUNCT_2:2;
rng f = Seg n by A3,FUNCT_2:def 3;
then g is onto by A5,FUNCT_2:def 3;
hence thesis by A3,MATRIX_1:def 16;
end;
theorem Th6:
Permutations 2 = { idseq 2, Rev idseq 2 }
proof
now
let p be object;
assume p in Permutations 2;
then reconsider q = p as Permutation of Seg 2 by MATRIX_1:def 16;
A1: rng q = Seg 2 by FUNCT_2:def 3;
A2: dom q = Seg 2 by FUNCT_2:52;
then reconsider q as FinSequence by FINSEQ_1:def 2;
q = idseq 2 or q = Rev idseq 2 by A1,A2,Th3;
hence p in {idseq 2, Rev idseq 2} by TARSKI:def 2;
end;
then
A3: Permutations 2 c= {idseq 2, Rev idseq 2 } by TARSKI:def 3;
now
let x be object;
assume x in {idseq 2, Rev idseq 2 };
then x = idseq 2 or x = Rev idseq 2 by TARSKI:def 2;
hence x in Permutations 2 by Th4,MATRIX_1:def 16;
end;
then {idseq 2, Rev idseq 2 } c= Permutations 2 by TARSKI:def 3;
hence thesis by A3,XBOOLE_0:def 10;
end;
begin :: The Permanent of a Matrix
definition
let n,K;
let M be Matrix of n,K;
func PPath_product M -> Function of Permutations n, the carrier of K means
:
Def1: for p being Element of Permutations(n) holds it.p = (the multF of K) $$
Path_matrix(p,M);
existence
proof
deffunc V(Element of Permutations n) = (the multF of K) $$ Path_matrix($1,
M);
consider f being Function of Permutations(n),the carrier of K such that
A1: for p being Element of Permutations(n) holds f.p = V(p) from
FUNCT_2:sch 4;
take f;
thus thesis by A1;
end;
uniqueness
proof
let f1,f2 be Function of Permutations(n), the carrier of K;
assume that
A2: for p being Element of Permutations(n) holds f1.p = (the multF of
K) $$ Path_matrix(p,M) and
A3: for p being Element of Permutations(n) holds f2.p = (the multF of
K) $$ Path_matrix(p,M);
now
let p be Element of Permutations(n);
f1.p = (the multF of K) $$ Path_matrix(p,M) by A2;
hence f1.p=f2.p by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
definition
let n, K;
let M be Matrix of n,K;
func Per M -> Element of K equals
(the addF of K) $$ (In (Permutations n, Fin Permutations n),
PPath_product M);
coherence;
end;
reserve a,b,c,d for Element of K;
theorem
Per <*<*a*>*> = a
proof
set M = <*<*a*>*>;
A1: (PPath_product M).(idseq 1)=a
proof
reconsider p = idseq 1 as Element of Permutations 1 by MATRIX_1:def 16;
A2: len Path_matrix(p,M) = 1 by MATRIX_3:def 7;
then
A3: dom Path_matrix(p,M) = Seg 1 by FINSEQ_1:def 3;
then
A4: 1 in dom Path_matrix(p,M);
then 1 = p.1 by A3,FUNCT_1:18;
then Path_matrix(p,M).1 = M*(1,1) by A4,MATRIX_3:def 7;
then Path_matrix(p,M).1 = a by MATRIX_0:49;
then
A5: Path_matrix(p,M) = <*a*> by A2,FINSEQ_1:40;
(PPath_product M).p = (the multF of K) $$ Path_matrix(p,M) & <*a*> = 1
|->a by Def1,FINSEQ_2:59;
hence thesis by A5,FINSOP_1:16;
end;
Permutations 1 in Fin Permutations 1 by FINSUB_1:def 5; then
In (Permutations 1, Fin Permutations 1) = Permutations 1 by SUBSET_1:def 8;
then
In (Permutations 1, Fin Permutations 1) = {idseq 1} &
idseq 1 in Permutations 1 by MATRIX_1:10,TARSKI:def 1;
hence thesis by A1,SETWISEO:17;
end;
theorem
for K being Field, n being Element of NAT st n >= 1 holds Per (0.(K,n,
n)) = 0.K
proof
let K be Field, n be Element of NAT;
set B = In (Permutations n, Fin Permutations n);
set f = PPath_product(0.(K,n,n));
set F = the addF of K;
set Y = the carrier of K;
set X = Permutations n;
reconsider G0= Fin X --> 0.K as Function of Fin X, Y;
A1: for e being Element of Y st e is_a_unity_wrt F holds G0.({}) = e
proof
let e be Element of Y;
0.K is_a_unity_wrt F by FVSUM_1:6;
then
A2: F.(0.K,e) = e by BINOP_1:3;
assume e is_a_unity_wrt F;
then F.(0.K,e) = 0.K by BINOP_1:3;
hence thesis by A2,FINSUB_1:7,FUNCOP_1:7;
end;
assume
A3: n>=1;
A4: for x being object st x in dom PPath_product(0.(K,n,n)) holds (
PPath_product(0.(K,n,n))).x = (Permutations(n) --> 0.K).x
proof
let x be object;
assume x in dom PPath_product(0.(K,n,n));
for p being Element of Permutations n holds (Permutations(n) --> 0.K).
p = (the multF of K) $$ Path_matrix(p,(0.(K,n,n)))
proof
defpred P[Nat] means (the multF of K) $$ (($1+1) |-> 0.K)=0.K;
let p be Element of Permutations(n);
A5: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
A6: (k+1+1) |-> 0.K = ((k+1) |-> 0.K) ^ <* 0.K *> by FINSEQ_2:60;
assume P[k];
then (the multF of K) $$ ( (k+1+1) |-> 0.K) = (0.K)*(0.K) by A6,
FINSOP_1:4
.= 0.K;
hence thesis;
end;
A7: for i,j st i in dom (n |-> 0.K) & j=p.i holds (n |-> 0.K).i = (0.(K,
n,n))*(i,j)
proof
let i,j;
assume that
A8: i in dom (n |-> 0.K) and
A9: j=p.i;
A10: i in Seg n by A8,FUNCOP_1:13;
then j in Seg n by A9,MATRIX_7:14;
then
A11: j in Seg width (0.(K,n,n)) by A3,MATRIX_0:23;
i in dom (0.(K,n,n)) by A10,MATRIX_7:13;
then [i,j] in [:dom (0.(K,n,n)),Seg width (0.(K,n,n)):] by A11,
ZFMISC_1:def 2;
then
A12: [i,j] in Indices (0.(K,n,n)) by MATRIX_0:def 4;
(n |-> 0.K).i=0.K by A10,FUNCOP_1:7;
hence thesis by A12,MATRIX_3:1;
end;
len (n |-> 0.K) = n by CARD_1:def 7;
then
A13: Path_matrix(p,(0.(K,n,n))) = n |-> 0.K by A7,MATRIX_3:def 7;
A14: n-'1+1=n by A3,XREAL_1:235;
1 |-> 0.K = <* 0.K *> by FINSEQ_2:59;
then
A15: P[0] by FINSOP_1:11;
for k being Nat holds P[k] from NAT_1:sch 2(A15,A5);
then (the multF of K) $$ Path_matrix(p,(0.(K,n,n))) = 0.K by A13,A14;
hence thesis by FUNCOP_1:7;
end;
hence thesis by Def1;
end;
dom (Permutations(n) --> 0.K) = Permutations(n) by FUNCOP_1:13;
then dom (PPath_product(0.(K,n,n))) = dom (Permutations(n) --> 0.K) by
FUNCT_2:def 1;
then
A16: PPath_product(0.(K,n,n)) = Permutations(n) --> 0.K by A4,FUNCT_1:2;
A17: for x being Element of X holds G0.({x}) = f.x
proof
let x be Element of X;
G0.({.x.}) = 0.K by FUNCOP_1:7;
hence thesis by A16,FUNCOP_1:7;
end;
A18: for B9 being Element of Fin X st B9 c= B & B9 <> {} for x being Element
of X st x in B\B9 holds G0.(B9 \/ {x}) = F.(G0.B9,f.x)
proof
let B9 be Element of Fin X;
assume that
B9 c= B and
B9 <> {};
thus for x being Element of X st x in B\B9 holds G0.(B9 \/ {x}) = F.(G0.B9
,f.x)
proof
let x be Element of X;
assume x in B \ B9;
A19: G0.(B9 \/ {.x.})=0.K & G0.B9 = 0.K by FUNCOP_1:7;
f.x = 0.K & 0.K is_a_unity_wrt F by A16,FUNCOP_1:7,FVSUM_1:6;
hence thesis by A19,BINOP_1:3;
end;
end;
Permutations n in Fin Permutations n by FINSUB_1:def 5; then
In (Permutations n, Fin Permutations n) = Permutations n
by SUBSET_1:def 8; then
In (Permutations n, Fin Permutations n) <> {} & G0.B=0.K by FUNCOP_1:7;
hence thesis by A1,A17,A18,SETWISEO:def 3;
end;
theorem Th9:
for p being Element of Permutations 2 st p = idseq 2 holds
Path_matrix (p, (a,b)][(c,d)) = <* a,d *>
proof
let p be Element of Permutations 2 such that
A1: p = idseq 2;
A2: len Path_matrix (p, (a,b)][(c,d)) = 2 by MATRIX_3:def 7;
then
A3: dom Path_matrix (p, (a,b)][(c,d)) = Seg 2 by FINSEQ_1:def 3;
then
A4: 2 in dom Path_matrix (p, (a,b)][(c,d));
then 2 = p.2 by A1,A3,FUNCT_1:18;
then
A5: Path_matrix (p, (a,b)][(c,d)).2=(a,b)][(c,d)*(2,2) by A4,MATRIX_3:def 7
.= d by MATRIX_0:50;
A6: 1 in dom Path_matrix (p, (a,b)][(c,d)) by A3;
then 1 = p.1 by A1,A3,FUNCT_1:18;
then Path_matrix (p, (a,b)][(c,d)).1=(a,b)][(c,d)*(1,1) by A6,MATRIX_3:def 7
.= a by MATRIX_0:50;
hence thesis by A2,A5,FINSEQ_1:44;
end;
theorem Th10:
for p being Element of Permutations 2 st p = Rev idseq 2 holds
Path_matrix (p, (a,b)][(c,d)) = <* b,c *>
proof
let p be Element of Permutations 2 such that
A1: p = Rev idseq 2;
A2: len Path_matrix (p, (a,b)][(c,d)) = 2 by MATRIX_3:def 7;
then
A3: dom Path_matrix (p, (a,b)][(c,d)) = Seg 2 by FINSEQ_1:def 3;
then 1 in dom Path_matrix (p, (a,b)][(c,d));
then
A4: Path_matrix (p, (a,b)][(c,d)).1=(a,b)][(c,d)*(1,2) by A1,Th2,MATRIX_3:def 7
.= b by MATRIX_0:50;
2 in dom Path_matrix (p, (a,b)][(c,d)) by A3;
then Path_matrix (p, (a,b)][(c,d)).2=(a,b)][(c,d)*(2,1) by A1,Th2,
MATRIX_3:def 7
.=c by MATRIX_0:50;
hence thesis by A2,A4,FINSEQ_1:44;
end;
theorem Th11:
(the multF of K) $$ <* a,b *> = a * b
proof
(the multF of K) $$ <* a,b *> = Product <*a,b*> by GROUP_4:def 2
.= a * b by GROUP_4:10;
hence thesis;
end;
begin
registration
cluster odd for Permutation of Seg 2;
existence
proof
reconsider g = <*2,1*> as Permutation of Seg 2 by Lm2,MATRIX_1:def 16;
not ex l be FinSequence of Group_of_Perm 2 st (len l) mod 2 = 0 & g =
Product l & for i st i in dom l ex q being Element of Permutations 2 st l.i = q
& q is being_transposition by Lm1,MATRIX_7:11;
then g is odd by MATRIX_1:def 19;
hence thesis;
end;
end;
registration
let n be Nat;
cluster even for Permutation of Seg n;
existence
proof
reconsider f = id Seg n as Permutation of Seg n;
f is even by MATRIX_1:16;
hence thesis;
end;
end;
theorem Th12:
<*2,1*> is odd Permutation of Seg 2
proof
reconsider g = <*2,1*> as Permutation of Seg 2 by Lm2,MATRIX_1:def 16;
not ex l be FinSequence of Group_of_Perm 2 st (len l) mod 2 = 0 & g =
Product l & for i st i in dom l ex q being Element of Permutations 2 st l.i = q
& q is being_transposition by Lm1,MATRIX_7:11;
hence thesis by MATRIX_1:def 19;
end;
theorem
Det (a,b)][(c,d) = a * d - b * c
proof
reconsider rid2 = Rev idseq 2 as Element of Permutations 2 by Th4;
set M = (a,b)][(c,d);
reconsider id2 = idseq 2 as Permutation of Seg 2;
reconsider Id2 = idseq 2 as Element of Permutations 2 by MATRIX_1:def 16;
set F = the addF of K;
set f = Path_product M;
A1: rid2 = <*2,1*> & len Permutations 2 = 2 by FINSEQ_2:52,FINSEQ_5:61
,MATRIX_1:9;
A2: f.rid2 = -((the multF of K) $$ Path_matrix (rid2,M),rid2) by MATRIX_3:def 8
.= -(the multF of K) $$ Path_matrix (rid2,M) by A1,Th12,MATRIX_1:def 20
.= -(the multF of K) $$ <*b,c*> by Th10
.= -b*c by Th11;
len Permutations 2 = 2 by MATRIX_1:9;
then
A3: Id2 is even by MATRIX_1:16;
1 in Seg 2;
then
A4: id2 <> rid2 by Th2,FUNCT_1:18;
A5: f.id2 = -((the multF of K) $$ Path_matrix (Id2,M),Id2) by MATRIX_3:def 8
.= (the multF of K) $$ Path_matrix (Id2,M) by A3,MATRIX_1:def 20
.= (the multF of K) $$ <*a,d*> by Th9
.= a*d by Th11;
Permutations 2 in Fin Permutations 2 by FINSUB_1:def 5; then
In (Permutations 2, Fin Permutations 2) = Permutations 2
by SUBSET_1:def 8;
then Det M = F $$ ({.Id2,rid2.},f) by Th6,MATRIX_3:def 9
.= a*d - b*c by A5,A4,A2,SETWOP_2:1;
hence thesis;
end;
theorem
Per (a,b)][(c,d) = a * d + b * c
proof
reconsider rid2 = Rev idseq 2 as Element of Permutations 2 by Th4;
set M = (a,b)][(c,d);
reconsider Id2 = idseq 2 as Element of Permutations 2 by MATRIX_1:def 16;
reconsider id2 = Id2 as Permutation of Seg 2;
set f = PPath_product M;
A0: 1 in Seg 2;
Permutations 2 in Fin Permutations 2 by FINSUB_1:def 5; then
A1: In (Permutations 2, Fin Permutations 2) = Permutations 2 &
id2 <> rid2 by A0,Th2,FUNCT_1:18,SUBSET_1:def 8;
A2: f.rid2 = (the multF of K) $$ Path_matrix (rid2,M) by Def1
.= (the multF of K) $$ <*b,c*> by Th10
.= b*c by Th11;
f.id2 = (the multF of K) $$ Path_matrix (Id2,M) by Def1
.= (the multF of K) $$ <*a,d*> by Th9
.= a*d by Th11;
hence thesis by A2,A1,Th6,SETWOP_2:1;
end;
theorem Th15:
Rev idseq 3 = <*3,2,1*>
proof
reconsider h = <*2,3*> as FinSequence of NAT;
<*1*>^h = <*1,2,3*> & Rev h = <*3,2*> by FINSEQ_1:43,FINSEQ_5:61;
hence thesis by FINSEQ_2:53,FINSEQ_6:24;
end;
reserve D for non empty set;
theorem
for x,y,z being Element of D for f being FinSequence of D st f = <*x,y
,z*> holds Rev f = <*z,y,x*>
proof
let x,y,z be Element of D;
let f be FinSequence of D;
reconsider h = <*y,z*> as FinSequence of D;
assume f = <*x,y,z*>;
then
A1: f = <*x*>^h by FINSEQ_1:43;
Rev h = <*z,y*> by FINSEQ_5:61;
hence thesis by A1,FINSEQ_6:24;
end;
theorem Th17:
for f, g being FinSequence st f ^ g in Permutations n holds f ^
Rev g in Permutations n
proof
let f, g be FinSequence;
A1: rng g = rng Rev g by FINSEQ_5:57;
set h = f ^ Rev g;
assume f ^ g in Permutations n;
then
A2: f ^ g is Permutation of Seg n by MATRIX_1:def 16;
then
A3: g is one-to-one by FINSEQ_3:91;
dom (f ^ g) = Seg n by A2,FUNCT_2:52;
then
A4: Seg n = Seg (len f + len g) by FINSEQ_1:def 7;
len g = len Rev g by FINSEQ_5:def 3;
then
A5: dom h = Seg n by A4,FINSEQ_1:def 7;
A6: rng (f^g) = rng f \/ rng g by FINSEQ_1:31
.= rng (f^Rev g) by A1,FINSEQ_1:31;
A7: rng (f^g) = Seg n by A2,FUNCT_2:def 3;
then reconsider h as FinSequence-like Function of Seg n, Seg n by A6,A5,
FUNCT_2:2;
A8: h is onto by A7,A6,FUNCT_2:def 3;
rng f misses rng g & f is one-to-one by A2,FINSEQ_3:91;
then h is one-to-one by A1,A3,FINSEQ_3:91;
hence thesis by A8,MATRIX_1:def 16;
end;
theorem Th18:
for f, g being FinSequence st f ^ g in Permutations n holds g ^
f in Permutations n
proof
let f, g be FinSequence;
A1: Seg len(f^g) = dom (f^g) by FINSEQ_1:def 3;
len(f^g) = len f + len g by FINSEQ_1:22
.= len (g^f) by FINSEQ_1:22;
then
A2: dom (f^g) = dom (g^f) by A1,FINSEQ_1:def 3;
A3: rng (f^g) = rng f \/ rng g by FINSEQ_1:31
.= rng (g^f) by FINSEQ_1:31;
assume f ^ g in Permutations n;
then
A4: f ^ g is Permutation of Seg n by MATRIX_1:def 16;
then
A5: rng (f ^ g) = Seg n by FUNCT_2:def 3;
A6: g is one-to-one by A4,FINSEQ_3:91;
dom (f ^ g) = Seg n by A4,FUNCT_2:52;
then reconsider
h = g ^ f as FinSequence-like Function of Seg n, Seg n by A5,A2,A3,FUNCT_2:2;
rng f misses rng g & f is one-to-one by A4,FINSEQ_3:91;
then
A7: h is one-to-one by A6,FINSEQ_3:91;
h is onto by A5,A3,FUNCT_2:def 3;
hence thesis by A7,MATRIX_1:def 16;
end;
theorem Th19:
Permutations 3 = {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,
3*>,<*3,1,2*>}
proof
now
let x be object;
A1: idseq 3 in Permutations 3 by MATRIX_1:def 16;
A2: <*3,1,2*> in Permutations 3
proof
reconsider h = <*1,2*> as FinSequence of NAT;
<*3*> ^ h = <*3,1,2*> by FINSEQ_1:43;
hence thesis by A1,Th18,FINSEQ_2:53;
end;
A3: <*2,3,1*> in Permutations 3
proof
reconsider h = <*2,3*> as FinSequence of NAT;
reconsider f = <*1,2,3*> as one-to-one FinSequence-like Function of Seg
3,Seg 3 by FINSEQ_2:53;
f = <*1*> ^ h by FINSEQ_1:43;
hence thesis by A1,Th18,FINSEQ_2:53;
end;
A4: <*1,3,2*> in Permutations 3
proof
reconsider h = <*2,3*> as FinSequence of NAT;
reconsider f = <*1,2,3*> as one-to-one FinSequence-like Function of Seg
3,Seg 3 by FINSEQ_2:53;
Rev h = <*3,2*> by FINSEQ_5:61;
then f = <*1*> ^ h & <*1*>^Rev h = <*1,3,2*> by FINSEQ_1:43;
hence thesis by A1,Th17,FINSEQ_2:53;
end;
A5: <*2,1,3*> in Permutations 3
proof
reconsider h = <*1,2*> as FinSequence of NAT;
<*3*> ^ h in Permutations 3 by A1,Th18,FINSEQ_2:53;
then Rev h = <*2,1*> & <*3*> ^ Rev h in Permutations 3 by Th17,
FINSEQ_5:61;
hence thesis by Th18;
end;
assume
x in {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>, <*2,1,3*>,<*3,1,2 *>};
then
x in {<*1,2,3*>,<*3,2,1*>}\/{<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2 *>
} by ENUMSET1:12;
then
x in {<*1,2,3*>,<*3,2,1*>} or x in {<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3
,1,2*>} by XBOOLE_0:def 3;
then x in {<*1,2,3*>,<*3,2,1*>} or x in {<*1,3,2*>,<*2,3,1*>} \/ {<*2,1,3
*>,<*3,1,2*>} by ENUMSET1:5;
then
A6: x in {<*1,2,3*>,<*3,2,1*>} or x in {<*1,3,2*>,<*2,3,1*>} or x in {<*2
,1,3*>,<*3,1,2*>} by XBOOLE_0:def 3;
Rev idseq 3 in Permutations 3 by Th4;
hence x in Permutations 3 by A6,A1,A4,A3,A5,A2,Th15,FINSEQ_2:53
,TARSKI:def 2;
end;
then
A7: {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} c=
Permutations 3 by TARSKI:def 3;
now
let p be object;
assume p in Permutations 3;
then reconsider q=p as Permutation of Seg 3 by MATRIX_1:def 16;
A8: rng q = Seg 3 by FUNCT_2:def 3;
A9: 3 in Seg 3;
then q.3 in Seg 3 by A8,FUNCT_2:4;
then
A10: q.3 = 1 or q.3 = 2 or q.3 = 3 by ENUMSET1:def 1,FINSEQ_3:1;
A11: 2 in Seg 3;
then q.2 in Seg 3 by A8,FUNCT_2:4;
then
A12: q.2 = 1 or q.2 = 2 or q.2 = 3 by ENUMSET1:def 1,FINSEQ_3:1;
A13: dom q = Seg 3 by FUNCT_2:52;
A14: q.1=1 & q.2=2 & q.3=3 or q.1=3 & q.2=2 & q.3=1 or q.1=1 & q.2=3 & q.3
=2 or q.1=2 & q.2=3 & q.3=1 or q.1=2 & q.2=1 & q.3=3 or q.1=3 & q.2=1 & q.3=2
implies q=<*1,2,3*> or q=<*3,2,1*> or q=<*1,3,2*> or q=<*2,3,1*> or q=<*2,1,3*>
or q=<*3,1,2*>
proof
reconsider q as FinSequence by A13,FINSEQ_1:def 2;
len q = 3 by A13,FINSEQ_1:def 3;
hence thesis by FINSEQ_1:45;
end;
A15: 1 in Seg 3;
then q.1 in Seg 3 by A8,FUNCT_2:4;
then q.1 = 1 or q.1 = 2 or q.1 = 3 by ENUMSET1:def 1,FINSEQ_3:1;
then
p = <*1,2,3*> or p = <*3,2,1*> or q = <*1,3,2*> or q = <*2,3,1*> or
q = <*2,1,3*> or q = <*3,1,2*> by A13,A15,A11,A9,A12,A10,A14,FUNCT_1:def 4;
then
p in {<*1,2,3*>,<*3,2,1*>} or q in {<*1,3,2*>,<*2,3,1*>} or
q in {<*2,1,3*>,<*3,1,2*>} by TARSKI:def 2;
then
p in {<*1,2,3*>,<*3,2,1*>} or q in {<*1,3,2*>,<*2,3,1*>}\/ {<*2,1,3*>
,<*3,1,2*>} by XBOOLE_0:def 3;
then
p in {<*1,2,3*>,<*3,2,1*>} or q in {<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3
,1,2*>} by ENUMSET1:5;
then p in {<*1,2,3*>,<*3,2,1*>} \/ {<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2
*>} by XBOOLE_0:def 3;
hence
p in {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>}
by ENUMSET1:12;
end;
then
Permutations 3 c= {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*
3,1,2*>} by TARSKI:def 3;
hence thesis by A7,XBOOLE_0:def 10;
end;
theorem Th20:
for a,b,c,d,e,f,g,h,i being Element of K for M being Matrix of 3
,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> for p being Element of Permutations
3 st p = <*1,2,3*> holds Path_matrix (p,M) = <* a,e,i *>
proof
let a,b,c,d,e,f,g,h,i be Element of K;
let M be Matrix of 3, K;
[1,1] in Indices M by MATRIX_0:31;
then consider r being FinSequence of the carrier of K such that
A1: r = M.1 and
A2: M*(1,1) = r.1 by MATRIX_0:def 5;
assume
A3: M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*>;
then M.1 = <*a,b,c*>;
then
A4: r.1 = a by A1;
[3,3] in Indices M by MATRIX_0:31;
then consider z being FinSequence of the carrier of K such that
A5: z = M.3 and
A6: M*(3,3) = z.3 by MATRIX_0:def 5;
M.3 = <*g,h,i*> by A3;
then
A7: z.3 = i by A5;
[2,2] in Indices M by MATRIX_0:31;
then consider y being FinSequence of the carrier of K such that
A8: y = M.2 and
A9: M*(2,2) = y.2 by MATRIX_0:def 5;
M.2 = <*d,e,f*> by A3;
then
A10: y.2 = e by A8;
let p be Element of Permutations 3;
assume
A11: p = <*1,2,3*>;
then
A12: 1 = p.1;
A13: 3 = p.3 by A11;
A14: 2 = p.2 by A11;
A15: len Path_matrix (p,M) = 3 by MATRIX_3:def 7;
then
A16: dom Path_matrix (p,M) = Seg 3 by FINSEQ_1:def 3;
then 2 in dom Path_matrix (p,M);
then
A17: Path_matrix (p,M).2 = e by A14,A9,A10,MATRIX_3:def 7;
3 in dom Path_matrix (p,M) by A16;
then
A18: Path_matrix (p,M).3 = i by A13,A6,A7,MATRIX_3:def 7;
1 in dom Path_matrix (p,M) by A16;
then Path_matrix (p,M).1 = a by A12,A2,A4,MATRIX_3:def 7;
hence thesis by A15,A17,A18,FINSEQ_1:45;
end;
theorem Th21:
for a,b,c,d,e,f,g,h,i being Element of K for M being Matrix of 3
,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> for p being Element of Permutations
3 st p = <*3,2,1*> holds Path_matrix (p,M) = <* c,e,g *>
proof
let a,b,c,d,e,f,g,h,i be Element of K;
let M be Matrix of 3, K;
[1,3] in Indices M by MATRIX_0:31;
then consider r being FinSequence of the carrier of K such that
A1: r = M.1 and
A2: M*(1,3) = r.3 by MATRIX_0:def 5;
assume
A3: M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*>;
then M.1 = <*a,b,c*>;
then
A4: r.3 = c by A1;
[3,1] in Indices M by MATRIX_0:31;
then consider z being FinSequence of the carrier of K such that
A5: z = M.3 and
A6: M*(3,1) = z.1 by MATRIX_0:def 5;
M.3 = <*g,h,i*> by A3;
then
A7: z.1 = g by A5;
[2,2] in Indices M by MATRIX_0:31;
then consider y being FinSequence of the carrier of K such that
A8: y = M.2 and
A9: M*(2,2) = y.2 by MATRIX_0:def 5;
M.2 = <*d,e,f*> by A3;
then
A10: y.2 = e by A8;
let p be Element of Permutations 3;
assume
A11: p = <*3,2,1*>;
then
A12: 3 = p.1;
A13: 1 = p.3 by A11;
A14: 2 = p.2 by A11;
A15: len Path_matrix (p,M) = 3 by MATRIX_3:def 7;
then
A16: dom Path_matrix (p,M)= Seg 3 by FINSEQ_1:def 3;
then 2 in dom Path_matrix (p,M);
then
A17: Path_matrix (p,M).2 = e by A14,A9,A10,MATRIX_3:def 7;
3 in dom Path_matrix (p,M) by A16;
then
A18: Path_matrix (p,M).3 = g by A13,A6,A7,MATRIX_3:def 7;
1 in dom Path_matrix (p,M) by A16;
then Path_matrix (p,M).1 = c by A12,A2,A4,MATRIX_3:def 7;
hence thesis by A15,A17,A18,FINSEQ_1:45;
end;
theorem Th22:
for a,b,c,d,e,f,g,h,i being Element of K for M being Matrix of 3
,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> for p being Element of Permutations
3 st p = <*1,3,2*> holds Path_matrix (p,M) = <* a,f,h *>
proof
let a,b,c,d,e,f,g,h,i be Element of K;
let M be Matrix of 3, K;
[1,1] in Indices M by MATRIX_0:31;
then consider r being FinSequence of the carrier of K such that
A1: r = M.1 and
A2: M*(1,1) = r.1 by MATRIX_0:def 5;
assume
A3: M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*>;
then M.1 = <*a,b,c*>;
then
A4: r.1 = a by A1;
[3,2] in Indices M by MATRIX_0:31;
then consider z being FinSequence of the carrier of K such that
A5: z = M.3 and
A6: M*(3,2) = z.2 by MATRIX_0:def 5;
M.3 = <*g,h,i*> by A3;
then
A7: z.2 = h by A5;
[2,3] in Indices M by MATRIX_0:31;
then consider y being FinSequence of the carrier of K such that
A8: y = M.2 and
A9: M*(2,3) = y.3 by MATRIX_0:def 5;
M.2 = <*d,e,f*> by A3;
then
A10: y.3 = f by A8;
let p be Element of Permutations 3;
assume
A11: p = <*1,3,2*>;
then
A12: 1 = p.1;
A13: 2 = p.3 by A11;
A14: 3 = p.2 by A11;
A15: len Path_matrix (p,M) = 3 by MATRIX_3:def 7;
then
A16: dom Path_matrix (p,M)= Seg 3 by FINSEQ_1:def 3;
then 2 in dom Path_matrix (p,M);
then
A17: Path_matrix (p,M).2 = f by A14,A9,A10,MATRIX_3:def 7;
3 in dom Path_matrix (p,M) by A16;
then
A18: Path_matrix (p,M).3 = h by A13,A6,A7,MATRIX_3:def 7;
1 in dom Path_matrix (p,M) by A16;
then Path_matrix (p,M).1 = a by A12,A2,A4,MATRIX_3:def 7;
hence thesis by A15,A17,A18,FINSEQ_1:45;
end;
theorem Th23:
for a,b,c,d,e,f,g,h,i being Element of K for M being Matrix of 3
,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> for p being Element of Permutations
3 st p = <*2,3,1*> holds Path_matrix (p,M) = <* b,f,g *>
proof
let a,b,c,d,e,f,g,h,i be Element of K;
let M be Matrix of 3, K;
[1,2] in Indices M by MATRIX_0:31;
then consider r being FinSequence of the carrier of K such that
A1: r = M.1 and
A2: M*(1,2) = r.2 by MATRIX_0:def 5;
assume
A3: M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*>;
then M.1 = <*a,b,c*>;
then
A4: r.2 = b by A1;
[3,1] in Indices M by MATRIX_0:31;
then consider z being FinSequence of the carrier of K such that
A5: z = M.3 and
A6: M*(3,1) = z.1 by MATRIX_0:def 5;
M.3 = <*g,h,i*> by A3;
then
A7: z.1 = g by A5;
[2,3] in Indices M by MATRIX_0:31;
then consider y being FinSequence of the carrier of K such that
A8: y = M.2 and
A9: M*(2,3) = y.3 by MATRIX_0:def 5;
M.2 = <*d,e,f*> by A3;
then
A10: y.3 = f by A8;
let p be Element of Permutations 3;
assume
A11: p = <*2,3,1*>;
then
A12: 2 = p.1;
A13: 1 = p.3 by A11;
A14: 3 = p.2 by A11;
A15: len Path_matrix (p,M) = 3 by MATRIX_3:def 7;
then
A16: dom Path_matrix (p,M)= Seg 3 by FINSEQ_1:def 3;
then 2 in dom Path_matrix (p,M);
then
A17: Path_matrix (p,M).2 = f by A14,A9,A10,MATRIX_3:def 7;
3 in dom Path_matrix (p,M) by A16;
then
A18: Path_matrix (p,M).3 = g by A13,A6,A7,MATRIX_3:def 7;
1 in dom Path_matrix (p,M) by A16;
then Path_matrix (p,M).1 = b by A12,A2,A4,MATRIX_3:def 7;
hence thesis by A15,A17,A18,FINSEQ_1:45;
end;
theorem Th24:
for a,b,c,d,e,f,g,h,i being Element of K for M being Matrix of 3
,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> for p being Element of Permutations
3 st p = <*2,1,3*> holds Path_matrix (p,M) = <* b,d,i *>
proof
let a,b,c,d,e,f,g,h,i be Element of K;
let M be Matrix of 3, K;
[1,2] in Indices M by MATRIX_0:31;
then consider r being FinSequence of the carrier of K such that
A1: r = M.1 and
A2: M*(1,2) = r.2 by MATRIX_0:def 5;
assume
A3: M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*>;
then M.1 = <*a,b,c*>;
then
A4: r.2 = b by A1;
[3,3] in Indices M by MATRIX_0:31;
then consider z being FinSequence of the carrier of K such that
A5: z = M.3 and
A6: M*(3,3) = z.3 by MATRIX_0:def 5;
M.3 = <*g,h,i*> by A3;
then
A7: z.3 = i by A5;
[2,1] in Indices M by MATRIX_0:31;
then consider y being FinSequence of the carrier of K such that
A8: y = M.2 and
A9: M*(2,1) = y.1 by MATRIX_0:def 5;
M.2 = <*d,e,f*> by A3;
then
A10: y.1 = d by A8;
let p be Element of Permutations 3;
assume
A11: p = <*2,1,3*>;
then
A12: 2 = p.1;
A13: 3 = p.3 by A11;
A14: 1 = p.2 by A11;
A15: len Path_matrix (p,M) = 3 by MATRIX_3:def 7;
then
A16: dom Path_matrix (p,M)= Seg 3 by FINSEQ_1:def 3;
then 2 in dom Path_matrix (p,M);
then
A17: Path_matrix (p,M).2 = d by A14,A9,A10,MATRIX_3:def 7;
3 in dom Path_matrix (p,M) by A16;
then
A18: Path_matrix (p,M).3 = i by A13,A6,A7,MATRIX_3:def 7;
1 in dom Path_matrix (p,M) by A16;
then Path_matrix (p,M).1 = b by A12,A2,A4,MATRIX_3:def 7;
hence thesis by A15,A17,A18,FINSEQ_1:45;
end;
theorem Th25:
for a,b,c,d,e,f,g,h,i being Element of K for M being Matrix of 3
,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> for p being Element of Permutations
3 st p = <*3,1,2*> holds Path_matrix (p,M) = <* c,d,h *>
proof
let a,b,c,d,e,f,g,h,i be Element of K;
let M be Matrix of 3, K;
[1,3] in Indices M by MATRIX_0:31;
then consider r being FinSequence of the carrier of K such that
A1: r = M.1 and
A2: M*(1,3) = r.3 by MATRIX_0:def 5;
assume
A3: M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*>;
then M.1 = <*a,b,c*>;
then
A4: r.3 = c by A1;
[3,2] in Indices M by MATRIX_0:31;
then consider z being FinSequence of the carrier of K such that
A5: z = M.3 and
A6: M*(3,2) = z.2 by MATRIX_0:def 5;
M.3 = <*g,h,i*> by A3;
then
A7: z.2 = h by A5;
[2,1] in Indices M by MATRIX_0:31;
then consider y being FinSequence of the carrier of K such that
A8: y = M.2 and
A9: M*(2,1) = y.1 by MATRIX_0:def 5;
M.2 = <*d,e,f*> by A3;
then
A10: y.1 = d by A8;
let p be Element of Permutations 3;
assume
A11: p = <*3,1,2*>;
then
A12: 3 = p.1;
A13: 2 = p.3 by A11;
A14: 1 = p.2 by A11;
A15: len Path_matrix (p,M) = 3 by MATRIX_3:def 7;
then
A16: dom Path_matrix (p,M) = Seg 3 by FINSEQ_1:def 3;
then 2 in dom Path_matrix (p,M);
then
A17: Path_matrix (p,M).2 = d by A14,A9,A10,MATRIX_3:def 7;
3 in dom Path_matrix (p,M) by A16;
then
A18: Path_matrix (p,M).3 = h by A13,A6,A7,MATRIX_3:def 7;
1 in dom Path_matrix (p,M) by A16;
then Path_matrix (p,M).1 = c by A12,A2,A4,MATRIX_3:def 7;
hence thesis by A15,A17,A18,FINSEQ_1:45;
end;
theorem Th26:
(the multF of K) $$ <* a,b,c *> = a * b * c
proof
(the multF of K) $$ <* a,b,c *> = Product <* a,b,c *> by GROUP_4:def 2
.= a * b * c by FVSUM_1:79;
hence thesis;
end;
theorem Th27:
<*1,3,2*> in Permutations 3 & <*2,3,1*> in Permutations 3 & <*2,
1,3*> in Permutations 3 & <*3,1,2*> in Permutations 3 & <*1,2,3*> in
Permutations 3 & <*3,2,1*> in Permutations 3
proof
set h = <*1,2*>;
reconsider f = <*1,2,3*> as one-to-one FinSequence-like Function of Seg 3,
Seg 3 by FINSEQ_2:53;
A1: <*3*> ^ h = <*3,1,2*> by FINSEQ_1:43;
A2: <*1,3,2*> in Permutations 3
proof
set h = <*2,3*>;
Rev h = <*3,2*> by FINSEQ_5:61;
then
A3: <*1*>^Rev h = <*1,3,2*> by FINSEQ_1:43;
f = <*1*> ^ h & f in Permutations 3 by FINSEQ_1:43,FINSEQ_2:53
,MATRIX_1:def 16;
hence thesis by A3,Th17;
end;
A4: idseq 3 in Permutations 3 by MATRIX_1:def 16;
then <*3*> ^ h in Permutations 3 by Th18,FINSEQ_2:53;
then
A5: <*3*> ^ Rev h in Permutations 3 by Th17;
f = <*1*> ^ <*2,3*> & Rev h = <*2,1*> by FINSEQ_1:43,FINSEQ_5:61;
hence thesis by A4,A2,A5,A1,Th5,Th15,Th18,FINSEQ_2:53;
end;
Lm3: <*1,2,3*> <> <*3,2,1*> by FINSEQ_1:78;
Lm4: <*1,2,3*> <> <*1,3,2*> by FINSEQ_1:78;
Lm5: <*1,2,3*> <> <*2,1,3*> by FINSEQ_1:78;
Lm6: <*1,2,3*> <> <*2,3,1*> & <*1,2,3*> <> <*3,1,2*> by FINSEQ_1:78;
Lm7: <*3,2,1*> <> <*2,3,1*> & <*3,2,1*> <> <*3,1,2*> by FINSEQ_1:78;
Lm8: <*3,2,1*> <> <*2,1,3*> & <*1,3,2*> <> <*2,1,3*> by FINSEQ_1:78;
Lm9: <*1,3,2*> <> <*2,3,1*> & <*1,3,2*> <> <*3,1,2*> by FINSEQ_1:78;
Lm10: <*3,2,1*> <> <*1,3,2*> & <*2,3,1*> <> <*3,1,2*> by FINSEQ_1:78;
Lm11: <*2,3,1*> <> <*2,1,3*> & <*2,1,3*> <> <*3,1,2*> by FINSEQ_1:78;
theorem Th28:
<*2,3,1*>" = <*3,1,2*>
proof
set f = <*2,3,1*>, g = <*3,1,2*>;
rng f = {2,3,1} by FINSEQ_2:128
.= {1,2,3} by ENUMSET1:59;
then
A1: dom f = {1,2,3} & rng f = dom g by FINSEQ_1:89,FINSEQ_3:1;
then
A2: dom (g * f) = {1,2,3} by RELAT_1:27;
A3: for x being object st x in dom (g * f) holds (g * f).x = (id {1,2,3}).x
proof
let x be object;
assume
A4: x in dom (g * f);
per cases by A2,A4,ENUMSET1:def 1;
suppose
A5: x = 1;
then g.(f.x) = g.2
.= 1
.= (id {1,2,3}).x by A2,A4,A5,FUNCT_1:18;
hence thesis by A4,FUNCT_1:12;
end;
suppose
A6: x = 2;
then g.(f.x) = g.3
.= 2
.= (id {1,2,3}).x by A2,A4,A6,FUNCT_1:18;
hence thesis by A4,FUNCT_1:12;
end;
suppose
A7: x = 3;
then g.(f.x) = g.1
.= 3
.= (id {1,2,3}).x by A2,A4,A7,FUNCT_1:18;
hence thesis by A4,FUNCT_1:12;
end;
end;
f is one-to-one & dom (g * f) = dom id {1,2,3} by A2,FINSEQ_3:95,RELAT_1:45;
hence thesis by A1,A3,FUNCT_1:2,41;
end;
theorem
for a being Element of Group_of_Perm 3 st a = <*2,3,1*> holds a" = <*3 ,1,2*>
proof
let a be Element of Group_of_Perm 3;
reconsider a1 = a as Element of Permutations 3 by MATRIX_1:def 17;
assume a = <*2,3,1*>;
then a1" = <*3,1,2*> by Th28;
hence thesis by MATRIX_7:27;
end;
begin :: Transpositions
theorem Th30:
for p being Permutation of Seg 3 st p = <* 1,3,2 *> holds p is
being_transposition
proof
let p be Permutation of Seg 3;
assume
A1: p = <*1,3,2*>;
then
A2: dom p = {1,2,3} by FINSEQ_1:89,FINSEQ_3:1;
ex i,j st i in dom p & j in dom p & i <> j & p.i = j & p.j = i & for k
st k <> i & k <> j & k in dom p holds p.k = k
proof
take i = 2, j = 3;
thus i in dom p & j in dom p by A2,ENUMSET1:def 1;
for k st k <> i & k <> j & k in dom p holds p.k = k
proof
let k;
assume k <> i & k <> j & k in dom p;
then k = 1 by A2,ENUMSET1:def 1;
hence thesis by A1;
end;
hence thesis by A1;
end;
hence thesis by MATRIX_1:def 18;
end;
theorem Th31:
for p being Permutation of Seg 3 st p = <* 2,1,3 *> holds p is
being_transposition
proof
let p be Permutation of Seg 3;
assume
A1: p = <*2,1,3*>;
then
A2: dom p = {1,2,3} by FINSEQ_1:89,FINSEQ_3:1;
ex i,j st i in dom p & j in dom p & i <> j & p.i = j & p.j = i & for k
st k <> i & k <> j & k in dom p holds p.k = k
proof
take i = 1, j = 2;
thus i in dom p & j in dom p by A2,ENUMSET1:def 1;
for k st k <> i & k <> j & k in dom p holds p.k = k
proof
let k;
assume k <> i & k <> j & k in dom p;
then k = 3 by A2,ENUMSET1:def 1;
hence thesis by A1;
end;
hence thesis by A1;
end;
hence thesis by MATRIX_1:def 18;
end;
theorem
for p being Permutation of Seg 3 st p = <* 3,2,1 *> holds p is
being_transposition
proof
let p be Permutation of Seg 3;
assume
A1: p = <*3,2,1*>;
then
A2: dom p = {1,2,3} by FINSEQ_1:89,FINSEQ_3:1;
ex i,j st i in dom p & j in dom p & i <> j & p.i = j & p.j = i & for k
st k <> i & k <> j & k in dom p holds p.k = k
proof
take i = 1, j = 3;
thus i in dom p & j in dom p by A2,ENUMSET1:def 1;
for k st k <> i & k <> j & k in dom p holds p.k = k
proof
let k;
assume k <> i & k <> j & k in dom p;
then k = 2 by A2,ENUMSET1:def 1;
hence thesis by A1;
end;
hence thesis by A1;
end;
hence thesis by MATRIX_1:def 18;
end;
theorem Th33:
for p being Permutation of Seg n st p = id Seg n holds not p is
being_transposition
proof
let p be Permutation of Seg n;
assume
A1: p = id Seg n;
then dom p = Seg n by FUNCT_1:17;
then
not ex i,j st i in dom p & j in dom p & i <> j & p.i = j & p.j = i & for
k st k <> i & k <> j & k in dom p holds p.k = k by A1,FUNCT_1:17;
hence thesis by MATRIX_1:def 18;
end;
theorem Th34:
for p being Permutation of Seg 3 st p = <* 3,1,2 *> holds not p
is being_transposition
proof
let p be Permutation of Seg 3;
assume
A1: p = <*3,1,2*>;
then
A2: dom p = {1,2,3} by FINSEQ_1:89,FINSEQ_3:1;
not ex i,j st i in dom p & j in dom p & i <> j & p.i = j & p.j = i & for
k st k <> i & k <> j & k in dom p holds p.k = k
proof
given i,j such that
A3: i in dom p and
A4: j in dom p & i <> j and
p.i = j and
p.j = i and
A5: for k st k <> i & k <> j & k in dom p holds p.k = k;
ex k being Element of NAT st k <> i & k <> j & k in dom p
proof
A6: i = 1 or i = 2 or i = 3 by A2,A3,ENUMSET1:def 1;
per cases by A2,A4,A6,ENUMSET1:def 1;
suppose
A7: i = 1 & j = 2;
take 3;
thus thesis by A2,A7,ENUMSET1:def 1;
end;
suppose
A8: i = 2 & j = 3;
take 1;
thus thesis by A2,A8,ENUMSET1:def 1;
end;
suppose
A9: i = 1 & j = 3;
take 2;
thus thesis by A2,A9,ENUMSET1:def 1;
end;
suppose
A10: i = 2 & j = 1;
take 3;
thus thesis by A2,A10,ENUMSET1:def 1;
end;
suppose
A11: i = 3 & j = 1;
take 2;
thus thesis by A2,A11,ENUMSET1:def 1;
end;
suppose
A12: i = 3 & j = 2;
take 1;
thus thesis by A2,A12,ENUMSET1:def 1;
end;
end;
then consider k such that
A13: k <> i & k <> j and
A14: k in dom p;
A15: p.k = k by A5,A13,A14;
per cases by A2,A14,ENUMSET1:def 1;
suppose
k = 1;
hence thesis by A1,A15;
end;
suppose
k = 2;
hence thesis by A1,A15;
end;
suppose
k = 3;
hence thesis by A1,A15;
end;
end;
hence thesis by MATRIX_1:def 18;
end;
theorem Th35:
for p being Permutation of Seg 3 st p = <* 2,3,1 *> holds not p
is being_transposition
proof
let p be Permutation of Seg 3;
assume
A1: p = <*2,3,1*>;
then
A2: dom p = {1,2,3} by FINSEQ_1:89,FINSEQ_3:1;
not ex i,j st i in dom p & j in dom p & i <> j & p.i = j & p.j = i & for
k st k <> i & k <> j & k in dom p holds p.k = k
proof
given i,j such that
A3: i in dom p and
A4: j in dom p & i <> j and
p.i = j and
p.j = i and
A5: for k st k <> i & k <> j & k in dom p holds p.k = k;
ex k being Element of NAT st k <> i & k <> j & k in dom p
proof
A6: i = 1 or i = 2 or i = 3 by A2,A3,ENUMSET1:def 1;
per cases by A2,A4,A6,ENUMSET1:def 1;
suppose
A7: i = 1 & j = 2;
take 3;
thus thesis by A2,A7,ENUMSET1:def 1;
end;
suppose
A8: i = 2 & j = 3;
take 1;
thus thesis by A2,A8,ENUMSET1:def 1;
end;
suppose
A9: i = 1 & j = 3;
take 2;
thus thesis by A2,A9,ENUMSET1:def 1;
end;
suppose
A10: i = 2 & j = 1;
take 3;
thus thesis by A2,A10,ENUMSET1:def 1;
end;
suppose
A11: i = 3 & j = 1;
take 2;
thus thesis by A2,A11,ENUMSET1:def 1;
end;
suppose
A12: i = 3 & j = 2;
take 1;
thus thesis by A2,A12,ENUMSET1:def 1;
end;
end;
then consider k such that
A13: k <> i & k <> j and
A14: k in dom p;
A15: p.k = k by A5,A13,A14;
per cases by A2,A14,ENUMSET1:def 1;
suppose
k = 1;
hence thesis by A1,A15;
end;
suppose
k = 2;
hence thesis by A1,A15;
end;
suppose
k = 3;
hence thesis by A1,A15;
end;
end;
hence thesis by MATRIX_1:def 18;
end;
begin :: Corrollaries
theorem Th36:
for f being Permutation of Seg n holds f is FinSequence of Seg n
proof
let f be Permutation of Seg n;
A1: rng f c= Seg n by RELAT_1:def 19;
per cases;
suppose
n = 0;
hence thesis by A1,FINSEQ_1:def 4;
end;
suppose
n <> 0;
then dom f = Seg n by FUNCT_2:def 1;
then f is FinSequence by FINSEQ_1:def 2;
hence thesis by A1,FINSEQ_1:def 4;
end;
end;
theorem Th37:
<*2,1,3*> * <*1,3,2*> = <*2,3,1*> & <*1,3,2*> * <*2,1,3*> = <*3,
1,2*> & <*2,1,3*> * <*3,2,1*> = <*3,1,2*> & <*3,2,1*> * <*2,1,3*> = <*2,3,1*> &
<*3,2,1*> * <*3,2,1*> = <*1,2,3*> & <*2,1,3*> * <*2,1,3*> = <*1,2,3*> & <*1,3,2
*> * <*1,3,2*> = <*1,2,3*> & <*1,3,2*> * <*2,3,1*> = <*3,2,1*> & <*2,3,1*> * <*
2,3,1*> = <*3,1,2*> & <*2,3,1*> * <*3,1,2*> = <*1,2,3*> & <*3,1,2*> * <*2,3,1*>
= <*1,2,3*> & <*3,1,2*> * <*3,1,2*> = <*2,3,1*> & <*1,3,2*> * <*3,2,1*> = <*2,3
,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*>
proof
set F = <*2,3,1*>, G = <*3,1,2*>;
set f = <*1,3,2*>, g = <*2,1,3*>, h = <*3,2,1*>;
A1: dom f = {1,2,3} by FINSEQ_1:89,FINSEQ_3:1;
then
A2: 1 in dom f by ENUMSET1:def 1;
A3: f is Permutation of Seg 3 by Th27,MATRIX_1:def 16;
A4: g is Permutation of Seg 3 by Th27,MATRIX_1:def 16;
A5: 2 in dom f by A1,ENUMSET1:def 1;
A6: dom G = {1,2,3} by FINSEQ_1:89,FINSEQ_3:1;
then
A7: 1 in dom G by ENUMSET1:def 1;
A8: 3 in dom G by A6,ENUMSET1:def 1;
A9: 2 in dom G by A6,ENUMSET1:def 1;
A10: 3 in dom f by A1,ENUMSET1:def 1;
A11: dom g = {1,2,3} by FINSEQ_1:89,FINSEQ_3:1;
then
A12: 1 in dom g by ENUMSET1:def 1;
A13: 3 in dom g by A11,ENUMSET1:def 1;
A14: 2 in dom g by A11,ENUMSET1:def 1;
A15: dom h = {1,2,3} by FINSEQ_1:89,FINSEQ_3:1;
then
A16: 1 in dom h by ENUMSET1:def 1;
A17: 3 in dom h by A15,ENUMSET1:def 1;
A18: 2 in dom h by A15,ENUMSET1:def 1;
A19: f is Permutation of Seg 3 by Th27,MATRIX_1:def 16;
A20: G is Permutation of Seg 3 by Th27,MATRIX_1:def 16;
A21: dom F = {1,2,3} by FINSEQ_1:89,FINSEQ_3:1;
then
A22: 1 in dom F by ENUMSET1:def 1;
A23: 3 in dom F by A21,ENUMSET1:def 1;
A24: 2 in dom F by A21,ENUMSET1:def 1;
A25: h is Permutation of Seg 3 by Th27,MATRIX_1:def 16;
A26: F is Permutation of Seg 3 by Th27,MATRIX_1:def 16;
then reconsider f,g,h,F,G as FinSequence of Seg 3 by A4,A25,A20,A19,Th36;
A27: 3 = len g by FINSEQ_1:45;
then reconsider gf = g * f as FinSequence of Seg 3 by A3,FINSEQ_2:46;
A28: gf.1 = g.(f.1) by A2,FUNCT_1:13
.= g.1
.= 2;
A29: g is Permutation of Seg 3 by Th27,MATRIX_1:def 16;
then reconsider gg = g * g as FinSequence of Seg 3 by A27,FINSEQ_2:46;
A30: gg.1 = g.(g.1) by A12,FUNCT_1:13
.= g.2
.= 1;
A31: 3 = len f by FINSEQ_1:45;
then reconsider fg = f * g as FinSequence of Seg 3 by A4,FINSEQ_2:46;
A32: fg.2 = f.(g.2) by A14,FUNCT_1:13
.= f.1
.= 1;
A33: gf.3 = g.(f.3) by A10,FUNCT_1:13
.= g.2
.= 1;
A34: gf.2 = g.(f.2) by A5,FUNCT_1:13
.= g.3
.= 3;
A35: f is Permutation of Seg 3 by Th27,MATRIX_1:def 16;
then reconsider ff = f * f as FinSequence of Seg 3 by A31,FINSEQ_2:46;
len gf = 3 by A27,A35,FINSEQ_2:43;
hence <*2,1,3*> * <*1,3,2*> = <*2,3,1*> by A28,A34,A33,FINSEQ_1:45;
A36: fg.1 = f.(g.1) by A12,FUNCT_1:13
.= f.2
.= 3;
A37: fg.3 = f.(g.3) by A13,FUNCT_1:13
.= f.3
.= 2;
len fg = 3 by A31,A29,FINSEQ_2:43;
hence <*1,3,2*> * <*2,1,3*> = <*3,1,2*> by A36,A32,A37,FINSEQ_1:45;
A38: ff.2 = f.(f.2) by A5,FUNCT_1:13
.= f.3
.= 2;
A39: gg.3 = g.(g.3) by A13,FUNCT_1:13
.= g.3
.= 3;
A40: gg.2 = g.(g.2) by A14,FUNCT_1:13
.= g.1
.= 2;
A41: h is Permutation of Seg 3 by Th27,MATRIX_1:def 16;
then reconsider gh = g * h as FinSequence of Seg 3 by A27,FINSEQ_2:46;
A42: gh.1 = g.(h.1) by A16,FUNCT_1:13
.= g.3
.= 3;
A43: gh.3 = g.(h.3) by A17,FUNCT_1:13
.= g.1
.= 2;
A44: gh.2 = g.(h.2) by A18,FUNCT_1:13
.= g.2
.= 1;
A45: 3 = len h by FINSEQ_1:45;
then reconsider hf = h * f as FinSequence of Seg 3 by A19,FINSEQ_2:46;
reconsider hh = h * h as FinSequence of Seg 3 by A45,A41,FINSEQ_2:46;
A46: hh.1 = h.(h.1) by A16,FUNCT_1:13
.= h.3
.= 1;
reconsider fh = f * h as FinSequence of Seg 3 by A25,A31,FINSEQ_2:46;
A47: fh.1 = f.(h.1) by A16,FUNCT_1:13
.= f.3
.= 2;
A48: fh.3 = f.(h.3) by A17,FUNCT_1:13
.= f.1
.= 1;
reconsider fF = f * F as FinSequence of Seg 3 by A26,A31,FINSEQ_2:46;
A49: fF.1 = f.(F.1) by A22,FUNCT_1:13
.= f.2
.= 3;
A50: fF.2 = f.(F.2) by A24,FUNCT_1:13
.= f.3
.= 2;
reconsider hg = h * g as FinSequence of Seg 3 by A45,A29,FINSEQ_2:46;
A51: hg.1 = h.(g.1) by A12,FUNCT_1:13
.= h.2
.= 2;
A52: hg.2 = h.(g.2) by A14,FUNCT_1:13
.= h.1
.= 3;
A53: hh.3 = h.(h.3) by A17,FUNCT_1:13
.= h.1
.= 3;
A54: hh.2 = h.(h.2) by A18,FUNCT_1:13
.= h.2
.= 2;
len gh = 3 by A27,A41,FINSEQ_2:43;
hence <*2,1,3*> * <*3,2,1*> = <*3,1,2*> by A42,A44,A43,FINSEQ_1:45;
A55: ff.3 = f.(f.3) by A10,FUNCT_1:13
.= f.2
.= 3;
A56: hg.3 = h.(g.3) by A13,FUNCT_1:13
.= h.3
.= 1;
len hg = 3 by A45,A29,FINSEQ_2:43;
hence <*3,2,1*> * <*2,1,3*> = <*2,3,1*> by A51,A52,A56,FINSEQ_1:45;
len hh = 3 by A45,A41,FINSEQ_2:43;
hence <*3,2,1*> * <*3,2,1*> = <*1,2,3*> by A46,A54,A53,FINSEQ_1:45;
len gg = 3 by A27,A29,FINSEQ_2:43;
hence <*2,1,3*> * <*2,1,3*> = <*1,2,3*> by A30,A40,A39,FINSEQ_1:45;
A57: ff.1 = f.(f.1) by A2,FUNCT_1:13
.= f.1
.= 1;
A58: fF.3 = f.(F.3) by A23,FUNCT_1:13
.= f.1
.= 1;
len ff = 3 by A31,A35,FINSEQ_2:43;
hence <*1,3,2*> * <*1,3,2*> = <*1,2,3*> by A57,A38,A55,FINSEQ_1:45;
A59: F is Permutation of Seg 3 by Th27,MATRIX_1:def 16;
then len fF = 3 by A31,FINSEQ_2:43;
hence <*1,3,2*> * <*2,3,1*> = <*3,2,1*> by A49,A50,A58,FINSEQ_1:45;
A60: fh.2 = f.(h.2) by A18,FUNCT_1:13
.= f.2
.= 3;
A61: 3 = len F by FINSEQ_1:45;
then reconsider FF = F * F as FinSequence of Seg 3 by A26,FINSEQ_2:46;
reconsider FG = F * G as FinSequence of Seg 3 by A20,A61,FINSEQ_2:46;
A62: FG.1 = F.(G.1) by A7,FUNCT_1:13
.= F.3
.= 1;
A63: FG.2 = F.(G.2) by A9,FUNCT_1:13
.= F.1
.= 2;
A64: FF.3 = F.(F.3) by A23,FUNCT_1:13
.= F.1
.= 2;
A65: FG.3 = F.(G.3) by A8,FUNCT_1:13
.= F.2
.= 3;
A66: FF.2 = F.(F.2) by A24,FUNCT_1:13
.= F.3
.= 1;
A67: FF.1 = F.(F.1) by A22,FUNCT_1:13
.= F.2
.= 3;
A68: 3 = len G by FINSEQ_1:45;
then reconsider GF = G * F as FinSequence of Seg 3 by A26,FINSEQ_2:46;
reconsider GG = G * G as FinSequence of Seg 3 by A20,A68,FINSEQ_2:46;
A69: GG.1 = G.(G.1) by A7,FUNCT_1:13
.= G.3
.= 2;
A70: GG.2 = G.(G.2) by A9,FUNCT_1:13
.= G.1
.= 3;
A71: GF.3 = G.(F.3) by A23,FUNCT_1:13
.= G.1
.= 3;
A72: GG.3 = G.(G.3) by A8,FUNCT_1:13
.= G.2
.= 1;
A73: GF.2 = G.(F.2) by A24,FUNCT_1:13
.= G.3
.= 2;
A74: GF.1 = G.(F.1) by A22,FUNCT_1:13
.= G.2
.= 1;
len FF = 3 by A61,A59,FINSEQ_2:43;
hence <*2,3,1*> * <*2,3,1*> = <*3,1,2*> by A67,A66,A64,FINSEQ_1:45;
A75: G is Permutation of Seg 3 by Th27,MATRIX_1:def 16;
then len FG = 3 by A61,FINSEQ_2:43;
hence <*2,3,1*> * <*3,1,2*> = <*1,2,3*> by A62,A63,A65,FINSEQ_1:45;
A76: hf.3 = h.(f.3) by A10,FUNCT_1:13
.= h.2
.= 2;
len GF = 3 by A68,A59,FINSEQ_2:43;
hence <*3,1,2*> * <*2,3,1*> = <*1,2,3*> by A74,A73,A71,FINSEQ_1:45;
len GG = 3 by A68,A75,FINSEQ_2:43;
hence <*3,1,2*> * <*3,1,2*> = <*2,3,1*> by A69,A70,A72,FINSEQ_1:45;
A77: hf.2 = h.(f.2) by A5,FUNCT_1:13
.= h.3
.= 1;
len fh = 3 by A31,A41,FINSEQ_2:43;
hence <*1,3,2*> * <*3,2,1*> = <*2,3,1*> by A47,A60,A48,FINSEQ_1:45;
A78: hf.1 = h.(f.1) by A2,FUNCT_1:13
.= h.1
.= 3;
len hf = 3 by A45,A35,FINSEQ_2:43;
hence <*3,2,1*> * <*1,3,2*> = <*3,1,2*> by A78,A77,A76,FINSEQ_1:45;
end;
theorem Th38:
for p being Permutation of Seg 3 st p is being_transposition
holds p = <*2,1,3*> or p = <*1,3,2*> or p = <*3,2,1*>
proof
let p be Permutation of Seg 3;
p in Permutations 3 by MATRIX_1:def 16;
then
A1: p=<*1,2,3*> or p=<*2,1,3*> or p=<*2,3,1*> or p=<*3,1,2*> or p=<*3,2,1*>
or p=<*1,3,2*> by Th19,ENUMSET1:def 4;
assume p is being_transposition;
hence thesis by A1,Th33,Th34,Th35,FINSEQ_2:53;
end;
theorem Th39:
for f, g being Element of Permutations n holds f * g in Permutations n
proof
let f, g be Element of Permutations n;
reconsider F = f, G = g as Permutation of Seg n by MATRIX_1:def 16;
F * G is Permutation of Seg n;
hence thesis by MATRIX_1:def 16;
end;
Lm12: <*1,2,3*> is even Permutation of Seg 3 by FINSEQ_2:53,MATRIX_1:16;
Lm13: <*2,3,1*> is even Permutation of Seg 3
proof
reconsider f = <*2,3,1*> as Permutation of Seg 3 by Th27,MATRIX_1:def 16;
ex l be FinSequence of Group_of_Perm 3 st (len l) mod 2 = 0 & f =
Product l & for i st i in dom l ex q being Element of Permutations 3 st l.i = q
& q is being_transposition
proof
reconsider l1 = <*2,1,3*>, l2 = <*1,3,2*> as Element of Group_of_Perm 3 by
Th27,MATRIX_1:def 17;
reconsider l = <* l2, l1 *> as FinSequence of Group_of_Perm 3;
take l;
A1: len l = 2 * 1 by FINSEQ_1:44;
hence (len l) mod 2 = 0 by NAT_D:13;
reconsider L2 = l2, L1 = l1 as Element of Permutations 3 by Th27;
Product l = l2 * l1 by GROUP_4:10
.= L1 * L2 by MATRIX_1:def 17
.= <*2,3,1*> by Th37;
hence f = Product l;
A2: dom l = {1,2} by A1,FINSEQ_1:2,def 3;
for i st i in dom l ex q being Element of Permutations 3 st l.i = q &
q is being_transposition
proof
let i;
assume
A3: i in dom l;
per cases by A2,A3,TARSKI:def 2;
suppose
A4: i = 2;
then reconsider q = l.i as Element of Permutations 3 by Th27;
A5: len Permutations 3 = 3 by MATRIX_1:9;
l.i = <*2,1,3*> by A4;
then q is being_transposition by A5,Th31;
hence thesis;
end;
suppose
A6: i = 1;
then reconsider q = l.i as Element of Permutations 3 by Th27;
A7: len Permutations 3 = 3 by MATRIX_1:9;
l.i = <*1,3,2*> by A6;
then q is being_transposition by A7,Th30;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis by MATRIX_1:def 19;
end;
Lm14: <*3,1,2*> is even Permutation of Seg 3
proof
reconsider f = <*3,1,2*> as Permutation of Seg 3 by Th27,MATRIX_1:def 16;
ex l be FinSequence of Group_of_Perm 3 st (len l) mod 2 = 0 & f =
Product l & for i st i in dom l ex q being Element of Permutations 3 st l.i = q
& q is being_transposition
proof
reconsider l1 = <*2,1,3*>, l2 = <*1,3,2*> as Element of Group_of_Perm 3 by
Th27,MATRIX_1:def 17;
reconsider l = <* l1, l2 *> as FinSequence of Group_of_Perm 3;
take l;
A1: len l = 2 * 1 by FINSEQ_1:44;
hence (len l) mod 2 = 0 by NAT_D:13;
reconsider L2 = l2, L1 = l1 as Element of Permutations 3 by Th27;
Product l = l1 * l2 by GROUP_4:10
.= L2 * L1 by MATRIX_1:def 17
.= <*3,1,2*> by Th37;
hence f = Product l;
A2: dom l = {1,2} by A1,FINSEQ_1:2,def 3;
for i st i in dom l ex q being Element of Permutations 3 st l.i = q &
q is being_transposition
proof
let i;
assume
A3: i in dom l;
per cases by A2,A3,TARSKI:def 2;
suppose
A4: i = 2;
then reconsider q = l.i as Element of Permutations 3 by Th27;
A5: len Permutations 3 = 3 by MATRIX_1:9;
l.i = <*1,3,2*> by A4;
then q is being_transposition by A5,Th30;
hence thesis;
end;
suppose
A6: i = 1;
then reconsider q = l.i as Element of Permutations 3 by Th27;
A7: len Permutations 3 = 3 by MATRIX_1:9;
l.i = <*2,1,3*> by A6;
then q is being_transposition by A7,Th31;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis by MATRIX_1:def 19;
end;
theorem
for l being FinSequence of Group_of_Perm n st (len l) mod 2 = 0 & (for
i being Element of NAT st i in dom l ex q being Element of Permutations n st l.
i = q & q is being_transposition) holds Product l is even Permutation of Seg n
proof
let l be FinSequence of Group_of_Perm n;
Product l in the carrier of Group_of_Perm n;
then Product l in Permutations n by MATRIX_1:def 17;
then reconsider Pf = Product l as Permutation of Seg n by MATRIX_1:def 16;
assume
A1: (len l) mod 2 = 0 & for i being Element of NAT st i in dom l ex q
being Element of Permutations n st l.i = q & q is being_transposition;
ex l be FinSequence of the carrier of Group_of_Perm n st (len l) mod 2 =
0 & Pf = Product l & for i st i in dom l ex q being Element of Permutations n
st l.i=q & q is being_transposition
proof
consider l be FinSequence of the carrier of Group_of_Perm n such that
A2: (len l) mod 2 = 0 & Pf = Product l and
A3: for i be Element of NAT st i in dom l ex q being Element of
Permutations n st l.i=q & q is being_transposition by A1;
take l;
thus (len l) mod 2 = 0 & Pf = Product l by A2;
let i;
thus thesis by A3;
end;
hence thesis by MATRIX_1:def 19;
end;
Lm15: for p being Permutation of Seg 3 holds p * <*1,2,3*> = p
proof
let p be Permutation of Seg 3;
p is Element of Permutations 3 by MATRIX_1:def 16;
hence thesis by FINSEQ_2:53,MATRIX_1:12;
end;
Lm16: for p being Permutation of Seg 3 holds <*1,2,3*> * p = p
proof
let p be Permutation of Seg 3;
p is Element of Permutations 3 by MATRIX_1:def 16;
hence thesis by FINSEQ_2:53,MATRIX_1:12;
end;
theorem Th41:
for l being FinSequence of Group_of_Perm 3 st (len l) mod 2 = 0
& (for i being Element of NAT st i in dom l ex q being Element of Permutations
3 st l.i = q & q is being_transposition) holds Product l = <*1,2,3*> or Product
l = <*2,3,1*> or Product l = <*3,1,2*>
proof
defpred P[Nat] means for f being FinSequence of Group_of_Perm 3 st len f = 2
* $1 & (for i be Element of NAT st i in dom f holds ex q being Element of
Permutations 3 st f.i=q & q is being_transposition) holds Product f = <*1,2,3*>
or Product f = <*2,3,1*> or Product f = <*3,1,2*>;
let l be FinSequence of Group_of_Perm 3;
assume that
A1: (len l) mod 2 = 0 and
A2: for i being Element of NAT st i in dom l ex q being Element of
Permutations 3 st l.i = q & q is being_transposition;
A3: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A4: P[k];
let f be FinSequence of Group_of_Perm 3;
assume that
A5: len f = 2 * (k+1) and
A6: for i be Element of NAT st i in dom f holds ex q being Element of
Permutations 3 st f.i = q & q is being_transposition;
reconsider k as Element of NAT by ORDINAL1:def 12;
set l = 2*k;
A7: 1 <= l+1 by NAT_1:11;
rng (f|Seg (2*k)) c= the carrier of Group_of_Perm 3 by RELAT_1:def 19;
then reconsider g = f|Seg (2*k) as FinSequence of Group_of_Perm 3 by
FINSEQ_1:def 4;
A8: l <= l+1 by NAT_1:11;
A9: (f | Seg (l+1)) | Seg l = (f | (l+1)) | l .= f | l by A8,FINSEQ_5:77
.= f | Seg l;
A10: dom g c= dom f by RELAT_1:60;
A11: for i be Element of NAT st i in dom g holds ex q being Element of
Permutations 3 st g.i = q & q is being_transposition
proof
let i be Element of NAT;
assume
A12: i in dom g;
then consider q being Element of Permutations 3 such that
A13: f.i = q & q is being_transposition by A6,A10;
take q;
thus thesis by A12,A13,FUNCT_1:47;
end;
set h = f | Seg (l+1);
len f = l + 1 + 1 by A5;
then len h = l + 1 by FINSEQ_3:53;
then
A14: h = h | Seg l ^ <*h.(l+1)*> by FINSEQ_3:55;
A15: dom f = Seg (2*(k+1)) by A5,FINSEQ_1:def 3;
l+1 <= l+2 by XREAL_1:6;
then 1 <= l+2 by A7,XXREAL_0:2;
then
A16: l+2 in dom f by A15;
then consider q1 being Element of Permutations 3 such that
A17: f.(l+2) = q1 and
A18: q1 is being_transposition by A6;
A19: f.(l+1+1) = f/.(l+2) by A16,PARTFUN1:def 6;
l+1 <= l+2 by XREAL_1:6;
then
A20: l+1 in dom f by A15,A7;
then consider q2 being Element of Permutations 3 such that
A21: f.(l+1) = q2 and
A22: q2 is being_transposition by A6;
reconsider q12 = q1 * q2 as Element of Permutations 3 by Th39;
h.(l+1) = f.(l+1) by FINSEQ_1:4,FUNCT_1:49;
then
A23: h.(l+1) = f/.(l+1) by A20,PARTFUN1:def 6;
f = f | Seg (l+1) ^ <*f.(l+1+1)*> by A5,FINSEQ_3:55;
then f = g ^ (<*f/.(l+1)*> ^ <*f/.(l+2)*>) by A14,A9,A23,A19,FINSEQ_1:32;
then
A24: Product f = Product g * Product (<*f/.(l+1)*> ^ <*f/.(l+2)*>) by GROUP_4:5
.= Product g * (Product(<*f/.(l+1)*>) * f/.(l+2)) by GROUP_4:6
.= Product g * (f/.(l+1) * f/.(l+2)) by GROUP_4:9;
reconsider Pg = Product g as Element of Permutations 3 by MATRIX_1:def 17;
Product g in the carrier of Group_of_Perm 3;
then Product g in Permutations 3 by MATRIX_1:def 17;
then
A25: Product g is Permutation of Seg 3 by MATRIX_1:def 16;
A26: len Permutations 3 = 3 by MATRIX_1:9;
then
A27: q1 = <*2,1,3*> or q1 = <*1,3,2*> or q1 = <*3,2,1*> by A18,Th38;
A28: q1 = f/.(l+2) by A16,A17,PARTFUN1:def 6;
q1 * q2 in Permutations 3 by Th39;
then
A29: q1 * q2 is Permutation of Seg 3 by MATRIX_1:def 16;
q2 = f/.(l+1) by A20,A21,PARTFUN1:def 6;
then
A30: f/.(l+1) * f/.(l+2) = q1 * q2 by A28,MATRIX_7:9;
then
A31: Product f = q12 * Pg by A24,MATRIX_7:9;
2*k <= 2*k + 2 by NAT_1:11;
then Seg (2*k) c= Seg (2*(k+1)) by FINSEQ_1:5;
then dom g = Seg (2*k) by A15,RELAT_1:62;
then
A32: len g = 2*k by FINSEQ_1:def 3;
then
A33: Product g = <*1,2,3*> or Product g = <*2,3,1*> or Product g = <*3,1,2
*> by A4,A11;
Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2 *>
proof
per cases by A4,A32,A11,A22,A26,A27,Th37,Th38;
suppose
Pg = <*1,2,3*> & q1 * q2 = <*2,3,1*>;
hence thesis by A29,A31,Lm15;
end;
suppose
Pg = <*2,3,1*> & q1 * q2 = <*2,3,1*>;
hence thesis by A24,A30,Th37,MATRIX_7:9;
end;
suppose
Pg = <*2,3,1*> & q1 * q2 = <*3,1,2*>;
hence thesis by A31,Th37;
end;
suppose
q1 * q2 = <*1,2,3*>;
hence thesis by A33,A25,A31,Lm16;
end;
suppose
Pg = <*1,2,3*> & q1 * q2 = <*3,1,2*>;
hence thesis by A29,A31,Lm15;
end;
suppose
Pg = <*3,1,2*> & q1 * q2 = <*2,3,1*>;
hence thesis by A31,Th37;
end;
suppose
Pg = <*3,1,2*> & q1 * q2 = <*3,1,2*>;
hence thesis by A24,A30,Th37,MATRIX_7:9;
end;
end;
hence thesis;
end;
A34: P[0]
proof
set G = Group_of_Perm 3;
let f be FinSequence of Group_of_Perm 3;
assume that
A35: len f = 2*0 and
for i be Element of NAT st i in dom f holds ex q being Element of
Permutations 3 st f.i = q & q is being_transposition;
A36: 1_G = <*1,2,3*> by FINSEQ_2:53,MATRIX_1:15;
f = <*>the carrier of G by A35;
hence thesis by A36,GROUP_4:8;
end;
A37: for s being Nat holds P[s] from NAT_1:sch 2(A34,A3);
ex t being Nat st len l = 2 * t + 0 & 0 < 2 by A1,NAT_D:def 2;
hence thesis by A2,A37;
end;
Lm17: for l being FinSequence of Group_of_Perm 3 st (len l) mod 2 = 0 & (for i
being Nat st i in dom l ex q being Element of Permutations 3 st l.i = q & q is
being_transposition) holds Product l = <*1,2,3*> or Product l = <*2,3,1*> or
Product l = <*3,1,2*>
proof
let l being FinSequence of Group_of_Perm 3 such that
A1: (len l) mod 2 = 0 and
A2: for i st i in dom l ex q being Element of Permutations 3 st l.i = q
& q is being_transposition;
for i be Element of NAT st i in dom l ex q being Element of Permutations
3 st l.i = q & q is being_transposition by A2;
hence thesis by A1,Th41;
end;
registration
cluster odd for Permutation of Seg 3;
existence
proof
reconsider f = <*3,2,1*> as Permutation of Seg 3 by Th27,MATRIX_1:def 16;
not ex l be FinSequence of Group_of_Perm 3 st (len l) mod 2 = 0 & f =
Product l & for i st i in dom l ex q being Element of Permutations 3 st l.i = q
& q is being_transposition by Lm3,Lm7,Lm17;
then f is odd by MATRIX_1:def 19;
hence thesis;
end;
end;
theorem Th42:
<*3,2,1*> is odd Permutation of Seg 3
proof
reconsider f = <*3,2,1*> as Permutation of Seg 3 by Th27,MATRIX_1:def 16;
not ex l be FinSequence of Group_of_Perm 3 st (len l) mod 2 = 0 & f =
Product l & for i st i in dom l ex q being Element of Permutations 3 st l.i = q
& q is being_transposition by Lm3,Lm7,Lm17;
hence thesis by MATRIX_1:def 19;
end;
theorem Th43:
<*2,1,3*> is odd Permutation of Seg 3
proof
reconsider f = <*2,1,3*> as Permutation of Seg 3 by Th27,MATRIX_1:def 16;
not ex l be FinSequence of Group_of_Perm 3 st (len l) mod 2 = 0 & f =
Product l & for i st i in dom l ex q being Element of Permutations 3 st l.i = q
& q is being_transposition by Lm5,Lm11,Lm17;
hence thesis by MATRIX_1:def 19;
end;
theorem Th44:
<*1,3,2*> is odd Permutation of Seg 3
proof
reconsider f = <*1,3,2*> as Permutation of Seg 3 by Th27,MATRIX_1:def 16;
not ex l be FinSequence of Group_of_Perm 3 st (len l) mod 2 = 0 & f =
Product l & for i st i in dom l ex q being Element of Permutations 3 st l.i = q
& q is being_transposition by Lm4,Lm9,Lm17;
hence thesis by MATRIX_1:def 19;
end;
theorem
for p being odd Permutation of Seg 3 holds p = <*3,2,1*> or p = <*1,3,
2*> or p = <*2,1,3*>
proof
let p be odd Permutation of Seg 3;
p in Permutations 3 by MATRIX_1:def 16;
hence thesis by Lm12,Lm13,Lm14,Th19,ENUMSET1:def 4;
end;
begin :: Determinant and Permanent
theorem
for a,b,c,d,e,f,g,h,i being Element of K for M being Matrix of 3,K st
M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds Det M = a*e*i - c*e*g - a*f*h + b*f
*g - b*d*i + c*d*h
proof
reconsider a3 = <*1,3,2*>, a4 = <*2,3,1*>, a5 = <*2,1,3*>, a6 = <*3,1,2*> as
Element of Permutations 3 by Th27;
reconsider id3 = idseq 3 as Permutation of Seg 3;
reconsider Id3 = idseq 3 as Element of Permutations 3 by MATRIX_1:def 16;
A1: id3 is even by MATRIX_1:16;
reconsider rid3 = Rev idseq 3 as Element of Permutations 3 by Th4;
let a,b,c,d,e,f,g,h,i be Element of K;
let M be Matrix of 3,K;
assume
A2: M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*>;
Permutations 3 in Fin Permutations 3 by FINSUB_1:def 5; then
In(Permutations 3,Fin Permutations 3) = Permutations 3 by SUBSET_1:def 8;
then reconsider
X = {Id3,rid3,a3,a4,a5,a6} as Element of Fin Permutations 3 by Th15,Th19,
FINSEQ_2:53;
reconsider B1 = {.Id3,rid3,a3.}, B2 = {.a4,a5,a6.} as Element of Fin
Permutations 3;
set F = the addF of K;
A3: In(Permutations 3,Fin Permutations 3) = X &
X = {Id3,rid3,a3} \/ {a4,a5,a6} by Th15,Th19,ENUMSET1:13,FINSEQ_2:53;
now
let x be object;
assume
A4: x in B1;
then x=Id3 or x=rid3 or x=a3 by ENUMSET1:def 1;
then not x in B2 by Lm5,Lm6,Lm7,Lm8,Lm9,Th15,ENUMSET1:def 1,FINSEQ_2:53;
hence x in B1 \ B2 by A4,XBOOLE_0:def 5;
end;
then
A5: B1 c= B1 \ B2 by TARSKI:def 3;
for x be object st x in B1 \ B2 holds x in B1 by XBOOLE_0:def 5;
then B1 \ B2 c= B1 by TARSKI:def 3;
then B1 \ B2 = B1 by A5,XBOOLE_0:def 10;
then
A6: B1 misses B2 by XBOOLE_1:83;
set r = Path_product M;
A7: 3 = len Permutations 3 by MATRIX_1:9;
then Id3 is even by MATRIX_1:16;
then reconsider
r1 = r.id3, r2 = r.rid3, r3 = r.a3, r4 = r.a4, r5 = r.a5, r6 = r.
a6 as Element of K by FUNCT_2:5;
A8: r.id3 = -((the multF of K) $$ Path_matrix (Id3,M),Id3) by MATRIX_3:def 8
.= (the multF of K) $$ Path_matrix (Id3,M) by A1,A7,MATRIX_1:def 20
.= (the multF of K) $$ <* a,e,i *> by A2,Th20,FINSEQ_2:53
.= a*e*i by Th26;
A9: r.a6 = -((the multF of K) $$ Path_matrix (a6,M),a6) by MATRIX_3:def 8
.= (the multF of K) $$ Path_matrix (a6,M) by A7,Lm14,MATRIX_1:def 20
.= (the multF of K) $$ <* c,d,h *> by A2,Th25
.= c*d*h by Th26;
A10: r.a5 = -((the multF of K) $$ Path_matrix (a5,M),a5) by MATRIX_3:def 8
.= -(the multF of K) $$ Path_matrix (a5,M) by A7,Th43,MATRIX_1:def 20
.= -(the multF of K) $$ <* b,d,i *> by A2,Th24
.= -b*d*i by Th26;
A11: r.a4 = -((the multF of K) $$ Path_matrix (a4,M),a4) by MATRIX_3:def 8
.= (the multF of K) $$ Path_matrix (a4,M) by A7,Lm13,MATRIX_1:def 20
.= (the multF of K) $$ <* b,f,g *> by A2,Th23
.= b*f*g by Th26;
A12: r.a3 = -((the multF of K) $$ Path_matrix (a3,M),a3) by MATRIX_3:def 8
.= -(the multF of K) $$ Path_matrix (a3,M) by A7,Th44,MATRIX_1:def 20
.= -(the multF of K) $$ <* a,f,h *> by A2,Th22
.= -a*f*h by Th26;
A13: r.rid3 = -((the multF of K) $$ Path_matrix (rid3,M),rid3) by
MATRIX_3:def 8
.= -(the multF of K) $$ Path_matrix (rid3,M) by A7,Th15,Th42,
MATRIX_1:def 20
.= -(the multF of K) $$ <* c,e,g *> by A2,Th15,Th21
.= -c*e*g by Th26;
A14: F $$(B1,r) = r1 + r2 + r3 & F $$(B2,r) = r4 + r5 + r6 by Lm3,Lm4,Lm10,Lm11
,Th15,FINSEQ_2:53,SETWOP_2:3;
Det M = F $$ (In(Permutations 3,Fin Permutations 3), r) by MATRIX_3:def 9
.= F.(F $$ (B1,r),F $$ (B2,r)) by A3,A6,SETWOP_2:4
.= r1 + r2 + r3 + (r4 + (r5 + r6)) by A14,RLVECT_1:def 3
.= r1 + r2 + r3 + r4 + (r5 + r6) by RLVECT_1:def 3
.= a*e*i - c*e*g - a*f*h + b*f*g - b*d*i + c*d*h by A8,A13,A12,A11,A10,A9,
RLVECT_1:def 3;
hence thesis;
end;
theorem
for a,b,c,d,e,f,g,h,i being Element of K for M being Matrix of 3,K st
M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds Per M = a*e*i + c*e*g + a*f*h + b*f
*g + b*d*i + c*d*h
proof
reconsider rid3 = Rev idseq 3 as Element of Permutations 3 by Th4;
let a,b,c,d,e,f,g,h,i be Element of K;
let M be Matrix of 3,K;
assume
A1: M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*>;
reconsider a3 = <*1,3,2*>, a4 = <*2,3,1*>, a5 = <*2,1,3*>, a6 = <*3,1,2*> as
Element of Permutations 3 by Th27;
reconsider id3 = idseq 3 as Permutation of Seg 3;
reconsider Id3 = idseq 3 as Element of Permutations 3 by MATRIX_1:def 16;
reconsider B1 = {.Id3,rid3,a3.}, B2 = {.a4,a5,a6.} as Element of Fin
Permutations 3;
set r = PPath_product M;
A2: r.id3 = (the multF of K) $$ Path_matrix (Id3,M) by Def1
.= (the multF of K) $$ <* a,e,i *> by A1,Th20,FINSEQ_2:53
.= a*e*i by Th26;
A3: r.a6 = (the multF of K) $$ Path_matrix (a6,M) by Def1
.= (the multF of K) $$ <* c,d,h *> by A1,Th25
.= c*d*h by Th26;
A4: r.a5 = (the multF of K) $$ Path_matrix (a5,M) by Def1
.= (the multF of K) $$ <* b,d,i *> by A1,Th24
.= b*d*i by Th26;
A5: r.a4 = (the multF of K) $$ Path_matrix (a4,M) by Def1
.= (the multF of K) $$ <* b,f,g *> by A1,Th23
.= b*f*g by Th26;
now
let x be object;
assume
A6: x in B1;
then x=Id3 or x=rid3 or x=a3 by ENUMSET1:def 1;
then not x in B2 by Lm5,Lm6,Lm7,Lm8,Lm9,Th15,ENUMSET1:def 1,FINSEQ_2:53;
hence x in B1 \ B2 by A6,XBOOLE_0:def 5;
end;
then
A7: B1 c= B1 \ B2 by TARSKI:def 3;
for x be object st x in B1 \ B2 holds x in B1 by XBOOLE_0:def 5;
then B1 \ B2 c= B1 by TARSKI:def 3;
then B1 \ B2 = B1 by A7,XBOOLE_0:def 10;
then
A8: B1 misses B2 by XBOOLE_1:83;
set F = the addF of K;
id3 in Permutations 3 by MATRIX_1:def 16;
then reconsider
r1 = r.id3, r2 = r.rid3, r3 = r.a3, r4 = r.a4, r5 = r.a5, r6 = r.
a6 as Element of K by FUNCT_2:5;
Permutations 3 in Fin Permutations 3 by FINSUB_1:def 5; then
In(Permutations 3,Fin Permutations 3) = Permutations 3 by SUBSET_1:def 8;
then reconsider
X = {Id3,rid3,a3,a4,a5,a6} as Element of Fin Permutations 3 by Th15,Th19,
FINSEQ_2:53;
A9: F $$(B1,r) = r1 + r2 + r3 & F $$(B2,r) = r4 + r5 + r6 by Lm3,Lm4,Lm10,Lm11
,Th15,FINSEQ_2:53,SETWOP_2:3;
A10: r.rid3 = (the multF of K) $$ Path_matrix (rid3,M) by Def1
.= (the multF of K) $$ <* c,e,g *> by A1,Th15,Th21
.= c*e*g by Th26;
A11: r.a3 = (the multF of K) $$ Path_matrix (a3,M) by Def1
.= (the multF of K) $$ <* a,f,h *> by A1,Th22
.= a*f*h by Th26;
In(Permutations 3, Fin Permutations 3) = X &
X = {Id3,rid3,a3} \/ {a4,a5,a6} by Th15,Th19,ENUMSET1:13,FINSEQ_2:53;
then Per M = F.(F $$ (B1,r),F $$ (B2,r)) by A8,SETWOP_2:4
.= r1 + r2 + r3 + (r4 + (r5 + r6)) by A9,RLVECT_1:def 3
.= r1 + r2 + r3 + r4 + (r5 + r6) by RLVECT_1:def 3
.= a*e*i + c*e*g + a*f*h + b*f*g + b*d*i + c*d*h by A2,A10,A11,A5,A4,A3,
RLVECT_1:def 3;
hence thesis;
end;
theorem Th48:
for i,n being Element of NAT for p being Element of Permutations
n st i in Seg n holds ex k being Element of NAT st k in Seg n & i = p.k
proof
let i,n be Element of NAT;
let p be Element of Permutations n;
A1: p is Permutation of Seg n by MATRIX_1:def 16;
then
A2: dom p = Seg n by FUNCT_2:52;
then reconsider s = p as FinSequence by FINSEQ_1:def 2;
assume i in Seg n;
then i in rng s by A1,FUNCT_2:def 3;
then ex k being Nat st k in dom s & i = s.k by FINSEQ_2:10;
hence thesis by A2;
end;
theorem Th49:
for M being Matrix of n, K st (ex i being Element of NAT st i in
Seg n & for k being Element of NAT st k in Seg n holds Col(M,i).k = 0.K) holds
for p being Element of Permutations n holds ex l being Element of NAT st l in
Seg n & Path_matrix (p,M).l = 0.K
proof
let M be Matrix of n, K;
assume ex i being Element of NAT st i in Seg n & for k being Element of NAT
st k in Seg n holds Col(M,i).k = 0.K;
then consider i being Element of NAT such that
A1: i in Seg n and
A2: for k being Element of NAT st k in Seg n holds Col(M,i).k = 0.K;
let p be Element of Permutations n;
n in NAT by ORDINAL1:def 12;
then consider k being Element of NAT such that
A3: k in Seg n and
A4: i = p.k by A1,Th48;
A5: 1 <= k by A3,FINSEQ_1:1;
len M = n by MATRIX_0:def 2;
then k <= len M by A3,FINSEQ_1:1;
then
A6: k in dom M by A5,FINSEQ_3:25;
take k;
len Path_matrix (p, M) = n by MATRIX_3:def 7;
then dom Path_matrix (p, M) = Seg n by FINSEQ_1:def 3;
then Path_matrix (p, M).k = M*(k,i) by A3,A4,MATRIX_3:def 7;
then Path_matrix (p, M).k = Col(M,i).k by A6,MATRIX_0:def 8;
hence thesis by A2,A3;
end;
theorem Th50:
for p being Element of Permutations n for M being Matrix of n, K
st (ex i being Element of NAT st i in Seg n & for k being Element of NAT st k
in Seg n holds Col(M,i).k = 0.K) holds (Path_product M).p = 0.K
proof
let p be Element of Permutations n;
let M be Matrix of n, K;
A1: (Path_product M).p = -((the multF of K) $$ Path_matrix(p,M),p) by
MATRIX_3:def 8
.= - (Product (Path_matrix(p,M)),p) by GROUP_4:def 2;
assume ex i being Element of NAT st i in Seg n & for k being Element of NAT
st k in Seg n holds Col(M,i).k = 0.K;
then consider l being Element of NAT such that
A2: l in Seg n and
A3: Path_matrix (p,M).l = 0.K by Th49;
set k = l;
len Path_matrix (p, M) = n by MATRIX_3:def 7;
then k in dom (Path_matrix(p,M)) by A2,FINSEQ_1:def 3;
then
A4: Product Path_matrix(p,M) = 0.K by A3,FVSUM_1:82;
per cases;
suppose
p is even;
hence thesis by A4,A1,MATRIX_1:def 20;
end;
suppose
p is odd;
then -(Product (Path_matrix(p,M)),p) = -Product (Path_matrix(p,M)) by
MATRIX_1:def 20
.= 0.K by A4,RLVECT_1:12;
hence thesis by A1;
end;
end;
theorem Th51:
for M being Matrix of n, K st (ex i being Element of NAT st i in
Seg n & for k being Element of NAT st k in Seg n holds Col(M,i).k = 0.K) holds
(the addF of K) $$ (In(Permutations n,Fin Permutations n), Path_product M)
= 0.K
proof
let M be Matrix of n, K;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
reconsider M1=M as Matrix of n1, K;
given i being Element of NAT such that
A1: i in Seg n & for k being Element of NAT st k in Seg n holds Col(M,i)
.k = 0.K;
set P1 = In(Permutations n,Fin Permutations n);
set f = Path_product M1;
set F = the addF of K;
Permutations n in Fin Permutations n by FINSUB_1:def 5; then
P1 = Permutations n by SUBSET_1:def 8; then
reconsider P1 as non empty Element of Fin Permutations n1;
defpred P[non empty Element of Fin Permutations n1] means F $$ ($1, f) = 0.K;
A2: for x being Element of Permutations n1, B being non empty Element of Fin
Permutations n1 st x in P1 & B c= P1 & not x in B & P[B] holds P[B \/ {.x.}]
proof
let x be Element of Permutations n1, B be non empty Element of Fin
Permutations n1;
assume that
x in P1 and
B c= P1 and
A3: not x in B and
A4: P[B];
F $$ (B \/ {.x.}, f) = F.(F $$(B,f), f.x) by A3,SETWOP_2:2
.= F $$(B,f) + 0.K by A1,Th50
.= 0.K by A4,RLVECT_1:4;
hence thesis;
end;
A5: for x being Element of Permutations n1 st x in P1 holds P[{.x.}]
proof
let x be Element of Permutations n1;
assume x in P1;
F $$ ({.x.}, f) = f.x by SETWISEO:17
.= 0.K by A1,Th50;
hence thesis;
end;
P[P1] from NonEmptyFiniteX(A5,A2);
hence thesis;
end;
theorem Th52:
for p being Element of Permutations n for M being Matrix of n, K
st (ex i being Element of NAT st i in Seg n & (for k being Element of NAT st k
in Seg n holds Col(M,i).k = 0.K)) holds (PPath_product M).p = 0.K
proof
let p be Element of Permutations n;
let M be Matrix of n, K;
assume ex i being Element of NAT st i in Seg n & for k being Element of NAT
st k in Seg n holds Col(M,i).k = 0.K;
then consider l being Element of NAT such that
A1: l in Seg n and
A2: Path_matrix (p,M).l = 0.K by Th49;
len Path_matrix (p, M) = n by MATRIX_3:def 7;
then l in dom Path_matrix(p,M) by A1,FINSEQ_1:def 3;
then
A3: Product Path_matrix(p,M) = 0.K by A2,FVSUM_1:82;
(PPath_product M).p = (the multF of K) $$ Path_matrix(p,M) by Def1
.= 0.K by A3,GROUP_4:def 2;
hence thesis;
end;
Lm18: for M being Matrix of n, K st (ex i being Element of NAT st i in Seg n &
for k being Element of NAT st k in Seg n holds Col(M,i).k = 0.K) holds (the
addF of K) $$ (In (Permutations n,Fin Permutations n), PPath_product M) = 0.K
proof
let M be Matrix of n, K;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
reconsider M1=M as Matrix of n1, K;
set F = the addF of K;
set f = PPath_product M1;
set P1 = In (Permutations n1, Fin Permutations n1);
Permutations n1 in Fin Permutations n1 by FINSUB_1:def 5; then
reconsider P1 as non empty Element of Fin Permutations n1 by SUBSET_1:def 8;
defpred P[non empty Element of Fin Permutations n1] means F $$ ($1, f) = 0.K;
assume
A1: ex i being Element of NAT st i in Seg n & for k being Element of NAT
st k in Seg n holds Col(M,i).k = 0.K;
A2: for x being Element of Permutations n1, B being non empty Element of Fin
Permutations n1 st x in P1 & B c= P1 & not x in B & P[B] holds P[B \/ {.x.}]
proof
let x be Element of Permutations n1, B be non empty Element of Fin
Permutations n1;
assume that
x in P1 and
B c= P1 and
A3: not x in B and
A4: P[B];
F $$ (B \/ {.x.}, f) = F.(F $$(B,f), f.x) by A3,SETWOP_2:2
.= F $$(B,f) + 0.K by A1,Th52
.= 0.K by A4,RLVECT_1:4;
hence thesis;
end;
A5: for x being Element of Permutations n1 st x in P1 holds P[{.x.}]
proof
let x be Element of Permutations n1;
assume x in P1;
F $$ ({.x.}, f) = f.x by SETWISEO:17
.= 0.K by A1,Th52;
hence thesis;
end;
P[P1] from NonEmptyFiniteX(A5,A2);
hence thesis;
end;
theorem
for M being Matrix of n, K st (ex i being Element of NAT st i in Seg n
& for k being Element of NAT st k in Seg n holds Col(M,i).k = 0.K) holds Det M
= 0.K
proof
let M be Matrix of n,K;
assume
A1: ex i being Element of NAT st i in Seg n & for k being Element of NAT
st k in Seg n holds Col(M,i).k = 0.K;
set f = Path_product M;
set F = the addF of K;
Det M = F $$ (In(Permutations n,Fin Permutations n),f) by MATRIX_3:def 9
.= 0.K by A1,Th51;
hence thesis;
end;
theorem
for M being Matrix of n, K st (ex i being Element of NAT st i in Seg n
& for k being Element of NAT st k in Seg n holds Col(M,i).k = 0.K) holds Per M
= 0.K by Lm18;
begin :: Auxiliary Lemmas for Further Work
theorem
for M,N being Matrix of n, K st i in Seg n for p being Element of
Permutations n holds ex k being Element of NAT st k in Seg n & i = p.k & Col(N,
i)/.k = Path_matrix (p, N)/.k
proof
let M,N be Matrix of n, K;
assume
A1: i in Seg n;
let p be Element of Permutations n;
n in NAT by ORDINAL1:def 12;
then consider k being Element of NAT such that
A2: k in Seg n and
A3: i = p.k by A1,Th48;
len Path_matrix (p, N) = n by MATRIX_3:def 7;
then
A4: k in dom Path_matrix (p, N) by A2,FINSEQ_1:def 3;
then Path_matrix (p, N).k = N*(k,i) by A3,MATRIX_3:def 7;
then
A5: Path_matrix (p, N)/.k = N*(k,i) by A4,PARTFUN1:def 6;
take k;
A6: len N = n by MATRIX_0:def 2;
then k in dom N by A2,FINSEQ_1:def 3;
then
A7: Col(N,i).k = N*(k,i) by MATRIX_0:def 8;
len Col(N,i) = len N by MATRIX_0:def 8;
then k in dom Col(N,i) by A2,A6,FINSEQ_1:def 3;
hence thesis by A2,A3,A5,A7,PARTFUN1:def 6;
end;
theorem
for a being Element of K for M,N being Matrix of n, K st (ex i being
Element of NAT st i in Seg n & (for k being Element of NAT st k in Seg n holds
Col(M,i).k = a * Col(N,i)/.k) & (for l being Element of NAT st l <> i & l in
Seg n holds Col(M,l) = Col(N,l))) for p being Element of Permutations n holds
ex l being Element of NAT st l in Seg n & Path_matrix (p,M)/.l = a * (
Path_matrix (p,N)/.l)
proof
let a be Element of K;
let M,N be Matrix of n, K;
assume ex i being Element of NAT st i in Seg n & (for k being Element of
NAT st k in Seg n holds Col(M,i).k = a * Col(N,i)/.k) & for l being Element of
NAT st l <> i & l in Seg n holds Col(M,l) = Col(N,l);
then consider i being Element of NAT such that
A1: i in Seg n and
A2: for k being Element of NAT st k in Seg n holds Col(M,i).k = a * Col(
N,i )/.k and
for l being Element of NAT st l <> i & l in Seg n holds Col(M,l) = Col(N ,l);
let p be Element of Permutations n;
n in NAT by ORDINAL1:def 12;
then consider k being Element of NAT such that
A3: k in Seg n and
A4: i = p.k by A1,Th48;
A5: 1 <= k by A3,FINSEQ_1:1;
len Path_matrix (p, N) = n by MATRIX_3:def 7;
then
A6: k in dom Path_matrix (p, N) by A3,FINSEQ_1:def 3;
then Path_matrix (p, N).k = N*(k,i) by A4,MATRIX_3:def 7;
then
A7: Path_matrix (p, N)/.k = N*(k,i) by A6,PARTFUN1:def 6;
len Col(N,i) = len N by MATRIX_0:def 8;
then
A8: dom Col(N,i) = dom N by FINSEQ_3:29;
len N = n by MATRIX_0:def 2;
then k <= len N by A3,FINSEQ_1:1;
then
A9: k in dom N by A5,FINSEQ_3:25;
then Col(N,i).k = N*(k,i) by MATRIX_0:def 8;
then
A10: Col(N,i)/.k = Path_matrix (p, N)/.k by A9,A7,A8,PARTFUN1:def 6;
len M = n by MATRIX_0:def 2;
then k <= len M by A3,FINSEQ_1:1;
then
A11: k in dom M by A5,FINSEQ_3:25;
take k;
len Path_matrix (p, M) = n by MATRIX_3:def 7;
then
A12: dom Path_matrix (p, M) = Seg n by FINSEQ_1:def 3;
then Path_matrix (p, M).k = M*(k,i) by A3,A4,MATRIX_3:def 7;
then Path_matrix (p, M).k = Col(M,i).k by A11,MATRIX_0:def 8
.= a * (Path_matrix (p, N)/.k) by A2,A3,A10;
hence thesis by A12,A3,PARTFUN1:def 6;
end;