set I = I_YG ;
A1: ( 1 / 2 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1;
BA: for x, y, z being Element of [.0,1.] holds I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z)))
proof
let x, y, z be Element of [.0,1.]; :: thesis: I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z)))
per cases ( ( x = 0 & y = 0 & z = 0 ) or z > 0 or ( y > 0 & x > 0 & z = 0 ) or ( y = 0 & x > 0 & z = 0 ) or ( y > 0 & x = 0 & z = 0 ) or ( y > 0 & x > 0 & z = 0 ) ) by XXREAL_1:1;
suppose Y0: ( x = 0 & y = 0 & z = 0 ) ; :: thesis: I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z)))
then Y1: I_YG . (x,(I_YG . (y,z))) = I_YG . (x,1) by FUZIMPL1:def 21
.= 1 to_power x by
.= 1 by POWER:26 ;
I_YG . (y,(I_YG . (x,z))) = I_YG . (y,1) by
.= 1 to_power y by
.= 1 by POWER:26 ;
hence I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z))) by Y1; :: thesis: verum
end;
suppose R1: z > 0 ; :: thesis: I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z)))
then r4: I_YG . (y,z) = z to_power y by FUZIMPL1:def 21;
r6: I_YG . (x,z) = z to_power x by ;
R2: z to_power y > 0 by ;
R3: z to_power x > 0 by ;
R5: I_YG . (x,(I_YG . (y,z))) = (z to_power y) to_power x by
.= z to_power (y * x) by ;
I_YG . (y,(I_YG . (x,z))) = (z to_power x) to_power y by
.= z to_power (x * y) by ;
hence I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z))) by R5; :: thesis: verum
end;
suppose R1: ( y > 0 & x > 0 & z = 0 ) ; :: thesis: I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z)))
then r4: I_YG . (y,z) = z to_power y by FUZIMPL1:def 21;
r6: I_YG . (x,z) = z to_power x by ;
R2: z to_power y = 0 by ;
R3: z to_power x = 0 by ;
R5: I_YG . (x,(I_YG . (y,z))) = (z to_power y) to_power x by
.= 0 by ;
I_YG . (y,(I_YG . (x,z))) = (z to_power x) to_power y by
.= 0 by ;
hence I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z))) by R5; :: thesis: verum
end;
suppose R1: ( y = 0 & x > 0 & z = 0 ) ; :: thesis: I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z)))
R3: z to_power x = 0 by ;
R5: I_YG . (x,(I_YG . (y,z))) = I_YG . (x,1) by
.= 1 to_power x by
.= 1 by POWER:26 ;
I_YG . (y,(I_YG . (x,z))) = I_YG . (y,(z to_power x)) by
.= 1 by ;
hence I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z))) by R5; :: thesis: verum
end;
suppose R1: ( y > 0 & x = 0 & z = 0 ) ; :: thesis: I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z)))
then R2: z to_power y = 0 by POWER:def 2;
R5: I_YG . (x,(I_YG . (y,z))) = I_YG . (x,(z to_power y)) by
.= 1 by ;
I_YG . (y,(I_YG . (x,z))) = I_YG . (y,1) by
.= 1 to_power y by
.= 1 by POWER:26 ;
hence I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z))) by R5; :: thesis: verum
end;
suppose R1: ( y > 0 & x > 0 & z = 0 ) ; :: thesis: I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z)))
then r6: I_YG . (x,z) = z to_power x by FUZIMPL1:def 21;
R2: z to_power y = 0 by ;
R3: z to_power x = 0 by ;
R5: I_YG . (x,(I_YG . (y,z))) = I_YG . (x,(z to_power y)) by
.= (z to_power y) to_power x by
.= 0 by ;
I_YG . (y,(I_YG . (x,z))) = (z to_power x) to_power y by
.= 0 by ;
hence I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z))) by R5; :: thesis: verum
end;
end;
end;
B2: for y being Element of [.0,1.] holds I_YG . (1,y) = y
proof
let y be Element of [.0,1.]; :: thesis: I_YG . (1,y) = y
I_YG . (1,y) = y to_power 1 by ;
hence I_YG . (1,y) = y by POWER:25; :: thesis: verum
end;
I_YG . ((1 / 2),(1 / 2)) = (1 / 2) to_power (1 / 2) by ;
hence ( I_YG is satisfying_(NP) & I_YG is satisfying_(EP) & not I_YG is satisfying_(IP) & not I_YG is satisfying_(OP) ) by ; :: thesis: verum