set f = Hamacher_norm ;
FF: for a, b being Element of [.0,1.] holds Hamacher_norm . (a,b) = Hamacher_norm . (b,a)

proof

let a, b be Element of [.0,1.]; :: thesis: Hamacher_norm . (a,b) = Hamacher_norm . (b,a)
Hamacher_norm . (a,b) = (a * b) / ((a + b) - (a * b)) by HamDef
.= Hamacher_norm . (b,a) by HamDef ;
hence Hamacher_norm . (a,b) = Hamacher_norm . (b,a) ; :: thesis: verum

end;

TT: for a being Element of [.0,1.] holds Hamacher_norm . (a,1) = a

proof

let a be Element of [.0,1.]; :: thesis: Hamacher_norm . (a,1) = a
1 in [.0,1.] by XXREAL_1:1;
then Hamacher_norm . (a,1) = (a * 1) / ((a + 1) - (a * 1)) by HamDef;
hence Hamacher_norm . (a,1) = a ; :: thesis: verum

end;

D1: for a, b, c, d being Element of [.0,1.] st a <= c & b <= d holds
Hamacher_norm . (a,b) <= Hamacher_norm . (c,d)

proof

let a, b, c, d be Element of [.0,1.]; :: thesis: ( a <= c & b <= d implies Hamacher_norm . (a,b) <= Hamacher_norm . (c,d) )
JJ: ( 0 <= a & 0 <= b & 0 <= c & 0 <= d ) by XXREAL_1:1;
B2: Hamacher_norm . (c,d) >= 0 by XXREAL_1:1;
assume S1: ( a <= c & b <= d ) ; :: thesis: Hamacher_norm . (a,b) <= Hamacher_norm . (c,d)
D1: Hamacher_norm . (a,b) = (a * b) / ((a + b) - (a * b)) by HamDef;
D2: Hamacher_norm . (c,d) = (c * d) / ((c + d) - (c * d)) by HamDef;
d2: Hamacher_norm . (a,d) = (a * d) / ((a + d) - (a * d)) by HamDef;
set A = (a + b) - (a * b);
set B = (c + d) - (c * d);

per cases ( (a + b) - (a * b) = 0 or (c + d) - (c * d) = 0 or ( (a + b) - (a * b) <> 0 & (c + d) - (c * d) <> 0 ) ) ;

suppose (a + b) - (a * b) = 0 ; :: thesis: Hamacher_norm . (a,b) <= Hamacher_norm . (c,d)

hence Hamacher_norm . (a,b) <= Hamacher_norm . (c,d) by B2, XCMPLX_1:49, D1; :: thesis: verum

end;

suppose DD: (c + d) - (c * d) = 0 ; :: thesis: Hamacher_norm . (a,b) <= Hamacher_norm . (c,d)

reconsider ad = (a + d) - (a * d), ab = (a + b) - (a * b) as Element of [.0,1.] by abMinab01;
reconsider B = (c + d) - (c * d) as Element of [.0,1.] by abMinab01;
1 - a in [.0,1.] by OpIn01;
then 1 - a >= 0 by XXREAL_1:1;
then b * (1 - a) <= d * (1 - a) by S1, XREAL_1:64;
then w0: (b * (1 - a)) + a <= (d * (1 - a)) + a by XREAL_1:6;
1 - d in [.0,1.] by OpIn01;
then 1 - d >= 0 by XXREAL_1:1;
then a * (1 - d) <= c * (1 - d) by S1, XREAL_1:64;
then WC: (a * (1 - d)) + d <= (c * (1 - d)) + d by XREAL_1:6;
then de: ab = 0 by XXREAL_1:1, DD, w0;
dg: ad >= 0 by XXREAL_1:1;
hf: ad = 0 by DD, WC, XXREAL_1:1;
df: (Hamacher_norm . (a,d)) - (Hamacher_norm . (a,b)) = ((a * d) / ad) - 0 by XCMPLX_1:49, de, D1, d2
.= (a * d) / ad ;
WA: Hamacher_norm . (a,b) <= (Hamacher_norm . (a,d)) - 0 by XREAL_1:11, df, dg, JJ;
(Hamacher_norm . (c,d)) - (Hamacher_norm . (a,d)) = ((c * d) / B) - 0 by XCMPLX_1:49, hf, d2, D2
.= 0 by XCMPLX_1:49, DD ;
hence Hamacher_norm . (a,b) <= Hamacher_norm . (c,d) by WA; :: thesis: verum

end;

