:: by Katarzyna Zawadzka

::

:: Received October 23, 1994

:: Copyright (c) 1994-2019 Association of Mizar Users

definition

let IT be Group;

end;
attr IT 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 ) ) ) );

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 ) ) ) );

:: 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 ) ) ) ) );

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
end;

theorem Th1: :: GRSOLV_1:1

for G being 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

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

proof end;

theorem :: GRSOLV_1:2

for G being Group

for F2 being Subgroup of G

for F1 being normal Subgroup of F2

for a, b being Element of F2 holds (a * F1) * (b * F1) = (a * b) * F1

for F2 being Subgroup of G

for F1 being normal Subgroup of F2

for a, b being Element of F2 holds (a * F1) * (b * F1) = (a * b) * F1

proof end;

theorem :: GRSOLV_1:3

for G being Group

for H, F2 being Subgroup of G

for F1 being normal Subgroup of F2

for G2 being 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

for H, F2 being Subgroup of G

for F1 being normal Subgroup of F2

for G2 being 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

proof end;

theorem Th4: :: GRSOLV_1:4

for G being Group

for H, F2 being Subgroup of G

for F1 being normal Subgroup of F2

for G2 being 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

for H, F2 being Subgroup of G

for F1 being normal Subgroup of F2

for G2 being 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

proof end;

theorem :: GRSOLV_1:6

for G being 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

( 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

proof end;

definition

let G, H be Group;

let g be Homomorphism of G,H;

let A be Subgroup of G;

coherence

g | the carrier of A is Homomorphism of A,H

end;
let g be Homomorphism of G,H;

let A be Subgroup of G;

coherence

g | the carrier of A is Homomorphism of A,H

proof 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;

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 Group;

let g be Homomorphism of G,H;

let A be Subgroup of G;

coherence

Image (g | A) is strict Subgroup of H ;

end;
let g be Homomorphism of G,H;

let A be Subgroup of G;

coherence

Image (g | A) is strict Subgroup of H ;

:: deftheorem defines .: GRSOLV_1:def 3 :

for G, H being Group

for g being Homomorphism of G,H

for A being Subgroup of G holds g .: A = Image (g | A);

for G, H being 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 Group

for g being Homomorphism of G,H

for A being Subgroup of G holds the carrier of (g .: A) = g .: the carrier of A

for g being Homomorphism of G,H

for A being Subgroup of G holds the carrier of (g .: A) = g .: the carrier of A

proof end;

theorem Th9: :: GRSOLV_1:9

for G, H being 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

for h being Homomorphism of G,H

for A being strict Subgroup of G holds Image (h | A) is strict Subgroup of Image h

proof end;

theorem :: GRSOLV_1:10

theorem Th11: :: GRSOLV_1:11

for G, H being Group

for h being Homomorphism of G,H holds

( h .: ((1). G) = (1). H & h .: ((Omega). G) = (Omega). (Image h) )

for h being Homomorphism of G,H holds

( h .: ((1). G) = (1). H & h .: ((Omega). G) = (Omega). (Image h) )

proof end;

theorem Th12: :: GRSOLV_1:12

for G, H being Group

for h being Homomorphism of G,H

for A, B being Subgroup of G st A is Subgroup of B holds

h .: A is Subgroup of h .: B

for h being Homomorphism of G,H

for A, B being Subgroup of G st A is Subgroup of B holds

h .: A is Subgroup of h .: B

proof end;

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) )

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) )

proof end;

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)

for h being Homomorphism of G,H

for A, B being Subset of G holds (h .: A) * (h .: B) = h .: (A * B)

proof end;

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

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

proof end;

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

for h being Homomorphism of G,H st G is solvable Group holds

Image h is solvable

proof end;