set f = Lukasiewicz_norm ;

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

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

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

proof

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

Lukasiewicz_norm . (a,b) = max (0,((a + b) - 1)) by LukNorm

.= Lukasiewicz_norm . (b,a) by LukNorm ;

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

end;Lukasiewicz_norm . (a,b) = max (0,((a + b) - 1)) by LukNorm

.= Lukasiewicz_norm . (b,a) by LukNorm ;

hence Lukasiewicz_norm . (a,b) = Lukasiewicz_norm . (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: Lukasiewicz_norm . ((Lukasiewicz_norm . (a,b)),c) = Lukasiewicz_norm . (a,(Lukasiewicz_norm . (b,c)))

set B = max (0,((a + b) - 1));

set C = max (0,((b + c) - 1));

G1: max (0,((a + b) - 1)) in [.0,1.] by Lemma2;

G2: max (0,((b + c) - 1)) in [.0,1.] by Lemma2;

Lukasiewicz_norm . ((Lukasiewicz_norm . (a,b)),c) = Lukasiewicz_norm . ((max (0,((a + b) - 1))),c) by LukNorm

.= max (0,(((max (0,((a + b) - 1))) + c) - 1)) by LukNorm, G1

.= max (0,((a + (max (0,((b + c) - 1)))) - 1)) by Lemma3

.= Lukasiewicz_norm . (a,(max (0,((b + c) - 1)))) by LukNorm, G2

.= Lukasiewicz_norm . (a,(Lukasiewicz_norm . (b,c))) by LukNorm ;

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

end;set B = max (0,((a + b) - 1));

set C = max (0,((b + c) - 1));

G1: max (0,((a + b) - 1)) in [.0,1.] by Lemma2;

G2: max (0,((b + c) - 1)) in [.0,1.] by Lemma2;

Lukasiewicz_norm . ((Lukasiewicz_norm . (a,b)),c) = Lukasiewicz_norm . ((max (0,((a + b) - 1))),c) by LukNorm

.= max (0,(((max (0,((a + b) - 1))) + c) - 1)) by LukNorm, G1

.= max (0,((a + (max (0,((b + c) - 1)))) - 1)) by Lemma3

.= Lukasiewicz_norm . (a,(max (0,((b + c) - 1)))) by LukNorm, G2

.= Lukasiewicz_norm . (a,(Lukasiewicz_norm . (b,c))) by LukNorm ;

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

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

proof

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

assume ( a <= c & b <= d ) ; :: thesis: Lukasiewicz_norm . (a,b) <= Lukasiewicz_norm . (c,d)

then a + b <= c + d by XREAL_1:7;

then (a + b) - 1 <= (c + d) - 1 by XREAL_1:9;

then max (0,((a + b) - 1)) <= max (0,((c + d) - 1)) by XXREAL_0:26;

then max (0,((a + b) - 1)) <= Lukasiewicz_norm . (c,d) by LukNorm;

hence Lukasiewicz_norm . (a,b) <= Lukasiewicz_norm . (c,d) by LukNorm; :: thesis: verum

end;assume ( a <= c & b <= d ) ; :: thesis: Lukasiewicz_norm . (a,b) <= Lukasiewicz_norm . (c,d)

then a + b <= c + d by XREAL_1:7;

then (a + b) - 1 <= (c + d) - 1 by XREAL_1:9;

then max (0,((a + b) - 1)) <= max (0,((c + d) - 1)) by XXREAL_0:26;

then max (0,((a + b) - 1)) <= Lukasiewicz_norm . (c,d) by LukNorm;

hence Lukasiewicz_norm . (a,b) <= Lukasiewicz_norm . (c,d) by LukNorm; :: thesis: verum

proof

hence
( Lukasiewicz_norm is commutative & Lukasiewicz_norm is associative & Lukasiewicz_norm is monotonic & Lukasiewicz_norm is with-1-identity )
by BINOP_1:def 2, BINOP_1:def 3, A1, C1, D1; :: thesis: verum
let a be Element of [.0,1.]; :: thesis: Lukasiewicz_norm . (a,1) = a

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

T2: 0 <= a by XXREAL_1:1;

Lukasiewicz_norm . (a,1) = max (0,((a + 1) - 1)) by LukNorm, T1

.= a by T2, XXREAL_0:def 10 ;

hence Lukasiewicz_norm . (a,1) = a ; :: thesis: verum

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

T2: 0 <= a by XXREAL_1:1;

Lukasiewicz_norm . (a,1) = max (0,((a + 1) - 1)) by LukNorm, T1

.= a by T2, XXREAL_0:def 10 ;

hence Lukasiewicz_norm . (a,1) = a ; :: thesis: verum