set I = I_FD ;
A1: I_FD is satisfying_(OP)
proof
let x, y be Element of [.0,1.]; :: according to FUZIMPL2:def 4 :: thesis: ( I_FD . (x,y) = 1 iff x <= y )
thus ( I_FD . (x,y) = 1 implies x <= y ) :: thesis: ( x <= y implies I_FD . (x,y) = 1 )
proof
assume T2: I_FD . (x,y) = 1 ; :: thesis: x <= y
assume T3: x > y ; :: thesis: contradiction
then I_FD . (x,y) = max ((1 - x),y) by FUZIMPL1:def 23;
then ( 1 - x = 1 or y = 1 ) by ;
hence contradiction by T3, XXREAL_1:1; :: thesis: verum
end;
thus ( x <= y implies I_FD . (x,y) = 1 ) by FUZIMPL1:def 23; :: thesis: verum
end;
for x, y, z being Element of [.0,1.] holds I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z)))
proof
let x, y, z be Element of [.0,1.]; :: thesis: I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z)))
Ff: 1 in [.0,1.] by XXREAL_1:1;
F0: ( x <= 1 & y <= 1 & z >= 0 ) by XXREAL_1:1;
per cases ( ( y <= z & x <= z ) or ( y <= z & x > z ) or ( y > z & x > z ) or ( y > z & x <= z ) ) ;
suppose F1: ( y <= z & x <= z ) ; :: thesis: I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z)))
then F2: I_FD . (x,(I_FD . (y,z))) = I_FD . (x,1) by FUZIMPL1:def 23
.= 1 by A1, F0, Ff ;
I_FD . (y,(I_FD . (x,z))) = I_FD . (y,1) by
.= 1 by A1, F0, Ff ;
hence I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z))) by F2; :: thesis: verum
end;
suppose F1: ( y <= z & x > z ) ; :: thesis: I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z)))
ff: z <= max ((1 - x),z) by XXREAL_0:25;
f4: I_FD . (x,z) = max ((1 - x),z) by ;
I_FD . (x,(I_FD . (y,z))) = I_FD . (x,1) by
.= 1 by A1, F0, Ff ;
hence I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z))) by ; :: thesis: verum
end;
suppose F1: ( y > z & x > z ) ; :: thesis: I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z)))
x2: I_FD . (y,z) = max ((1 - y),z) by ;
x4: I_FD . (x,z) = max ((1 - x),z) by ;
per cases ( x <= max ((1 - y),z) or 1 - x < y or 1 - x >= y ) ;
suppose X1: x <= max ((1 - y),z) ; :: thesis: I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z)))
then ( x <= 1 - y or x <= z ) by XXREAL_0:def 10;
then x + y <= (1 - y) + y by ;
then y1: (x + y) - x <= 1 - x by XREAL_1:9;
1 - x <= max ((1 - x),z) by XXREAL_0:25;
then X3: y <= max ((1 - x),z) by ;
I_FD . (x,(I_FD . (y,z))) = 1 by ;
hence I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z))) by ; :: thesis: verum
end;
suppose we: 1 - x < y ; :: thesis: I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z)))
then X3: y > max ((1 - x),z) by ;
(1 - x) - y < y - y by ;
then ((1 - x) - y) + x < 0 + x by XREAL_1:6;
then X1: x > max ((1 - y),z) by ;
F2: I_FD . (x,(I_FD . (y,z))) = max ((1 - x),(max ((1 - y),z))) by ;
I_FD . (y,(I_FD . (x,z))) = max ((1 - y),(max ((1 - x),z))) by ;
hence I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z))) by ; :: thesis: verum
end;
suppose SE: 1 - x >= y ; :: thesis: I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z)))
then (1 - x) + x >= y + x by XREAL_1:6;
then ww: 1 - y >= (y + x) - y by XREAL_1:9;
then SA: max ((1 - y),z) = 1 - y by ;
P0: ( 1 - x in [.0,1.] & 1 - y in [.0,1.] ) by FUZNORM1:7;
F2: I_FD . (x,(I_FD . (y,z))) = I_FD . (x,(max ((1 - y),z))) by
.= 1 by ;
I_FD . (y,(I_FD . (x,z))) = I_FD . (y,(max ((1 - x),z))) by
.= I_FD . (y,(1 - x)) by
.= 1 by A1, P0, SE ;
hence I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z))) by F2; :: thesis: verum
end;
end;
end;
suppose F1: ( y > z & x <= z ) ; :: thesis: I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z)))
f3: z <= max ((1 - y),z) by XXREAL_0:25;
f4: I_FD . (y,z) = max ((1 - y),z) by ;
I_FD . (y,(I_FD . (x,z))) = I_FD . (y,1) by
.= 1 by A1, F0, Ff ;
hence I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z))) by ; :: thesis: verum
end;
end;
end;
then I_FD is satisfying_(EP) ;
hence ( I_FD is satisfying_(NP) & I_FD is satisfying_(EP) & I_FD is satisfying_(IP) & I_FD is satisfying_(OP) ) by A1; :: thesis: verum