let n be Element of NAT ; :: thesis: for IT being Element of Permutations n st IT is even & n >= 1 holds
IT " is even
let IT be Element of Permutations n; :: thesis: ( IT is even & n >= 1 implies IT " is even )
assume A1:
( IT is even & n >= 1 )
; :: thesis: IT " is even
A2:
len (Permutations n) = n
by MATRIX_2:20;
then consider l being FinSequence of (Group_of_Perm n) such that
A3:
( (len l) mod 2 = 0 & IT = Product l & ( for i being Nat st i in dom l holds
ex q being Element of Permutations n st
( l . i = q & q is being_transposition ) ) )
by A1, MATRIX_2:def 15;
reconsider lv = (Rev l) " as FinSequence of (Group_of_Perm n) ;
A4:
len l = len (Rev l)
by FINSEQ_5:def 3;
then A5:
len l = len lv
by Def4;
set m = len l;
reconsider ITP = IT as Element of Permutations n ;
reconsider ITG = ITP as Element of (Group_of_Perm n) by MATRIX_2:def 13;
ITG " = ITP "
by A1, Th27;
then A6:
IT " = Product lv
by A3, Th26;
for i being Nat st i in dom lv holds
ex q2 being Element of Permutations n st
( lv . i = q2 & q2 is being_transposition )
proof
let i be
Nat;
:: thesis: ( i in dom lv implies ex q2 being Element of Permutations n st
( lv . i = q2 & q2 is being_transposition ) )
assume A7:
i in dom lv
;
:: thesis: ex q2 being Element of Permutations n st
( lv . i = q2 & q2 is being_transposition )
then
i in Seg (len lv)
by FINSEQ_1:def 3;
then A8:
( 1
<= i &
i <= len l )
by A5, FINSEQ_1:3;
then A9:
(len l) - i >= 0
by XREAL_1:50;
then A10:
((len l) - i) + 1
>= 0 + 1
by XREAL_1:9;
(len l) + 1
<= (len l) + i
by A8, XREAL_1:9;
then A11:
((len l) + 1) - i <= ((len l) + i) - i
by XREAL_1:11;
((len l) - i) + 1
= ((len l) -' i) + 1
by A9, XREAL_0:def 2;
then reconsider j =
((len l) - i) + 1 as
Element of
NAT ;
reconsider ii =
i as
Element of
NAT by ORDINAL1:def 13;
A12:
i + j = (len l) + 1
;
j in Seg (len l)
by A10, A11;
then A13:
j in dom l
by FINSEQ_1:def 3;
then consider q being
Element of
Permutations n such that A14:
(
l . j = q &
q is
being_transposition )
by A3;
lv . i = lv /. i
by A7, PARTFUN1:def 8;
then reconsider qq =
lv . i as
Element of
Permutations n by MATRIX_2:def 13;
consider i1,
j1 being
Nat such that A15:
(
i1 in dom q &
j1 in dom q &
i1 <> j1 &
q . i1 = j1 &
q . j1 = i1 & ( for
k being
Nat st
k <> i1 &
k <> j1 &
k in dom q holds
q . k = k ) )
by A14, MATRIX_2:def 14;
reconsider qf =
q as
Function of
(Seg n),
(Seg n) by MATRIX_2:def 11;
A16:
Seg n <> {}
by A1;
then A17:
dom qf = Seg n
by FUNCT_2:def 1;
reconsider qqf =
qq as
Function of
(Seg n),
(Seg n) by MATRIX_2:def 11;
A18:
dom qqf = Seg n
by A16, FUNCT_2:def 1;
A19:
i in dom (Rev l)
by A4, A5, A7, FINSEQ_3:31;
A20:
qq =
((Rev l) " ) /. i
by A7, PARTFUN1:def 8
.=
((Rev l) /. ii) "
by A19, Def4
.=
(l /. j) "
by A12, A13, FINSEQ_5:69
.=
q "
by A1, A13, A14, Th27, PARTFUN1:def 8
;
A21:
for
k being
Element of
NAT st
k <> j1 &
k <> i1 &
k in dom qq holds
qq . k = k
A23:
qq =
((Rev l) " ) /. i
by A7, PARTFUN1:def 8
.=
((Rev l) /. ii) "
by A19, Def4
.=
(l /. j) "
by A12, A13, FINSEQ_5:69
.=
q "
by A1, A13, A14, Th27, PARTFUN1:def 8
;
ex
i,
j being
Nat st
(
i in dom qq &
j in dom qq &
i <> j &
qq . i = j &
qq . j = i & ( for
k being
Nat st
k <> i &
k <> j &
k in dom qq holds
qq . k = k ) )
then
qq is
being_transposition
by MATRIX_2:def 14;
hence
ex
q2 being
Element of
Permutations n st
(
lv . i = q2 &
q2 is
being_transposition )
;
:: thesis: verum
end;
hence
IT " is even
by A2, A3, A5, A6, MATRIX_2:def 15; :: thesis: verum