let G be Group; :: thesis: for a being Element of G
for A being Subset of G holds
( a in gr A iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= A & Product (F |^ I) = a ) )
let a be Element of G; :: thesis: for A being Subset of G holds
( a in gr A iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= A & Product (F |^ I) = a ) )
let A be Subset of G; :: thesis: ( a in gr A iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= A & Product (F |^ I) = a ) )
thus ( a in gr A implies ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= A & Product (F |^ I) = a ) ) :: thesis: ( ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= A & Product (F |^ I) = a ) implies a in gr A )
proof
defpred S1[ set ] means ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( $1 = Product (F |^ I) & len F = len I & rng F c= A );
assume A1: a in gr A ; :: thesis: ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= A & Product (F |^ I) = a )
reconsider B = { b where b is Element of G : S1[b] } as Subset of G from DOMAIN_1:sch 7();
A2: now :: thesis: for c, d being Element of G st c in B & d in B holds
c * d in B
let c, d be Element of G; :: thesis: ( c in B & d in B implies c * d in B )
assume that
A3: c in B and
A4: d in B ; :: thesis: c * d in B
ex d1 being Element of G st
( c = d1 & ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( d1 = Product (F |^ I) & len F = len I & rng F c= A ) ) by A3;
then consider F1 being FinSequence of the carrier of G, I1 being FinSequence of INT such that
A5: c = Product (F1 |^ I1) and
A6: len F1 = len I1 and
A7: rng F1 c= A ;
ex d2 being Element of G st
( d = d2 & ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( d2 = Product (F |^ I) & len F = len I & rng F c= A ) ) by A4;
then consider F2 being FinSequence of the carrier of G, I2 being FinSequence of INT such that
A8: d = Product (F2 |^ I2) and
A9: len F2 = len I2 and
A10: rng F2 c= A ;
A11: len (F1 ^ F2) = (len I1) + (len I2) by A6, A9, FINSEQ_1:22
.= len (I1 ^ I2) by FINSEQ_1:22 ;
rng (F1 ^ F2) = (rng F1) \/ (rng F2) by FINSEQ_1:31;
then A12: rng (F1 ^ F2) c= A by A7, A10, XBOOLE_1:8;
c * d = Product ((F1 |^ I1) ^ (F2 |^ I2)) by A5, A8, FINSOP_1:5
.= Product ((F1 ^ F2) |^ (I1 ^ I2)) by A6, A9, Th19 ;
hence c * d in B by A12, A11; :: thesis: verum
end;
A13: now :: thesis: for c being Element of G st c in B holds
c " in B
let c be Element of G; :: thesis: ( c in B implies c " in B )
assume c in B ; :: thesis: c " in B
then ex d1 being Element of G st
( c = d1 & ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( d1 = Product (F |^ I) & len F = len I & rng F c= A ) ) ;
then consider F1 being FinSequence of the carrier of G, I1 being FinSequence of INT such that
A14: c = Product (F1 |^ I1) and
A15: len F1 = len I1 and
A16: rng F1 c= A ;
deffunc H1( Nat) -> set = F1 . (((len F1) - $1) + 1);
consider F2 being FinSequence such that
A17: len F2 = len F1 and
A18: for k being Nat st k in dom F2 holds
F2 . k = H1(k) from FINSEQ_1:sch 2();
A19: Seg (len I1) = dom I1 by FINSEQ_1:def 3;
A20: rng F2 c= rng F1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F2 or x in rng F1 )
assume x in rng F2 ; :: thesis: x in rng F1
then consider y being object such that
A21: y in dom F2 and
A22: F2 . y = x by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A21;
reconsider n = ((len F1) - y) + 1 as Element of NAT by A17, A21, Lm3;
( 1 <= n & n <= len F1 ) by A17, A21, Lm3;
then A23: n in dom F1 by FINSEQ_3:25;
x = F1 . (((len F1) - y) + 1) by A18, A21, A22;
hence x in rng F1 by A23, FUNCT_1:def 3; :: thesis: verum
end;
then A24: rng F2 c= A by A16;
defpred S2[ Nat, object ] means ex i being Integer st
( i = I1 . (((len I1) - $1) + 1) & $2 = - i );
A25: for k being Nat st k in Seg (len I1) holds
ex x being object st S2[k,x]
proof
let k be Nat; :: thesis: ( k in Seg (len I1) implies ex x being object st S2[k,x] )
assume k in Seg (len I1) ; :: thesis: ex x being object st S2[k,x]
then A26: k in dom I1 by FINSEQ_1:def 3;
then reconsider n = ((len I1) - k) + 1 as Element of NAT by Lm3;
( 1 <= n & n <= len I1 ) by A26, Lm3;
then n in dom I1 by FINSEQ_3:25;
then A27: I1 . n in rng I1 by FUNCT_1:def 3;
rng I1 c= INT by FINSEQ_1:def 4;
then reconsider i = I1 . n as Element of INT by A27;
take - i ; :: thesis: S2[k, - i]
take i ; :: thesis: ( i = I1 . (((len I1) - k) + 1) & - i = - i )
thus ( i = I1 . (((len I1) - k) + 1) & - i = - i ) ; :: thesis: verum
end;
consider I2 being FinSequence such that
A28: dom I2 = Seg (len I1) and
A29: for k being Nat st k in Seg (len I1) holds
S2[k,I2 . k] from FINSEQ_1:sch 1(A25);
A30: len F2 = len I2 by A15, A17, A28, FINSEQ_1:def 3;
A31: rng I2 c= INT
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng I2 or x in INT )
assume x in rng I2 ; :: thesis: x in INT
then consider y being object such that
A32: y in dom I2 and
A33: x = I2 . y by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A32;
ex i being Integer st
( i = I1 . (((len I1) - y) + 1) & x = - i ) by A28, A29, A32, A33;
hence x in INT by INT_1:def 2; :: thesis: verum
end;
rng F1 c= the carrier of G by FINSEQ_1:def 4;
then A34: rng F2 c= the carrier of G by A20;
set p = F1 |^ I1;
A35: Seg (len F1) = dom F1 by FINSEQ_1:def 3;
A36: len (F1 |^ I1) = len F1 by Def3;
A37: dom F2 = dom I2 by A15, A17, A28, FINSEQ_1:def 3;
reconsider I2 = I2 as FinSequence of INT by A31, FINSEQ_1:def 4;
reconsider F2 = F2 as FinSequence of the carrier of G by A34, FINSEQ_1:def 4;
set q = F2 |^ I2;
A38: len (F2 |^ I2) = len F2 by Def3;
then A39: dom (F2 |^ I2) = dom F2 by FINSEQ_3:29;
A40: dom F1 = dom I1 by A15, FINSEQ_3:29;
now :: thesis: for k being Nat st k in dom (F2 |^ I2) holds
((F2 |^ I2) /. k) " = (F1 |^ I1) . (((len (F1 |^ I1)) - k) + 1)
let k be Nat; :: thesis: ( k in dom (F2 |^ I2) implies ((F2 |^ I2) /. k) " = (F1 |^ I1) . (((len (F1 |^ I1)) - k) + 1) )
A41: I2 /. k = @ (I2 /. k) ;
assume A42: k in dom (F2 |^ I2) ; :: thesis: ((F2 |^ I2) /. k) " = (F1 |^ I1) . (((len (F1 |^ I1)) - k) + 1)
then reconsider n = ((len (F1 |^ I1)) - k) + 1 as Element of NAT by A17, A36, A38, Lm3;
A43: ( I1 /. n = @ (I1 /. n) & (F2 |^ I2) /. k = (F2 |^ I2) . k ) by A42, PARTFUN1:def 6;
dom (F2 |^ I2) = dom I1 by A15, A17, A38, FINSEQ_3:29;
then consider i being Integer such that
A44: i = I1 . n and
A45: I2 . k = - i by A15, A29, A19, A36, A42;
I2 . k = I2 /. k by A37, A39, A42, PARTFUN1:def 6;
then A46: (F2 |^ I2) . k = (F2 /. k) |^ (- i) by A39, A42, A45, A41, Def3;
A47: ( F2 /. k = F2 . k & F2 . k = F1 . n ) by A18, A36, A39, A42, PARTFUN1:def 6;
( 1 <= n & len (F1 |^ I1) >= n ) by A17, A36, A38, A42, Lm3;
then A48: n in dom I2 by A17, A30, A36, FINSEQ_3:25;
then A49: I1 . n = I1 /. n by A28, A19, PARTFUN1:def 6;
F1 /. n = F1 . n by A15, A35, A28, A48, PARTFUN1:def 6;
then (F2 |^ I2) . k = ((F1 /. n) |^ i) " by A46, A47, GROUP_1:36;
hence ((F2 |^ I2) /. k) " = (F1 |^ I1) . (((len (F1 |^ I1)) - k) + 1) by A40, A28, A19, A48, A44, A49, A43, Def3; :: thesis: verum
end;
then (Product (F1 |^ I1)) " = Product (F2 |^ I2) by A17, A36, A38, Th14;
hence c " in B by A14, A30, A24; :: thesis: verum
end;
A50: len {} = 0 ;
A51: ( rng (<*> the carrier of G) = {} & {} c= A ) ;
( 1_ G = Product (<*> the carrier of G) & (<*> the carrier of G) |^ (<*> INT) = {} ) by Th8, Th21;
then 1_ G in B by A51, A50;
then consider H being strict Subgroup of G such that
A52: the carrier of H = B by A2, A13, GROUP_2:52;
A c= B
proof
reconsider p = 1 as Integer ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in B )
assume A53: x in A ; :: thesis: x in B
then reconsider a = x as Element of G ;
A54: ( rng <*a*> = {a} & {a} c= A ) by A53, FINSEQ_1:39, ZFMISC_1:31;
A55: ( len <*a*> = 1 & len <*(@ p)*> = 1 ) by FINSEQ_1:39;
Product (<*a*> |^ <*(@ p)*>) = Product <*(a |^ 1)*> by Th22
.= a |^ 1 by FINSOP_1:11
.= a by GROUP_1:26 ;
hence x in B by A55, A54; :: thesis: verum
end;
then gr A is Subgroup of H by A52, Def4;
then a in H by A1, GROUP_2:40;
then a in B by A52, STRUCT_0:def 5;
then ex b being Element of G st
( b = a & ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( b = Product (F |^ I) & len F = len I & rng F c= A ) ) ;
hence ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= A & Product (F |^ I) = a ) ; :: thesis: verum
end;
given F being FinSequence of the carrier of G, I being FinSequence of INT such that len F = len I and
A56: rng F c= A and
A57: Product (F |^ I) = a ; :: thesis: a in gr A
A c= the carrier of (gr A) by Def4;
then rng F c= carr (gr A) by A56;
hence a in gr A by A57, Th20; :: thesis: verum