REALSET1

:: Group and Field Definitions
::  by J\'ozef Bia{\l}as
::
:: Received October 27, 1989
:: Copyright (c) 1990-2017 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies FUNCT_1, ZFMISC_1, XBOOLE_0, RELAT_1, TARSKI, BINOP_1, SUBSET_1,
      MCART_1, REALSET1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
      BINOP_1, DOMAIN_1, FUNCOP_1, FUNCT_3;
 constructors BINOP_1, DOMAIN_1, FUNCT_3, FUNCOP_1, RELSET_1, SETFAM_1;
 registrations XBOOLE_0, FUNCT_1, RELSET_1, ZFMISC_1, FUNCT_2;
 requirements SUBSET;
 equalities BINOP_1;
 theorems FUNCT_1, FUNCT_2, FUNCT_3, ZFMISC_1, RELAT_1, PARTFUN1;

begin

theorem Th1:
  for X,x being set,
      F being Function of [:X,X:],X st
    x in [:X,X:] holds F.x in X
proof
  let X,x be set;
  let F be Function of [:X,X:],X;
A1: dom F = [:X,X:] by PARTFUN1:def 2;
  assume x in [:X,X:];
  then rng F c= X & F.x in rng F by A1,FUNCT_1:def 3,RELAT_1:def 19;
  hence thesis;
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:
    for x being set holds x in [:A,A:] implies F.x in A;
end;

registration
  let X be set;
  let F be BinOp of X;
  cluster F-binopclosed for Subset of X;
  existence
  proof
    X c= X;
    then reconsider Z = X as Subset of X;
    take Z;
    thus thesis by Th1;
  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
  R | [:A,A:];
  coherence;
end;

registration
  let R be Relation;
  let A be set;
  cluster R || A -> Relation-like;
  coherence;
end;

registration
  let R be Function;
  let A be set;
  cluster R || A -> Function-like;
  coherence;
end;

theorem Th2:
  for X being set, F being BinOp of X,
      A being F-binopclosed Subset of X holds
    F || A is BinOp of A
proof
  let X be set, F be BinOp of X, A be F-binopclosed Subset of X;
  dom F = [:X,X:] by PARTFUN1:def 2; then
A1: dom (F||A) = [:A,A:] by RELAT_1:62,ZFMISC_1:96;
  for x being object holds x in [:A,A:] implies F||A.x in A
  proof
    let x be object;
    assume
A2: x in [:A,A:];
    then F||A.x=F.x by A1,FUNCT_1:47;
    hence thesis by A2,Def1;
  end;
  hence thesis by A1,FUNCT_2:3;
end;

definition
  let X be set;
  let F be BinOp of X;
  let A be F-binopclosed Subset of X;
  redefine func F || A -> BinOp of A;  :: redefines || (REALSET1, definition)
  coherence by Th2;
end;

::$CT 2

theorem Th3:
  for X being set
  for A being Subset of X holds A is pr1(X,X)-binopclosed
proof
  let X be set;
  let A be Subset of X;
  set S = pr1(X,X);
  for x being set holds x in [:A,A:] implies S.x in A
  proof
    let x be set;
    assume x in [:A,A:];
    then consider p,q being object such that
A1: p in A & q in A and
A2: x = [p,q] by ZFMISC_1:def 2;
    S.x = S.(p,q) by A2;
    hence thesis by A1,FUNCT_3:def 4;
  end;
  hence thesis;
end;

definition
::$CD
  let X be set;
  let A be Subset of X;
  let F be BinOp of X;
  attr F is A-subsetpreserving means :Def4:
    for x being set holds x in [:A, A:] implies F.x in A;
end;

registration
  let X be set;
  let A be Subset of X;
  cluster A-subsetpreserving for BinOp of X;
  existence
  proof
    take F = pr1(X,X);
    A is F-binopclosed by Th3;
    hence thesis;
  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:
  for X being set,
      A being Subset of X,
      F being A-subsetpreserving BinOp of X holds
    F||A is BinOp of A
proof
  let X be set;
  let A be Subset of X;
  let F be A-subsetpreserving BinOp of X;
  dom F = [:X,X:] by PARTFUN1:def 2; then
A1: dom (F||A) = [:A,A:] by RELAT_1:62,ZFMISC_1:96;
  for x being object holds x in [:A,A:] implies F||A.x in A
  proof
    let x be object;
    assume
A2: x in [:A,A:];
    then F||A.x=F.x by A1,FUNCT_1:47;
    hence thesis by A2,Def4;
  end;
  hence thesis by A1,FUNCT_2:3;
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
  F||A;
  coherence by Th4;
end;

theorem Th5:
  for A being non trivial set
  for x being Element of A
  for F being (A \ {x})-subsetpreserving BinOp of A holds
    F||(A\{x}) is BinOp of A \ {x}
proof
  let A be non trivial set;
  let x be Element of A;
  let F be (A \ {x})-subsetpreserving BinOp of A;
  dom F = [:A,A:] by FUNCT_2:def 1; then
A1: dom(F||(A\{x})) = [:A\{x},A\{x}:] by RELAT_1:62,ZFMISC_1:96;
  for y being object holds y in [:A\{x},A\{x}:] implies F||(A\{x}).y in A\{x}
  proof
    let y be object;
    assume
A2: y in [:A\{x},A\{x}:];
    then F||(A\{x}).y=F.y by A1,FUNCT_1:47;
    hence thesis by A2,Def4;
  end;
  hence thesis by A1,FUNCT_2:3;
end;

definition
::$CD
  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
  F || (A\{x});
  coherence by Th5;
end;