:: Group and Field Definitions
:: by J\'ozef Bia{\l}as
::
:: Received October 27, 1989
:: Copyright (c) 1990-2017 Association of Mizar Users

theorem Th1: :: REALSET1:1

for X, x being set
for F being Function of [:X,X:],X st x in [:X,X:] holds
F . x in X

proof end;

definition

let X be set ;
let F be BinOp of X;
let A be Subset of X;

attr A is F -binopclosed means :Def1: :: REALSET1:def 1
for x being set st x in [:A,A:] holds
F . x in A;

end;

:: deftheorem Def1 defines -binopclosed REALSET1:def 1 :
for X being set
for F being BinOp of X
for A being Subset of X holds
( A is F -binopclosed iff for x being set st x in [:A,A:] holds
F . x in A );

registration

let X be set ;
let F be BinOp of X;

cluster F -binopclosed for Element of bool X;

existence
ex b₁ being Subset of X st b₁ is F -binopclosed

proof end;

end;

definition

let X be set ;
let F be BinOp of X;
mode Preserv of F is F -binopclosed Subset of X;

end;

definition

let R be Relation;
let A be set ;

func R || A -> set equals :: REALSET1:def 2
R | [:A,A:];

coherence
R | [:A,A:] is set ;

end;

:: deftheorem defines || REALSET1:def 2 :
for R being Relation
for A being set holds R || A = R | [:A,A:];

registration

let R be Relation;
let A be set ;

cluster R || A -> Relation-like ;

coherence
R || A is Relation-like ;

end;

registration

let R be Function;
let A be set ;

cluster R || A -> Function-like ;

coherence
R || A is Function-like ;

end;

theorem Th2: :: REALSET1:2

for X being set
for F being BinOp of X
for A being b₂ -binopclosed Subset of X holds F || A is BinOp of A

proof end;

definition

let X be set ;
let F be BinOp of X;
let A be F -binopclosed Subset of X;
:: original: ||
redefine func F || A -> BinOp of A;
coherence
F || A is BinOp of A by Th2;

end;

theorem :: REALSET1:3

canceled;

theorem :: REALSET1:4

canceled;

::$CT 2

theorem Th3: :: REALSET1:5

for X being set
for A being Subset of X holds A is pr1 (X,X) -binopclosed

proof end;

definition

let X be set ;
let A be Subset of X;
let F be BinOp of X;

attr F is A -subsetpreserving means :Def4: :: REALSET1:def 4
for x being set st x in [:A,A:] holds
F . x in A;

end;

:: deftheorem REALSET1:def 3 :
canceled;

:: deftheorem Def4 defines -subsetpreserving REALSET1:def 4 :
for X being set
for A being Subset of X
for F being BinOp of X holds
( F is A -subsetpreserving iff for x being set st x in [:A,A:] holds
F . x in A );

registration

let X be set ;
let A be Subset of X;

cluster Relation-like [:X,X:] -defined X -valued Function-like V14([:X,X:]) V18([:X,X:],X) A -subsetpreserving for Element of bool [:[:X,X:],X:];

existence
ex b₁ being BinOp of X st b₁ is A -subsetpreserving

proof end;

end;

definition

let X be set ;
let A be Subset of X;
mode Presv of X,A is A -subsetpreserving BinOp of X;

end;

theorem Th4: :: REALSET1:6

for X being set
for A being Subset of X
for F being b₂ -subsetpreserving BinOp of X holds F || A is BinOp of A

proof end;

definition

let X be set ;
let A be Subset of X;
let F be A -subsetpreserving BinOp of X;

func F ||| A -> BinOp of A equals :: REALSET1:def 5
F || A;

coherence
F || A is BinOp of A by Th4;

end;

:: deftheorem defines ||| REALSET1:def 5 :
for X being set
for A being Subset of X
for F being b₂ -subsetpreserving BinOp of X holds F ||| A = F || A;

theorem Th5: :: REALSET1:7

for A being non trivial set
for x being Element of A
for F being b₁ \ {b₂} -subsetpreserving BinOp of A holds F || (A \ {x}) is BinOp of (A \ {x})

proof end;

definition

let A be non trivial set ;
let x be Element of A;
let F be A \ {x} -subsetpreserving BinOp of A;

func F ! (A,x) -> BinOp of (A \ {x}) equals :: REALSET1:def 7
F || (A \ {x});

coherence
F || (A \ {x}) is BinOp of (A \ {x}) by Th5;

end;

:: deftheorem REALSET1:def 6 :
canceled;

:: deftheorem defines ! REALSET1:def 7 :
for A being non trivial set
for x being Element of A
for F being b₁ \ {b₂} -subsetpreserving BinOp of A holds F ! (A,x) = F || (A \ {x});