set I = I_GG ;
for x, y being Element of [.0,1.] holds
( I_GG . (x,y) = 1 iff x <= y )
proof
let x, y be Element of [.0,1.]; :: thesis: ( I_GG . (x,y) = 1 iff x <= y )
thus ( I_GG . (x,y) = 1 implies x <= y ) :: thesis: ( x <= y implies I_GG . (x,y) = 1 )
proof
assume T2: I_GG . (x,y) = 1 ; :: thesis: x <= y
assume T3: x > y ; :: thesis: contradiction
then T4: x > 0 by XXREAL_1:1;
I_GG . (x,y) = y / x by ;
then y = 1 * x by ;
hence contradiction by T3; :: thesis: verum
end;
thus ( x <= y implies I_GG . (x,y) = 1 ) by FUZIMPL1:def 19; :: thesis: verum
end;
then A1: I_GG is satisfying_(OP) ;
for x, y, z being Element of [.0,1.] holds I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z)))
proof
let x, y, z be Element of [.0,1.]; :: thesis: I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z)))
AB: ( 0 <= x & x <= 1 ) by XXREAL_1:1;
AC: ( 0 <= y & y <= 1 ) by XXREAL_1:1;
AA: 1 in [.0,1.] 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 YY: ( y <= z & x <= z ) ; :: thesis: I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z)))
then Y1: I_GG . (x,(I_GG . (y,z))) = I_GG . (x,1) by FUZIMPL1:def 19
.= 1 by ;
I_GG . (y,(I_GG . (x,z))) = I_GG . (y,1) by
.= 1 by ;
hence I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z))) by Y1; :: thesis: verum
end;
suppose YY: ( y > z & x <= z ) ; :: thesis: I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z)))
x * y <= x by ;
then ( x * y <= z & y > 0 ) by ;
then F1: x <= z / y by XREAL_1:77;
F2: z / y in [.0,1.] by ;
Y1: I_GG . (x,(I_GG . (y,z))) = I_GG . (x,(z / y)) by
.= 1 by ;
I_GG . (y,(I_GG . (x,z))) = I_GG . (y,1) by
.= 1 by ;
hence I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z))) by Y1; :: thesis: verum
end;
suppose YY: ( y > z & x > z ) ; :: thesis: I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z)))
then JJ: ( x > 0 & y > 0 ) by XXREAL_1:1;
per cases ( x <= z / y or x > z / y ) ;
suppose IK: x <= z / y ; :: thesis: I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z)))
J1: y > 0 by ;
then x * y <= (z / y) * y by ;
then x * y <= z by ;
then (x * y) / x <= z / x by ;
then FF: y <= z / x by ;
F2: z / x in [.0,1.] by ;
F4: z / y in [.0,1.] by ;
Y1: I_GG . (x,(I_GG . (y,z))) = I_GG . (x,(z / y)) by
.= 1 by ;
I_GG . (y,(I_GG . (x,z))) = I_GG . (y,(z / x)) by
.= 1 by ;
hence I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z))) by Y1; :: thesis: verum
end;
suppose F5: x > z / y ; :: thesis: I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z)))
then x * y > (z / y) * y by ;
then x * y > z by ;
then (x * y) / x > z / x by ;
then F1: y > z / x by ;
F2: z / x in [.0,1.] by ;
F4: z / y in [.0,1.] by ;
Y1: I_GG . (x,(I_GG . (y,z))) = I_GG . (x,(z / y)) by
.= (z / y) / x by ;
I_GG . (y,(I_GG . (x,z))) = I_GG . (y,(z / x)) by
.= (z / x) / y by ;
hence I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z))) by Y1; :: thesis: verum
end;
end;
end;
suppose YY: ( y <= z & x > z ) ; :: thesis: I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z)))
then F2: z / x in [.0,1.] by FUZIMPL1:6;
x * y <= y by ;
then ( x * y <= z & x > 0 ) by ;
then F1: y <= z / x by XREAL_1:77;
Y1: I_GG . (x,(I_GG . (y,z))) = I_GG . (x,1) by
.= 1 by ;
I_GG . (y,(I_GG . (x,z))) = I_GG . (y,(z / x)) by
.= 1 by ;
hence I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z))) by Y1; :: thesis: verum
end;
end;
end;
then I_GG is satisfying_(EP) ;
hence ( I_GG is satisfying_(NP) & I_GG is satisfying_(EP) & I_GG is satisfying_(IP) & I_GG is satisfying_(OP) ) by A1; :: thesis: verum