suppose ( (a + b) - (a * b) <> 0 & (c + d) - (c * d) <> 0 ) ; :: thesis: Hamacher_norm . (a,b) <= Hamacher_norm . (c,d)

then D8: (Hamacher_norm . (c,d)) - (Hamacher_norm . (a,b)) = ((((a + b) - (a * b)) * (c * d)) - (((c + d) - (c * d)) * (a * b))) / (((a + b) - (a * b)) * ((c + d) - (c * d))) by XCMPLX_1:130, D1, D2
.= (((a * c) * (d - b)) + ((b * d) * (c - a))) / (((a + b) - (a * b)) * ((c + d) - (c * d))) ;
( (a + b) - (a * b) in [.0,1.] & (c + d) - (c * d) in [.0,1.] ) by abMinab01;
then d6: ( (a + b) - (a * b) >= 0 & (c + d) - (c * d) >= 0 ) by XXREAL_1:1;
b <= d - 0 by S1;
then D3: d - b >= 0 by XREAL_1:11;
a <= c - 0 by S1;
then c - a >= 0 by XREAL_1:11;
then ((Hamacher_norm . (c,d)) - (Hamacher_norm . (a,b))) + (Hamacher_norm . (a,b)) >= 0 + (Hamacher_norm . (a,b)) by XREAL_1:6, d6, D8, JJ, D3;
hence Hamacher_norm . (a,b) <= Hamacher_norm . (c,d) ; :: thesis: verum

end;

end;

end;

H1: 0 in [.0,1.] by XXREAL_1:1;
BU: for a being Element of [.0,1.] holds Hamacher_norm . (a,0) = 0

proof

let a be Element of [.0,1.]; :: thesis: Hamacher_norm . (a,0) = 0
Hamacher_norm . (a,0) = (a * 0) / ((a + 0) - (a * 0)) by HamDef, H1;
hence Hamacher_norm . (a,0) = 0 ; :: thesis: verum

end;

for a, b, c being Element of [.0,1.] holds Hamacher_norm . (a,(Hamacher_norm . (b,c))) = Hamacher_norm . ((Hamacher_norm . (a,b)),c)

proof

let a, b, c be Element of [.0,1.]; :: thesis: Hamacher_norm . (a,(Hamacher_norm . (b,c))) = Hamacher_norm . ((Hamacher_norm . (a,b)),c)
J1: Hamacher_norm . (a,b) = (a * b) / ((a + b) - (a * b)) by HamDef;
J2: Hamacher_norm . (b,c) = (b * c) / ((b + c) - (b * c)) by HamDef;
reconsider bc = (b * c) / ((b + c) - (b * c)) as Element of [.0,1.] by HamIn01;
set ab = (a * b) / ((a + b) - (a * b));
set bb = (b + c) - (b * c);
set AB = (a + b) - (a * b);

per cases ( ( a <> 0 & b <> 0 & c <> 0 ) or ( a <> 0 & b <> 0 & c = 0 ) or ( a = 0 & b <> 0 ) or ( a <> 0 & b = 0 ) or ( a = 0 & b = 0 ) ) ;

suppose Z1: ( a <> 0 & b <> 0 & c <> 0 ) ; :: thesis: Hamacher_norm . (a,(Hamacher_norm . (b,c))) = Hamacher_norm . ((Hamacher_norm . (a,b)),c)

then P1: a * b <> 0 by XCMPLX_1:6;
j3: (a * b) / ((a + b) - (a * b)) in [.0,1.] by HamIn01;

per cases ( (a * b) / ((a + b) - (a * b)) = 0 or bc = 0 or ( (a * b) / ((a + b) - (a * b)) <> 0 & bc <> 0 ) ) ;

suppose (a * b) / ((a + b) - (a * b)) = 0 ; :: thesis: Hamacher_norm . (a,(Hamacher_norm . (b,c))) = Hamacher_norm . ((Hamacher_norm . (a,b)),c)

then (a + b) - (a * b) = 0 by XCMPLX_1:50, P1;
hence Hamacher_norm . (a,(Hamacher_norm . (b,c))) = Hamacher_norm . ((Hamacher_norm . (a,b)),c) by Z1, Lemacik; :: thesis: verum

end;

suppose T1: bc = 0 ; :: thesis: Hamacher_norm . (a,(Hamacher_norm . (b,c))) = Hamacher_norm . ((Hamacher_norm . (a,b)),c)

