Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### Binary Operations Applied to Functions

by
Andrzej Trybulec

MML identifier: FUNCOP_1
[ Mizar article, MML identifier index ]

```environ

vocabulary RELAT_1, BOOLE, FUNCT_1, FUNCT_3, PARTFUN1, BINOP_1, MCART_1,
FUNCOP_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, RELSET_1, RELAT_1,
FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_3, BINOP_1;
constructors MCART_1, FUNCT_3, BINOP_1, PARTFUN1, RELAT_2, XBOOLE_0;
clusters FUNCT_1, RELSET_1, SUBSET_1, XBOOLE_0, ZFMISC_1, PARTFUN1, FUNCT_2;
requirements SUBSET, BOOLE;

begin

:::::::::::::::::::::::::::::::::::::::::::::::::::
:: A u x i l i a r y   t h e o r e m s
:::::::::::::::::::::::::::::::::::::::::::::::::::

theorem :: FUNCOP_1:1
for R being Relation, A,B being set st A <> {} & B <> {} & R = [:A,B:]
holds dom R = A & rng R = B;

reserve f,g,h for Function,
A for set;

theorem :: FUNCOP_1:2
delta A = <:id A, id A:>;

theorem :: FUNCOP_1:3
dom f = dom g implies dom(f*h) = dom (g*h);

theorem :: FUNCOP_1:4
dom f = {} & dom g = {} implies f = g;

:::::::::::::::::::::::::::::::::::::::::::::::::::
:: M a i n   p a r t
:::::::::::::::::::::::::::::::::::::::::::::::::::

reserve F for Function,
B,x,y,y1,y2,z for set;

definition let f;
func f~ -> Function means
:: FUNCOP_1:def 1
dom it = dom f &
for x st x in dom f holds
(for y,z st f.x = [y,z] holds it.x = [z,y])
& (f.x = it.x or ex y,z st f.x =[y,z]);
end;

canceled;

theorem :: FUNCOP_1:6
<:f,g:> = <:g,f:>~;

theorem :: FUNCOP_1:7
(f|A)~ = f~|A;

theorem :: FUNCOP_1:8
f~~ = f;

theorem :: FUNCOP_1:9
(delta A)~ = delta A;

theorem :: FUNCOP_1:10
<:f,g:>|A = <:f|A,g:>;

theorem :: FUNCOP_1:11
<:f,g:>|A = <:f,g|A:>;

definition let A, z be set;
func A --> z -> set equals
:: FUNCOP_1:def 2
[:A, {z}:];
end;

definition let A, z be set;
cluster A --> z -> Function-like Relation-like;
end;

canceled;

theorem :: FUNCOP_1:13
x in A implies (A --> z).x = z;

theorem :: FUNCOP_1:14
A <> {} implies rng (A --> x) = {x};

theorem :: FUNCOP_1:15
rng f = {x} implies f = (dom f) --> x;

theorem :: FUNCOP_1:16
dom ({} --> x) = {} & rng ({} --> x) = {};

theorem :: FUNCOP_1:17
(for z st z in dom f holds f.z = x) implies f = dom f --> x;

theorem :: FUNCOP_1:18
(A --> x)|B = A /\ B --> x;

theorem :: FUNCOP_1:19
dom (A --> x) = A & rng (A --> x) c= {x};

theorem :: FUNCOP_1:20
x in B implies (A --> x)"B = A;

theorem :: FUNCOP_1:21
(A --> x)"{x} = A;

theorem :: FUNCOP_1:22
not x in B implies (A --> x)"B = {};

theorem :: FUNCOP_1:23
x in dom h implies h*(A --> x) = A --> h.x;

theorem :: FUNCOP_1:24
A <> {} & x in dom h implies dom(h*(A --> x)) <> {};

theorem :: FUNCOP_1:25
(A --> x)*h = h"A --> x;

theorem :: FUNCOP_1:26
(A --> [x,y])~ = A --> [y,x];

definition
let F,f,g;
func F.:(f,g) -> set equals
:: FUNCOP_1:def 3
F * <:f,g:>;
end;

definition
let F,f,g;
cluster F.:(f,g) -> Function-like Relation-like;
end;

theorem :: FUNCOP_1:27
for h st dom h = dom(F.:(f,g)) &
for z being set st z in dom (F.:(f,g)) holds h.z = F.(f.z,g.z)
holds h = F.:(f,g);

theorem :: FUNCOP_1:28
x in dom (F.:(f,g)) implies (F.:(f,g)).x = F.(f.x,g.x);

theorem :: FUNCOP_1:29
f|A = g|A implies (F.:(f,h))|A = (F.:(g,h))|A;

theorem :: FUNCOP_1:30
f|A = g|A implies (F.:(h,f))|A = (F.:(h,g))|A;

theorem :: FUNCOP_1:31
F.:(f,g)*h = F.:(f*h, g*h);

theorem :: FUNCOP_1:32
h*F.:(f,g) = (h*F).:(f,g);

definition
let F,f,x;
func F[:](f,x) -> set equals
:: FUNCOP_1:def 4
F * <:f, dom f --> x:>;
end;

definition
let F,f,x;
cluster F[:](f,x) -> Function-like Relation-like;
end;

canceled;

theorem :: FUNCOP_1:34
F[:](f,x) = F.:(f, dom f --> x);

theorem :: FUNCOP_1:35
x in dom (F[:](f,z)) implies (F[:](f,z)).x = F.(f.x,z);

theorem :: FUNCOP_1:36
f|A = g|A implies (F[:](f,x))|A = (F[:](g,x))|A;

theorem :: FUNCOP_1:37
F[:](f,x)*h = F[:](f*h,x);

theorem :: FUNCOP_1:38
h*F[:](f,x) = (h*F)[:](f,x);

theorem :: FUNCOP_1:39
F[:](f,x)*id A = F[:](f|A,x);

definition
let F,x,g;
func F[;](x,g) -> set equals
:: FUNCOP_1:def 5
F * <:dom g --> x, g:>;
end;

definition
let F,x,g;
cluster F[;](x,g) -> Function-like Relation-like;
end;

canceled;

theorem :: FUNCOP_1:41
F[;](x,g) = F.:(dom g --> x, g);

theorem :: FUNCOP_1:42
x in dom (F[;](z,f)) implies (F[;](z,f)).x = F.(z,f.x);

theorem :: FUNCOP_1:43
f|A = g|A implies (F[;](x,f))|A = (F[;](x,g))|A;

theorem :: FUNCOP_1:44
F[;](x,f)*h = F[;](x,f*h);

theorem :: FUNCOP_1:45
h*F[;](x,f) = (h*F)[;](x,f);

theorem :: FUNCOP_1:46
F[;](x,f)*id A = F[;](x,f|A);

reserve X,Y for non empty set,
F for BinOp of X,
f,g,h for Function of Y,X,
x,x1,x2 for Element of X;

theorem :: FUNCOP_1:47
F.:(f,g) is Function of Y,X;

definition let X,Z be non empty set;
let F be BinOp of X, f,g be Function of Z,X;
redefine func F.:(f,g) -> Function of Z,X;
end;

theorem :: FUNCOP_1:48
for z being Element of Y holds (F.:(f,g)).z = F.(f.z,g.z);

theorem :: FUNCOP_1:49
for h being Function of Y,X holds
(for z being Element of Y holds h.z = F.(f.z,g.z)) implies h = F.:(f,g);

canceled;

theorem :: FUNCOP_1:51
for g being Function of X,X holds F.:(id X, g)*f = F.:(f,g*f);

theorem :: FUNCOP_1:52
for g being Function of X,X holds F.:(g, id X)*f = F.:(g*f,f);

theorem :: FUNCOP_1:53
F.:(id X, id X)*f = F.:(f,f);

theorem :: FUNCOP_1:54
for g being Function of X,X holds F.:(id X, g).x = F.(x,g.x);

theorem :: FUNCOP_1:55
for g being Function of X,X holds F.:(g, id X).x = F.(g.x,x);

theorem :: FUNCOP_1:56
F.:(id X, id X).x = F.(x,x);

theorem :: FUNCOP_1:57
for A,B for x being set st x in B holds A --> x is Function of A, B;

theorem :: FUNCOP_1:58
for A,X,x holds A --> x is Function of A, X;

theorem :: FUNCOP_1:59
F[:](f,x) is Function of Y,X;

definition let X,Z be non empty set;
let F be BinOp of X, f be Function of Z,X, x be Element of X;
redefine func F[:](f,x) -> Function of Z,X;
end;

theorem :: FUNCOP_1:60
for y being Element of Y holds (F[:](f,x)).y = F.(f.y,x);

theorem :: FUNCOP_1:61
(for y being Element of Y holds g.y = F.(f.y,x)) implies g = F[:](f,x);

canceled;

theorem :: FUNCOP_1:63
F[:](id X, x)*f = F[:](f,x);

theorem :: FUNCOP_1:64
F[:](id X, x).x = F.(x,x);

theorem :: FUNCOP_1:65
F[;](x,g) is Function of Y,X;

definition let X,Z be non empty set;
let F be BinOp of X, x be Element of X; let g be Function of Z,X;
redefine func F[;](x,g) -> Function of Z,X;
end;

theorem :: FUNCOP_1:66
for y being Element of Y holds (F[;](x,f)).y = F.(x,f.y);

theorem :: FUNCOP_1:67
(for y being Element of Y holds g.y = F.(x,f.y)) implies g = F[;](x,f);

canceled;

theorem :: FUNCOP_1:69
F[;](x, id X)*f = F[;](x,f);

theorem :: FUNCOP_1:70
F[;](x, id X).x = F.(x,x);

theorem :: FUNCOP_1:71
for X,Y,Z being non empty set
for f being Function of X, [:Y,Z:]
for x being Element of X holds f~.x =[(f.x)`2,(f.x)`1];

theorem :: FUNCOP_1:72
for X,Y,Z being non empty set
for f being Function of X, [:Y,Z:]
holds rng f is Relation of Y,Z;

definition let X,Y,Z be non empty set;
let f be Function of X, [:Y,Z:];
redefine func rng f -> Relation of Y,Z;
end;

definition let X,Y,Z be non empty set;
let f be Function of X, [:Y,Z:];
redefine func f~ -> Function of X, [:Z,Y:];
end;

theorem :: FUNCOP_1:73
for X,Y,Z being non empty set
for f being Function of X, [:Y,Z:]
holds rng (f~) = (rng f)~;

reserve y for Element of Y;

theorem :: FUNCOP_1:74
F is associative implies F[:](F[;](x1,f),x2) = F[;](x1,F[:](f,x2));

theorem :: FUNCOP_1:75
F is associative implies F.:(F[:](f,x),g) = F.:(f,F[;](x,g));

theorem :: FUNCOP_1:76
F is associative implies F.:(F.:(f,g),h) = F.:(f,F.:(g,h));

theorem :: FUNCOP_1:77
F is associative implies F[;](F.(x1,x2),f) = F[;](x1,F[;](x2,f));

theorem :: FUNCOP_1:78
F is associative implies F[:](f, F.(x1,x2)) = F[:](F[:](f,x1),x2);

theorem :: FUNCOP_1:79
F is commutative implies F[;](x,f) = F[:](f,x);

theorem :: FUNCOP_1:80
F is commutative implies F.:(f,g) = F.:(g,f);

theorem :: FUNCOP_1:81
F is idempotent implies F.:(f,f) = f;

theorem :: FUNCOP_1:82
F is idempotent implies F[;](f.y,f).y = f.y;

theorem :: FUNCOP_1:83
F is idempotent implies F[:](f,f.y).y = f.y;