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) = 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 ; :: 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 ;
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 ;
then WC: (a * (1 - d)) + d <= (c * (1 - d)) + d by XREAL_1:6;
then de: ab = 0 by ;
dg: ad >= 0 by XXREAL_1:1;
hf: ad = 0 by ;
df: (Hamacher_norm . (a,d)) - (Hamacher_norm . (a,b)) = ((a * d) / ad) - 0 by
.= (a * d) / ad ;
WA: Hamacher_norm . (a,b) <= (Hamacher_norm . (a,d)) - 0 by ;
(Hamacher_norm . (c,d)) - (Hamacher_norm . (a,d)) = ((c * d) / B) - 0 by
.= 0 by ;
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
.= (((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 ;
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) = (a * 0) / ((a + 0) - (a * 0)) by ;
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)) = 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 ;
hence Hamacher_norm . (a,(Hamacher_norm . (b,c))) = Hamacher_norm . ((Hamacher_norm . (a,b)),c) by ; :: 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
.= ((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
.= (((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
.= (((a * b) / ((a + b) - (a * b))) * c) / ((((a * b) / ((a + b) - (a * b))) + c) - (((a * b) / ((a + b) - (a * b))) * c)) by
.= Hamacher_norm . ((Hamacher_norm . (a,b)),c) by ;
hence Hamacher_norm . (a,(Hamacher_norm . (b,c))) = Hamacher_norm . ((Hamacher_norm . (a,b)),c) ; :: 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 ; :: 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) = () / (() - ()) 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 ; :: thesis: verum