let n be Nat; for IT being Element of Permutations n st IT is even & n >= 1 holds
IT " is even
let IT be Element of Permutations n; ( IT is even & n >= 1 implies IT " is even )
assume that
A1:
IT is even
and
A2:
n >= 1
; IT " is even
reconsider ITP = IT as Element of Permutations n ;
reconsider ITG = ITP as Element of (Group_of_Perm n) by MATRIX_1:def 13;
A3:
len (Permutations n) = n
by MATRIX_1:9;
then consider l being FinSequence of (Group_of_Perm n) such that
A4:
(len l) mod 2 = 0
and
A5:
IT = Product l
and
A6:
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;
set m = len l;
reconsider lv = (Rev l) " as FinSequence of (Group_of_Perm n) ;
A7:
len l = len (Rev l)
by FINSEQ_5:def 3;
then A8:
len l = len lv
by Def3;
A9:
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;
( i in dom lv implies ex q2 being Element of Permutations n st
( lv . i = q2 & q2 is being_transposition ) )
reconsider ii =
i as
Nat ;
assume A10:
i in dom lv
;
ex q2 being Element of Permutations n st
( lv . i = q2 & q2 is being_transposition )
then A11:
i in dom (Rev l)
by A7, A8, FINSEQ_3:29;
A12:
i in Seg (len lv)
by A10, FINSEQ_1:def 3;
then
1
<= i
by FINSEQ_1:1;
then
(len l) + 1
<= (len l) + i
by XREAL_1:7;
then A13:
((len l) + 1) - i <= ((len l) + i) - i
by XREAL_1:9;
i <= len l
by A8, A12, FINSEQ_1:1;
then A14:
(len l) - i >= 0
by XREAL_1:48;
then
((len l) - i) + 1
= ((len l) -' i) + 1
by XREAL_0:def 2;
then reconsider j =
((len l) - i) + 1 as
Nat ;
((len l) - i) + 1
>= 0 + 1
by A14, XREAL_1:7;
then
j in Seg (len l)
by A13;
then A15:
j in dom l
by FINSEQ_1:def 3;
then consider q being
Element of
Permutations n such that A16:
l . j = q
and A17:
q is
being_transposition
by A6;
lv . i = lv /. i
by A10, PARTFUN1:def 6;
then reconsider qq =
lv . i as
Element of
Permutations n by MATRIX_1:def 13;
reconsider qqf =
qq as
Function of
(Seg n),
(Seg n) by MATRIX_1:def 12;
A18:
i + j = (len l) + 1
;
reconsider qf =
q as
Function of
(Seg n),
(Seg n) by MATRIX_1:def 12;
consider i1,
j1 being
Nat such that A19:
(
i1 in dom q &
j1 in dom q &
i1 <> j1 &
q . i1 = j1 &
q . j1 = i1 )
and A20:
for
k being
Nat st
k <> i1 &
k <> j1 &
k in dom q holds
q . k = k
by A17;
A21:
(
dom qf = Seg n &
dom qqf = Seg n )
by A2, FUNCT_2:def 1;
A22:
qq =
((Rev l) ") /. i
by A10, PARTFUN1:def 6
.=
((Rev l) /. ii) "
by A11, Def3
.=
(l /. j) "
by A18, A15, FINSEQ_5:66
.=
q "
by A2, A15, A16, Th26, PARTFUN1:def 6
;
A23:
for
k being
Nat st
k <> j1 &
k <> i1 &
k in dom qq holds
qq . k = k
A26:
qq =
((Rev l) ") /. i
by A10, PARTFUN1:def 6
.=
((Rev l) /. ii) "
by A11, Def3
.=
(l /. j) "
by A18, A15, FINSEQ_5:66
.=
q "
by A2, A15, A16, Th26, PARTFUN1:def 6
;
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
;
hence
ex
q2 being
Element of
Permutations n st
(
lv . i = q2 &
q2 is
being_transposition )
;
verum
end;
ITG " = ITP "
by A2, Th26;
then
IT " = Product lv
by A5, Th25;
hence
IT " is even
by A3, A4, A8, A9; verum