:: The Sylow Theorems
:: by Marco Riccardi
::
:: Received August 13, 2007
:: Copyright (c) 2007-2018 Association of Mizar Users


notation
let S be non empty 1-sorted ;
let E be set ;
let A be Action of the carrier of S,E;
let s be Element of S;
synonym A ^ s for S . E;
end;

definition
let S be non empty 1-sorted ;
let E be set ;
let A be Action of the carrier of S,E;
let s be Element of S;
:: original: ^
redefine func A ^ s -> Function of E,E;
correctness
coherence
^ is Function of E,E
;
proof end;
end;

definition
let S be non empty unital multMagma ;
let E be set ;
let A be Action of the carrier of S,E;
attr A is being_left_operation means :Def1: :: GROUP_10:def 1
( A ^ (1_ S) = id E & ( for s1, s2 being Element of S holds A ^ (s1 * s2) = (A ^ s1) * (A ^ s2) ) );
end;

:: deftheorem Def1 defines being_left_operation GROUP_10:def 1 :
for S being non empty unital multMagma
for E being set
for A being Action of the carrier of S,E holds
( A is being_left_operation iff ( A ^ (1_ S) = id E & ( for s1, s2 being Element of S holds A ^ (s1 * s2) = (A ^ s1) * (A ^ s2) ) ) );

registration
let S be non empty unital multMagma ;
let E be set ;
cluster Relation-like the carrier of S -defined Funcs (E,E) -valued non empty Function-like total quasi_total being_left_operation for Action of ,;
correctness
existence
ex b1 being Action of the carrier of S,E st b1 is being_left_operation
;
proof end;
end;

:: ALG I.5.1 DEF 1
definition
let S be non empty unital multMagma ;
let E be set ;
mode LeftOperation of S,E is being_left_operation Action of the carrier of S,E;
end;

scheme :: GROUP_10:sch 1
ExLeftOperation{ F1() -> set , F2() -> non empty Group-like multMagma , F3( Element of F2()) -> Function of F1(),F1() } :
ex T being LeftOperation of F2(),F1() st
for s being Element of F2() holds T . s = F3(s)
provided
A1: F3((1_ F2())) = id F1() and
A2: for s1, s2 being Element of F2() holds F3((s1