let G be Group; 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 multF of G || A;
A4:
dom ( the multF of G || A) = (dom the multF of G) /\ [:A,A:]
by RELAT_1:90;
dom the multF of G = [: the carrier of G, the carrier of G:]
by FUNCT_2:def 1;
then A5:
dom ( the multF of G || A) = [:A,A:]
by A4, XBOOLE_1:28;
rng ( the multF of G || A) c= A
proof
let x be
set ;
TARSKI:def 3 ( not x in rng ( the multF of G || A) or x in A )
assume
x in rng ( the multF of G || A)
;
x in A
then consider y being
set such that A6:
y in dom ( the multF of G || A)
and A7:
( the multF of G || A) . y = x
by FUNCT_1:def 5;
consider y1,
y2 being
set 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:106;
reconsider y1 =
y1,
y2 =
y2 as
Element of
G by A4, A6, A8, ZFMISC_1:106;
x = y1 * y2
by A6, A7, A8, FUNCT_1:70;
hence
x in A
by A2, A9;
verum
end;
then reconsider o = the multF of G || A as BinOp of D by A5, FUNCT_2:def 1, RELSET_1:11;
set H = multMagma(# D,o #);
multMagma(# D,o #) is Group-like
then reconsider H = multMagma(# D,o #) as non empty Group-like multMagma ;
reconsider H = H as strict Subgroup of G by Def5;
take
H
; the carrier of H = A
thus
the carrier of H = A
; verum