let G be Group; :: thesis: 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; :: thesis: ( 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
; :: thesis: 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:] & dom the multF of G = [:the carrier of G,the carrier of G:] & [:A,A:] c= [:the carrier of G,the carrier of G:] )
by FUNCT_2:def 1, RELAT_1:90;
then A5:
dom (the multF of G || A) = [:A,A:]
by XBOOLE_1:28;
rng (the multF of G || A) c= A
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in rng (the multF of G || A) or x in A )
assume
x in rng (the multF of G || A)
;
:: thesis: 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;
:: thesis: 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
; :: thesis: the carrier of H = A
thus
the carrier of H = A
; :: thesis: verum