:: GRSOLV_1 semantic presentation

definition
let c1 be Group;
attr a1 is solvable means :Def1: :: GRSOLV_1:def 1
ex b1 being FinSequence of Subgroups a1 st
( len b1 > 0 & b1 . 1 = (Omega). a1 & b1 . (len b1) = (1). a1 & ( for b2 being Nat st b2 in dom b1 & b2 + 1 in dom b1 holds
for b3, b4 being strict Subgroup of a1 st b3 = b1 . b2 & b4 = b1 . (b2 + 1) holds
( b4 is strict normal Subgroup of b3 & ( for b5 being normal Subgroup of b3 st b5 = b4 holds
b3 ./. b5 is commutative ) ) ) );
end;

:: deftheorem Def1 defines solvable GRSOLV_1:def 1 :
for b1 being Group holds
( b1 is solvable iff ex b2 being FinSequence of Subgroups b1 st
( len b2 > 0 & b2 . 1 = (Omega). b1 & b2 . (len b2) = (1). b1 & ( for b3 being Nat st b3 in dom b2 & b3 + 1 in dom b2 holds
for b4, b5 being strict Subgroup of b1 st b4 = b2 . b3 & b5 = b2 . (b3 + 1) holds
( b5 is strict normal Subgroup of b4 & ( for b6 being normal Subgroup of b4 st b6 = b5 holds
b4 ./. b6 is commutative ) ) ) ) );

registration
cluster strict solvable HGrStr ;
existence
ex b1 being Group st
( b1 is solvable & b1 is strict )
proof end;
end;

theorem Th1: :: GRSOLV_1:1
for b1 being strict Group
for b2, b3, b4 being strict Subgroup of b1 st b3 is normal Subgroup of b4 holds
b3 /\ b2 is normal Subgroup of b4 /\ b2
proof end;

theorem Th2: :: GRSOLV_1:2
for b1 being strict Group
for b2 being strict Subgroup of b1
for b3 being strict normal Subgroup of b2
for b4, b5 being Element of b2 holds (b4 * b3) * (b5 * b3) = (b4 * b5) * b3
proof end;

theorem Th3: :: GRSOLV_1:3
for b1 being strict Group
for b2, b3 being strict Subgroup of b1
for b4 being strict normal Subgroup of b3
for b5 being strict Subgroup of b1 st b5 = b2 /\ b3 holds
for b6 being normal Subgroup of b5 st b6 = b2 /\ b4 holds
ex b7 being Subgroup of b3 ./. b4 st b5 ./. b6,b7 are_isomorphic
proof end;

theorem Th4: :: GRSOLV_1:4
for b1 being strict Group
for b2, b3 being strict Subgroup of b1
for b4 being strict normal Subgroup of b3
for b5 being strict Subgroup of b1 st b5 = b3 /\ b2 holds
for b6 being normal Subgroup of b5 st b6 = b4 /\ b2 holds
ex b7 being Subgroup of b3 ./. b4 st b5 ./. b6,b7 are_isomorphic
proof end;

theorem Th5: :: GRSOLV_1:5
for b1 being strict solvable Group
for b2 being strict Subgroup of b1 holds b2 is solvable
proof end;

theorem Th6: :: GRSOLV_1:6
for b1 being strict Group st ex b2 being FinSequence of Subgroups b1 st
( len b2 > 0 & b2 . 1 = (Omega). b1 & b2 . (len b2) = (1). b1 & ( for b3 being Nat st b3 in dom b2 & b3 + 1 in dom b2 holds
for b4, b5 being strict Subgroup of b1 st b4 = b2 . b3 & b5 = b2 . (b3 + 1) holds
( b5 is strict normal Subgroup of b4 & ( for b6 being normal Subgroup of b4 st b6 = b5 holds
b4 ./. b6 is cyclic Group ) ) ) ) holds
b1 is solvable
proof end;

theorem Th7: :: GRSOLV_1:7
for b1 being strict commutative Group holds
( b1 is strict & b1 is solvable )
proof end;