b * c <> 0 by Z1, XCMPLX_1:6;
then (b + c) - (b * c) = 0 by T1, XCMPLX_1:50;
hence Hamacher_norm . (a,(Hamacher_norm . (b,c))) = Hamacher_norm . ((Hamacher_norm . (a,b)),c) by Z1, Lemacik; :: thesis: verum

end;

suppose ( (a * b) / ((a + b) - (a * b)) <> 0 & bc <> 0 ) ; :: thesis: Hamacher_norm . (a,(Hamacher_norm . (b,c))) = Hamacher_norm . ((Hamacher_norm . (a,b)),c)

then f1: ( (a + b) - (a * b) <> 0 & (b + c) - (b * c) <> 0 ) by XCMPLX_1:49;
WA: (a * bc) * ((((a * b) / ((a + b) - (a * b))) + c) - (((a * b) / ((a + b) - (a * b))) * c)) = ((a * (b * c)) / ((b + c) - (b * c))) * (c + (((a * b) / ((a + b) - (a * b))) - (((a * b) / ((a + b) - (a * b))) * c))) by XCMPLX_1:74
.= ((a * (b * c)) / ((b + c) - (b * c))) * (((c * ((a + b) - (a * b))) / ((a + b) - (a * b))) + (((a * b) / ((a + b) - (a * b))) * (1 - c))) by XCMPLX_1:89, f1
.= ((a * (b * c)) / ((b + c) - (b * c))) * (((c * ((a + b) - (a * b))) / ((a + b) - (a * b))) + (((a * b) * (1 - c)) / ((a + b) - (a * b)))) by XCMPLX_1:74
.= ((a * (b * c)) / ((b + c) - (b * c))) * (((c * ((a + b) - (a * b))) + ((a * b) * (1 - c))) / ((a + b) - (a * b))) by XCMPLX_1:62
.= ((a * (b * c)) * ((c * ((a + b) - (a * b))) + ((a * b) * (1 - c)))) / (((a + b) - (a * b)) * ((b + c) - (b * c))) by XCMPLX_1:76
.= (((a * b) * c) / ((a + b) - (a * b))) * (((a * ((b + c) - (b * c))) + ((b * c) * (1 - a))) / ((b + c) - (b * c))) by XCMPLX_1:76
.= (((a * b) * c) / ((a + b) - (a * b))) * (((a * ((b + c) - (b * c))) / ((b + c) - (b * c))) + (((b * c) * (1 - a)) / ((b + c) - (b * c)))) by XCMPLX_1:62
.= (((a * b) * c) / ((a + b) - (a * b))) * (((a * ((b + c) - (b * c))) / ((b + c) - (b * c))) + (((b * c) / ((b + c) - (b * c))) * (1 - a))) by XCMPLX_1:74
.= (((a * b) / ((a + b) - (a * b))) * c) * (((a * ((b + c) - (b * c))) / ((b + c) - (b * c))) + (((b * c) / ((b + c) - (b * c))) * (1 - a))) by XCMPLX_1:74
.= (((a * b) / ((a + b) - (a * b))) * c) * (a + (((b * c) / ((b + c) - (b * c))) * (1 - a))) by XCMPLX_1:89, f1
.= (((a * b) / ((a + b) - (a * b))) * c) * ((a + bc) - (a * bc)) ;

per cases ( ( (a + bc) - (a * bc) <> 0 & (((a * b) / ((a + b) - (a * b))) + c) - (((a * b) / ((a + b) - (a * b))) * c) <> 0 ) or (a + bc) - (a * bc) = 0 or (((a * b) / ((a + b) - (a * b))) + c) - (((a * b) / ((a + b) - (a * b))) * c) = 0 ) ;

suppose that f2: (a + bc) - (a * bc) <> 0 and
f3: (((a * b) / ((a + b) - (a * b))) + c) - (((a * b) / ((a + b) - (a * b))) * c) <> 0 ; :: thesis: Hamacher_norm . (a,(Hamacher_norm . (b,c))) = Hamacher_norm . ((Hamacher_norm . (a,b)),c)

Hamacher_norm . (a,(Hamacher_norm . (b,c))) = (a * bc) / ((a + bc) - (a * bc)) by HamDef, J2
.= (((a * b) / ((a + b) - (a * b))) * c) / ((((a * b) / ((a + b) - (a * b))) + c) - (((a * b) / ((a + b) - (a * b))) * c)) by WA, XCMPLX_1:94, f2, f3
.= Hamacher_norm . ((Hamacher_norm . (a,b)),c) by J1, HamDef ;
hence Hamacher_norm . (a,(Hamacher_norm . (b,c))) = Hamacher_norm . ((Hamacher_norm . (a,b)),c) ; :: thesis: verum

