set f = Hamacher_norm ;
FF:
for a, b being Element of [.0,1.] holds Hamacher_norm . (a,b) = Hamacher_norm . (b,a)
TT:
for a being Element of [.0,1.] holds Hamacher_norm . (a,1) = a
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.];
( 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 )
;
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 DD:
(c + d) - (c * d) = 0
;
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;
verum end; suppose
(
(a + b) - (a * b) <> 0 &
(c + d) - (c * d) <> 0 )
;
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)
;
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
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.];
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 )
;
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 &
bc <> 0 )
;
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
;
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)
;
verum end; end; end; end; end; suppose Z1:
(
a <> 0 &
b <> 0 &
c = 0 )
;
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)
;
verum end; suppose Z1:
(
a = 0 &
b <> 0 )
;
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)
;
verum end; suppose Z1:
(
a <> 0 &
b = 0 )
;
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)
;
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; verum