definition
let c1, c2 be strict Group;
let c3 be Homomorphism of c1,c2;
let c4 be Subgroup of c1;
func c3 | c4 -> Homomorphism of a4,a2 equals :: GRSOLV_1:def 2
a3 | the carrier of a4;
coherence
c3 | the carrier of c4 is Homomorphism of c4,c2
proof end;
end;

:: deftheorem Def2 defines | GRSOLV_1:def 2 :
for b1, b2 being strict Group
for b3 being Homomorphism of b1,b2
for b4 being Subgroup of b1 holds b3 | b4 = b3 | the carrier of b4;

definition
let c1, c2 be strict Group;
let c3 be Homomorphism of c1,c2;
let c4 be Subgroup of c1;
func c3 .: c4 -> strict Subgroup of a2 equals :: GRSOLV_1:def 3
 Image (a3 | a4);
correctness
coherence
Image (c3 | c4) is strict Subgroup of c2;
;
end;

:: deftheorem Def3 defines .: GRSOLV_1:def 3 :
for b1, b2 being strict Group
for b3 being Homomorphism of b1,b2
for b4 being Subgroup of b1 holds b3 .: b4 = Image (b3 | b4);

theorem Th8: :: GRSOLV_1:8
for b1, b2 being strict Group
for b3 being Homomorphism of b1,b2
for b4 being Subgroup of b1 holds rng (b3 | b4) = b3 .: the carrier of b4 by RELAT_1:148;

theorem Th9: :: GRSOLV_1:9
for b1, b2 being strict Group
for b3 being Homomorphism of b1,b2
for b4 being strict Subgroup of b1 holds the carrier of (b3 .: b4) = b3 .: the carrier of b4
proof end;

theorem Th10: :: GRSOLV_1:10
for b1, b2 being strict Group
for b3 being Homomorphism of b1,b2
for b4 being strict Subgroup of b1 holds Image (b3 | b4) is strict Subgroup of Image b3
proof end;

theorem Th11: :: GRSOLV_1:11
for b1, b2 being strict Group
for b3 being Homomorphism of b1,b2
for b4 being strict Subgroup of b1 holds b3 .: b4 is strict Subgroup of Image b3 by Th10;

theorem Th12: :: GRSOLV_1:12
for b1, b2 being strict Group
for b3 being Homomorphism of b1,b2 holds
( b3 .: ((1). b1) = (1). b2 & b3 .: ((Omega). b1) = (Omega). (Image b3) )
proof end;

theorem Th13: :: GRSOLV_1:13
for b1, b2 being strict Group
for b3 being Homomorphism of b1,b2
for b4, b5 being strict Subgroup of b1 st b4 is Subgroup of b5 holds
b3 .: b4 is Subgroup of b3 .: b5
proof end;

theorem Th14: :: GRSOLV_1:14
for b1, b2 being strict Group
for b3 being Homomorphism of b1,b2
for b4 being strict Subgroup of b1
for b5 being Element of b1 holds
( (b3 . b5) * (b3 .: b4) = b3 .: (b5 * b4) & (b3 .: b4) * (b3 . b5) = b3 .: (b4 * b5) )
proof end;

theorem Th15: :: GRSOLV_1:15
for b1, b2 being strict Group
for b3 being Homomorphism of b1,b2
for b4, b5 being Subset of b1 holds (b3 .: b4) * (b3 .: b5) = b3 .: (b4 * b5)
proof end;

theorem Th16: :: GRSOLV_1:16
for b1, b2 being strict Group
for b3 being Homomorphism of b1,b2
for b4, b5 being strict Subgroup of b1 st b4 is strict normal Subgroup of b5 holds
b3 .: b4 is strict normal Subgroup of b3 .: b5
proof end;

theorem Th17: :: GRSOLV_1:17
for b1, b2 being strict Group
for b3 being Homomorphism of b1,b2 st b1 is solvable Group holds
Image b3 is solvable
proof end;