:: Group and Field Definitions :: by J\'ozef Bia{\l}as :: :: Received October 27, 1989 :: Copyright (c) 1990-2018 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, BOOLE; equalities BINOP_1; theorems FUNCT_1, FUNCT_2, FUNCT_3, ZFMISC_1, RELAT_1, PARTFUN1; begin theorem Th1: for X,x being set holds for F being Function of [:X,X:],X holds x in [:X,X:] implies 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; mode Preserv of F -> Subset of X means :Def1: for x being set holds x in [: it,it:] implies F.x in it; existence proof X c= X; then reconsider Z = X as Subset of X; take Z; thus thesis by Th1; end; 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 Preserv of F holds F ||A is BinOp of A proof let X be set, F be BinOp of X, A be Preserv of F; 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 Preserv of F; redefine func F||A -> BinOp of A; coherence by Th2; end; definition let X be non trivial set; let F be BinOp of X; let x be Element of X; pred F is_Bin_Op_Preserv x means X\{x} is Preserv of F & F||X\{x} is BinOp of X\{x}; correctness; end; ::\$CT 2 theorem Th3: for X being set holds for A being Subset of X holds ex F being BinOp of X st for x being set holds x in [:A,A:] implies F.x in A proof let X be set; let A be Subset of X; set S = pr1(X,X); take S; 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 let X be set; let A be Subset of X; mode Presv of X,A -> BinOp of X means :Def4: for x being set holds x in [:A, A:] implies it.x in A; existence by Th3; end; theorem Th4: for X being set, A being Subset of X, F being Presv of X,A holds F||A is BinOp of A proof let X be set; let A be Subset of X; let F be Presv of X,A; 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 Presv of X,A; func F|||A -> BinOp of A equals F||A; coherence by Th4; end; definition let A be set; let x be Element of A; mode DnT of x,A -> BinOp of A means :Def6: for y being set holds y in [:A\{x },A\{x}:] implies it.y in A\{x}; existence by Th3; end; theorem Th5: for A being non trivial set holds for x being Element of A holds for F being DnT of x,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 DnT of x,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,Def6; end; hence thesis by A1,FUNCT_2:3; end; definition let A be non trivial set; let x be Element of A; let F be DnT of x,A; func F!(A,x) -> BinOp of A\{x} equals F||(A\{x}); coherence by Th5; end;