let n be Nat; :: thesis: for K being commutative Ring
for tr being Element of Permutations (n + 2) st tr is being_transposition holds
sgn (tr,K) = - (1_ K)
let K be commutative Ring; :: thesis: for tr being Element of Permutations (n + 2) st tr is being_transposition holds
sgn (tr,K) = - (1_ K)
set n2 = n + 2;
set S = Seg (n + 2);
let tr be Element of Permutations (n + 2); :: thesis: ( tr is being_transposition implies sgn (tr,K) = - (1_ K) )
assume A1: tr is being_transposition ; :: thesis: sgn (tr,K) = - (1_ K)
reconsider Tr = tr as Permutation of (Seg (n + 2)) by MATRIX_1:def 12;
reconsider Id = idseq (n + 2), IdTr = (id (Seg (n + 2))) * Tr as Element of Permutations (n + 2) by MATRIX_1:def 12;
rng Tr = Seg (n + 2) by FUNCT_2:def 3;
then IdTr = Tr by RELAT_1:54;
then sgn (tr,K) = - (sgn (Id,K)) by A1, Th13;
hence sgn (tr,K) = - (1_ K) by Th12; :: thesis: verum