let n be Nat; :: thesis: for K being commutative Ring
for p2, q2 being Element of Permutations (n + 2)
for i, j being Nat st i in Seg (n + 2) & j in Seg (n + 2) & i < j & p2 . i = q2 . i & p2 . j = q2 . j holds
(Part_sgn (p2,K)) . {i,j} = (Part_sgn (q2,K)) . {i,j}
let K be commutative Ring; :: thesis: for p2, q2 being Element of Permutations (n + 2)
for i, j being Nat st i in Seg (n + 2) & j in Seg (n + 2) & i < j & p2 . i = q2 . i & p2 . j = q2 . j holds
(Part_sgn (p2,K)) . {i,j} = (Part_sgn (q2,K)) . {i,j}
let p2, q2 be Element of Permutations (n + 2); :: thesis: for i, j being Nat st i in Seg (n + 2) & j in Seg (n + 2) & i < j & p2 . i = q2 . i & p2 . j = q2 . j holds
(Part_sgn (p2,K)) . {i,j} = (Part_sgn (q2,K)) . {i,j}
set n2 = n + 2;
let i, j be Nat; :: thesis: ( i in Seg (n + 2) & j in Seg (n + 2) & i < j & p2 . i = q2 . i & p2 . j = q2 . j implies (Part_sgn (p2,K)) . {i,j} = (Part_sgn (q2,K)) . {i,j} )
assume that
A1: i in Seg (n + 2) and
A2: j in Seg (n + 2) and
A3: i < j and
A4: p2 . i = q2 . i and
A5: p2 . j = q2 . j ; :: thesis: (Part_sgn (p2,K)) . {i,j} = (Part_sgn (q2,K)) . {i,j}
reconsider p29 = p2 as Permutation of (Seg (n + 2)) by MATRIX_1:def 12;
A6: p29 . i <> p29 . j by A1, A2, A3, FUNCT_2:19;
now :: thesis: (Part_sgn (p2,K)) . {i,j} = (Part_sgn (q2,K)) . {i,j}
per cases ( p2 . i < p2 . j or p2 . i > p2 . j ) by A6, XXREAL_0:1;
suppose A7: p2 . i < p2 . j ; :: thesis: (Part_sgn (p2,K)) . {i,j} = (Part_sgn (q2,K)) . {i,j}
then (Part_sgn (p2,K)) . {i,j} = 1_ K by A1, A2, A3, Def1;
hence (Part_sgn (p2,K)) . {i,j} = (Part_sgn (q2,K)) . {i,j} by A1, A2, A3, A4, A5, A7, Def1; :: thesis: verum
end;
suppose A8: p2 . i > p2 . j ; :: thesis: (Part_sgn (p2,K)) . {i,j} = (Part_sgn (q2,K)) . {i,j}
then (Part_sgn (p2,K)) . {i,j} = - (1_ K) by A1, A2, A3, Def1;
hence (Part_sgn (p2,K)) . {i,j} = (Part_sgn (q2,K)) . {i,j} by A1, A2, A3, A4, A5, A8, Def1; :: thesis: verum
end;
end;
end;
hence (Part_sgn (p2,K)) . {i,j} = (Part_sgn (q2,K)) . {i,j} ; :: thesis: verum