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

### Group and Field Definitions

by
Jozef Bialas

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

```environ

vocabulary FUNCT_1, RELAT_1, BOOLE, BINOP_1, RLVECT_1, VECTSP_1, FUNCT_3,
QC_LANG1, REALSET1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
BINOP_1, FUNCT_3, STRUCT_0, RLVECT_1, VECTSP_1;
constructors BINOP_1, FUNCT_3, VECTSP_1, MEMBERED, XBOOLE_0;
clusters FUNCT_1, RLVECT_1, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements SUBSET, BOOLE;

begin

canceled 9;

theorem :: REALSET1:10
for X,x being set holds
for F being Function of [:X,X:],X holds
x in [:X,X:] implies F.x in X;

theorem :: REALSET1:11
for X being set,
F being BinOp of X
ex A being Subset of X st
for x being set holds x in [:A,A:] implies F.x in A;

definition
let X be set;
let F be BinOp of X;
let A be Subset of X;
pred F is_in A means
:: REALSET1:def 1
for x being set holds x in [:A,A:] implies F.x in A;
end;

definition
let X be set;
let F be BinOp of X;
mode Preserv of F -> Subset of X means
:: REALSET1:def 2
for x being set holds x in [:it,it:] implies F.x in it;
end;

canceled 2;

theorem :: REALSET1:14
for X being set,
F being BinOp of X,
A being Preserv of F holds F|([:A,A:]) is BinOp of A;

definition
let X be set;
let F be BinOp of X;
let A be Preserv of F;
func F||A -> BinOp of A equals
:: REALSET1:def 3
F | [:A,A:];
end;

definition ::group
let IT be LoopStr;
canceled;

attr IT is zeroed means
:: REALSET1:def 5
for a being Element of IT holds
(the add of IT).[a,the Zero of IT] = a &
(the add of IT).[the Zero of IT,a] = a;
attr IT is complementable means
:: REALSET1:def 6
for a being Element of IT
ex b being Element of IT st
(the add of IT).[a,b] = the Zero of IT &
(the add of IT).[b,a] = the Zero of IT;
end;

definition let L be non empty LoopStr;
redefine attr L is add-associative means
:: REALSET1:def 7
for a,b,c being Element of L holds
redefine attr L is Abelian means
:: REALSET1:def 8

for a,b being Element of L holds
end;

definition let X be non empty set, a be BinOp of X, Z be Element of X;
cluster LoopStr(#X,a,Z#) -> non empty;
end;

definition
complementable (non empty LoopStr);
end;

definition ::group
mode Group is Abelian add-associative zeroed complementable
(non empty LoopStr);
end;

definition
let IT be set;
canceled 3;

attr IT is trivial means
:: REALSET1:def 12
IT is empty or ex x being set st IT = {x};
end;

definition
cluster trivial non empty set;
cluster non trivial non empty set;
cluster non trivial -> non empty set;
end;

canceled 17;

theorem :: REALSET1:32
for X being non empty set holds
X is non trivial iff for x being set holds X\{x} is non empty set;

theorem :: REALSET1:33
ex A being non empty set st for z being Element of A holds
A \ {z} is non empty set;

theorem :: REALSET1:34
for X being non empty set
st for x being Element of X holds X\{x} is non empty set
holds X is non trivial;

definition
let IT be 1-sorted;
attr IT is trivial means
:: REALSET1:def 13
the carrier of IT is trivial;
end;

definition
cluster trivial 1-sorted;
end;

theorem :: REALSET1:35
for A being non empty set st
(for x being Element of A holds A\{x} is non empty set) holds
A is non trivial set;

definition
cluster non trivial strict doubleLoopStr;
end;

definition ::field operator
let A be non trivial set;
let od,om be BinOp of A;
let nd be Element of A;
let nm be Element of A\{nd};
func field(A,od,om,nd,nm) -> non trivial strict doubleLoopStr means
:: REALSET1:def 14
A = the carrier of it &
od = the add of it &
om = the mult of it &
nd = the Zero of it &
nm = the unity of it;
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
:: REALSET1:def 15
(X\{x} is Preserv of F) &
F|[:X\{x},X\{x}:] is BinOp of X\{x};
end;

canceled 3;

theorem :: REALSET1:39
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;

definition
let X be set;
let A be Subset of X;
mode Presv of X,A -> BinOp of X means
:: REALSET1:def 16
for x being set holds x in [:A,A:] implies it.x in A;
end;

canceled;

theorem :: REALSET1:41
for X being set,
A being Subset of X,
F being Presv of X,A holds
F|([:A,A:]) is BinOp of A;

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
:: REALSET1:def 17
F | [:A,A:];
end;

canceled;

theorem :: REALSET1:43
for A being non trivial set holds
for x being Element of A holds
ex F being BinOp of A st
for y being set holds y in [:A\{x},A\{x}:] implies F.y in A\{x};

definition
let A be non trivial set;
let x be Element of A;
mode DnT of x,A -> BinOp of A means
:: REALSET1:def 18
for y being set holds y in [:A\{x},A\{x}:] implies it.y in A\{x};
end;

canceled;

theorem :: REALSET1:45
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},A\{x}:] is BinOp of A\{x};

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
:: REALSET1:def 19
F | [:A\{x},A\{x}:];
end;

definition
let IT be 1-sorted;
redefine attr IT is trivial means
:: REALSET1:def 20
for x,y being Element of IT holds x = y;
end;

```