:: Solvable Groups
:: by Katarzyna Zawadzka
::
:: Received October 23, 1994
:: Copyright (c) 1994-2012 Association of Mizar Users


begin

definition
let IT be Group;
attrIT is solvable  means :Def1: :: GRSOLV_1:def 1
 ex F being FinSequence of Subgroups IT st
( len F > 0 & F . 1 = (Omega). IT & F . (len F) = (1). IT & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds
for G1, G2 being strict Subgroup of IT st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) ) ) );
end;

:: deftheorem Def1 defines solvable GRSOLV_1:def_1_:_
 for IT being Group holds
( IT is solvable iff ex F being FinSequence of Subgroups IT st
( len F > 0 & F . 1 = (Omega). IT & F . (len F) = (1). IT & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds
for G1, G2 being strict Subgroup of IT st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) ) ) ) );

registration
cluster non empty strict Group-like associative solvable for multMagma ;
existence
 ex b1 being Group st
( b1 is solvable & b1 is strict )
proofend;
end;

theorem Th1: :: GRSOLV_1:1
for G being strict Group
for H, F1, F2 being strict Subgroup of G st F1 is normal Subgroup of F2 holds
F1 /\ H is normal Subgroup of F2 /\ H
proofend;

theorem :: GRSOLV_1:2
for G being strict Group
for F2 being strict Subgroup of G
for F1 being strict normal Subgroup of F2
for a, b being Element of F2 holds (a * F1) * (b * F1) = (a * b) * F1
proofend;

theorem :: GRSOLV_1:3
for G being strict Group
for H, F2 being strict Subgroup of G
for F1 being strict normal Subgroup of F2
for G2 being strict Subgroup of G st G2 = H /\ F2 holds
for G1 being normal Subgroup of G2 st G1 = H /\ F1 holds
ex G3 being Subgroup of F2 ./. F1 st G2 ./. G1,G3 are_isomorphic
proofend;

theorem Th4: :: GRSOLV_1:4
for G being strict Group
for H, F2 being strict Subgroup of G
for F1 being strict normal Subgroup of F2
for G2 being strict Subgroup of G st G2 = F2 /\ H holds
for G1 being normal Subgroup of G2 st G1 = F1 /\ H holds
ex G3 being Subgroup of F2 ./. F1 st G2 ./. G1,G3 are_isomorphic
proofend;

theorem :: GRSOLV_1:5
for G being strict solvable Group
for H being strict Subgroup of G holds H is solvable
proofend;

theorem :: GRSOLV_1:6
for G being strict Group st ex F being FinSequence of Subgroups G st
( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds
for G1, G2 being strict Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is cyclic Group ) ) ) ) holds
G is solvable
proofend;

theorem :: GRSOLV_1:7
for G being strict commutative Group holds G is solvable
proofend;

definition
let G, H be Group;
let g be Homomorphism of G,H;
let A be Subgroup of G;
funcg | A ->  Homomorphism of A,H equals :: GRSOLV_1:def 2
g | the carrier of A;
coherence
 g | the carrier of A is Homomorphism of A,H
proofend;
end;

:: deftheorem  defines | GRSOLV_1:def_2_:_
 for G, H being Group
for g being Homomorphism of G,H
for A being Subgroup of G holds g | A = g | the carrier of A;

definition
let G, H be strict Group;
let g be Homomorphism of G,H;
let A be Subgroup of G;
funcg .: A ->  strict Subgroup of H equals :: GRSOLV_1:def 3
 Image (g | A);
coherence
 Image (g | A) is strict Subgroup of H ;
end;

:: deftheorem  defines .: GRSOLV_1:def_3_:_
 for G, H being strict Group
for g being Homomorphism of G,H
for A being Subgroup of G holds g .: A = Image (g | A);

theorem Th8: :: GRSOLV_1:8
for G, H being strict Group
for g being Homomorphism of G,H
for A being strict Subgroup of G holds the carrier of (g .: A) = g .: the carrier of A
proofend;

theorem Th9: :: GRSOLV_1:9
for G, H being strict Group
for h being Homomorphism of G,H
for A being strict Subgroup of G holds Image (h | A) is strict Subgroup of Image h
proofend;

theorem :: GRSOLV_1:10
for G, H being strict Group
for h being Homomorphism of G,H
for A being strict Subgroup of G holds h .: A is strict Subgroup of Image h by Th9;

theorem Th11: :: GRSOLV_1:11
for G, H being strict Group
for h being Homomorphism of G,H holds
( h .: ((1). G) = (1). H & h .: ((Omega). G) = (Omega). (Image h) )
proofend;

theorem Th12: :: GRSOLV_1:12
for G, H being strict Group
for h being Homomorphism of G,H
for A, B being strict Subgroup of G st A is Subgroup of B holds
h .: A is Subgroup of h .: B
proofend;

theorem Th13: :: GRSOLV_1:13
for G, H being strict Group
for h being Homomorphism of G,H
for A being strict Subgroup of G
for a being Element of G holds
( (h . a) * (h .: A) = h .: (a * A) & (h .: A) * (h . a) = h .: (A * a) )
proofend;

theorem Th14: :: GRSOLV_1:14
for G, H being strict Group
for h being Homomorphism of G,H
for A, B being Subset of G holds (h .: A) * (h .: B) = h .: (A * B)
proofend;

theorem Th15: :: GRSOLV_1:15
for G, H being strict Group
for h being Homomorphism of G,H
for A, B being strict Subgroup of G st A is strict normal Subgroup of B holds
h .: A is strict normal Subgroup of h .: B
proofend;

theorem :: GRSOLV_1:16
for G, H being strict Group
for h being Homomorphism of G,H st G is solvable Group holds
Image h is solvable
proofend;