set f = maxnorm ;

A1: for a, b being Element of [.0,1.] holds maxnorm . (a,b) = maxnorm . (b,a)

maxnorm . (a,b) <= maxnorm . (c,d)

A1: for a, b being Element of [.0,1.] holds maxnorm . (a,b) = maxnorm . (b,a)

proof

DD:
for a, b, c being Element of [.0,1.] holds maxnorm . ((maxnorm . (a,b)),c) = maxnorm . (a,(maxnorm . (b,c)))
let a, b be Element of [.0,1.]; :: thesis: maxnorm . (a,b) = maxnorm . (b,a)

maxnorm . (a,b) = max (a,b) by MaxDef

.= maxnorm . (b,a) by MaxDef ;

hence maxnorm . (a,b) = maxnorm . (b,a) ; :: thesis: verum

end;maxnorm . (a,b) = max (a,b) by MaxDef

.= maxnorm . (b,a) by MaxDef ;

hence maxnorm . (a,b) = maxnorm . (b,a) ; :: thesis: verum

proof

D1:
for a, b, c, d being Element of [.0,1.] st a <= c & b <= d holds
let a, b, c be Element of [.0,1.]; :: thesis: 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))) ; :: thesis: verum

end;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))) ; :: thesis: verum

maxnorm . (a,b) <= maxnorm . (c,d)

proof

for a being Element of [.0,1.] holds maxnorm . (a,0) = a
let a, b, c, d be Element of [.0,1.]; :: thesis: ( a <= c & b <= d implies maxnorm . (a,b) <= maxnorm . (c,d) )

assume ( a <= c & b <= d ) ; :: thesis: 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; :: thesis: verum

end;assume ( a <= c & b <= d ) ; :: thesis: 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; :: thesis: verum

proof

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; :: thesis: verum
let a be Element of [.0,1.]; :: thesis: maxnorm . (a,0) = a

T1: 0 in [.0,1.] by XXREAL_1:1;

a >= 0 by XXREAL_1:1;

then max (a,0) = a by XXREAL_0:def 10;

hence maxnorm . (a,0) = a by MaxDef, T1; :: thesis: verum

end;T1: 0 in [.0,1.] by XXREAL_1:1;

a >= 0 by XXREAL_1:1;

then max (a,0) = a by XXREAL_0:def 10;

hence maxnorm . (a,0) = a by MaxDef, T1; :: thesis: verum