:: Basic Algebraic Structures
:: 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;
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
(# 1,
op2
#);
coherence
addMagma
(# 1,
op2
#) is
addMagma
;
end;
::
deftheorem
defines
Trivial-addMagma
ALGSTR_0:def 2 :
Trivial-addMagma
=
addMagma
(# 1,
op2
#);
registration
cluster
Trivial-addMagma
->
1
-element
strict
;
coherence
(
Trivial-addMagma
is 1
-element
&
Trivial-addMagma
is
strict
)
by
CARD_1:49
;
end;
registration
cluster
1
-element
strict
for
addMagma
;
existence
ex
b
1
being
addMagma
st
(
b
1
is
strict
&
b
1
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
:
Def4
:
:: 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
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
);
definition
let
M
be
addMagma
;
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
);
end;
::
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
) );
registration
let
M
be
addMagma
;
cluster
left_add-cancelable
right_add-cancelable
->
add-cancelable
for
Element
of the
carrier
of
M
;
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
;
cluster
add-cancelable
->
left_add-cancelable
right_add-cancelable
for
Element
of the
carrier
of
M
;
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;
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
:
Def8
:
:: ALGSTR_0:def 8
(
M
is
right_add-cancelable
&
M
is
left_add-cancelable
);
end;
::
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
) );
registration
cluster
left_add-cancelable
right_add-cancelable
->
add-cancelable
for
addMagma
;
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
;
cluster
add-cancelable
->
left_add-cancelable
right_add-cancelable
for
addMagma
;
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;
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
1
being
addMagma
st
(
b
1
is
add-cancelable
&
b
1
is
strict
&
b
1
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
1
being
Element
of
M
holds
b
1
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
1
being
Element
of
M
holds
b
1
is
right_add-cancelable
by
Def7
;
end;
definition
attr
c
1
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
(# 1,
op2
,
op0
#);
coherence
addLoopStr
(# 1,
op2
,
op0
#) is
addLoopStr
;
end;
::
deftheorem
defines
Trivial-addLoopStr
ALGSTR_0:def 9 :
Trivial-addLoopStr
=
addLoopStr
(# 1,
op2
,
op0
#);
registration
cluster
Trivial-addLoopStr
->
1
-element
strict
;
coherence
(
Trivial-addLoopStr
is 1
-element
&
Trivial-addLoopStr
is
strict
)
by
CARD_1:49
;
end;
registration
cluster
1
-element
strict
for
addLoopStr
;
existence
ex
b
1
being
addLoopStr
st
(
b
1
is
strict
&
b
1
is 1
-element
)
proof
end;
end;
definition
let
M
be
addLoopStr
;
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
;
attr
x
is
right_complementable
means
:: ALGSTR_0:def 11
ex
y
being
Element
of
M
st
x
+
y
=
0.
M
;
end;
::
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
);
::
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
:
Def12
:
:: ALGSTR_0:def 12
(
x
is
right_complementable
&
x
is
left_complementable
);
end;
::
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
) );
registration
let
M
be
addLoopStr
;
cluster
left_complementable
right_complementable
->
complementable
for
Element
of the
carrier
of
M
;
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
;
cluster
complementable
->
left_complementable
right_complementable
for
Element
of the
carrier
of
M
;
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;
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
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;
::
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
);
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
:
Def17
:
:: ALGSTR_0:def 17
(
M
is
right_complementable
&
M
is
left_complementable
);
end;
::
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
) );
registration
cluster
left_complementable
right_complementable
->
complementable
for
addLoopStr
;
coherence
for
b
1
being
addLoopStr
st
b
1
is
right_complementable
&
b
1
is
left_complementable
holds
b
1
is
complementable
by
Def17
;
cluster
complementable
->
left_complementable
right_complementable
for
addLoopStr
;
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;
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
1
being
addLoopStr
st
(
b
1
is
complementable
&
b
1
is
add-cancelable
&
b
1
is
strict
&
b
1
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
1
being
Element
of
M
holds
b
1
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
1
being
Element
of
M
holds
b
1
is
right_complementable
by
Def16
;
end;
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;
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
(# 1,
op2
#);
coherence
multMagma
(# 1,
op2
#) is
multMagma
;
end;
::
deftheorem
defines
Trivial-multMagma
ALGSTR_0:def 19 :
Trivial-multMagma
=
multMagma
(# 1,
op2
#);
registration
cluster
Trivial-multMagma
->
1
-element
strict
;
coherence
(
Trivial-multMagma
is 1
-element
&
Trivial-multMagma
is
strict
)
by
CARD_1:49
;
end;
registration
cluster
1
-element
strict
for
multMagma
;
existence
ex
b
1
being
multMagma
st
(
b
1
is
strict
&
b
1
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
:
Def21
:
:: 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
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
);
definition
let
M
be
multMagma
;
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
);
end;
::
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
) );
registration
let
M
be
multMagma
;
cluster
left_mult-cancelable
right_mult-cancelable
->
mult-cancelable
for
Element
of the
carrier
of
M
;
coherence
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
;
cluster
mult-cancelable
->
left_mult-cancelable
right_mult-cancelable
for
Element
of the
carrier
of
M
;
coherence
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;
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
:
Def25
:
:: ALGSTR_0:def 25
(
M
is
left_mult-cancelable
&
M
is
right_mult-cancelable
);
end;
::
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
) );
registration
cluster
left_mult-cancelable
right_mult-cancelable
->
mult-cancelable
for
multMagma
;
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
;
cluster
mult-cancelable
->
left_mult-cancelable
right_mult-cancelable
for
multMagma
;
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;
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
1
being
multMagma
st
(
b
1
is
mult-cancelable
&
b
1
is
strict
&
b
1
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
1
being
Element
of
M
holds
b
1
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
1
being
Element
of
M
holds
b
1
is
right_mult-cancelable
by
Def24
;
end;
definition
attr
c
1
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
(# 1,
op2
,
op0
#);
coherence
multLoopStr
(# 1,
op2
,
op0
#) is
multLoopStr
;
end;
::
deftheorem
defines
Trivial-multLoopStr
ALGSTR_0:def 26 :
Trivial-multLoopStr
=
multLoopStr
(# 1,
op2
,
op0
#);
registration
cluster
Trivial-multLoopStr
->
1
-element
strict
;
coherence
(
Trivial-multLoopStr
is 1
-element
&
Trivial-multLoopStr
is
strict
)
by
CARD_1:49
;
end;
registration
cluster
1
-element
strict
for
multLoopStr
;
existence
ex
b
1
being
multLoopStr
st
(
b
1
is
strict
&
b
1
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
:
Def27
:
:: 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
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
);
::
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
:
Def29
:
:: ALGSTR_0:def 29
(
x
is
right_invertible
&
x
is
left_invertible
);
end;
::
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
) );
registration
let
M
be
multLoopStr
;
cluster
left_invertible
right_invertible
->
invertible
for
Element
of the
carrier
of
M
;
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
;
cluster
invertible
->
left_invertible
right_invertible
for
Element
of the
carrier
of
M
;
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;
definition
let
M
be
multLoopStr
;
let
x
be
Element
of
M
;
assume
A1
: (
x
is
left_invertible
&
x
is
right_mult-cancelable
) ;
func
/
x
->
Element
of
M
means
:: ALGSTR_0:def 30
it
*
x
=
1.
M
;
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;
::
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
);
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
:
Def33
:
:: ALGSTR_0:def 33
(
M
is
right_invertible
&
M
is
left_invertible
);
end;
::
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
) );
registration
cluster
left_invertible
right_invertible
->
invertible
for
multLoopStr
;
coherence
for
b
1
being
multLoopStr
st
b
1
is
right_invertible
&
b
1
is
left_invertible
holds
b
1
is
invertible
by
Def33
;
cluster
invertible
->
left_invertible
right_invertible
for
multLoopStr
;
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;
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
1
being
multLoopStr
st
(
b
1
is
invertible
&
b
1
is
mult-cancelable
&
b
1
is
strict
&
b
1
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
1
being
Element
of
M
holds
b
1
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
1
being
Element
of
M
holds
b
1
is
right_invertible
by
Def32
;
end;
begin
definition
attr
c
1
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
(# 1,
op2
,
op0
,
op0
#);
coherence
multLoopStr_0
(# 1,
op2
,
op0
,
op0
#) is
multLoopStr_0
;
end;
::
deftheorem
defines
Trivial-multLoopStr_0
ALGSTR_0:def 34 :
Trivial-multLoopStr_0
=
multLoopStr_0
(# 1,
op2
,
op0
,
op0
#);
registration
cluster
Trivial-multLoopStr_0
->
1
-element
strict
;
coherence
(
Trivial-multLoopStr_0
is 1
-element
&
Trivial-multLoopStr_0
is
strict
)
by
CARD_1:49
;
end;
registration
cluster
1
-element
strict
for
multLoopStr_0
;
existence
ex
b
1
being
multLoopStr_0
st
(
b
1
is
strict
&
b
1
is 1
-element
)
proof
end;
end;
definition
let
M
be
multLoopStr_0
;
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
( (
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;
::
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
) ) );
definition
let
M
be
multLoopStr_0
;
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
;
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
;
end;
::
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
);
::
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
);
definition
let
M
be
multLoopStr_0
;
attr
M
is
almost_cancelable
means
:
Def38
:
:: ALGSTR_0:def 38
(
M
is
almost_left_cancelable
&
M
is
almost_right_cancelable
);
end;
::
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
) );
registration
cluster
almost_left_cancelable
almost_right_cancelable
->
almost_cancelable
for
multLoopStr_0
;
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
;
cluster
almost_cancelable
->
almost_left_cancelable
almost_right_cancelable
for
multLoopStr_0
;
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;
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
1
being
multLoopStr_0
st
(
b
1
is
almost_cancelable
&
b
1
is
strict
&
b
1
is 1
-element
)
proof
end;
end;
definition
let
M
be
multLoopStr_0
;
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
;
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
;
end;
::
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
);
::
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
);
definition
let
M
be
multLoopStr_0
;
attr
M
is
almost_invertible
means
:
Def41
:
:: ALGSTR_0:def 41
(
M
is
almost_right_invertible
&
M
is
almost_left_invertible
);
end;
::
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
) );
registration
cluster
almost_left_invertible
almost_right_invertible
->
almost_invertible
for
multLoopStr_0
;
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
;
cluster
almost_invertible
->
almost_left_invertible
almost_right_invertible
for
multLoopStr_0
;
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;
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
1
being
multLoopStr_0
st
(
b
1
is
almost_invertible
&
b
1
is
almost_cancelable
&
b
1
is
strict
&
b
1
is 1
-element
)
proof
end;
end;
begin
definition
attr
c
1
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 42
doubleLoopStr
(# 1,
op2
,
op2
,
op0
,
op0
#);
coherence
doubleLoopStr
(# 1,
op2
,
op2
,
op0
,
op0
#) is
doubleLoopStr
;
end;
::
deftheorem
defines
Trivial-doubleLoopStr
ALGSTR_0:def 42 :
Trivial-doubleLoopStr
=
doubleLoopStr
(# 1,
op2
,
op2
,
op0
,
op0
#);
registration
cluster
Trivial-doubleLoopStr
->
1
-element
strict
;
coherence
(
Trivial-doubleLoopStr
is 1
-element
&
Trivial-doubleLoopStr
is
strict
)
by
CARD_1:49
;
end;
registration
cluster
1
-element
strict
for
doubleLoopStr
;
existence
ex
b
1
being
doubleLoopStr
st
(
b
1
is
strict
&
b
1
is 1
-element
)
proof
end;
end;