:: Basic Algebraic Structures
:: by Library Committee
::
:: Received December 8, 2007
:: Copyright (c) 2007-2026 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 XBOOLE_0, SUBSET_1, BINOP_1, ZFMISC_1, STRUCT_0, ARYTM_3,
FUNCT_1, FUNCT_5, SUPINF_2, ARYTM_1, RELAT_1, MESFUNC1, ALGSTR_0, CARD_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, BINOP_1, FUNCT_5, ORDINAL1,
CARD_1, STRUCT_0;
constructors BINOP_1, STRUCT_0, ZFMISC_1, FUNCT_5;
registrations ZFMISC_1, CARD_1, STRUCT_0;
theorems STRUCT_0;
begin :: Additive structures
reserve D for non empty set,
d,e for Element of D,
o,o1 for BinOp of D;
reserve T for trivial set,
s,t for Element of T,
f,f1 for BinOp of T;
reserve N for non trivial set,
n,m for Element of N,
b,b1 for BinOp of N;
definition
struct (1-sorted) addMagma (# carrier -> set, addF -> BinOp of the carrier
#);
end;
registration
let D,o;
cluster addMagma(#D,o#) -> non empty;
coherence;
end;
registration
let T,f;
cluster addMagma(#T,f#) -> trivial;
coherence;
end;
registration
let N,b;
cluster addMagma(#N,b#) -> non trivial;
coherence;
end;
definition
let M be addMagma;
let x,y be Element of M;
func x+y -> Element of M equals
(the addF of M).(x,y);
coherence;
end;
definition
func Trivial-addMagma -> addMagma equals
addMagma(#{0}, op2 #);
coherence;
end;
registration
cluster Trivial-addMagma -> 1-element strict;
coherence;
end;
registration
cluster strict 1-element for addMagma;
existence
proof
take Trivial-addMagma;
thus thesis;
end;
end;
definition
let M be addMagma, x be Element of M;
attr x is left_add-cancelable means
for y,z being Element of M st x+y = x+z holds y = z;
attr x is right_add-cancelable means
for y,z being Element of M st y+ x = z+x holds y = z;
end;
definition
let M be addMagma, x be Element of M;
attr x is add-cancelable means
x is right_add-cancelable left_add-cancelable;
end;
registration
let M be addMagma;
cluster right_add-cancelable left_add-cancelable -> add-cancelable for
Element
of M;
coherence;
cluster add-cancelable -> right_add-cancelable left_add-cancelable for
Element
of M;
coherence;
end;
definition
let M be addMagma;
attr M is left_add-cancelable means
:Def6:
for x being Element of M holds x is left_add-cancelable;
attr M is right_add-cancelable means
:Def7:
for x being Element of M holds x is right_add-cancelable;
end;
definition
let M be addMagma;
attr M is add-cancelable means
M is right_add-cancelable left_add-cancelable;
end;
registration
cluster right_add-cancelable left_add-cancelable -> add-cancelable for
addMagma;
coherence;
cluster add-cancelable -> right_add-cancelable left_add-cancelable for
addMagma;
coherence;
end;
registration
cluster Trivial-addMagma -> add-cancelable;
coherence
proof
set M = Trivial-addMagma;
thus M is right_add-cancelable
proof
let x,y,z be Element of M;
assume y+x = z+x;
thus thesis by STRUCT_0:def 10;
end;
let x,y,z being Element of M;
assume x+y = x+z;
thus thesis by STRUCT_0:def 10;
end;
end;
registration
cluster add-cancelable strict 1-element for addMagma;
existence
proof
take Trivial-addMagma;
thus thesis;
end;
end;
registration
let M be left_add-cancelable addMagma;
cluster -> left_add-cancelable for Element of M;
coherence by Def6;
end;
registration
let M be right_add-cancelable addMagma;
cluster -> right_add-cancelable for Element of M;
coherence by Def7;
end;
definition
struct (ZeroStr,addMagma) addLoopStr (# carrier -> set, addF -> BinOp of the
carrier, ZeroF -> Element of the carrier #);
end;
registration
let D,o,d;
cluster addLoopStr(#D,o,d#) -> non empty;
coherence;
end;
registration
let T,f,t;
cluster addLoopStr(#T,f,t#) -> trivial;
coherence;
end;
registration
let N,b,m;
cluster addLoopStr(#N,b,m#) -> non trivial;
coherence;
end;
definition
func Trivial-addLoopStr -> addLoopStr equals
addLoopStr(#{0}, op2, op0 #);
coherence;
end;
registration
cluster Trivial-addLoopStr -> 1-element strict;
coherence;
end;
registration
cluster strict 1-element for addLoopStr;
existence
proof
take Trivial-addLoopStr;
thus thesis;
end;
end;
definition
let M be addLoopStr, x be Element of M;
attr x is left_complementable means
ex y being Element of M st y+x = 0.M;
attr x is right_complementable means
ex y being Element of M st x+y = 0.M;
end;
definition
let M be addLoopStr, x be Element of M;
attr x is complementable means
x is right_complementable left_complementable;
end;
registration
let M be addLoopStr;
cluster right_complementable left_complementable -> complementable for
Element
of M;
coherence;
cluster complementable -> right_complementable left_complementable for
Element
of M;
coherence;
end;
definition
let M be addLoopStr, x be Element of M;
assume
A1: x is left_complementable right_add-cancelable;
func -x -> Element of M means
it + x = 0.M;
existence by A1;
uniqueness by A1;
end;
definition
let V be addLoopStr;
let v,w be Element of V;
func v - w -> Element of V equals
v + -w;
correctness;
end;
registration
cluster Trivial-addLoopStr -> add-cancelable;
coherence
proof
set M = Trivial-addLoopStr;
thus M is right_add-cancelable
proof
let x,y,z be Element of M;
assume y+x = z+x;
thus thesis by STRUCT_0:def 10;
end;
let x,y,z being Element of M;
assume x+y = x+z;
thus thesis by STRUCT_0:def 10;
end;
end;
definition
let M be addLoopStr;
attr M is left_complementable means
:Def15:
for x being Element of M holds x is left_complementable;
attr M is right_complementable means
:Def16:
for x being Element of M holds x is right_complementable;
end;
definition
let M be addLoopStr;
attr M is complementable means
M is right_complementable left_complementable;
end;
registration
cluster right_complementable left_complementable -> complementable
for addLoopStr;
coherence;
cluster complementable -> right_complementable left_complementable
for addLoopStr;
coherence;
end;
registration
cluster Trivial-addLoopStr -> complementable;
coherence
proof
set M = Trivial-addLoopStr;
thus M is right_complementable
proof
let x be Element of M;
take x;
thus thesis by STRUCT_0:def 10;
end;
let x being Element of M;
take x;
thus thesis by STRUCT_0:def 10;
end;
end;
registration
cluster complementable add-cancelable strict 1-element for addLoopStr;
existence
proof
take Trivial-addLoopStr;
thus thesis;
end;
end;
registration
let M be left_complementable addLoopStr;
cluster -> left_complementable for Element of M;
coherence by Def15;
end;
registration
let M be right_complementable addLoopStr;
cluster -> right_complementable for Element of M;
coherence by Def16;
end;
begin :: Multiplicative structures
definition
struct (1-sorted) multMagma (#
carrier -> set,
multF -> BinOp of the carrier #);
end;
registration
let D,o;
cluster multMagma(#D,o#) -> non empty;
coherence;
end;
registration
let T,f;
cluster multMagma(#T,f#) -> trivial;
coherence;
end;
registration
let N,b;
cluster multMagma(#N,b#) -> non trivial;
coherence;
end;
definition
let M be multMagma;
let x,y be Element of M;
func x*y -> Element of M equals
(the multF of M).(x,y);
coherence;
end;
definition
func Trivial-multMagma -> multMagma equals
multMagma(#{0}, op2 #);
coherence;
end;
registration
cluster Trivial-multMagma -> 1-element strict;
coherence;
end;
registration
cluster strict 1-element for multMagma;
existence
proof
take Trivial-multMagma;
thus thesis;
end;
end;
definition
let M be multMagma, x be Element of M;
attr x is left_mult-cancelable means
for y,z being Element of M st x*y = x*z holds y = z;
attr x is right_mult-cancelable means
for y,z being Element of M st y*x = z*x holds y = z;
end;
definition
let M be multMagma, x be Element of M;
attr x is mult-cancelable means
x is right_mult-cancelable left_mult-cancelable;
end;
registration
let M be multMagma;
cluster right_mult-cancelable left_mult-cancelable -> mult-cancelable
for Element of M;
coherence;
cluster mult-cancelable -> right_mult-cancelable left_mult-cancelable
for Element of M;
coherence;
end;
definition
let M be multMagma;
attr M is left_mult-cancelable means
:Def23:
for x being Element of M holds x is left_mult-cancelable;
attr M is right_mult-cancelable means
:Def24:
for x being Element of M holds x is right_mult-cancelable;
end;
definition
let M be multMagma;
attr M is mult-cancelable means
M is left_mult-cancelable right_mult-cancelable;
end;
registration
cluster right_mult-cancelable left_mult-cancelable -> mult-cancelable
for multMagma;
coherence;
cluster mult-cancelable -> right_mult-cancelable left_mult-cancelable
for multMagma;
coherence;
end;
registration
cluster Trivial-multMagma -> mult-cancelable;
coherence
proof
set M = Trivial-multMagma;
thus M is left_mult-cancelable
proof
let x,y,z be Element of M;
assume x*y = x*z;
thus thesis by STRUCT_0:def 10;
end;
let x,y,z being Element of M;
assume y*x = z*x;
thus thesis by STRUCT_0:def 10;
end;
end;
registration
cluster mult-cancelable strict 1-element for multMagma;
existence
proof
take Trivial-multMagma;
thus thesis;
end;
end;
registration
let M be left_mult-cancelable multMagma;
cluster -> left_mult-cancelable for Element of M;
coherence by Def23;
end;
registration
let M be right_mult-cancelable multMagma;
cluster -> right_mult-cancelable for Element of M;
coherence by Def24;
end;
definition
struct (OneStr,multMagma) multLoopStr (#
carrier -> set,
multF -> BinOp of the carrier,
OneF -> Element of the carrier #);
end;
registration
let D,o,d;
cluster multLoopStr(#D,o,d#) -> non empty;
coherence;
end;
registration
let T,f,t;
cluster multLoopStr(#T,f,t#) -> trivial;
coherence;
end;
registration
let N,b,m;
cluster multLoopStr(#N,b,m#) -> non trivial;
coherence;
end;
definition
func Trivial-multLoopStr -> multLoopStr equals
multLoopStr(#{0}, op2, op0 #);
coherence;
end;
registration
cluster Trivial-multLoopStr -> 1-element strict;
coherence;
end;
registration
cluster strict 1-element for multLoopStr;
existence
proof
take Trivial-multLoopStr;
thus thesis;
end;
end;
registration
cluster Trivial-multLoopStr -> mult-cancelable;
coherence
proof
set M = Trivial-multLoopStr;
thus M is left_mult-cancelable
proof
let x,y,z be Element of M;
assume x*y = x*z;
thus thesis by STRUCT_0:def 10;
end;
let x,y,z be Element of M;
assume y*x = z*x;
thus thesis by STRUCT_0:def 10;
end;
end;
definition
let M be multLoopStr, x be Element of M;
attr x is left_invertible means
ex y being Element of M st y*x = 1.M;
attr x is right_invertible means
ex y being Element of M st x*y = 1.M;
end;
definition
let M be multLoopStr, x be Element of M;
attr x is invertible means
x is right_invertible left_invertible;
end;
registration
let M be multLoopStr;
cluster right_invertible left_invertible -> invertible for Element of M;
coherence;
cluster invertible -> right_invertible left_invertible for Element of M;
coherence;
end;
definition
let M be multLoopStr, x be Element of M;
assume that
A1: x is left_invertible and
A2: x is right_mult-cancelable;
func /x -> Element of M means
it * x = 1.M;
existence by A1;
uniqueness by A2;
end;
definition
let M be multLoopStr;
attr M is left_invertible means :Def31:
for x being Element of M holds x is left_invertible;
attr M is right_invertible means :Def32:
for x being Element of M holds x is right_invertible;
end;
definition
let M be multLoopStr;
attr M is invertible means
M is right_invertible left_invertible;
end;
registration
cluster right_invertible left_invertible -> invertible for multLoopStr;
coherence;
cluster invertible -> right_invertible left_invertible for multLoopStr;
coherence;
end;
registration
cluster Trivial-multLoopStr -> invertible;
coherence
proof
set M = Trivial-multLoopStr;
thus M is right_invertible
proof
let x be Element of M;
take x;
thus thesis by STRUCT_0:def 10;
end;
let x being Element of M;
take x;
thus thesis by STRUCT_0:def 10;
end;
end;
registration
cluster invertible mult-cancelable strict 1-element for multLoopStr;
existence
proof
take Trivial-multLoopStr;
thus thesis;
end;
end;
registration
let M be left_invertible multLoopStr;
cluster -> left_invertible for Element of M;
coherence by Def31;
end;
registration
let M be right_invertible multLoopStr;
cluster -> right_invertible for Element of M;
coherence by Def32;
end;
begin :: Almost
definition
struct (multLoopStr,ZeroOneStr) multLoopStr_0 (#
carrier -> set,
multF -> BinOp of the carrier,
ZeroF, OneF -> Element of the carrier #);
end;
registration
let D,o,d,e;
cluster multLoopStr_0(#D,o,d,e#) -> non empty;
coherence;
end;
registration
let T,f,s,t;
cluster multLoopStr_0(#T,f,s,t#) -> trivial;
coherence;
end;
registration
let N,b,m,n;
cluster multLoopStr_0(#N,b,m,n#) -> non trivial;
coherence;
end;
definition
func Trivial-multLoopStr_0 -> multLoopStr_0 equals
multLoopStr_0(#{0}, op2,op0, op0 #);
coherence;
end;
registration
cluster Trivial-multLoopStr_0 -> 1-element strict;
coherence;
end;
registration
cluster strict 1-element for multLoopStr_0;
existence
proof
take Trivial-multLoopStr_0;
thus thesis;
end;
end;
::$CD
definition
let M be multLoopStr_0;
attr M is almost_left_cancelable means
for x being Element of M st x <> 0.M holds x is left_mult-cancelable;
attr M is almost_right_cancelable means
for x being Element of M st x <> 0.M holds x is right_mult-cancelable;
end;
definition
let M be multLoopStr_0;
attr M is almost_cancelable means
M is almost_left_cancelable almost_right_cancelable;
end;
registration
cluster almost_right_cancelable almost_left_cancelable -> almost_cancelable
for multLoopStr_0;
coherence;
cluster almost_cancelable -> almost_right_cancelable almost_left_cancelable
for multLoopStr_0;
coherence;
end;
registration
cluster Trivial-multLoopStr_0 -> almost_cancelable;
coherence
proof
set M = Trivial-multLoopStr_0;
thus M is almost_left_cancelable by STRUCT_0:def 10;
let x be Element of M;
assume x <> 0.M;
let y,z be Element of M;
assume y*x = z*x;
thus thesis by STRUCT_0:def 10;
end;
end;
registration
cluster almost_cancelable strict 1-element for multLoopStr_0;
existence
proof
take Trivial-multLoopStr_0;
thus thesis;
end;
end;
definition
let M be multLoopStr_0;
attr M is almost_left_invertible means
for x being Element of M st x <> 0.M holds x is left_invertible;
attr M is almost_right_invertible means
for x being Element of M st x <> 0.M holds x is right_invertible;
end;
definition
let M be multLoopStr_0;
attr M is almost_invertible means
M is almost_right_invertible almost_left_invertible;
end;
registration
cluster almost_right_invertible almost_left_invertible -> almost_invertible
for multLoopStr_0;
coherence;
cluster almost_invertible -> almost_right_invertible almost_left_invertible
for multLoopStr_0;
coherence;
end;
registration
cluster Trivial-multLoopStr_0 -> almost_invertible;
coherence
proof
set M = Trivial-multLoopStr_0;
thus M is almost_right_invertible by STRUCT_0:def 10;
let x be Element of M;
assume x <> 0.M;
take x;
thus thesis by STRUCT_0:def 10;
end;
end;
registration
cluster almost_invertible almost_cancelable strict 1-element
for multLoopStr_0;
existence
proof
take Trivial-multLoopStr_0;
thus thesis;
end;
end;
begin :: Double
definition
struct (addLoopStr, multMagma) RngStr (#
carrier -> set,
addF, multF -> BinOp of the carrier,
ZeroF -> Element of the carrier #);
end;
registration
let D,o,o1,e;
cluster RngStr(#D,o,o1,e#) -> non empty;
coherence;
end;
registration
let T,f,f1,t;
cluster RngStr(#T,f,f1,t#) -> trivial;
coherence;
end;
registration
let N,b,b1,n;
cluster RngStr(#N,b,b1,n#) -> non trivial;
coherence;
end;
definition
struct (addLoopStr, multLoopStr_0, RngStr) doubleLoopStr (#
carrier -> set,
addF, multF -> BinOp of the carrier,
OneF, ZeroF -> Element of the carrier #);
end;
registration
let D,o,o1,d,e;
cluster doubleLoopStr(#D,o,o1,d,e#) -> non empty;
coherence;
end;
registration
let T,f,f1,s,t;
cluster doubleLoopStr(#T,f,f1,s,t#) -> trivial;
coherence;
end;
registration
let N,b,b1,m,n;
cluster doubleLoopStr(#N,b,b1,m,n#) -> non trivial;
coherence;
end;
definition
func Trivial-doubleLoopStr -> doubleLoopStr equals
doubleLoopStr(#{0}, op2, op2, op0, op0 #);
coherence;
end;
registration
cluster Trivial-doubleLoopStr -> 1-element strict;
coherence;
end;
registration
cluster strict 1-element for doubleLoopStr;
existence
proof
take Trivial-doubleLoopStr;
thus thesis;
end;
end;
definition
let M be multLoopStr, x,y be Element of M;
func x/y -> Element of M equals x*/y;
coherence;
end;