begin
definition
let E be non
empty set ;
let n be
Nat;
let S be non
empty Group-like multMagma ;
let s be
Element of
S;
let LO be
LeftOperation of
S,
E;
assume A1:
card n c= card E
;
existence
ex b1 being Function of (the_subsets_of_card (n,E)),(the_subsets_of_card (n,E)) st
for X being Element of the_subsets_of_card (n,E) holds b1 . X = (LO ^ s) .: X
uniqueness
for b1, b2 being Function of (the_subsets_of_card (n,E)),(the_subsets_of_card (n,E)) st ( for X being Element of the_subsets_of_card (n,E) holds b1 . X = (LO ^ s) .: X ) & ( for X being Element of the_subsets_of_card (n,E) holds b2 . X = (LO ^ s) .: X ) holds
b1 = b2
end;
definition
let E be non
empty set ;
let n be
Nat;
let S be non
empty Group-like multMagma ;
let LO be
LeftOperation of
S,
E;
assume A1:
card n c= card E
;
existence
ex b1 being LeftOperation of S,(the_subsets_of_card (n,E)) st
for s being Element of S holds b1 . s = the_extension_of_left_translation_of (n,s,LO)
uniqueness
for b1, b2 being LeftOperation of S,(the_subsets_of_card (n,E)) st ( for s being Element of S holds b1 . s = the_extension_of_left_translation_of (n,s,LO) ) & ( for s being Element of S holds b2 . s = the_extension_of_left_translation_of (n,s,LO) ) holds
b1 = b2
end;
definition
let S be non
empty multMagma ;
let s be
Element of
S;
let Z be non
empty set ;
existence
ex b1 being Function of [: the carrier of S,Z:],[: the carrier of S,Z:] st
for z1 being Element of [: the carrier of S,Z:] ex z2 being Element of [: the carrier of S,Z:] ex s1, s2 being Element of S ex z being Element of Z st
( z2 = b1 . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] )
uniqueness
for b1, b2 being Function of [: the carrier of S,Z:],[: the carrier of S,Z:] st ( for z1 being Element of [: the carrier of S,Z:] ex z2 being Element of [: the carrier of S,Z:] ex s1, s2 being Element of S ex z being Element of Z st
( z2 = b1 . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) ) & ( for z1 being Element of [: the carrier of S,Z:] ex z2 being Element of [: the carrier of S,Z:] ex s1, s2 being Element of S ex z being Element of Z st
( z2 = b2 . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) ) holds
b1 = b2
end;
begin
begin
Lm1:
for n being non zero Nat holds card (INT.Group n) = n
begin
Lm2:
for n being Nat
for p being prime Nat st n <> 0 holds
ex m, r being Nat st
( n = (p |^ r) * m & not p divides m )
Lm3:
for X, Y being non empty set holds card { [:X,{y}:] where y is Element of Y : verum } = card Y
Lm4:
for G being finite Group
for E, T being non empty set
for LO being LeftOperation of G,E
for n being Nat st LO = the_left_operation_of (G,T) & n = card G & E = [: the carrier of G,T:] & card n c= card E holds
the_fixed_points_of (the_extension_of_left_operation_of (n,LO)) = { [: the carrier of G,{t}:] where t is Element of T : verum }
Lm5:
for n, m, r being Nat
for p being prime Nat st n = (p |^ r) * m & not p divides m holds
(n choose (p |^ r)) mod p <> 0
Lm6:
for r, n, m1, m2 being Nat
for p being prime Nat st (p |^ r) * n = m1 * m2 & not p divides n & not p divides m2 holds
p |^ r divides m1
Lm7:
for G being Group
for A being non empty Subset of G
for x being Element of G holds card A = card (A * x)
Lm8:
for n, r being Nat
for p being prime Nat st n divides p |^ r & n > 1 holds
p divides n
definition
let G be
finite Group;
let p be
prime Nat;
let H be
Subgroup of
G;
let h be
Element of
H;
existence
ex b1 being Function of (the_sylow_p-subgroups_of_prime (p,G)),(the_sylow_p-subgroups_of_prime (p,G)) st
for P1 being Element of the_sylow_p-subgroups_of_prime (p,G) ex P2 being Element of the_sylow_p-subgroups_of_prime (p,G) ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P2 = b1 . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g )
uniqueness
for b1, b2 being Function of (the_sylow_p-subgroups_of_prime (p,G)),(the_sylow_p-subgroups_of_prime (p,G)) st ( for P1 being Element of the_sylow_p-subgroups_of_prime (p,G) ex P2 being Element of the_sylow_p-subgroups_of_prime (p,G) ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P2 = b1 . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) ) & ( for P1 being Element of the_sylow_p-subgroups_of_prime (p,G) ex P2 being Element of the_sylow_p-subgroups_of_prime (p,G) ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P2 = b2 . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) ) holds
b1 = b2
end;
Lm9:
for G, H being finite Group
for p being prime Nat
for I being Subgroup of G
for P being Subgroup of H st I = P & I is_Sylow_p-subgroup_of_prime p & H is Subgroup of G holds
P is_Sylow_p-subgroup_of_prime p
begin