let G be strict Group; :: thesis: the carrier of (Phi G) = { a where a is Element of G : not a is generating }
set A = { a where a is Element of G : not a is generating } ;
thus
the carrier of (Phi G) c= { a where a is Element of G : not a is generating }
:: according to XBOOLE_0:def 10 :: thesis: { a where a is Element of G : not a is generating } c= the carrier of (Phi G)proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (Phi G) or x in { a where a is Element of G : not a is generating } )
assume A1:
x in the
carrier of
(Phi G)
;
:: thesis: x in { a where a is Element of G : not a is generating }
assume A2:
not
x in { a where a is Element of G : not a is generating }
;
:: thesis: contradiction
x in Phi G
by A1, STRUCT_0:def 5;
then
x in G
by GROUP_2:49;
then reconsider a =
x as
Element of
G by STRUCT_0:def 5;
a is
generating
by A2;
then consider B being
Subset of
G such that A3:
gr B = G
and A4:
gr (B \ {a}) <> G
by Def6;
set M =
B \ {a};
defpred S1[
Subgroup of
G]
means (
B \ {a} c= carr $1 & not
a in $1 );
consider X being
set such that A5:
X c= Subgroups G
and A6:
for
H being
strict Subgroup of
G holds
(
H in X iff
S1[
H] )
from GROUP_4:sch 2();
A7:
B \ {a} c= carr (gr (B \ {a}))
by Def5;
then reconsider X =
X as non
empty set by A6, A7;
defpred S2[
set ,
set ]
means ex
H1,
H2 being
strict Subgroup of
G st
( $1
= H1 & $2
= H2 &
H1 is
Subgroup of
H2 );
A17:
for
x being
Element of
X holds
S2[
x,
x]
A18:
for
x,
y being
Element of
X st
S2[
x,
y] &
S2[
y,
x] holds
x = y
by GROUP_2:64;
A19:
for
x,
y,
z being
Element of
X st
S2[
x,
y] &
S2[
y,
z] holds
S2[
x,
z]
proof
let x,
y,
z be
Element of
X;
:: thesis: ( S2[x,y] & S2[y,z] implies S2[x,z] )
given H1,
H2 being
strict Subgroup of
G such that A20:
(
x = H1 &
y = H2 &
H1 is
Subgroup of
H2 )
;
:: thesis: ( not S2[y,z] or S2[x,z] )
given H3,
H4 being
strict Subgroup of
G such that A21:
(
y = H3 &
z = H4 &
H3 is
Subgroup of
H4 )
;
:: thesis: S2[x,z]
H1 is
Subgroup of
H4
by A20, A21, GROUP_2:65;
hence
S2[
x,
z]
by A20, A21;
:: thesis: verum
end;
A22:
for
Y being
set st
Y c= X & ( for
x,
y being
Element of
X st
x in Y &
y in Y & not
S2[
x,
y] holds
S2[
y,
x] ) holds
ex
y being
Element of
X st
for
x being
Element of
X st
x in Y holds
S2[
x,
y]
proof
let Y be
set ;
:: thesis: ( Y c= X & ( for x, y being Element of X st x in Y & y in Y & not S2[x,y] holds
S2[y,x] ) implies ex y being Element of X st
for x being Element of X st x in Y holds
S2[x,y] )
assume A23:
Y c= X
;
:: thesis: ( ex x, y being Element of X st
( x in Y & y in Y & not S2[x,y] & not S2[y,x] ) or ex y being Element of X st
for x being Element of X st x in Y holds
S2[x,y] )
assume A24:
for
x,
y being
Element of
X st
x in Y &
y in Y & not
S2[
x,
y] holds
S2[
y,
x]
;
:: thesis: ex y being Element of X st
for x being Element of X st x in Y holds
S2[x,y]
set C =
{ D where D is Subset of G : ex H being strict Subgroup of G st
( H in Y & D = carr H ) } ;
then reconsider E =
union { D where D is Subset of G : ex H being strict Subgroup of G st
( H in Y & D = carr H ) } as
Subset of
G by ZFMISC_1:94;
now per cases
( Y = {} or Y <> {} )
;
suppose A26:
Y <> {}
;
:: thesis: ex y being Element of X st
for x being Element of X st x in Y holds
ex K, H being strict Subgroup of G st
( x = K & y = H & K is Subgroup of H )consider s being
Element of
Y;
A27:
s in X
by A23, A26, TARSKI:def 3;
then reconsider s =
s as
strict Subgroup of
G by A5, GROUP_3:def 1;
A28:
carr s in { D where D is Subset of G : ex H being strict Subgroup of G st
( H in Y & D = carr H ) }
by A26;
then
(
carr s c= E &
B \ {a} c= carr s )
by A6, A27, ZFMISC_1:92;
then A29:
B \ {a} c= E
by XBOOLE_1:1;
A30:
E <> {}
by A28, ORDERS_1:91;
then consider H being
strict Subgroup of
G such that A49:
the
carrier of
H = E
by A30, A31, GROUP_2:61;
the
carrier of
H = carr H
;
then reconsider y =
H as
Element of
X by A6, A29, A49, A50;
take y =
y;
:: thesis: for x being Element of X st x in Y holds
ex K, H being strict Subgroup of G st
( x = K & y = H & K is Subgroup of H )let x be
Element of
X;
:: thesis: ( x in Y implies ex K, H being strict Subgroup of G st
( x = K & y = H & K is Subgroup of H ) )assume A56:
x in Y
;
:: thesis: ex K, H being strict Subgroup of G st
( x = K & y = H & K is Subgroup of H )
x in Subgroups G
by A5, TARSKI:def 3;
then reconsider K =
x as
strict Subgroup of
G by GROUP_3:def 1;
take K =
K;
:: thesis: ex H being strict Subgroup of G st
( x = K & y = H & K is Subgroup of H )take H =
H;
:: thesis: ( x = K & y = H & K is Subgroup of H )thus
(
x = K &
y = H )
;
:: thesis: K is Subgroup of H
carr K = the
carrier of
K
;
then
the
carrier of
K in { D where D is Subset of G : ex H being strict Subgroup of G st
( H in Y & D = carr H ) }
by A56;
hence
K is
Subgroup of
H
by A49, GROUP_2:66, ZFMISC_1:92;
:: thesis: verum end;
hence
ex
y being
Element of
X st
for
x being
Element of
X st
x in Y holds
S2[
x,
y]
;
:: thesis: verum
end;
consider s being
Element of
X such that A57:
for
y being
Element of
X st
s <> y holds
not
S2[
s,
y]
from ORDERS_1:sch 1(A17, A18, A19, A22);
reconsider H =
s as
strict Subgroup of
G by A16;
H is
maximal
proof
not
a in H
by A6;
hence
multMagma(# the
carrier of
H,the
multF of
H #)
<> multMagma(# the
carrier of
G,the
multF of
G #)
by STRUCT_0:def 5;
:: according to GROUP_4:def 7 :: thesis: for K being strict Subgroup of G st multMagma(# the carrier of H,the multF of H #) <> K & H is Subgroup of K holds
K = multMagma(# the carrier of G,the multF of G #)
let K be
strict Subgroup of
G;
:: thesis: ( multMagma(# the carrier of H,the multF of H #) <> K & H is Subgroup of K implies K = multMagma(# the carrier of G,the multF of G #) )
assume that A58:
K <> multMagma(# the
carrier of
H,the
multF of
H #)
and A59:
H is
Subgroup of
K
and A60:
K <> multMagma(# the
carrier of
G,the
multF of
G #)
;
:: thesis: contradiction
( the
carrier of
H = carr H & the
carrier of
K = carr K & the
carrier of
H c= the
carrier of
K &
B \ {a} c= carr H )
by A6, A59, GROUP_2:def 5;
then A61:
B \ {a} c= carr K
by XBOOLE_1:1;
then reconsider v =
K as
Element of
X by A6, A61;
not
S2[
s,
v]
by A57, A58;
hence
contradiction
by A59;
:: thesis: verum
end;
then
Phi G is
Subgroup of
H
by Th54;
then
the
carrier of
(Phi G) c= the
carrier of
H
by GROUP_2:def 5;
then
(
x in H & not
a in H )
by A1, A6, STRUCT_0:def 5;
hence
contradiction
;
:: thesis: verum
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { a where a is Element of G : not a is generating } or x in the carrier of (Phi G) )
assume
x in { a where a is Element of G : not a is generating }
; :: thesis: x in the carrier of (Phi G)
then consider a being Element of G such that
A64:
x = a
and
A65:
not a is generating
;
hence
x in the carrier of (Phi G)
; :: thesis: verum