let C be non empty set ; :: thesis: for f, g, h being Membership_Func of C holds min f,(g * h) c=
let f, g, h be Membership_Func of C; :: thesis: min f,(g * h) c=
let c be Element of C; :: according to FUZZY_1:def 3 :: thesis: ((min f,g) * (min f,h)) . c <= (min f,(g * h)) . c
A1: (min (f . c),(g . c)) * (min (f . c),(h . c)) <= (min f,(g * h)) . c
proof
now
per cases ( min (f . c),(g . c) = f . c or min (f . c),(g . c) = g . c ) by XXREAL_0:15;
suppose A2: min (f . c),(g . c) = f . c ; :: thesis: (min (f . c),(g . c)) * (min (f . c),(h . c)) <= (min f,(g * h)) . c
(min (f . c),(g . c)) * (min (f . c),(h . c)) <= (min f,(g * h)) . c
proof
per cases ( min (f . c),(h . c) = f . c or min (f . c),(h . c) = h . c ) by XXREAL_0:15;
suppose A3: min (f . c),(h . c) = f . c ; :: thesis: (min (f . c),(g . c)) * (min (f . c),(h . c)) <= (min f,(g * h)) . c
A4: 0 <= g . c by Th1;
f . c <= h . c by A3, XXREAL_0:def 9;
then A5: (g . c) * (f . c) <= (h . c) * (g . c) by A4, XREAL_1:66;
A6: 0 <= f . c by Th1;
f c= by Th33;
then A7: (f * f) . c <= f . c by FUZZY_1:def 3;
f . c <= g . c by A2, XXREAL_0:def 9;
then (f . c) * (f . c) <= (g . c) * (f . c) by A6, XREAL_1:66;
then (f . c) * (f . c) <= (g . c) * (h . c) by A5, XXREAL_0:2;
then min ((f * f) . c),((f . c) * (f . c)) <= min (f . c),((g . c) * (h . c)) by A7, XXREAL_0:18;
then min ((f . c) * (f . c)),((f . c) * (f . c)) <= min (f . c),((g . c) * (h . c)) by Def2;
then (f . c) * (f . c) <= min (f . c),((g * h) . c) by Def2;
hence (min (f . c),(g . c)) * (min (f . c),(h . c)) <= (min f,(g * h)) . c by A2, A3, FUZZY_1:6; :: thesis: verum
end;
suppose A8: min (f . c),(h . c) = h . c ; :: thesis: (min (f . c),(g . c)) * (min (f . c),(h . c)) <= (min f,(g * h)) . c
A9: 1 >= h . c by Th1;
A10: h . c >= 0 by Th1;
f . c <= g . c by A2, XXREAL_0:def 9;
then A11: (f . c) * (h . c) <= (g . c) * (h . c) by A10, XREAL_1:66;
f . c >= 0 by Th1;
then (f . c) * (h . c) <= (f . c) * 1 by A9, XREAL_1:66;
then (f . c) * (h . c) <= min (f . c),((g . c) * (h . c)) by A11, XXREAL_0:20;
then (f . c) * (h . c) <= min (f . c),((g * h) . c) by Def2;
hence (min (f . c),(g . c)) * (min (f . c),(h . c)) <= (min f,(g * h)) . c by A2, A8, FUZZY_1:6; :: thesis: verum
end;
end;
end;
hence (min (f . c),(g . c)) * (min (f . c),(h . c)) <= (min f,(g * h)) . c ; :: thesis: verum
end;
suppose A12: min (f . c),(g . c) = g . c ; :: thesis: (min (f . c),(g . c)) * (min (f . c),(h . c)) <= (min f,(g * h)) . c
(min (f . c),(g . c)) * (min (f . c),(h . c)) <= (min f,(g * h)) . c
proof
per cases ( min (f . c),(h . c) = f . c or min (f . c),(h . c) = h . c ) by XXREAL_0:15;
suppose A13: min (f . c),(h . c) = f . c ; :: thesis: (min (f . c),(g . c)) * (min (f . c),(h . c)) <= (min f,(g * h)) . c
A14: g . c >= 0 by Th1;
f . c <= h . c by A13, XXREAL_0:def 9;
then A15: (f . c) * (g . c) <= (h . c) * (g . c) by A14, XREAL_1:66;
A16: 1 >= g . c by Th1;
f . c >= 0 by Th1;
then (g . c) * (f . c) <= (f . c) * 1 by A16, XREAL_1:66;
then (f . c) * (g . c) <= min (f . c),((h . c) * (g . c)) by A15, XXREAL_0:20;
then (f . c) * (g . c) <= min (f . c),((g * h) . c) by Def2;
hence (min (f . c),(g . c)) * (min (f . c),(h . c)) <= (min f,(g * h)) . c by A12, A13, FUZZY_1:6; :: thesis: verum
end;
suppose A17: min (f . c),(h . c) = h . c ; :: thesis: (min (f . c),(g . c)) * (min (f . c),(h . c)) <= (min f,(g * h)) . c
A18: g . c <= f . c by A12, XXREAL_0:def 9;
f . c >= 0 by Th1;
then A19: (g . c) * (f . c) <= (f . c) * (f . c) by A18, XREAL_1:66;
f c= by Th33;
then (f * f) . c <= f . c by FUZZY_1:def 3;
then A20: (f . c) * (f . c) <= f . c by Def2;
A21: h . c <= f . c by A17, XXREAL_0:def 9;
g . c >= 0 by Th1;
then (h . c) * (g . c) <= (f . c) * (g . c) by A21, XREAL_1:66;
then (h . c) * (g . c) <= (f . c) * (f . c) by A19, XXREAL_0:2;
then (h . c) * (g . c) <= f . c by A20, XXREAL_0:2;
then (h . c) * (g . c) <= min (f . c),((h . c) * (g . c)) by XXREAL_0:20;
then (g . c) * (h . c) <= min (f . c),((g * h) . c) by Def2;
hence (min (f . c),(g . c)) * (min (f . c),(h . c)) <= (min f,(g * h)) . c by A12, A17, FUZZY_1:6; :: thesis: verum
end;
end;
end;
hence (min (f . c),(g . c)) * (min (f . c),(h . c)) <= (min f,(g * h)) . c ; :: thesis: verum
end;
end;
end;
hence (min (f . c),(g . c)) * (min (f . c),(h . c)) <= (min f,(g * h)) . c ; :: thesis: verum
end;
((min f,g) * (min f,h)) . c = ((min f,g) . c) * ((min f,h) . c) by Def2
.= (min (f . c),(g . c)) * ((min f,h) . c) by FUZZY_1:6
.= (min (f . c),(g . c)) * (min (f . c),(h . c)) by FUZZY_1:6 ;
hence ((min f,g) * (min f,h)) . c <= (min f,(g * h)) . c by A1; :: thesis: verum