:: Basic Algebraic Structures
:: by Library Committee
::
:: Received December 8, 2007
:: Copyright (c) 2007-2021 Association of Mizar Users

definition

attr c₁ is strict ;
struct addMagma -> 1-sorted ;
aggr addMagma(# carrier, addF #) -> addMagma ;
sel addF c₁ -> BinOp of the carrier of c₁;

end;

registration

let D be non empty set ;
let o be BinOp of D;

cluster addMagma(# D,o #) -> non empty ;

coherence
not addMagma(# D,o #) is empty ;

end;

registration

let T be trivial set ;
let f be BinOp of T;

cluster addMagma(# T,f #) -> trivial ;

coherence
addMagma(# T,f #) is trivial ;

end;

registration

let N be non trivial set ;
let b be BinOp of N;

cluster addMagma(# N,b #) -> non trivial ;

coherence
not addMagma(# N,b #) is trivial ;

end;

definition

let M be addMagma ;
let x, y be Element of M;

func x + y -> Element of M equals :: ALGSTR_0:def 1
the addF of M . (x,y);

coherence
the addF of M . (x,y) is Element of M ;

end;

:: deftheorem defines + ALGSTR_0:def 1 :
for M being addMagma
for x, y being Element of M holds x + y = the addF of M . (x,y);

definition

func Trivial-addMagma -> addMagma equals :: ALGSTR_0:def 2
addMagma(# {0},op2 #);

coherence
addMagma(# {0},op2 #) is addMagma ;

end;

:: deftheorem defines Trivial-addMagma ALGSTR_0:def 2 :
Trivial-addMagma = addMagma(# {0},op2 #);

registration

cluster Trivial-addMagma -> 1 -element strict ;

coherence
( Trivial-addMagma is 1 -element & Trivial-addMagma is strict ) ;

end;

registration

cluster 1 -element strict for addMagma ;

existence
ex b₁ being addMagma st
( b₁ is strict & b₁ is 1 -element )

proof end;

end;

definition

let M be addMagma ;
let x be Element of M;

attr x is left_add-cancelable means :: ALGSTR_0:def 3
for y, z being Element of M st x + y = x + z holds
y = z;

attr x is right_add-cancelable means :: ALGSTR_0:def 4
for y, z being Element of M st y + x = z + x holds
y = z;

end;

:: deftheorem defines left_add-cancelable ALGSTR_0:def 3 :
for M being addMagma
for x being Element of M holds
( x is left_add-cancelable iff for y, z being Element of M st x + y = x + z holds
y = z );

:: deftheorem defines right_add-cancelable ALGSTR_0:def 4 :
for M being addMagma
for x being Element of M holds
( x is right_add-cancelable iff for y, z being Element of M st y + x = z + x holds
y = z );

definition

let M be addMagma ;
let x be Element of M;

attr x is add-cancelable means :: ALGSTR_0:def 5
( x is right_add-cancelable & x is left_add-cancelable );

end;

:: deftheorem defines add-cancelable ALGSTR_0:def 5 :
for M being addMagma
for x being Element of M holds
( x is add-cancelable iff ( x is right_add-cancelable & x is left_add-cancelable ) );

registration

let M be addMagma ;

cluster left_add-cancelable right_add-cancelable -> add-cancelable for Element of the carrier of M;

coherence
for b₁ being Element of M st b₁ is right_add-cancelable & b₁ is left_add-cancelable holds
b₁ is add-cancelable ;

cluster add-cancelable -> left_add-cancelable right_add-cancelable for Element of the carrier of M;

coherence
for b₁ being Element of M st b₁ is add-cancelable holds
( b₁ is right_add-cancelable & b₁ is left_add-cancelable ) ;

end;

definition

let M be addMagma ;

attr M is left_add-cancelable means :Def6: :: ALGSTR_0:def 6
for x being Element of M holds x is left_add-cancelable ;

attr M is right_add-cancelable means :Def7: :: ALGSTR_0:def 7
for x being Element of M holds x is right_add-cancelable ;

end;

:: deftheorem Def6 defines left_add-cancelable ALGSTR_0:def 6 :
for M being addMagma holds
( M is left_add-cancelable iff for x being Element of M holds x is left_add-cancelable );

:: deftheorem Def7 defines right_add-cancelable ALGSTR_0:def 7 :
for M being addMagma holds
( M is right_add-cancelable iff for x being Element of M holds x is right_add-cancelable );

definition

let M be addMagma ;

attr M is add-cancelable means :: ALGSTR_0:def 8
( M is right_add-cancelable & M is left_add-cancelable );

end;

:: deftheorem defines add-cancelable ALGSTR_0:def 8 :
for M being addMagma holds
( M is add-cancelable iff ( M is right_add-cancelable & M is left_add-cancelable ) );

registration

cluster left_add-cancelable right_add-cancelable -> add-cancelable for addMagma ;

coherence
for b₁ being addMagma st b₁ is right_add-cancelable & b₁ is left_add-cancelable holds
b₁ is add-cancelable ;

cluster add-cancelable -> left_add-cancelable right_add-cancelable for addMagma ;

coherence
for b₁ being addMagma st b₁ is add-cancelable holds
( b₁ is right_add-cancelable & b₁ is left_add-cancelable ) ;

end;

registration

cluster Trivial-addMagma -> add-cancelable ;

coherence
Trivial-addMagma is add-cancelable

proof end;

end;

registration

cluster 1 -element strict add-cancelable for addMagma ;

existence
ex b₁ being addMagma st
( b₁ is add-cancelable & b₁ is strict & b₁ is 1 -element )

proof end;

end;

registration

let M be left_add-cancelable addMagma ;

cluster -> left_add-cancelable for Element of the carrier of M;

coherence
for b₁ being Element of M holds b₁ is left_add-cancelable by Def6;

end;

registration

let M be right_add-cancelable addMagma ;

cluster -> right_add-cancelable for Element of the carrier of M;

coherence
for b₁ being Element of M holds b₁ is right_add-cancelable by Def7;

end;

definition

attr c₁ is strict ;
struct addLoopStr -> ZeroStr , addMagma ;
aggr addLoopStr(# carrier, addF, ZeroF #) -> addLoopStr ;

end;

registration

let D be non empty set ;
let o be BinOp of D;
let d be Element of D;

cluster addLoopStr(# D,o,d #) -> non empty ;

coherence
not addLoopStr(# D,o,d #) is empty ;

end;

registration

let T be trivial set ;
let f be BinOp of T;
let t be Element of T;

cluster addLoopStr(# T,f,t #) -> trivial ;

coherence
addLoopStr(# T,f,t #) is trivial ;

end;

registration

let N be non trivial set ;
let b be BinOp of N;
let m be Element of N;

cluster addLoopStr(# N,b,m #) -> non trivial ;

coherence
not addLoopStr(# N,b,m #) is trivial ;

end;

definition

func Trivial-addLoopStr -> addLoopStr equals :: ALGSTR_0:def 9
addLoopStr(# {0},op2,op0 #);

coherence
addLoopStr(# {0},op2,op0 #) is addLoopStr ;

end;

:: deftheorem defines Trivial-addLoopStr ALGSTR_0:def 9 :
Trivial-addLoopStr = addLoopStr(# {0},op2,op0 #);

registration

cluster Trivial-addLoopStr -> 1 -element strict ;

coherence
( Trivial-addLoopStr is 1 -element & Trivial-addLoopStr is strict ) ;

end;

registration

cluster 1 -element strict for addLoopStr ;

existence
ex b₁ being addLoopStr st
( b₁ is strict & b₁ is 1 -element )

proof end;

end;

definition

let M be addLoopStr ;
let x be Element of M;

attr x is left_complementable means :: ALGSTR_0:def 10
ex y being Element of M st y + x = 0. M;

attr x is right_complementable means :: ALGSTR_0:def 11
ex y being Element of M st x + y = 0. M;

end;

:: deftheorem defines left_complementable ALGSTR_0:def 10 :
for M being addLoopStr
for x being Element of M holds
( x is left_complementable iff ex y being Element of M st y + x = 0. M );

:: deftheorem defines right_complementable ALGSTR_0:def 11 :
for M being addLoopStr
for x being Element of M holds
( x is right_complementable iff ex y being Element of M st x + y = 0. M );

definition

let M be addLoopStr ;
let x be Element of M;

attr x is complementable means :: ALGSTR_0:def 12
( x is right_complementable & x is left_complementable );

end;

:: deftheorem defines complementable ALGSTR_0:def 12 :
for M being addLoopStr
for x being Element of M holds
( x is complementable iff ( x is right_complementable & x is left_complementable ) );

registration

let M be addLoopStr ;

cluster left_complementable right_complementable -> complementable for Element of the carrier of M;

coherence
for b₁ being Element of M st b₁ is right_complementable & b₁ is left_complementable holds
b₁ is complementable ;

cluster complementable -> left_complementable right_complementable for Element of the carrier of M;

coherence
for b₁ being Element of M st b₁ is complementable holds
( b₁ is right_complementable & b₁ is left_complementable ) ;

end;

definition

let M be addLoopStr ;
let x be Element of M;
assume A1: ( x is left_complementable & x is right_add-cancelable ) ;

func - x -> Element of M means :: ALGSTR_0:def 13
it + x = 0. M;

existence
ex b₁ being Element of M st b₁ + x = 0. M by A1;
uniqueness
for b₁, b₂ being Element of M st b₁ + x = 0. M & b₂ + x = 0. M holds
b₁ = b₂ by A1;

end;

:: deftheorem defines - ALGSTR_0:def 13 :
for M being addLoopStr
for x being Element of M st x is left_complementable & x is right_add-cancelable holds
for b₃ being Element of M holds
( b₃ = - x iff b₃ + x = 0. M );

definition

let V be addLoopStr ;
let v, w be Element of V;

func v - w -> Element of V equals :: ALGSTR_0:def 14
v + (- w);

correctness
coherence
v + (- w) is Element of V;
;

end;

:: deftheorem defines - ALGSTR_0:def 14 :
for V being addLoopStr
for v, w being Element of V holds v - w = v + (- w);

registration

cluster Trivial-addLoopStr -> add-cancelable ;

coherence
Trivial-addLoopStr is add-cancelable

proof end;

end;

definition

let M be addLoopStr ;

attr M is left_complementable means :Def15: :: ALGSTR_0:def 15
for x being Element of M holds x is left_complementable ;

attr M is right_complementable means :Def16: :: ALGSTR_0:def 16
for x being Element of M holds x is right_complementable ;

end;

:: deftheorem Def15 defines left_complementable ALGSTR_0:def 15 :
for M being addLoopStr holds
( M is left_complementable iff for x being Element of M holds x is left_complementable );

:: deftheorem Def16 defines right_complementable ALGSTR_0:def 16 :
for M being addLoopStr holds
( M is right_complementable iff for x being Element of M holds x is right_complementable );

definition

let M be addLoopStr ;

attr M is complementable means :: ALGSTR_0:def 17
( M is right_complementable & M is left_complementable );

end;

:: deftheorem defines complementable ALGSTR_0:def 17 :
for M being addLoopStr holds
( M is complementable iff ( M is right_complementable & M is left_complementable ) );

registration

cluster left_complementable right_complementable -> complementable for addLoopStr ;

coherence
for b₁ being addLoopStr st b₁ is right_complementable & b₁ is left_complementable holds
b₁ is complementable ;

cluster complementable -> left_complementable right_complementable for addLoopStr ;

coherence
for b₁ being addLoopStr st b₁ is complementable holds
( b₁ is right_complementable & b₁ is left_complementable ) ;

end;

registration

cluster Trivial-addLoopStr -> complementable ;

coherence
Trivial-addLoopStr is complementable

proof end;

end;

registration

cluster 1 -element add-cancelable strict complementable for addLoopStr ;

existence
ex b₁ being addLoopStr st
( b₁ is complementable & b₁ is add-cancelable & b₁ is strict & b₁ is 1 -element )

proof end;

end;

registration

let M be left_complementable addLoopStr ;

cluster -> left_complementable for Element of the carrier of M;

coherence
for b₁ being Element of M holds b₁ is left_complementable by Def15;

end;

registration

let M be right_complementable addLoopStr ;

cluster -> right_complementable for Element of the carrier of M;

coherence
for b₁ being Element of M holds b₁ is right_complementable by Def16;

end;

definition

attr c₁ is strict ;
struct multMagma -> 1-sorted ;
aggr multMagma(# carrier, multF #) -> multMagma ;
sel multF c₁ -> BinOp of the carrier of c₁;

end;

registration

let D be non empty set ;
let o be BinOp of D;

cluster multMagma(# D,o #) -> non empty ;

coherence
not multMagma(# D,o #) is empty ;

end;

registration

let T be trivial set ;
let f be BinOp of T;

cluster multMagma(# T,f #) -> trivial ;

coherence
multMagma(# T,f #) is trivial ;

end;

registration

let N be non trivial set ;
let b be BinOp of N;

cluster multMagma(# N,b #) -> non trivial ;

coherence
not multMagma(# N,b #) is trivial ;

end;

definition

let M be multMagma ;
let x, y be Element of M;

func x * y -> Element of M equals :: ALGSTR_0:def 18
the multF of M . (x,y);

coherence
the multF of M . (x,y) is Element of M ;

end;

:: deftheorem defines * ALGSTR_0:def 18 :
for M being multMagma
for x, y being Element of M holds x * y = the multF of M . (x,y);

definition

func Trivial-multMagma -> multMagma equals :: ALGSTR_0:def 19
multMagma(# {0},op2 #);

coherence
multMagma(# {0},op2 #) is multMagma ;

end;

:: deftheorem defines Trivial-multMagma ALGSTR_0:def 19 :
Trivial-multMagma = multMagma(# {0},op2 #);

registration

cluster Trivial-multMagma -> 1 -element strict ;

coherence
( Trivial-multMagma is 1 -element & Trivial-multMagma is strict ) ;

end;

registration

cluster 1 -element strict for multMagma ;

existence
ex b₁ being multMagma st
( b₁ is strict & b₁ is 1 -element )

proof end;

end;

definition

let M be multMagma ;
let x be Element of M;

attr x is left_mult-cancelable means :: ALGSTR_0:def 20
for y, z being Element of M st x * y = x * z holds
y = z;

attr x is right_mult-cancelable means :: ALGSTR_0:def 21
for y, z being Element of M st y * x = z * x holds
y = z;

end;

:: deftheorem defines left_mult-cancelable ALGSTR_0:def 20 :
for M being multMagma
for x being Element of M holds
( x is left_mult-cancelable iff for y, z being Element of M st x * y = x * z holds
y = z );

:: deftheorem defines right_mult-cancelable ALGSTR_0:def 21 :
for M being multMagma
for x being Element of M holds
( x is right_mult-cancelable iff for y, z being Element of M st y * x = z * x holds
y = z );

definition

let M be multMagma ;
let x be Element of M;

attr x is mult-cancelable means :: ALGSTR_0:def 22
( x is right_mult-cancelable & x is left_mult-cancelable );

end;

:: deftheorem defines mult-cancelable ALGSTR_0:def 22 :
for M being multMagma
for x being Element of M holds
( x is mult-cancelable iff ( x is right_mult-cancelable & x is left_mult-cancelable ) );

registration

let M be multMagma ;

cluster left_mult-cancelable right_mult-cancelable -> mult-cancelable for Element of the carrier of M;

coherence
for b₁ being Element of M st b₁ is right_mult-cancelable & b₁ is left_mult-cancelable holds
b₁ is mult-cancelable ;

cluster mult-cancelable -> left_mult-cancelable right_mult-cancelable for Element of the carrier of M;

coherence
for b₁ being Element of M st b₁ is mult-cancelable holds
( b₁ is right_mult-cancelable & b₁ is left_mult-cancelable ) ;

end;

definition

let M be multMagma ;

attr M is left_mult-cancelable means :Def23: :: ALGSTR_0:def 23
for x being Element of M holds x is left_mult-cancelable ;

attr M is right_mult-cancelable means :Def24: :: ALGSTR_0:def 24
for x being Element of M holds x is right_mult-cancelable ;

end;

:: deftheorem Def23 defines left_mult-cancelable ALGSTR_0:def 23 :
for M being multMagma holds
( M is left_mult-cancelable iff for x being Element of M holds x is left_mult-cancelable );

:: deftheorem Def24 defines right_mult-cancelable ALGSTR_0:def 24 :
for M being multMagma holds
( M is right_mult-cancelable iff for x being Element of M holds x is right_mult-cancelable );

definition

let M be multMagma ;

attr M is mult-cancelable means :: ALGSTR_0:def 25
( M is left_mult-cancelable & M is right_mult-cancelable );

end;

:: deftheorem defines mult-cancelable ALGSTR_0:def 25 :
for M being multMagma holds
( M is mult-cancelable iff ( M is left_mult-cancelable & M is right_mult-cancelable ) );

registration

cluster left_mult-cancelable right_mult-cancelable -> mult-cancelable for multMagma ;

coherence
for b₁ being multMagma st b₁ is right_mult-cancelable & b₁ is left_mult-cancelable holds
b₁ is mult-cancelable ;

cluster mult-cancelable -> left_mult-cancelable right_mult-cancelable for multMagma ;

coherence
for b₁ being multMagma st b₁ is mult-cancelable holds
( b₁ is right_mult-cancelable & b₁ is left_mult-cancelable ) ;

end;

registration

cluster Trivial-multMagma -> mult-cancelable ;

coherence
Trivial-multMagma is mult-cancelable

proof end;

end;

registration

cluster 1 -element strict mult-cancelable for multMagma ;

existence
ex b₁ being multMagma st
( b₁ is mult-cancelable & b₁ is strict & b₁ is 1 -element )

proof end;

end;

registration

let M be left_mult-cancelable multMagma ;

cluster -> left_mult-cancelable for Element of the carrier of M;

coherence
for b₁ being Element of M holds b₁ is left_mult-cancelable by Def23;

end;

registration

let M be right_mult-cancelable multMagma ;

cluster -> right_mult-cancelable for Element of the carrier of M;

coherence
for b₁ being Element of M holds b₁ is right_mult-cancelable by Def24;

end;

definition

attr c₁ is strict ;
struct multLoopStr -> OneStr , multMagma ;
aggr multLoopStr(# carrier, multF, OneF #) -> multLoopStr ;

end;

registration

let D be non empty set ;
let o be BinOp of D;
let d be Element of D;

cluster multLoopStr(# D,o,d #) -> non empty ;

coherence
not multLoopStr(# D,o,d #) is empty ;

end;

registration

let T be trivial set ;
let f be BinOp of T;
let t be Element of T;

cluster multLoopStr(# T,f,t #) -> trivial ;

coherence
multLoopStr(# T,f,t #) is trivial ;

end;

registration

let N be non trivial set ;
let b be BinOp of N;
let m be Element of N;

cluster multLoopStr(# N,b,m #) -> non trivial ;

coherence
not multLoopStr(# N,b,m #) is trivial ;

end;

definition

func Trivial-multLoopStr -> multLoopStr equals :: ALGSTR_0:def 26
multLoopStr(# {0},op2,op0 #);

coherence
multLoopStr(# {0},op2,op0 #) is multLoopStr ;

end;

:: deftheorem defines Trivial-multLoopStr ALGSTR_0:def 26 :
Trivial-multLoopStr = multLoopStr(# {0},op2,op0 #);

registration

cluster Trivial-multLoopStr -> 1 -element strict ;

coherence
( Trivial-multLoopStr is 1 -element & Trivial-multLoopStr is strict ) ;

end;

registration

cluster 1 -element strict for multLoopStr ;

existence
ex b₁ being multLoopStr st
( b₁ is strict & b₁ is 1 -element )

proof end;

end;

registration

cluster Trivial-multLoopStr -> mult-cancelable ;

coherence
Trivial-multLoopStr is mult-cancelable

proof end;

end;

definition

let M be multLoopStr ;
let x be Element of M;

attr x is left_invertible means :: ALGSTR_0:def 27
ex y being Element of M st y * x = 1. M;

attr x is right_invertible means :: ALGSTR_0:def 28
ex y being Element of M st x * y = 1. M;

end;

:: deftheorem defines left_invertible ALGSTR_0:def 27 :
for M being multLoopStr
for x being Element of M holds
( x is left_invertible iff ex y being Element of M st y * x = 1. M );

:: deftheorem defines right_invertible ALGSTR_0:def 28 :
for M being multLoopStr
for x being Element of M holds
( x is right_invertible iff ex y being Element of M st x * y = 1. M );

definition

let M be multLoopStr ;
let x be Element of M;

attr x is invertible means :: ALGSTR_0:def 29
( x is right_invertible & x is left_invertible );

end;

:: deftheorem defines invertible ALGSTR_0:def 29 :
for M being multLoopStr
for x being Element of M holds
( x is invertible iff ( x is right_invertible & x is left_invertible ) );

registration

let M be multLoopStr ;

cluster left_invertible right_invertible -> invertible for Element of the carrier of M;

coherence
for b₁ being Element of M st b₁ is right_invertible & b₁ is left_invertible holds
b₁ is invertible ;

cluster invertible -> left_invertible right_invertible for Element of the carrier of M;

coherence
for b₁ being Element of M st b₁ is invertible holds
( b₁ is right_invertible & b₁ is left_invertible ) ;

end;

definition

let M be multLoopStr ;
let 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 :: ALGSTR_0:def 30
it * x = 1. M;

existence
ex b₁ being Element of M st b₁ * x = 1. M by A1;
uniqueness
for b₁, b₂ being Element of M st b₁ * x = 1. M & b₂ * x = 1. M holds
b₁ = b₂ by A2;

end;

:: deftheorem defines / ALGSTR_0:def 30 :
for M being multLoopStr
for x being Element of M st x is left_invertible & x is right_mult-cancelable holds
for b₃ being Element of M holds
( b₃ = / x iff b₃ * x = 1. M );

definition

let M be multLoopStr ;

attr M is left_invertible means :Def31: :: ALGSTR_0:def 31
for x being Element of M holds x is left_invertible ;

attr M is right_invertible means :Def32: :: ALGSTR_0:def 32
for x being Element of M holds x is right_invertible ;

end;

:: deftheorem Def31 defines left_invertible ALGSTR_0:def 31 :
for M being multLoopStr holds
( M is left_invertible iff for x being Element of M holds x is left_invertible );

:: deftheorem Def32 defines right_invertible ALGSTR_0:def 32 :
for M being multLoopStr holds
( M is right_invertible iff for x being Element of M holds x is right_invertible );

definition

let M be multLoopStr ;

attr M is invertible means :: ALGSTR_0:def 33
( M is right_invertible & M is left_invertible );

end;

:: deftheorem defines invertible ALGSTR_0:def 33 :
for M being multLoopStr holds
( M is invertible iff ( M is right_invertible & M is left_invertible ) );

registration

cluster left_invertible right_invertible -> invertible for multLoopStr ;

coherence
for b₁ being multLoopStr st b₁ is right_invertible & b₁ is left_invertible holds
b₁ is invertible ;

cluster invertible -> left_invertible right_invertible for multLoopStr ;

coherence
for b₁ being multLoopStr st b₁ is invertible holds
( b₁ is right_invertible & b₁ is left_invertible ) ;

end;

registration

cluster Trivial-multLoopStr -> invertible ;

coherence
Trivial-multLoopStr is invertible

proof end;

end;

registration

cluster 1 -element mult-cancelable strict invertible for multLoopStr ;

existence
ex b₁ being multLoopStr st
( b₁ is invertible & b₁ is mult-cancelable & b₁ is strict & b₁ is 1 -element )

proof end;

end;

registration

let M be left_invertible multLoopStr ;

cluster -> left_invertible for Element of the carrier of M;

coherence
for b₁ being Element of M holds b₁ is left_invertible by Def31;

end;

registration

let M be right_invertible multLoopStr ;

cluster -> right_invertible for Element of the carrier of M;

coherence
for b₁ being Element of M holds b₁ is right_invertible by Def32;

end;

definition

attr c₁ is strict ;
struct multLoopStr_0 -> multLoopStr , ZeroOneStr ;
aggr multLoopStr_0(# carrier, multF, ZeroF, OneF #) -> multLoopStr_0 ;

end;

registration

let D be non empty set ;
let o be BinOp of D;
let d, e be Element of D;

cluster multLoopStr_0(# D,o,d,e #) -> non empty ;

coherence
not multLoopStr_0(# D,o,d,e #) is empty ;

end;

registration

let T be trivial set ;
let f be BinOp of T;
let s, t be Element of T;

cluster multLoopStr_0(# T,f,s,t #) -> trivial ;

coherence
multLoopStr_0(# T,f,s,t #) is trivial ;

end;

registration

let N be non trivial set ;
let b be BinOp of N;
let m, n be Element of N;

cluster multLoopStr_0(# N,b,m,n #) -> non trivial ;

coherence
not multLoopStr_0(# N,b,m,n #) is trivial ;

end;

definition

func Trivial-multLoopStr_0 -> multLoopStr_0 equals :: ALGSTR_0:def 34
multLoopStr_0(# {0},op2,op0,op0 #);

coherence
multLoopStr_0(# {0},op2,op0,op0 #) is multLoopStr_0 ;

end;

:: deftheorem defines Trivial-multLoopStr_0 ALGSTR_0:def 34 :
Trivial-multLoopStr_0 = multLoopStr_0(# {0},op2,op0,op0 #);

registration

cluster Trivial-multLoopStr_0 -> 1 -element strict ;

coherence
( Trivial-multLoopStr_0 is 1 -element & Trivial-multLoopStr_0 is strict ) ;

end;

registration

cluster 1 -element strict for multLoopStr_0 ;

existence
ex b₁ being multLoopStr_0 st
( b₁ is strict & b₁ is 1 -element )

proof end;

end;

canceled;

::$CD

definition

let M be multLoopStr_0 ;

attr M is almost_left_cancelable means :: ALGSTR_0:def 35
for x being Element of M st x <> 0. M holds
x is left_mult-cancelable ;

attr M is almost_right_cancelable means :: ALGSTR_0:def 36
for x being Element of M st x <> 0. M holds
x is right_mult-cancelable ;

end;

:: deftheorem defines almost_left_cancelable ALGSTR_0:def 35 :
for M being multLoopStr_0 holds
( M is almost_left_cancelable iff for x being Element of M st x <> 0. M holds
x is left_mult-cancelable );

:: deftheorem defines almost_right_cancelable ALGSTR_0:def 36 :
for M being multLoopStr_0 holds
( M is almost_right_cancelable iff for x being Element of M st x <> 0. M holds
x is right_mult-cancelable );

definition

let M be multLoopStr_0 ;

attr M is almost_cancelable means :: ALGSTR_0:def 37
( M is almost_left_cancelable & M is almost_right_cancelable );

end;

:: deftheorem defines almost_cancelable ALGSTR_0:def 37 :
for M being multLoopStr_0 holds
( M is almost_cancelable iff ( M is almost_left_cancelable & M is almost_right_cancelable ) );

registration

cluster almost_left_cancelable almost_right_cancelable -> almost_cancelable for multLoopStr_0 ;

coherence
for b₁ being multLoopStr_0 st b₁ is almost_right_cancelable & b₁ is almost_left_cancelable holds
b₁ is almost_cancelable ;

cluster almost_cancelable -> almost_left_cancelable almost_right_cancelable for multLoopStr_0 ;

coherence
for b₁ being multLoopStr_0 st b₁ is almost_cancelable holds
( b₁ is almost_right_cancelable & b₁ is almost_left_cancelable ) ;

end;

registration

cluster Trivial-multLoopStr_0 -> almost_cancelable ;

coherence
Trivial-multLoopStr_0 is almost_cancelable

proof end;

end;

registration

cluster 1 -element strict almost_cancelable for multLoopStr_0 ;

existence
ex b₁ being multLoopStr_0 st
( b₁ is almost_cancelable & b₁ is strict & b₁ is 1 -element )

proof end;

end;

definition

let M be multLoopStr_0 ;

attr M is almost_left_invertible means :: ALGSTR_0:def 38
for x being Element of M st x <> 0. M holds
x is left_invertible ;

attr M is almost_right_invertible means :: ALGSTR_0:def 39
for x being Element of M st x <> 0. M holds
x is right_invertible ;

end;

:: deftheorem defines almost_left_invertible ALGSTR_0:def 38 :
for M being multLoopStr_0 holds
( M is almost_left_invertible iff for x being Element of M st x <> 0. M holds
x is left_invertible );

:: deftheorem defines almost_right_invertible ALGSTR_0:def 39 :
for M being multLoopStr_0 holds
( M is almost_right_invertible iff for x being Element of M st x <> 0. M holds
x is right_invertible );

definition

let M be multLoopStr_0 ;

attr M is almost_invertible means :: ALGSTR_0:def 40
( M is almost_right_invertible & M is almost_left_invertible );

end;

:: deftheorem defines almost_invertible ALGSTR_0:def 40 :
for M being multLoopStr_0 holds
( M is almost_invertible iff ( M is almost_right_invertible & M is almost_left_invertible ) );

registration

cluster almost_left_invertible almost_right_invertible -> almost_invertible for multLoopStr_0 ;

coherence
for b₁ being multLoopStr_0 st b₁ is almost_right_invertible & b₁ is almost_left_invertible holds
b₁ is almost_invertible ;

cluster almost_invertible -> almost_left_invertible almost_right_invertible for multLoopStr_0 ;

coherence
for b₁ being multLoopStr_0 st b₁ is almost_invertible holds
( b₁ is almost_right_invertible & b₁ is almost_left_invertible ) ;

end;

registration

cluster Trivial-multLoopStr_0 -> almost_invertible ;

coherence
Trivial-multLoopStr_0 is almost_invertible

proof end;

end;

registration

cluster 1 -element strict almost_cancelable almost_invertible for multLoopStr_0 ;

existence
ex b₁ being multLoopStr_0 st
( b₁ is almost_invertible & b₁ is almost_cancelable & b₁ is strict & b₁ is 1 -element )

proof end;

end;

definition

attr c₁ is strict ;
struct doubleLoopStr -> addLoopStr , multLoopStr_0 ;
aggr doubleLoopStr(# carrier, addF, multF, OneF, ZeroF #) -> doubleLoopStr ;

end;

registration

let D be non empty set ;
let o, o1 be BinOp of D;
let d, e be Element of D;

cluster doubleLoopStr(# D,o,o1,d,e #) -> non empty ;

coherence
not doubleLoopStr(# D,o,o1,d,e #) is empty ;

end;

registration

let T be trivial set ;
let f, f1 be BinOp of T;
let s, t be Element of T;

cluster doubleLoopStr(# T,f,f1,s,t #) -> trivial ;

coherence
doubleLoopStr(# T,f,f1,s,t #) is trivial ;

end;

registration

let N be non trivial set ;
let b, b1 be BinOp of N;
let m, n be Element of N;

cluster doubleLoopStr(# N,b,b1,m,n #) -> non trivial ;

coherence
not doubleLoopStr(# N,b,b1,m,n #) is trivial ;

end;

definition

func Trivial-doubleLoopStr -> doubleLoopStr equals :: ALGSTR_0:def 41
doubleLoopStr(# {0},op2,op2,op0,op0 #);

coherence
doubleLoopStr(# {0},op2,op2,op0,op0 #) is doubleLoopStr ;

end;

:: deftheorem defines Trivial-doubleLoopStr ALGSTR_0:def 41 :
Trivial-doubleLoopStr = doubleLoopStr(# {0},op2,op2,op0,op0 #);

registration

cluster Trivial-doubleLoopStr -> 1 -element strict ;

coherence
( Trivial-doubleLoopStr is 1 -element & Trivial-doubleLoopStr is strict ) ;

end;

registration

cluster 1 -element strict for doubleLoopStr ;

existence
ex b₁ being doubleLoopStr st
( b₁ is strict & b₁ is 1 -element )

proof end;

end;

definition

let M be multLoopStr ;
let x, y be Element of M;

func x / y -> Element of M equals :: ALGSTR_0:def 42
x * (/ y);

coherence
x * (/ y) is Element of M ;

end;

:: deftheorem defines / ALGSTR_0:def 42 :
for M being multLoopStr
for x, y being Element of M holds x / y = x * (/ y);