let n be Nat; :: thesis: for K being commutative Ring
for P being FinSequence of (Group_of_Perm (n + 2))
for p2 being Element of Permutations (n + 2) st p2 = Product P & ( for i being Nat st i in dom P holds
ex trans being 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) ) )
let K be commutative Ring; :: thesis: for P being FinSequence of (Group_of_Perm (n + 2))
for p2 being Element of Permutations (n + 2) st p2 = Product P & ( for i being Nat st i in dom P holds
ex trans being 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) ) )
set n2 = n + 2;
set G = Group_of_Perm (n + 2);
defpred S1[ Nat] means for P being FinSequence of (Group_of_Perm (n + 2))
for p2 being Element of Permutations (n + 2) st p2 = Product P & len P = $1 & ( for i being Nat st i in dom P holds
ex trans being 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) ) );
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; :: thesis: S1[k + 1]
set k1 = k + 1;
let P be FinSequence of (Group_of_Perm (n + 2)); :: thesis: for p2 being Element of Permutations (n + 2) st p2 = Product P & len P = k + 1 & ( for i being Nat st i in dom P holds
ex trans being 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) ) )
let p2 be Element of Permutations (n + 2); :: thesis: ( p2 = Product P & len P = k + 1 & ( for i being Nat st i in dom P holds
ex trans being Element of Permutations (n + 2) st
( P . i = trans & trans is being_transposition ) ) implies ( ( (len P) mod 2 = 0 implies sgn (p2,K) = 1_ K ) & ( (len P) mod 2 = 1 implies sgn (p2,K) = - (1_ K) ) ) )
assume that
A3: p2 = Product P and
A4: len P = k + 1 and
A5: for i being Nat st i in dom P holds
ex trans being Element of Permutations (n + 2) st
( P . i = trans & trans is being_transposition ) ; :: thesis: ( ( (len P) mod 2 = 0 implies sgn (p2,K) = 1_ K ) & ( (len P) mod 2 = 1 implies sgn (p2,K) = - (1_ K) ) )
consider x being object , Q being 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 = Q as FinSequence of (Group_of_Perm (n + 2)) by A6, FINSEQ_1:36;
A8: for i being Nat st i in dom Q holds
ex trans being Element of Permutations (n + 2) st
( Q . i = trans & trans is being_transposition )
proof
let i be Nat; :: thesis: ( i in dom Q implies ex trans being Element of Permutations (n + 2) st
( Q . i = trans & trans is being_transposition ) )
assume A9: i in dom Q ; :: thesis: ex trans being Element of Permutations (n + 2) st
( Q . i = trans & trans is being_transposition )
Q . i = P . ((len X) + i) by A6, A9, FINSEQ_1:def 7;
hence ex trans being Element of Permutations (n + 2) st
( Q . i = trans & trans is being_transposition ) by A5, A6, A9, FINSEQ_1:28; :: thesis: verum
end;
1 + 0 <= k + 1 by XREAL_1:7;
then 1 in Seg (k + 1) ;
then A10: 1 in dom P by A4, FINSEQ_1:def 3;
P . 1 = x by A6, FINSEQ_1:41;
then consider tr being Element of Permutations (n + 2) such that
A11: x = tr and
A12: tr is being_transposition by A5, A10;
reconsider PQ = Product Q as Element of Permutations (n + 2) by MATRIX_1:def 13;
reconsider Tr = tr as Element of (Group_of_Perm (n + 2)) by MATRIX_1:def 13;
A13: p2 = Tr * (Product Q) by A3, A6, A11, GROUP_4:7
.= PQ * tr by MATRIX_1:def 13 ;
then A14: sgn (p2,K) = - (sgn (PQ,K)) by A12, Th13;
now :: thesis: ( ( (len P) mod 2 = 0 implies sgn (p2,K) = 1_ K ) & ( (len P) mod 2 = 1 implies sgn (p2,K) = - (1_ K) ) )
per cases ( (len Q) mod 2 = 0 or (len Q) mod 2 = 1 ) by NAT_D:12;
suppose A15: (len Q) mod 2 = 0 ; :: thesis: ( ( (len P) mod 2 = 0 implies sgn (p2,K) = 1_ K ) & ( (len P) mod 2 = 1 implies sgn (p2,K) = - (1_ K) ) )
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 ( ( (len P) mod 2 = 0 implies sgn (p2,K) = 1_ K ) & ( (len P) mod 2 = 1 implies sgn (p2,K) = - (1_ K) ) ) by A12, A13, A16, Th13; :: thesis: verum
end;
suppose A17: (len Q) mod 2 = 1 ; :: thesis: ( ( (len P) mod 2 = 0 implies sgn (p2,K) = 1_ K ) & ( (len P) mod 2 = 1 implies sgn (p2,K) = - (1_ K) ) )
A18: 2 - 1 = 1 ;
sgn (PQ,K) = - (1_ K) by A2, A4, A7, A8, A17;
hence ( ( (len P) mod 2 = 0 implies sgn (p2,K) = 1_ K ) & ( (len P) mod 2 = 1 implies sgn (p2,K) = - (1_ K) ) ) by A7, A14, A17, A18, NAT_D:69, RLVECT_1:17; :: thesis: verum
end;
end;
end;
hence ( ( (len P) mod 2 = 0 implies sgn (p2,K) = 1_ K ) & ( (len P) mod 2 = 1 implies sgn (p2,K) = - (1_ K) ) ) ; :: thesis: verum
end;
A19: S1[ 0 ]
proof
let P be FinSequence of (Group_of_Perm (n + 2)); :: thesis: for p2 being Element of Permutations (n + 2) st p2 = Product P & len P = 0 & ( for i being Nat st i in dom P holds
ex trans being 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) ) )
let p2 be Element of Permutations (n + 2); :: thesis: ( p2 = Product P & len P = 0 & ( for i being Nat st i in dom P holds
ex trans being Element of Permutations (n + 2) st
( P . i = trans & trans is being_transposition ) ) implies ( ( (len P) mod 2 = 0 implies sgn (p2,K) = 1_ K ) & ( (len P) mod 2 = 1 implies sgn (p2,K) = - (1_ K) ) ) )
assume that
A20: p2 = Product P and
A21: len P = 0 and
for i being Nat st i in dom P holds
ex trans being Element of Permutations (n + 2) st
( P . i = trans & trans is being_transposition ) ; :: thesis: ( ( (len P) mod 2 = 0 implies sgn (p2,K) = 1_ K ) & ( (len P) mod 2 = 1 implies sgn (p2,K) = - (1_ K) ) )
P = <*> the carrier of (Group_of_Perm (n + 2)) by A21;
then Product P = 1_ (Group_of_Perm (n + 2)) by GROUP_4:8;
then Product P = idseq (n + 2) by MATRIX_1:15;
hence ( ( (len P) mod 2 = 0 implies sgn (p2,K) = 1_ K ) & ( (len P) mod 2 = 1 implies sgn (p2,K) = - (1_ K) ) ) by A20, A21, Th12, NAT_D:26; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A19, A1);
 hence for P being FinSequence of (Group_of_Perm (n + 2))
for p2 being Element of Permutations (n + 2) st p2 = Product P & ( for i being Nat st i in dom P holds
ex trans being 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) ) ) ; :: thesis: verum