end;

suppose (a + bc) - (a * bc) = 0 ; :: thesis: Hamacher_norm . (a,(Hamacher_norm . (b,c))) = Hamacher_norm . ((Hamacher_norm . (a,b)),c)

hence Hamacher_norm . (a,(Hamacher_norm . (b,c))) = Hamacher_norm . ((Hamacher_norm . (a,b)),c) by Z1, Lemacik; :: thesis: verum

end;

suppose (((a * b) / ((a + b) - (a * b))) + c) - (((a * b) / ((a + b) - (a * b))) * c) = 0 ; :: thesis: Hamacher_norm . (a,(Hamacher_norm . (b,c))) = Hamacher_norm . ((Hamacher_norm . (a,b)),c)

hence Hamacher_norm . (a,(Hamacher_norm . (b,c))) = Hamacher_norm . ((Hamacher_norm . (a,b)),c) by Z1, Lemacik, j3; :: thesis: verum

end;

end;

end;

end;

end;

suppose Z1: ( a <> 0 & b <> 0 & c = 0 ) ; :: thesis: Hamacher_norm . (a,(Hamacher_norm . (b,c))) = Hamacher_norm . ((Hamacher_norm . (a,b)),c)

then Hamacher_norm . (a,(Hamacher_norm . (b,c))) = Hamacher_norm . (a,0) by BU
.= 0 by BU
.= Hamacher_norm . ((Hamacher_norm . (a,b)),c) by BU, Z1 ;
hence Hamacher_norm . (a,(Hamacher_norm . (b,c))) = Hamacher_norm . ((Hamacher_norm . (a,b)),c) ; :: thesis: verum

end;

suppose Z1: ( a = 0 & b <> 0 ) ; :: thesis: Hamacher_norm . (a,(Hamacher_norm . (b,c))) = Hamacher_norm . ((Hamacher_norm . (a,b)),c)

Hamacher_norm . (a,(Hamacher_norm . (b,c))) = Hamacher_norm . ((Hamacher_norm . (b,c)),a) by FF
.= 0 by BU, Z1
.= Hamacher_norm . (c,0) by BU
.= Hamacher_norm . (0,c) by FF, H1
.= Hamacher_norm . ((Hamacher_norm . (b,a)),c) by BU, Z1
.= Hamacher_norm . ((Hamacher_norm . (a,b)),c) by FF ;
hence Hamacher_norm . (a,(Hamacher_norm . (b,c))) = Hamacher_norm . ((Hamacher_norm . (a,b)),c) ; :: thesis: verum

end;

suppose Z1: ( a <> 0 & b = 0 ) ; :: thesis: Hamacher_norm . (a,(Hamacher_norm . (b,c))) = Hamacher_norm . ((Hamacher_norm . (a,b)),c)

then z1: Hamacher_norm . (a,b) = 0 by BU;
Hamacher_norm . (b,c) = Hamacher_norm . (c,b) by FF
.= 0 by Z1, BU ;
then Hamacher_norm . (a,(Hamacher_norm . (b,c))) = 0 by BU
.= Hamacher_norm . (c,0) by BU
.= Hamacher_norm . ((Hamacher_norm . (a,b)),c) by FF, z1 ;
hence Hamacher_norm . (a,(Hamacher_norm . (b,c))) = Hamacher_norm . ((Hamacher_norm . (a,b)),c) ; :: thesis: verum

end;

suppose Z1: ( a = 0 & b = 0 ) ; :: thesis: Hamacher_norm . (a,(Hamacher_norm . (b,c))) = Hamacher_norm . ((Hamacher_norm . (a,b)),c)

then Z2: Hamacher_norm . (a,b) = (0 * 0) / ((0 + 0) - (0 * 0)) by HamDef
.= 0 ;
Hamacher_norm . (b,c) = (b * c) / ((b + c) - (b * c)) by HamDef;
hence Hamacher_norm . (a,(Hamacher_norm . (b,c))) = Hamacher_norm . ((Hamacher_norm . (a,b)),c) by Z2, Z1; :: thesis: verum

end;

end;

end;

hence ( Hamacher_norm is commutative & Hamacher_norm is associative & Hamacher_norm is with-1-identity & Hamacher_norm is monotonic ) by FF, TT, D1, BINOP_1:def 3, BINOP_1:def 2; :: thesis: verum