let n be Nat; :: thesis: for K being Field
for p2, q2, pq2 being Element of Permutations (n + 2) st pq2 = p2 * q2 holds
sgn pq2,K = (sgn p2,K) * (sgn q2,K)
let K be Field; :: thesis: for p2, q2, pq2 being Element of Permutations (n + 2) st pq2 = p2 * q2 holds
sgn pq2,K = (sgn p2,K) * (sgn q2,K)
set n2 = n + 2;
let p, q, pq be Element of Permutations (n + 2); :: thesis: ( pq = p * q implies sgn pq,K = (sgn p,K) * (sgn q,K) )
assume A1: pq = p * q ; :: thesis: sgn pq,K = (sgn p,K) * (sgn q,K)
consider P1 being FinSequence of (Group_of_Perm (n + 2)) such that
A2: p = Product P1 and
A3: for i being Nat st i in dom P1 holds
ex trans being Element of Permutations (n + 2) st
( P1 . i = trans & trans is being_transposition ) by Th21;
consider P2 being FinSequence of (Group_of_Perm (n + 2)) such that
A4: q = Product P2 and
A5: for i being Nat st i in dom P2 holds
ex trans being Element of Permutations (n + 2) st
( P2 . i = trans & trans is being_transposition ) by Th21;
set PP = P2 ^ P1;
A6: Product (P2 ^ P1) = (Product P2) * (Product P1) by GROUP_4:8
.= pq by A1, A2, A4, MATRIX_2:def 13 ;
A7: for i being Nat st i in dom (P2 ^ P1) holds
ex trans being Element of Permutations (n + 2) st
( (P2 ^ P1) . i = trans & trans is being_transposition )

proof

let i be Nat; :: thesis: ( i in dom (P2 ^ P1) implies ex trans being Element of Permutations (n + 2) st
( (P2 ^ P1) . i = trans & trans is being_transposition ) )
assume A8: i in dom (P2 ^ P1) ; :: thesis: ex trans being Element of Permutations (n + 2) st
( (P2 ^ P1) . i = trans & trans is being_transposition )

now

per cases ( i in dom P2 or ex k being Nat st
( k in dom P1 & i = (len P2) + k ) ) by A8, FINSEQ_1:38;

suppose i in dom P2 ; :: thesis: ex trans being Element of Permutations (n + 2) st
( (P2 ^ P1) . i = trans & trans is being_transposition )

then ( P2 . i = (P2 ^ P1) . i & ex trans being Element of Permutations (n + 2) st
( P2 . i = trans & trans is being_transposition ) ) by A5, FINSEQ_1:def 7;
hence ex trans being Element of Permutations (n + 2) st
( (P2 ^ P1) . i = trans & trans is being_transposition ) ; :: thesis: verum

end;

suppose ex k being Nat st
( k in dom P1 & i = (len P2) + k ) ; :: thesis: ex trans being Element of Permutations (n + 2) st
( (P2 ^ P1) . i = trans & trans is being_transposition )

then consider k being Nat such that
A9: ( k in dom P1 & i = (len P2) + k ) ;
( P1 . k = (P2 ^ P1) . i & ex trans being Element of Permutations (n + 2) st
( P1 . k = trans & trans is being_transposition ) ) by A3, A9, FINSEQ_1:def 7;
hence ex trans being Element of Permutations (n + 2) st
( (P2 ^ P1) . i = trans & trans is being_transposition ) ; :: thesis: verum

end;

end;

end;

hence ex trans being Element of Permutations (n + 2) st
( (P2 ^ P1) . i = trans & trans is being_transposition ) ; :: thesis: verum

end;

now

per cases ( ( (len P1) mod 2 = 0 & (len P2) mod 2 = 0 ) or ( (len P1) mod 2 = 1 & (len P2) mod 2 = 0 ) or ( (len P1) mod 2 = 0 & (len P2) mod 2 = 1 ) or ( (len P1) mod 2 = 1 & (len P2) mod 2 = 1 ) ) by NAT_D:12;

suppose A10: ( (len P1) mod 2 = 0 & (len P2) mod 2 = 0 ) ; :: thesis: sgn pq,K = (sgn p,K) * (sgn q,K)

(len (P2 ^ P1)) mod 2 = ((len P2) + (len P1)) mod 2 by FINSEQ_1:35
.= ((0 + (len P1)) + 0 ) mod 2 by A10, NAT_D:22
.= 0 by A10 ;
then ( sgn pq,K = 1_ K & sgn p,K = 1_ K & sgn q,K = 1_ K ) by A2, A3, A4, A5, A6, A7, A10, Th15;
hence sgn pq,K = (sgn p,K) * (sgn q,K) by VECTSP_1:def 13; :: thesis: verum

end;

suppose A11: ( (len P1) mod 2 = 1 & (len P2) mod 2 = 0 ) ; :: thesis: sgn pq,K = (sgn p,K) * (sgn q,K)

(len (P2 ^ P1)) mod 2 = ((len P2) + (len P1)) mod 2 by FINSEQ_1:35
.= ((0 + (len P1)) + 0 ) mod 2 by A11, NAT_D:22
.= 1 by A11 ;
then ( sgn pq,K = - (1_ K) & sgn p,K = - (1_ K) & sgn q,K = 1_ K ) by A2, A3, A4, A5, A6, A7, A11, Th15;
hence sgn pq,K = (sgn p,K) * (sgn q,K) by VECTSP_1:def 13; :: thesis: verum

end;

suppose A12: ( (len P1) mod 2 = 0 & (len P2) mod 2 = 1 ) ; :: thesis: sgn pq,K = (sgn p,K) * (sgn q,K)

(len (P2 ^ P1)) mod 2 = ((len P2) + (len P1)) mod 2 by FINSEQ_1:35
.= (1 + (len P1)) mod 2 by A12, NAT_D:22
.= (1 + 0 ) mod 2 by A12, NAT_D:22
.= 1 by NAT_D:14 ;
then ( sgn pq,K = - (1_ K) & sgn p,K = 1_ K & sgn q,K = - (1_ K) ) by A2, A3, A4, A5, A6, A7, A12, Th15;
hence sgn pq,K = (sgn p,K) * (sgn q,K) by VECTSP_1:def 13; :: thesis: verum

end;

suppose A13: ( (len P1) mod 2 = 1 & (len P2) mod 2 = 1 ) ; :: thesis: sgn pq,K = (sgn p,K) * (sgn q,K)

(len (P2 ^ P1)) mod 2 = ((len P2) + (len P1)) mod 2 by FINSEQ_1:35
.= (1 + (len P1)) mod 2 by A13, NAT_D:22
.= (1 + 1) mod 2 by A13, NAT_D:22
.= 0 by NAT_D:25 ;
then ( sgn pq,K = 1_ K & sgn p,K = - (1_ K) & sgn q,K = - (1_ K) & (1_ K) * (1_ K) = 1_ K ) by A2, A3, A4, A5, A6, A7, A13, Th15, VECTSP_1:def 13;
hence sgn pq,K = (sgn p,K) * (sgn q,K) by VECTSP_1:42; :: thesis: verum

end;

end;

end;

hence sgn pq,K = (sgn p,K) * (sgn q,K) ; :: thesis: verum