set f = minnorm ;

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

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

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

proof

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

minnorm . (a,b) = min (a,b) by MinDef

.= minnorm . (b,a) by MinDef ;

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

end;minnorm . (a,b) = min (a,b) by MinDef

.= minnorm . (b,a) by MinDef ;

hence minnorm . (a,b) = minnorm . (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: 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))) ; :: thesis: verum

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

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

proof

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

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

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

proof

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

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

a <= 1 by XXREAL_1:1;

then min (a,1) = a by XXREAL_0:def 9;

hence minnorm . (a,1) = a by MinDef, T1; :: thesis: verum

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

a <= 1 by XXREAL_1:1;

then min (a,1) = a by XXREAL_0:def 9;

hence minnorm . (a,1) = a by MinDef, T1; :: thesis: verum