The abstract of the Mizar article:

Binary Operations Applied to Functions

by

Andrzej Trybulec

Received September 4, 1989

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;

:: Addendum, 2002.07.08

theorem :: FUNCOP_1:84
   for F,f,g being Function st [:rng f, rng g:] c= dom F
  holds dom(F.:(f,g)) = dom f /\ dom g;