let n be Nat; :: thesis: for K being Field
for p2, q2, pq2 being Element of Permutations (n + 2)
for i, j being Nat st pq2 = p2 * q2 & q2 is being_transposition & q2 . i = j & i < j holds
for s being Element of 2Set (Seg (n + 2)) holds
( not (Part_sgn p2,K) . s <> (Part_sgn pq2,K) . s or i in s or j in s )
let K be Field; :: thesis: for p2, q2, pq2 being Element of Permutations (n + 2)
for i, j being Nat st pq2 = p2 * q2 & q2 is being_transposition & q2 . i = j & i < j holds
for s being Element of 2Set (Seg (n + 2)) holds
( not (Part_sgn p2,K) . s <> (Part_sgn pq2,K) . s or i in s or j in s )
set n2 = n + 2;
let p, q, pq be Element of Permutations (n + 2); :: thesis: for i, j being Nat st pq = p * q & q is being_transposition & q . i = j & i < j holds
for s being Element of 2Set (Seg (n + 2)) holds
( not (Part_sgn p,K) . s <> (Part_sgn pq,K) . s or i in s or j in s )
let i, j be Nat; :: thesis: ( pq = p * q & q is being_transposition & q . i = j & i < j implies for s being Element of 2Set (Seg (n + 2)) holds
( not (Part_sgn p,K) . s <> (Part_sgn pq,K) . s or i in s or j in s ) )
assume that
A1: pq = p * q and
A2: q is being_transposition and
A3: q . i = j and
A4: i < j ; :: thesis: for s being Element of 2Set (Seg (n + 2)) holds
( not (Part_sgn p,K) . s <> (Part_sgn pq,K) . s or i in s or j in s )
reconsider q' = q, pq' = pq as Permutation of Seg (n + 2) by MATRIX_2:def 11;
let s be Element of 2Set (Seg (n + 2)); :: thesis: ( not (Part_sgn p,K) . s <> (Part_sgn pq,K) . s or i in s or j in s )
assume A5: (Part_sgn p,K) . s <> (Part_sgn pq,K) . s ; :: thesis: ( i in s or j in s )
A6: dom q' = Seg (n + 2) by FUNCT_2:67;
A7: dom pq' = Seg (n + 2) by FUNCT_2:67;
assume that
A8: not i in s and
A9: not j in s ; :: thesis: contradiction
consider i', j' being Nat such that
A10: i' in Seg (n + 2) and
A11: j' in Seg (n + 2) and
A12: i' < j' and
A13: s = {i',j'} by Th1;
A14: j <> j' by A13, A9, TARSKI:def 2;
A15: j <> i' by A13, A9, TARSKI:def 2;
i <> j' by A13, A8, TARSKI:def 2;
then q . j' = j' by A2, A3, A4, A11, A14, A6, Th8;
then A16: pq . j' = p . j' by A1, A11, A7, FUNCT_1:22;
i <> i' by A13, A8, TARSKI:def 2;
then q . i' = i' by A2, A3, A4, A10, A15, A6, Th8;
then pq . i' = p . i' by A1, A10, A7, FUNCT_1:22;
hence contradiction by A5, A10, A11, A12, A13, A16, Th6; :: thesis: verum