:: by Library Committee

::

:: Received December 8, 2007

:: Copyright (c) 2007-2012 Association of Mizar Users

begin

definition

attr c_{1} is strict ;

struct addMagma -> 1-sorted ;

aggr addMagma(# carrier, addF #) -> addMagma ;

sel addF c_{1} -> BinOp of the carrier of c_{1};

end;
struct addMagma -> 1-sorted ;

aggr addMagma(# carrier, addF #) -> addMagma ;

sel addF c

registration
end;

registration
end;

registration
end;

definition
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);

for M being addMagma

for x, y being Element of M holds x + y = the addF of M . (x,y);

registration
end;

registration
end;

definition

let M be addMagma ;

let x be Element of M;

end;
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;

for y, z being Element of M st x + y = x + z holds

y = z;

attr x is right_add-cancelable means :Def4: :: ALGSTR_0:def 4

for y, z being Element of M st y + x = z + x holds

y = z;

for y, z being Element of M st y + x = z + x holds

y = z;

:: 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 );

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 Def4 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 );

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;

end;
let x be Element of M;

attr x is add-cancelable means :Def5: :: ALGSTR_0:def 5

( x is right_add-cancelable & x is left_add-cancelable );

( x is right_add-cancelable & x is left_add-cancelable );

:: deftheorem Def5 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 ) );

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 ;

coherence

for b_{1} being Element of M st b_{1} is right_add-cancelable & b_{1} is left_add-cancelable holds

b_{1} is add-cancelable
by Def5;

coherence

for b_{1} being Element of M st b_{1} is add-cancelable holds

( b_{1} is right_add-cancelable & b_{1} is left_add-cancelable )
by Def5;

end;
coherence

for b

b

coherence

for b

( b

definition

let M be addMagma ;

end;
attr M is left_add-cancelable means :Def6: :: ALGSTR_0:def 6

for x being Element of M holds x is left_add-cancelable ;

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 ;

for x being Element of M holds x is right_add-cancelable ;

:: 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 );

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 );

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 ;

end;
attr M is add-cancelable means :Def8: :: ALGSTR_0:def 8

( M is right_add-cancelable & M is left_add-cancelable );

( M is right_add-cancelable & M is left_add-cancelable );

:: deftheorem Def8 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 ) );

for M being addMagma holds

( M is add-cancelable iff ( M is right_add-cancelable & M is left_add-cancelable ) );

registration

coherence

for b_{1} being addMagma st b_{1} is right_add-cancelable & b_{1} is left_add-cancelable holds

b_{1} is add-cancelable
by Def8;

coherence

for b_{1} being addMagma st b_{1} is add-cancelable holds

( b_{1} is right_add-cancelable & b_{1} is left_add-cancelable )
by Def8;

end;
for b

b

coherence

for b

