let n be Nat; :: thesis: for K being commutative Ring
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 commutative Ring; :: 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 P2 being FinSequence of (Group_of_Perm (n + 2)) such that
A2: q = Product P2 and
A3: 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;
consider P1 being FinSequence of (Group_of_Perm (n + 2)) such that
A4: p = Product P1 and
A5: 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;
set PP = P2 ^ P1;
A6: 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 A7: i in dom (P2 ^ P1) ; :: thesis: ex trans being Element of Permutations (n + 2) st
( (P2 ^ P1) . i = trans & trans is being_transposition )

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

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

suppose A8: 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 by FINSEQ_1:def 7;
hence ex trans being Element of Permutations (n + 2) st
( (P2 ^ P1) . i = trans & trans is being_transposition ) by A3, A8; :: 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 and
A10: i = (len P2) + k ;
P1 . k = (P2 ^ P1) . i by A9, A10, FINSEQ_1:def 7;
hence ex trans being Element of Permutations (n + 2) st
( (P2 ^ P1) . i = trans & trans is being_transposition ) by A5, A9; :: 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;

A11: Product (P2 ^ P1) = (Product P2) * (Product P1) by GROUP_4:5
.= pq by A1, A4, A2, MATRIX_1:def 13 ;

now :: thesis: sgn (pq,K) = (sgn (p,K)) * (sgn (q,K))

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 A12: ( (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: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 sgn (pq,K) = (sgn (p,K)) * (sgn (q,K)) by A13, A14; :: thesis: verum

end;

suppose A15: ( (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: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 sgn (pq,K) = (sgn (p,K)) * (sgn (q,K)) by A16, A17; :: thesis: verum

end;

suppose A18: ( (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: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 sgn (pq,K) = (sgn (p,K)) * (sgn (q,K)) by A19, A20; :: thesis: verum

end;

suppose A21: ( (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: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 sgn (pq,K) = (sgn (p,K)) * (sgn (q,K)) by A22, A24, A23, VECTSP_1:10; :: thesis: verum

end;

end;

end;

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