let n be Nat; 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; 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); 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; ( 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
; (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 (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
;
(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;
verum end; suppose A8:
p2 . i > p2 . j
;
(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;
verum end; end; end;
hence
(Part_sgn (p2,K)) . {i,j} = (Part_sgn (q2,K)) . {i,j}
; verum