( b

registration

existence

ex b_{1} being addMagma st

( b_{1} is add-cancelable & b_{1} is strict & b_{1} is 1 -element )

end;
ex b

( b

proof end;

registration

let M be left_add-cancelable addMagma ;

coherence

for b_{1} being Element of M holds b_{1} is left_add-cancelable
by Def6;

end;
coherence

for b

registration

let M be right_add-cancelable addMagma ;

coherence

for b_{1} being Element of M holds b_{1} is right_add-cancelable
by Def7;

end;
coherence

for b

definition

attr c_{1} is strict ;

struct addLoopStr -> ZeroStr , addMagma ;

aggr addLoopStr(# carrier, addF, ZeroF #) -> addLoopStr ;

end;
struct addLoopStr -> ZeroStr , addMagma ;

aggr addLoopStr(# carrier, addF, ZeroF #) -> addLoopStr ;

registration

let D be non empty set ;

let o be BinOp of D;

let d be Element of D;

coherence

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

end;
let o be BinOp of D;

let d be Element of D;

coherence

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

registration

let T be trivial set ;

let f be BinOp of T;

let t be Element of T;

coherence

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

end;
let f be BinOp of T;

let t be Element of T;

coherence

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

registration

let N be non trivial set ;

let b be BinOp of N;

let m be Element of N;

coherence

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

end;
let b be BinOp of N;

let m be Element of N;

coherence

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

:: deftheorem defines Trivial-addLoopStr ALGSTR_0:def 9 :

Trivial-addLoopStr = addLoopStr(# 1,op2,op0 #);

Trivial-addLoopStr = addLoopStr(# 1,op2,op0 #);

registration
end;

registration
end;

definition

let M be addLoopStr ;

let x be Element of M;

end;
let x be Element of M;

attr x is left_complementable means :Def10: :: ALGSTR_0:def 10

ex y being Element of M st y + x = 0. M;

ex y being Element of M st y + x = 0. M;

:: deftheorem Def10 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 );

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 );

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;

end;
let x be Element of M;

attr x is complementable means :Def12: :: ALGSTR_0:def 12

( x is right_complementable & x is left_complementable );

( x is right_complementable & x is left_complementable );

:: deftheorem Def12 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 ) );

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 ;

coherence

for b_{1} being Element of M st b_{1} is right_complementable & b_{1} is left_complementable holds

b_{1} is complementable
by Def12;

coherence

for b_{1} being Element of M st b_{1} is complementable holds

( b_{1} is right_complementable & b_{1} is left_complementable )
by Def12;

end;
coherence

for b

b

coherence

for b

( b

definition

let M be addLoopStr ;

let x be Element of M;

assume A1: ( x is left_complementable & x is right_add-cancelable ) ;

existence

ex b_{1} being Element of M st b_{1} + x = 0. M
by A1, Def10;

uniqueness

for b_{1}, b_{2} being Element of M st b_{1} + x = 0. M & b_{2} + x = 0. M holds

b_{1} = b_{2}
by A1, Def4;

end;
let x be Element of M;

assume A1: ( x is left_complementable & x is right_add-cancelable ) ;

existence

ex b

uniqueness

for b

b

:: 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_{3} being Element of M holds

( b_{3} = - x iff b_{3} + x = 0. M );

for M being addLoopStr

for x being Element of M st x is left_complementable & x is right_add-cancelable holds

for b

( b

definition
end;

:: deftheorem defines - ALGSTR_0:def 14 :

for V being addLoopStr

for v, w being Element of V holds v - w = v + (- w);

for V being addLoopStr

for v, w being Element of V holds v - w = v + (- w);

definition

let M be addLoopStr ;

end;
attr M is left_complementable means :Def15: :: ALGSTR_0:def 15

for x being Element of M holds x is left_complementable ;

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 ;

for x being Element of M holds x is right_complementable ;

:: 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 );

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 );

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 ;

end;
attr M is complementable means :Def17: :: ALGSTR_0:def 17

( M is right_complementable & M is left_complementable );

( M is right_complementable & M is left_complementable );

:: deftheorem Def17 defines complementable ALGSTR_0:def 17 :

for M being addLoopStr holds

( M is complementable iff ( M is right_complementable & M is left_complementable ) );

for M being addLoopStr holds

( M is complementable iff ( M is right_complementable & M is left_complementable ) );

registration

coherence

for b_{1} being addLoopStr st b_{1} is right_complementable & b_{1} is left_complementable holds

b_{1} is complementable
by Def17;

coherence

for b_{1} being addLoopStr st b_{1} is complementable holds

( b_{1} is right_complementable & b_{1} is left_complementable )
by Def17;

end;
for b

b

coherence

for b

( b

registration

existence

ex b_{1} being addLoopStr st

( b_{1} is complementable & b_{1} is add-cancelable & b_{1} is strict & b_{1} is 1 -element )

end;
ex b

( b

proof end;

registration

let M be left_complementable addLoopStr ;

coherence

for b_{1} being Element of M holds b_{1} is left_complementable
by Def15;

end;
coherence

for b

registration

let M be right_complementable addLoopStr ;

coherence

for b_{1} being Element of M holds b_{1} is right_complementable
by Def16;

end;
coherence

for b

begin

definition

attr c_{1} is strict ;

struct multMagma -> 1-sorted ;

aggr multMagma(# carrier, multF #) -> multMagma ;

sel multF c_{1} -> BinOp of the carrier of c_{1};

end;
struct multMagma -> 1-sorted ;

aggr multMagma(# carrier, multF #) -> multMagma ;

sel multF c

registration
end;

registration
end;

registration
end;

definition
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);

for M being multMagma

for x, y being Element of M holds x * y = the multF of M . (x,y);

registration
end;

registration
end;

definition

let M be multMagma ;

let x be Element of M;

end;
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;

for y, z being Element of M st x * y = x * z holds

y = z;

attr x is right_mult-cancelable means :Def21: :: ALGSTR_0:def 21

for y, z being Element of M st y * x = z * x holds

y = z;

for y, z being Element of M st y * x = z * x holds

y = z;

:: 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 );

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 Def21 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 );

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;

end;
let x be Element of M;

attr x is mult-cancelable means :Def22: :: ALGSTR_0:def 22

( x is right_mult-cancelable & x is left_mult-cancelable );

( x is right_mult-cancelable & x is left_mult-cancelable );

:: deftheorem Def22 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 ) );

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 ;

for b_{1} being Element of M st b_{1} is right_mult-cancelable & b_{1} is left_mult-cancelable holds

b_{1} is mult-cancelable
by Def22;

for b_{1} being Element of M st b_{1} is mult-cancelable holds

( b_{1} is right_mult-cancelable & b_{1} is left_mult-cancelable )
by Def22;

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

coherence for b

b

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

coherence for b

( b

definition

let M be multMagma ;

end;
attr M is left_mult-cancelable means :Def23: :: ALGSTR_0:def 23

for x being Element of M holds x is left_mult-cancelable ;

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 ;

for x being Element of M holds x is right_mult-cancelable ;

:: 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 );

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 );

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 ;

