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.];
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 )
;
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 A1, FUZIMPL1:def 21
.=
1
by POWER:26
;
I_YG . (
y,
(I_YG . (x,z))) =
I_YG . (
y,1)
by FUZIMPL1:def 21, Y0
.=
1
to_power y
by A1, FUZIMPL1:def 21
.=
1
by POWER:26
;
hence
I_YG . (
x,
(I_YG . (y,z)))
= I_YG . (
y,
(I_YG . (x,z)))
by Y1;
verum end; suppose R1:
z > 0
;
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 R1, FUZIMPL1:def 21;
R2:
z to_power y > 0
by R1, POWER:34;
R3:
z to_power x > 0
by R1, POWER:34;
R5:
I_YG . (
x,
(I_YG . (y,z))) =
(z to_power y) to_power x
by R2, r4, FUZIMPL1:def 21
.=
z to_power (y * x)
by R1, POWER:33
;
I_YG . (
y,
(I_YG . (x,z))) =
(z to_power x) to_power y
by R3, r6, FUZIMPL1:def 21
.=
z to_power (x * y)
by R1, POWER:33
;
hence
I_YG . (
x,
(I_YG . (y,z)))
= I_YG . (
y,
(I_YG . (x,z)))
by R5;
verum end; suppose R1:
(
y > 0 &
x > 0 &
z = 0 )
;
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 R1, FUZIMPL1:def 21;
R2:
z to_power y = 0
by R1, POWER:def 2;
R3:
z to_power x = 0
by R1, POWER:def 2;
R5:
I_YG . (
x,
(I_YG . (y,z))) =
(z to_power y) to_power x
by R1, r4, FUZIMPL1:def 21
.=
0
by R1, POWER:def 2, R2
;
I_YG . (
y,
(I_YG . (x,z))) =
(z to_power x) to_power y
by R1, r6, FUZIMPL1:def 21
.=
0
by R1, POWER:def 2, R3
;
hence
I_YG . (
x,
(I_YG . (y,z)))
= I_YG . (
y,
(I_YG . (x,z)))
by R5;
verum end; suppose R1:
(
y = 0 &
x > 0 &
z = 0 )
;
I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z)))R3:
z to_power x = 0
by R1, POWER:def 2;
R5:
I_YG . (
x,
(I_YG . (y,z))) =
I_YG . (
x,1)
by R1, FUZIMPL1:def 21
.=
1
to_power x
by FUZIMPL1:def 21, A1
.=
1
by POWER:26
;
I_YG . (
y,
(I_YG . (x,z))) =
I_YG . (
y,
(z to_power x))
by R1, FUZIMPL1:def 21
.=
1
by R1, R3, FUZIMPL1:def 21
;
hence
I_YG . (
x,
(I_YG . (y,z)))
= I_YG . (
y,
(I_YG . (x,z)))
by R5;
verum end; suppose R1:
(
y > 0 &
x = 0 &
z = 0 )
;
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 R1, FUZIMPL1:def 21
.=
1
by R1, R2, FUZIMPL1:def 21
;
I_YG . (
y,
(I_YG . (x,z))) =
I_YG . (
y,1)
by R1, FUZIMPL1:def 21
.=
1
to_power y
by FUZIMPL1:def 21, A1
.=
1
by POWER:26
;
hence
I_YG . (
x,
(I_YG . (y,z)))
= I_YG . (
y,
(I_YG . (x,z)))
by R5;
verum end; suppose R1:
(
y > 0 &
x > 0 &
z = 0 )
;
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 R1, POWER:def 2;
R3:
z to_power x = 0
by R1, POWER:def 2;
R5:
I_YG . (
x,
(I_YG . (y,z))) =
I_YG . (
x,
(z to_power y))
by R1, FUZIMPL1:def 21
.=
(z to_power y) to_power x
by R1, R2, FUZIMPL1:def 21
.=
0
by R1, POWER:def 2, R2
;
I_YG . (
y,
(I_YG . (x,z))) =
(z to_power x) to_power y
by R1, r6, FUZIMPL1:def 21
.=
0
by R1, POWER:def 2, R3
;
hence
I_YG . (
x,
(I_YG . (y,z)))
= I_YG . (
y,
(I_YG . (x,z)))
by R5;
verum end;
end;
B2:
for y being Element of [.0,1.] holds I_YG . (1,y) = y
I_YG . ((1 / 2),(1 / 2)) = (1 / 2) to_power (1 / 2)
by A1, FUZIMPL1:def 21;
hence
( I_YG is satisfying_(NP) & I_YG is satisfying_(EP) & not I_YG is satisfying_(IP) & not I_YG is satisfying_(OP) )
by BA, B2, A1, LemmaHalf; verum