let G be addGroup; for A being Subset of G st A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 + g2 in A ) & ( for g being Element of G st g in A holds
- g in A ) holds
ex H being strict Subgroup of G st the carrier of H = A
let A be Subset of G; ( A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 + g2 in A ) & ( for g being Element of G st g in A holds
- g in A ) implies ex H being strict Subgroup of G st the carrier of H = A )
assume that
A1:
A <> {}
and
A2:
for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 + g2 in A
and
A3:
for g being Element of G st g in A holds
- g in A
; ex H being strict Subgroup of G st the carrier of H = A
reconsider D = A as non empty set by A1;
set o = the addF of G || A;
A4:
dom ( the addF of G || A) = (dom the addF of G) /\ [:A,A:]
by RELAT_1:61;
dom the addF of G = [: the carrier of G, the carrier of G:]
by FUNCT_2:def 1;
then A5:
dom ( the addF of G || A) = [:A,A:]
by A4, XBOOLE_1:28;
rng ( the addF of G || A) c= A
proof
let x be
object ;
TARSKI:def 3 ( not x in rng ( the addF of G || A) or x in A )
assume
x in rng ( the addF of G || A)
;
x in A
then consider y being
object such that A6:
y in dom ( the addF of G || A)
and A7:
( the addF of G || A) . y = x
by FUNCT_1:def 3;
consider y1,
y2 being
object such that A8:
[y1,y2] = y
by A4, A6, RELAT_1:def 1;
A9:
(
y1 in A &
y2 in A )
by A5, A6, A8, ZFMISC_1:87;
reconsider y1 =
y1,
y2 =
y2 as
Element of
G by A4, A6, A8, ZFMISC_1:87;
x = y1 + y2
by A6, A7, A8, FUNCT_1:47;
hence
x in A
by A2, A9;
verum
end;
then reconsider o = the addF of G || A as BinOp of D by A5, FUNCT_2:def 1, RELSET_1:4;
set H = addMagma(# D,o #);
addMagma(# D,o #) is addGroup-like
proof
set a = the
Element of
addMagma(#
D,
o #);
reconsider x = the
Element of
addMagma(#
D,
o #) as
Element of
G by Lm1;
- x in A
by A3;
then
x + (- x) in A
by A2;
then reconsider t =
0_ G as
Element of
addMagma(#
D,
o #)
by Def5;
take
t
;
GROUP_1A:def 2 for h being Element of addMagma(# D,o #) holds
( h + t = h & t + h = h & ex g being Element of addMagma(# D,o #) st
( h + g = t & g + h = t ) )
let a be
Element of
addMagma(#
D,
o #);
( a + t = a & t + a = a & ex g being Element of addMagma(# D,o #) st
( a + g = t & g + a = t ) )
reconsider x =
a as
Element of
G by Lm1;
thus a + t =
x + (0_ G)
by A10
.=
a
by Def4
;
( t + a = a & ex g being Element of addMagma(# D,o #) st
( a + g = t & g + a = t ) )
thus t + a =
(0_ G) + x
by A10
.=
a
by Def4
;
ex g being Element of addMagma(# D,o #) st
( a + g = t & g + a = t )
reconsider s =
- x as
Element of
addMagma(#
D,
o #)
by A3;
take
s
;
( a + s = t & s + a = t )
thus a + s =
x + (- x)
by A10
.=
t
by Def5
;
s + a = t
thus s + a =
(- x) + x
by A10
.=
t
by Def5
;
verum
end;
then reconsider H = addMagma(# D,o #) as non empty addGroup-like addMagma ;
reconsider H = H as strict Subgroup of G by DefA5;
take
H
; the carrier of H = A
thus
the carrier of H = A
; verum