set f = minnorm ;
A1:
for a, b being Element of [.0,1.] holds minnorm . (a,b) = minnorm . (b,a)
AA:
for a, b, c being Element of [.0,1.] holds minnorm . ((minnorm . (a,b)),c) = minnorm . (a,(minnorm . (b,c)))
proof
let a,
b,
c be
Element of
[.0,1.];
minnorm . ((minnorm . (a,b)),c) = minnorm . (a,(minnorm . (b,c)))
a2:
(
min (
a,
b)
= a or
min (
a,
b)
= b )
by XXREAL_0:15;
a3:
(
min (
b,
c)
= b or
min (
b,
c)
= c )
by XXREAL_0:15;
minnorm . (
(minnorm . (a,b)),
c) =
minnorm . (
(min (a,b)),
c)
by MinDef
.=
min (
(min (a,b)),
c)
by MinDef, a2
.=
min (
a,
(min (b,c)))
by XXREAL_0:33
.=
minnorm . (
a,
(min (b,c)))
by a3, MinDef
.=
minnorm . (
a,
(minnorm . (b,c)))
by MinDef
;
hence
minnorm . (
(minnorm . (a,b)),
c)
= minnorm . (
a,
(minnorm . (b,c)))
;
verum
end;
D1:
for a, b, c, d being Element of [.0,1.] st a <= c & b <= d holds
minnorm . (a,b) <= minnorm . (c,d)
proof
let a,
b,
c,
d be
Element of
[.0,1.];
( a <= c & b <= d implies minnorm . (a,b) <= minnorm . (c,d) )
assume
(
a <= c &
b <= d )
;
minnorm . (a,b) <= minnorm . (c,d)
then
min (
a,
b)
<= min (
c,
d)
by XXREAL_0:18;
then
min (
a,
b)
<= minnorm . (
c,
d)
by MinDef;
hence
minnorm . (
a,
b)
<= minnorm . (
c,
d)
by MinDef;
verum
end;
for a being Element of [.0,1.] holds minnorm . (a,1) = a
hence
( minnorm is commutative & minnorm is associative & minnorm is monotonic & minnorm is with-1-identity )
by BINOP_1:def 2, BINOP_1:def 3, A1, AA, D1; verum