let n be Nat; for p2, q2, pq2 being Element of Permutations (n + 2)
for i, j being Nat
for K being commutative Ring st pq2 = p2 * q2 & q2 is being_transposition & q2 . i = j & i < j & 1_ K <> - (1_ K) holds
( (Part_sgn (p2,K)) . {i,j} <> (Part_sgn (pq2,K)) . {i,j} & ( for k being Nat st k in Seg (n + 2) & i <> k & j <> k holds
( (Part_sgn (p2,K)) . {i,k} <> (Part_sgn (pq2,K)) . {i,k} iff (Part_sgn (p2,K)) . {j,k} <> (Part_sgn (pq2,K)) . {j,k} ) ) )
set n2 = n + 2;
let p, q, pq be Element of Permutations (n + 2); for i, j being Nat
for K being commutative Ring st pq = p * q & q is being_transposition & q . i = j & i < j & 1_ K <> - (1_ K) holds
( (Part_sgn (p,K)) . {i,j} <> (Part_sgn (pq,K)) . {i,j} & ( for k being Nat st k in Seg (n + 2) & i <> k & j <> k holds
( (Part_sgn (p,K)) . {i,k} <> (Part_sgn (pq,K)) . {i,k} iff (Part_sgn (p,K)) . {j,k} <> (Part_sgn (pq,K)) . {j,k} ) ) )
let i, j be Nat; for K being commutative Ring st pq = p * q & q is being_transposition & q . i = j & i < j & 1_ K <> - (1_ K) holds
( (Part_sgn (p,K)) . {i,j} <> (Part_sgn (pq,K)) . {i,j} & ( for k being Nat st k in Seg (n + 2) & i <> k & j <> k holds
( (Part_sgn (p,K)) . {i,k} <> (Part_sgn (pq,K)) . {i,k} iff (Part_sgn (p,K)) . {j,k} <> (Part_sgn (pq,K)) . {j,k} ) ) )
let K be commutative Ring; ( pq = p * q & q is being_transposition & q . i = j & i < j & 1_ K <> - (1_ K) implies ( (Part_sgn (p,K)) . {i,j} <> (Part_sgn (pq,K)) . {i,j} & ( for k being Nat st k in Seg (n + 2) & i <> k & j <> k holds
( (Part_sgn (p,K)) . {i,k} <> (Part_sgn (pq,K)) . {i,k} iff (Part_sgn (p,K)) . {j,k} <> (Part_sgn (pq,K)) . {j,k} ) ) ) )
assume that
A1:
pq = p * q
and
A2:
q is being_transposition
and
A3:
q . i = j
and
A4:
i < j
and
A5:
1_ K <> - (1_ K)
; ( (Part_sgn (p,K)) . {i,j} <> (Part_sgn (pq,K)) . {i,j} & ( for k being Nat st k in Seg (n + 2) & i <> k & j <> k holds
( (Part_sgn (p,K)) . {i,k} <> (Part_sgn (pq,K)) . {i,k} iff (Part_sgn (p,K)) . {j,k} <> (Part_sgn (pq,K)) . {j,k} ) ) )
A6:
i in dom q
by A2, A3, A4, Th8;
set P2 = Part_sgn (pq,K);
set P1 = Part_sgn (p,K);
reconsider p9 = p, q9 = q, pq9 = pq as Permutation of (Seg (n + 2)) by MATRIX_1:def 12;
A7:
dom q9 = Seg (n + 2)
by FUNCT_2:52;
A8:
j in dom q
by A2, A3, A4, Th8;
A9:
dom pq9 = Seg (n + 2)
by FUNCT_2:52;
then A10:
pq . i = p . j
by A1, A3, A6, A7, FUNCT_1:12;
q . j = i
by A2, A3, A4, Th8;
then A11:
pq . j = p . i
by A1, A8, A9, A7, FUNCT_1:12;
dom p9 = Seg (n + 2)
by FUNCT_2:52;
then A12:
p9 . i <> p9 . j
by A4, A6, A8, A7, FUNCT_1:def 4;
now (Part_sgn (p,K)) . {i,j} <> (Part_sgn (pq,K)) . {i,j}per cases
( p . i < p . j or p . i > p . j )
by A12, XXREAL_0:1;
suppose A13:
p . i < p . j
;
(Part_sgn (p,K)) . {i,j} <> (Part_sgn (pq,K)) . {i,j}then
(Part_sgn (p,K)) . {i,j} = 1_ K
by A4, A6, A8, A7, Def1;
hence
(Part_sgn (p,K)) . {i,j} <> (Part_sgn (pq,K)) . {i,j}
by A4, A5, A6, A8, A7, A10, A11, A13, Def1;
verum end; suppose A14:
p . i > p . j
;
(Part_sgn (p,K)) . {i,j} <> (Part_sgn (pq,K)) . {i,j}then
(Part_sgn (p,K)) . {i,j} = - (1_ K)
by A4, A6, A8, A7, Def1;
hence
(Part_sgn (p,K)) . {i,j} <> (Part_sgn (pq,K)) . {i,j}
by A4, A5, A6, A8, A7, A10, A11, A14, Def1;
verum end;
hence
(Part_sgn (p,K)) . {i,j} <> (Part_sgn (pq,K)) . {i,j}
; for k being Nat st k in Seg (n + 2) & i <> k & j <> k holds
( (Part_sgn (p,K)) . {i,k} <> (Part_sgn (pq,K)) . {i,k} iff (Part_sgn (p,K)) . {j,k} <> (Part_sgn (pq,K)) . {j,k} )
let k be Nat; ( k in Seg (n + 2) & i <> k & j <> k implies ( (Part_sgn (p,K)) . {i,k} <> (Part_sgn (pq,K)) . {i,k} iff (Part_sgn (p,K)) . {j,k} <> (Part_sgn (pq,K)) . {j,k} ) )
assume that
A15:
k in Seg (n + 2)
and
A16:
i <> k
and
A17:
j <> k
; ( (Part_sgn (p,K)) . {i,k} <> (Part_sgn (pq,K)) . {i,k} iff (Part_sgn (p,K)) . {j,k} <> (Part_sgn (pq,K)) . {j,k} )
A18:
q . k = k
by A2, A3, A4, A7, A15, A16, A17, Th8;
A19:
pq . k = p . (q . k)
by A1, A9, A15, FUNCT_1:12;
( i < k or k < i )
by A16, XXREAL_0:1;
then A20:
{i,k} in 2Set (Seg (n + 2))
by A6, A7, A15, Th1;
A21:
( (Part_sgn (p,K)) . {i,k} = (Part_sgn (pq,K)) . {i,k} implies (Part_sgn (p,K)) . {j,k} = (Part_sgn (pq,K)) . {j,k} )
proof
A22:
(
j < k or
k < j )
by A17, XXREAL_0:1;
A23:
(
i < k or
i > k )
by A16, XXREAL_0:1;
assume A24:
(Part_sgn (p,K)) . {i,k} = (Part_sgn (pq,K)) . {i,k}
;
(Part_sgn (p,K)) . {j,k} = (Part_sgn (pq,K)) . {j,k}
(
(Part_sgn (p,K)) . {k,i} = 1_ K or
(Part_sgn (p,K)) . {k,i} = - (1_ K) )
by A20, Th5;
then
( (
pq . j < pq . k &
p . j < p . k ) or (
pq . j > pq . k &
p . j > p . k ) )
by A5, A6, A7, A10, A11, A15, A18, A19, A24, A23, Lm1;
then
( (
(Part_sgn (pq,K)) . {j,k} = 1_ K &
(Part_sgn (p,K)) . {j,k} = 1_ K ) or (
(Part_sgn (pq,K)) . {j,k} = - (1_ K) &
(Part_sgn (p,K)) . {j,k} = - (1_ K) ) )
by A8, A7, A15, A22, Def1;
hence
(Part_sgn (p,K)) . {j,k} = (Part_sgn (pq,K)) . {j,k}
;
verum
end;
( j < k or k < j )
by A17, XXREAL_0:1;
then A25:
{j,k} in 2Set (Seg (n + 2))
by A8, A7, A15, Th1;
( (Part_sgn (p,K)) . {j,k} = (Part_sgn (pq,K)) . {j,k} implies (Part_sgn (p,K)) . {i,k} = (Part_sgn (pq,K)) . {i,k} )
proof
A26:
(
i < k or
k < i )
by A16, XXREAL_0:1;
A27:
(
j < k or
j > k )
by A17, XXREAL_0:1;
assume A28:
(Part_sgn (p,K)) . {j,k} = (Part_sgn (pq,K)) . {j,k}
;
(Part_sgn (p,K)) . {i,k} = (Part_sgn (pq,K)) . {i,k}
(
(Part_sgn (p,K)) . {k,j} = 1_ K or
(Part_sgn (p,K)) . {k,j} = - (1_ K) )
by A25, Th5;
then
( (
pq . i < pq . k &
p . i < p . k ) or (
pq . i > pq . k &
p . i > p . k ) )
by A5, A8, A7, A10, A11, A15, A18, A19, A28, A27, Lm1;
then
( (
(Part_sgn (pq,K)) . {i,k} = 1_ K &
(Part_sgn (p,K)) . {i,k} = 1_ K ) or (
(Part_sgn (pq,K)) . {i,k} = - (1_ K) &
(Part_sgn (p,K)) . {i,k} = - (1_ K) ) )
by A6, A7, A15, A26, Def1;
hence
(Part_sgn (p,K)) . {i,k} = (Part_sgn (pq,K)) . {i,k}
;
verum
end;
hence
( (Part_sgn (p,K)) . {i,k} <> (Part_sgn (pq,K)) . {i,k} iff (Part_sgn (p,K)) . {j,k} <> (Part_sgn (pq,K)) . {j,k} )
by A21; verum