set f = maxnorm ;
A1:
for a, b being Element of [.0,1.] holds maxnorm . (a,b) = maxnorm . (b,a)
DD:
for a, b, c being Element of [.0,1.] holds maxnorm . ((maxnorm . (a,b)),c) = maxnorm . (a,(maxnorm . (b,c)))
proof
let a,
b,
c be
Element of
[.0,1.];
maxnorm . ((maxnorm . (a,b)),c) = maxnorm . (a,(maxnorm . (b,c)))
a2:
(
max (
a,
b)
= a or
max (
a,
b)
= b )
by XXREAL_0:16;
a3:
(
max (
b,
c)
= b or
max (
b,
c)
= c )
by XXREAL_0:16;
maxnorm . (
(maxnorm . (a,b)),
c) =
maxnorm . (
(max (a,b)),
c)
by MaxDef
.=
max (
(max (a,b)),
c)
by MaxDef, a2
.=
max (
a,
(max (b,c)))
by XXREAL_0:34
.=
maxnorm . (
a,
(max (b,c)))
by a3, MaxDef
.=
maxnorm . (
a,
(maxnorm . (b,c)))
by MaxDef
;
hence
maxnorm . (
(maxnorm . (a,b)),
c)
= maxnorm . (
a,
(maxnorm . (b,c)))
;
verum
end;
D1:
for a, b, c, d being Element of [.0,1.] st a <= c & b <= d holds
maxnorm . (a,b) <= maxnorm . (c,d)
proof
let a,
b,
c,
d be
Element of
[.0,1.];
( a <= c & b <= d implies maxnorm . (a,b) <= maxnorm . (c,d) )
assume
(
a <= c &
b <= d )
;
maxnorm . (a,b) <= maxnorm . (c,d)
then
max (
a,
b)
<= max (
c,
d)
by XXREAL_0:26;
then
max (
a,
b)
<= maxnorm . (
c,
d)
by MaxDef;
hence
maxnorm . (
a,
b)
<= maxnorm . (
c,
d)
by MaxDef;
verum
end;
for a being Element of [.0,1.] holds maxnorm . (a,0) = a
hence
( maxnorm is commutative & maxnorm is associative & maxnorm is monotonic & maxnorm is with-0-identity )
by BINOP_1:def 2, BINOP_1:def 3, A1, DD, D1; verum