end;
attr M is mult-cancelable means :Def25: :: ALGSTR_0:def 25

( M is left_mult-cancelable & M is right_mult-cancelable );

( M is left_mult-cancelable & M is right_mult-cancelable );

:: deftheorem Def25 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 ) );

for M being multMagma holds

( M is mult-cancelable iff ( M is left_mult-cancelable & M is right_mult-cancelable ) );

registration

coherence

for b_{1} being multMagma st b_{1} is right_mult-cancelable & b_{1} is left_mult-cancelable holds

b_{1} is mult-cancelable
by Def25;

coherence

for b_{1} being multMagma st b_{1} is mult-cancelable holds

( b_{1} is right_mult-cancelable & b_{1} is left_mult-cancelable )
by Def25;

end;
for b

b

coherence

for b

( b

registration

existence

ex b_{1} being multMagma st

( b_{1} is mult-cancelable & b_{1} is strict & b_{1} is 1 -element )

end;
ex b

( b

proof end;

registration

let M be left_mult-cancelable multMagma ;

coherence

for b_{1} being Element of M holds b_{1} is left_mult-cancelable
by Def23;

end;
coherence

for b

registration

let M be right_mult-cancelable multMagma ;

coherence

for b_{1} being Element of M holds b_{1} is right_mult-cancelable
by Def24;

end;
coherence

for b

definition

attr c_{1} is strict ;

struct multLoopStr -> OneStr , multMagma ;

aggr multLoopStr(# carrier, multF, OneF #) -> multLoopStr ;

end;
struct multLoopStr -> OneStr , multMagma ;

aggr multLoopStr(# carrier, multF, OneF #) -> multLoopStr ;

registration

let D be non empty set ;

let o be BinOp of D;

let d be Element of D;

coherence

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

end;
let o be BinOp of D;

let d be Element of D;

coherence

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

registration

let T be trivial set ;

let f be BinOp of T;

let t be Element of T;

coherence

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

end;
let f be BinOp of T;

let t be Element of T;

coherence

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

registration

let N be non trivial set ;

let b be BinOp of N;

let m be Element of N;

coherence

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

end;
let b be BinOp of N;

let m be Element of N;

coherence

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

:: deftheorem defines Trivial-multLoopStr ALGSTR_0:def 26 :

Trivial-multLoopStr = multLoopStr(# 1,op2,op0 #);

Trivial-multLoopStr = multLoopStr(# 1,op2,op0 #);

registration
end;

registration
end;

:: deftheorem Def27 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 );

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 );

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;

end;
let x be Element of M;

attr x is invertible means :Def29: :: ALGSTR_0:def 29

( x is right_invertible & x is left_invertible );

( x is right_invertible & x is left_invertible );

:: deftheorem Def29 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 ) );

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 ;

coherence

for b_{1} being Element of M st b_{1} is right_invertible & b_{1} is left_invertible holds

b_{1} is invertible
by Def29;

coherence

for b_{1} being Element of M st b_{1} is invertible holds

( b_{1} is right_invertible & b_{1} is left_invertible )
by Def29;

end;
coherence

for b

b

coherence

for b

( b

definition

let M be multLoopStr ;

let x be Element of M;

assume A1: ( x is left_invertible & x is right_mult-cancelable ) ;

existence

ex b_{1} being Element of M st b_{1} * x = 1. M
by A1, Def27;

uniqueness

for b_{1}, b_{2} being Element of M st b_{1} * x = 1. M & b_{2} * x = 1. M holds

b_{1} = b_{2}
by A1, Def21;

end;
let x be Element of M;

assume A1: ( x is left_invertible & x is right_mult-cancelable ) ;

existence

ex b

uniqueness

for b

b

:: 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_{3} being Element of M holds

( b_{3} = / x iff b_{3} * x = 1. M );

for M being multLoopStr

for x being Element of M st x is left_invertible & x is right_mult-cancelable holds

for b

( b

definition

let M be multLoopStr ;

end;
attr M is left_invertible means :Def31: :: ALGSTR_0:def 31

for x being Element of M holds x is left_invertible ;

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 ;

for x being Element of M holds x is right_invertible ;

:: 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 );

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 );

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 ;

end;
attr M is invertible means :Def33: :: ALGSTR_0:def 33

( M is right_invertible & M is left_invertible );

( M is right_invertible & M is left_invertible );

:: deftheorem Def33 defines invertible ALGSTR_0:def 33 :

for M being multLoopStr holds

( M is invertible iff ( M is right_invertible & M is left_invertible ) );

for M being multLoopStr holds

( M is invertible iff ( M is right_invertible & M is left_invertible ) );

registration

coherence

for b_{1} being multLoopStr st b_{1} is right_invertible & b_{1} is left_invertible holds

b_{1} is invertible
by Def33;

coherence

for b_{1} being multLoopStr st b_{1} is invertible holds

( b_{1} is right_invertible & b_{1} is left_invertible )
by Def33;

end;
for b

b

coherence

for b

( b

registration
end;

registration

existence

ex b_{1} being multLoopStr st

( b_{1} is invertible & b_{1} is mult-cancelable & b_{1} is strict & b_{1} is 1 -element )

end;
ex b

( b

proof end;

registration

let M be left_invertible multLoopStr ;

coherence

for b_{1} being Element of M holds b_{1} is left_invertible
by Def31;

end;
coherence

for b

registration

let M be right_invertible multLoopStr ;

coherence

for b_{1} being Element of M holds b_{1} is right_invertible
by Def32;

end;
coherence

for b

begin

definition

attr c_{1} is strict ;

struct multLoopStr_0 -> multLoopStr , ZeroOneStr ;

aggr multLoopStr_0(# carrier, multF, ZeroF, OneF #) -> multLoopStr_0 ;

end;
struct multLoopStr_0 -> multLoopStr , ZeroOneStr ;

aggr multLoopStr_0(# carrier, multF, ZeroF, OneF #) -> multLoopStr_0 ;

registration

let D be non empty set ;

let o be BinOp of D;

let d, e be Element of D;

coherence

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

end;
let o be BinOp of D;

let d, e be Element of D;

coherence

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

registration

let T be trivial set ;

let f be BinOp of T;

let s, t be Element of T;

coherence

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

end;
let f be BinOp of T;

let s, t be Element of T;

coherence

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

registration

let N be non trivial set ;

let b be BinOp of N;

let m, n be Element of N;

coherence

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

end;
let b be BinOp of N;

let m, n be Element of N;

coherence

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

definition

multLoopStr_0(# 1,op2,op0,op0 #) is multLoopStr_0 ;

end;

func Trivial-multLoopStr_0 -> multLoopStr_0 equals :: ALGSTR_0:def 34

multLoopStr_0(# 1,op2,op0,op0 #);

coherence multLoopStr_0(# 1,op2,op0,op0 #);

multLoopStr_0(# 1,op2,op0,op0 #) is multLoopStr_0 ;

:: deftheorem defines Trivial-multLoopStr_0 ALGSTR_0:def 34 :

Trivial-multLoopStr_0 = multLoopStr_0(# 1,op2,op0,op0 #);

Trivial-multLoopStr_0 = multLoopStr_0(# 1,op2,op0,op0 #);

registration
end;

registration
end;

definition

let M be multLoopStr_0 ;

let x be Element of M;

( ( x is left_invertible & x is right_mult-cancelable implies ex b_{1} being Element of M st b_{1} * x = 1. M ) & ( ( not x is left_invertible or not x is right_mult-cancelable ) implies ex b_{1} being Element of M st b_{1} = 0. M ) )
by Def27;

uniqueness

for b_{1}, b_{2} being Element of M holds

( ( x is left_invertible & x is right_mult-cancelable & b_{1} * x = 1. M & b_{2} * x = 1. M implies b_{1} = b_{2} ) & ( ( not x is left_invertible or not x is right_mult-cancelable ) & b_{1} = 0. M & b_{2} = 0. M implies b_{1} = b_{2} ) )
by Def21;

consistency

for b_{1} being Element of M holds verum
;

end;
let x be Element of M;

func x " -> Element of M means :: ALGSTR_0:def 35

it * x = 1. M if ( x is left_invertible & x is right_mult-cancelable )

otherwise it = 0. M;

existence it * x = 1. M if ( x is left_invertible & x is right_mult-cancelable )

otherwise it = 0. M;

( ( x is left_invertible & x is right_mult-cancelable implies ex b

uniqueness

for b

( ( x is left_invertible & x is right_mult-cancelable & b

consistency

for b

:: deftheorem defines " ALGSTR_0:def 35 :

for M being multLoopStr_0

for x, b_{3} being Element of M holds

( ( x is left_invertible & x is right_mult-cancelable implies ( b_{3} = x " iff b_{3} * x = 1. M ) ) & ( ( not x is left_invertible or not x is right_mult-cancelable ) implies ( b_{3} = x " iff b_{3} = 0. M ) ) );

for M being multLoopStr_0

for x, b

( ( x is left_invertible & x is right_mult-cancelable implies ( b

definition

let M be multLoopStr_0 ;

end;
attr M is almost_left_cancelable means :: ALGSTR_0:def 36

for x being Element of M st x <> 0. M holds

x is left_mult-cancelable ;

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 37

for x being Element of M st x <> 0. M holds

x is right_mult-cancelable ;

for x being Element of M st x <> 0. M holds

x is right_mult-cancelable ;

:: deftheorem defines almost_left_cancelable ALGSTR_0:def 36 :

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 );

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 37 :

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 );

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 ;

end;
attr M is almost_cancelable means :Def38: :: ALGSTR_0:def 38

( M is almost_left_cancelable & M is almost_right_cancelable );

( M is almost_left_cancelable & M is almost_right_cancelable );

:: deftheorem Def38 defines almost_cancelable ALGSTR_0:def 38 :

for M being multLoopStr_0 holds

( M is almost_cancelable iff ( M is almost_left_cancelable & M is almost_right_cancelable ) );

for M being multLoopStr_0 holds

( M is almost_cancelable iff ( M is almost_left_cancelable & M is almost_right_cancelable ) );

registration

coherence

for b_{1} being multLoopStr_0 st b_{1} is almost_right_cancelable & b_{1} is almost_left_cancelable holds

b_{1} is almost_cancelable
by Def38;

coherence

for b_{1} being multLoopStr_0 st b_{1} is almost_cancelable holds

( b_{1} is almost_right_cancelable & b_{1} is almost_left_cancelable )
by Def38;

end;
for b

b

coherence

for b

( b

registration

existence

ex b_{1} being multLoopStr_0 st

( b_{1} is almost_cancelable & b_{1} is strict & b_{1} is 1 -element )

end;
ex b

( b

proof end;

definition

let M be multLoopStr_0 ;

end;
attr M is almost_left_invertible means :: ALGSTR_0:def 39

for x being Element of M st x <> 0. M holds

x is left_invertible ;

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 40

for x being Element of M st x <> 0. M holds

x is right_invertible ;

for x being Element of M st x <> 0. M holds

x is right_invertible ;

:: deftheorem defines almost_left_invertible ALGSTR_0:def 39 :

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 );

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 40 :

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 );

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 ;

end;
attr M is almost_invertible means :Def41: :: ALGSTR_0:def 41

( M is almost_right_invertible & M is almost_left_invertible );

( M is almost_right_invertible & M is almost_left_invertible );

:: deftheorem Def41 defines almost_invertible ALGSTR_0:def 41 :

for M being multLoopStr_0 holds

( M is almost_invertible iff ( M is almost_right_invertible & M is almost_left_invertible ) );

for M being multLoopStr_0 holds

( M is almost_invertible iff ( M is almost_right_invertible & M is almost_left_invertible ) );

registration

coherence

for b_{1} being multLoopStr_0 st b_{1} is almost_right_invertible & b_{1} is almost_left_invertible holds

b_{1} is almost_invertible
by Def41;

coherence

for b_{1} being multLoopStr_0 st b_{1} is almost_invertible holds

( b_{1} is almost_right_invertible & b_{1} is almost_left_invertible )
by Def41;

end;
for b

b

coherence

for b

( b

registration

existence

ex b_{1} being multLoopStr_0 st

( b_{1} is almost_invertible & b_{1} is almost_cancelable & b_{1} is strict & b_{1} is 1 -element )

end;
ex b

( b

proof end;

begin

definition

attr c_{1} is strict ;

struct doubleLoopStr -> addLoopStr , multLoopStr_0 ;

aggr doubleLoopStr(# carrier, addF, multF, OneF, ZeroF #) -> doubleLoopStr ;

end;
struct doubleLoopStr -> addLoopStr , multLoopStr_0 ;

aggr doubleLoopStr(# carrier, addF, multF, OneF, ZeroF #) -> doubleLoopStr ;

registration

let D be non empty set ;

let o, o1 be BinOp of D;

let d, e be Element of D;

coherence

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

end;
let o, o1 be BinOp of D;

let d, e be Element of D;

coherence

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

registration

let T be trivial set ;

let f, f1 be BinOp of T;

let s, t be Element of T;

coherence

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

end;
let f, f1 be BinOp of T;

let s, t be Element of T;

coherence

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

registration

let N be non trivial set ;

let b, b1 be BinOp of N;

let m, n be Element of N;

coherence

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

end;
let b, b1 be BinOp of N;

let m, n be Element of N;

coherence

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

definition

doubleLoopStr(# 1,op2,op2,op0,op0 #) is doubleLoopStr ;

end;

func Trivial-doubleLoopStr -> doubleLoopStr equals :: ALGSTR_0:def 42

doubleLoopStr(# 1,op2,op2,op0,op0 #);

coherence doubleLoopStr(# 1,op2,op2,op0,op0 #);

doubleLoopStr(# 1,op2,op2,op0,op0 #) is doubleLoopStr ;

:: deftheorem defines Trivial-doubleLoopStr ALGSTR_0:def 42 :

Trivial-doubleLoopStr = doubleLoopStr(# 1,op2,op2,op0,op0 #);

Trivial-doubleLoopStr = doubleLoopStr(# 1,op2,op2,op0,op0 #);

registration
end;

registration
end;