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 T3, FUZIMPL1:def 19;
then y = 1 * x by XCMPLX_1:87, T4, T2;
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 FUZIMPL1:def 19, AA, AB ;
I_GG . (y,(I_GG . (x,z))) = I_GG . (y,1) by YY, FUZIMPL1:def 19
.= 1 by AC, FUZIMPL1:def 19, AA ;
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 XREAL_1:153, AC, AB;
then ( x * y <= z & y > 0 ) by YY, XXREAL_0:2;
then F1: x <= z / y by XREAL_1:77;
F2: z / y in [.0,1.] by YY, FUZIMPL1:6;
Y1: I_GG . (x,(I_GG . (y,z))) = I_GG . (x,(z / y)) by FUZIMPL1:def 19, YY
.= 1 by FUZIMPL1:def 19, F1, F2 ;
I_GG . (y,(I_GG . (x,z))) = I_GG . (y,1) by YY, FUZIMPL1:def 19
.= 1 by AC, AA, FUZIMPL1:def 19 ;
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 XXREAL_1:1, YY;
then x * y <= (z / y) * y by IK, XREAL_1:64;
then x * y <= z by J1, XCMPLX_1:87;
then (x * y) / x <= z / x by JJ, XREAL_1:72;
then FF: y <= z / x by JJ, XCMPLX_1:89;
F2: z / x in [.0,1.] by YY, FUZIMPL1:6;
F4: z / y in [.0,1.] by YY, FUZIMPL1:6;
Y1: I_GG . (x,(I_GG . (y,z))) = I_GG . (x,(z / y)) by FUZIMPL1:def 19, YY
.= 1 by FUZIMPL1:def 19, F4, IK ;
I_GG . (y,(I_GG . (x,z))) = I_GG . (y,(z / x)) by YY, FUZIMPL1:def 19
.= 1 by FUZIMPL1:def 19, F2, FF ;
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 JJ, XREAL_1:68;
then x * y > z by JJ, XCMPLX_1:87;
then (x * y) / x > z / x by XREAL_1:74, JJ;
then F1: y > z / x by XCMPLX_1:89, JJ;
F2: z / x in [.0,1.] by YY, FUZIMPL1:6;
F4: z / y in [.0,1.] by YY, FUZIMPL1:6;
Y1: I_GG . (x,(I_GG . (y,z))) = I_GG . (x,(z / y)) by FUZIMPL1:def 19, YY
.= (z / y) / x by FUZIMPL1:def 19, F5, F4 ;
I_GG . (y,(I_GG . (x,z))) = I_GG . (y,(z / x)) by YY, FUZIMPL1:def 19
.= (z / x) / y by FUZIMPL1:def 19, F2, F1 ;
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 XREAL_1:153, AC, AB;
then ( x * y <= z & x > 0 ) by YY, XXREAL_0:2;
then F1: y <= z / x by XREAL_1:77;
Y1: I_GG . (x,(I_GG . (y,z))) = I_GG . (x,1) by FUZIMPL1:def 19, YY
.= 1 by FUZIMPL1:def 19, AA, AB ;
I_GG . (y,(I_GG . (x,z))) = I_GG . (y,(z / x)) by YY, FUZIMPL1:def 19
.= 1 by FUZIMPL1:def 19, F2, F1 ;
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