defpred S1[ Nat] means for f being FinSequence of (Group_of_Perm 2) st len f = 2 * $1 & ( for i being Nat st i in dom f holds
ex q being Element of Permutations 2 st
( f . i = q & q is being_transposition ) ) holds
Product f = <*1,2*>;
let l be FinSequence of (Group_of_Perm 2); :: thesis: ( (len l) mod 2 = 0 & ( for i being Nat st i in dom l holds
ex q being Element of Permutations 2 st
( l . i = q & q is being_transposition ) ) implies Product l = <*1,2*> )
assume that
A1: (len l) mod 2 = 0 and
A2: for i being Nat st i in dom l holds
ex q being Element of Permutations 2 st
( l . i = q & q is being_transposition ) ; :: thesis: Product l = <*1,2*>
( ex t being Nat st
( len l = (2 * t) + 0 & 0 < 2 ) or ( 0 = 0 & 2 = 0 ) ) by A1, NAT_D:def 2;
then consider t being Nat such that
A3: len l = 2 * t ;
A4: for s being Nat st S1[s] holds
S1[s + 1]
proof
let s be Nat; :: thesis: ( S1[s] implies S1[s + 1] )
assume A5: S1[s] ; :: thesis: S1[s + 1]
for f being FinSequence of (Group_of_Perm 2) st len f = 2 * (s + 1) & ( for i being Nat st i in dom f holds
ex q being Element of Permutations 2 st
( f . i = q & q is being_transposition ) ) holds
Product f = <*1,2*>
proof
let f be FinSequence of (Group_of_Perm 2); :: thesis: ( len f = 2 * (s + 1) & ( for i being Nat st i in dom f holds
ex q being Element of Permutations 2 st
( f . i = q & q is being_transposition ) ) implies Product f = <*1,2*> )
assume that
A6: len f = 2 * (s + 1) and
A7: for i being Nat st i in dom f holds
ex q being Element of Permutations 2 st
( f . i = q & q is being_transposition ) ; :: thesis: Product f = <*1,2*>
A8: len f = (2 * s) + 2 by A6;
then A9: 2 <= len f by NAT_1:11;
then A10: (len f) -' 1 = (len f) - 1 by XREAL_1:233, XXREAL_0:2;
A11: ((len f) - ((len f) -' 1)) + 1 = ((len f) - ((len f) - 1)) + 1 by A9, XREAL_1:233, XXREAL_0:2
.= 2 ;
set g = mid (f,((len f) -' 1),(len f));
A12: (len f) -' 1 <= len f by NAT_D:35;
A13: 1 <= len f by A9, XXREAL_0:2;
then len f in Seg (len f) ;
then len f in dom f by FINSEQ_1:def 3;
then A14: ex q being Element of Permutations 2 st
( f . (len f) = q & q is being_transposition ) by A7;
reconsider pw2 = Product (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) as Element of (Group_of_Perm 2) ;
reconsider pw1 = Product ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) as Element of (Group_of_Perm 2) ;
A15: (1 + ((len f) -' 1)) -' 1 = (1 + ((len f) -' 1)) - 1 by NAT_1:11, XREAL_1:233
.= (len f) -' 1 ;
A16: (1 + 1) - 1 <= (len f) - 1 by A9, XREAL_1:13;
then A17: 1 <= (len f) -' 1 by A9, XREAL_1:233, XXREAL_0:2;
then A18: len (mid (f,((len f) -' 1),(len f))) = ((len f) -' ((len f) -' 1)) + 1 by A13, A12, FINSEQ_6:118
.= ((len f) - ((len f) -' 1)) + 1 by NAT_D:35, XREAL_1:233
.= ((len f) - ((len f) - 1)) + 1 by A9, XREAL_1:233, XXREAL_0:2
.= 2 ;
then (len (mid (f,((len f) -' 1),(len f)))) -' 1 = (len (mid (f,((len f) -' 1),(len f)))) - 1 by XREAL_1:233;
then A19: ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) . 1 = (mid (f,((len f) -' 1),(len f))) . 1 by A18, FINSEQ_3:112
.= f . ((len f) -' 1) by A16, A12, A11, A15, FINSEQ_6:122 ;
A20: for i being Nat st i in dom (f | ((len f) -' 2)) holds
ex q being Element of Permutations 2 st
( (f | ((len f) -' 2)) . i = q & q is being_transposition )
proof
let i be Nat; :: thesis: ( i in dom (f | ((len f) -' 2)) implies ex q being Element of Permutations 2 st
( (f | ((len f) -' 2)) . i = q & q is being_transposition ) )
assume i in dom (f | ((len f) -' 2)) ; :: thesis: ex q being Element of Permutations 2 st
( (f | ((len f) -' 2)) . i = q & q is being_transposition )
then A21: i in Seg (len (f | ((len f) -' 2))) by FINSEQ_1:def 3;
then A22: 1 <= i by FINSEQ_1:1;
A23: i <= len (f | ((len f) -' 2)) by A21, FINSEQ_1:1;
len (f | ((len f) -' 2)) <= len f by FINSEQ_5:16;
then i <= len f by A23, XXREAL_0:2;
then i in dom f by A22, FINSEQ_3:25;
then A24: ex q being Element of Permutations 2 st
( f . i = q & q is being_transposition ) by A7;
len (f | ((len f) -' 2)) = (len f) -' 2 by FINSEQ_1:59, NAT_D:35;
hence ex q being Element of Permutations 2 st
( (f | ((len f) -' 2)) . i = q & q is being_transposition ) by A23, A24, FINSEQ_3:112; :: thesis: verum
end;
len (f | ((len f) -' 2)) = (len f) -' 2 by FINSEQ_1:59, NAT_D:35
.= 2 * s by A8, NAT_D:34 ;
then Product (f | ((len f) -' 2)) = <*1,2*> by A5, A20;
then A25: 1_ (Group_of_Perm 2) = Product (f | ((len f) -' 2)) by FINSEQ_2:52, MATRIX_1:15;
f = (f | ((len f) -' 2)) ^ (mid (f,((len f) -' 1),(len f))) by A8, Th6, NAT_1:11;
then A26: Product f = (Product (f | ((len f) -' 2))) * (Product (mid (f,((len f) -' 1),(len f)))) by GROUP_4:5
.= Product (mid (f,((len f) -' 1),(len f))) by A25, GROUP_1:def 4 ;
2 <= 2 + ((len f) -' 1) by NAT_1:11;
then A27: (2 + ((len f) -' 1)) -' 1 = (2 + ((len f) -' 1)) - 1 by XREAL_1:233, XXREAL_0:2
.= len f by A10 ;
A28: ((len f) - ((len f) -' 1)) + 1 = ((len f) - ((len f) - 1)) + 1 by A9, XREAL_1:233, XXREAL_0:2
.= 1 + 1 ;
A29: (1 + (len (mid (f,((len f) -' 1),(len f))))) -' 1 = (1 + (len (mid (f,((len f) -' 1),(len f))))) - 1 by NAT_1:11, XREAL_1:233;
A30: len ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) = (len (mid (f,((len f) -' 1),(len f)))) -' 1 by FINSEQ_1:59, NAT_D:35
.= (len (mid (f,((len f) -' 1),(len f)))) - 1 by A18, XREAL_1:233
.= 1 by A18 ;
then 1 in Seg (len ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1))) ;
then 1 in dom ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) by FINSEQ_1:def 3;
then ( rng ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) c= the carrier of (Group_of_Perm 2) & ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) . 1 in rng ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) ) by FINSEQ_1:def 4, FUNCT_1:def 3;
then reconsider r = ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) . 1 as Element of (Group_of_Perm 2) ;
A31: pw1 = Product <*r*> by A30, FINSEQ_1:40
.= f . ((len f) -' 1) by A19, FINSOP_1:11 ;
1 <= ((len (mid (f,((len f) -' 1),(len f)))) - (len (mid (f,((len f) -' 1),(len f))))) + 1 ;
then A32: (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) . 1 = (mid (f,((len f) -' 1),(len f))) . ((1 + (len (mid (f,((len f) -' 1),(len f))))) -' 1) by A18, FINSEQ_6:122
.= f . (len f) by A16, A12, A18, A28, A29, A27, FINSEQ_6:122 ;
A33: len (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) = ((len (mid (f,((len f) -' 1),(len f)))) -' (len (mid (f,((len f) -' 1),(len f))))) + 1 by A18, FINSEQ_6:118
.= 0 + 1 by XREAL_1:232
.= 1 ;
then 1 in Seg (len (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f))))))) ;
then 1 in dom (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) by FINSEQ_1:def 3;
then ( rng (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) c= the carrier of (Group_of_Perm 2) & (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) . 1 in rng (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) ) by FINSEQ_1:def 4, FUNCT_1:def 3;
then reconsider s = (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) . 1 as Element of (Group_of_Perm 2) ;
A34: pw2 = Product <*s*> by A33, FINSEQ_1:40
.= f . (len f) by A32, FINSOP_1:11 ;
(len f) -' 1 in Seg (len f) by A17, A12;
then (len f) -' 1 in dom f by FINSEQ_1:def 3;
then A35: ex q being Element of Permutations 2 st
( f . ((len f) -' 1) = q & q is being_transposition ) by A7;
mid (f,((len f) -' 1),(len f)) = ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) ^ (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) by A18, Th7;
then Product (mid (f,((len f) -' 1),(len f))) = (Product ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1))) * (Product (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f))))))) by GROUP_4:5
.= <*1,2*> by A35, A14, A31, A34, Th10 ;
hence Product f = <*1,2*> by A26; :: thesis: verum
end;
hence S1[s + 1] ; :: thesis: verum
end;
for f being FinSequence of (Group_of_Perm 2) st len f = 2 * 0 & ( for i being Nat st i in dom f holds
ex q being Element of Permutations 2 st
( f . i = q & q is being_transposition ) ) holds
Product f = <*1,2*>
proof
set G = Group_of_Perm 2;
let f be FinSequence of (Group_of_Perm 2); :: thesis: ( len f = 2 * 0 & ( for i being Nat st i in dom f holds
ex q being Element of Permutations 2 st
( f . i = q & q is being_transposition ) ) implies Product f = <*1,2*> )
assume that
A36: len f = 2 * 0 and
for i being Nat st i in dom f holds
ex q being Element of Permutations 2 st
( f . i = q & q is being_transposition ) ; :: thesis: Product f = <*1,2*>
A37: 1_ (Group_of_Perm 2) = <*1,2*> by FINSEQ_2:52, MATRIX_1:15;
f = <*> the carrier of (Group_of_Perm 2) by A36;
hence Product f = <*1,2*> by A37, GROUP_4:8; :: thesis: verum
end;
then A38: S1[ 0 ] ;
A39: for s being Nat holds S1[s] from NAT_1:sch 2(A38, A4);
 reconsider t = t as Nat ;
len l = 2 * t by A3;
hence Product l = <*1,2*> by A2, A39; :: thesis: verum