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