let G be Group; 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; 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; ( 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 ) )
( 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
;
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 for c, d being Element of G st c in B & d in B holds
c * d in Blet c,
d be
Element of
G;
( c in B & d in B implies c * d in B )assume that A3:
c in B
and A4:
d in B
;
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;
verum end;
A13:
now for c being Element of G st c in B holds
c " in Blet c be
Element of
G;
( c in B implies c " in B )assume
c in B
;
c " in Bthen
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
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]
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
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 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;
( 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)
;
((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;
verum end; then
(Product (F1 |^ I1)) " = Product (F2 |^ I2)
by A17, A36, A38, Th14;
hence
c " in B
by A14, A30, A24;
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
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 )
;
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
; 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; verum