let C be non empty set ; :: thesis: for f, g, h being Membership_Func of C holds f ++ (min g,h) = min (f ++ g),(f ++ h)
let f, g, h be Membership_Func of C; :: thesis: f ++ (min g,h) = min (f ++ g),(f ++ h)
A1:
( C = dom (f ++ (min g,h)) & C = dom (min (f ++ g),(f ++ h)) )
by FUNCT_2:def 1;
for c being Element of C st c in C holds
(f ++ (min g,h)) . c = (min (f ++ g),(f ++ h)) . c
proof
let c be
Element of
C;
:: thesis: ( c in C implies (f ++ (min g,h)) . c = (min (f ++ g),(f ++ h)) . c )
A2:
(f ++ (min g,h)) . c =
((f . c) + ((min g,h) . c)) - ((f . c) * ((min g,h) . c))
by Def3
.=
((f . c) + (min (g . c),(h . c))) - ((f . c) * ((min g,h) . c))
by FUZZY_1:6
;
now per cases
( min (g . c),(h . c) = g . c or min (g . c),(h . c) = h . c )
by XXREAL_0:15;
suppose A3:
min (g . c),
(h . c) = g . c
;
:: thesis: ( c in C implies (f ++ (min g,h)) . c = (min (f ++ g),(f ++ h)) . c )
(f ++ (min g,h)) . c = (min (f ++ g),(f ++ h)) . c
proof
(
g . c <= h . c &
(1_minus f) . c >= 0 )
by A3, Th1, XXREAL_0:def 9;
then
(g . c) * ((1_minus f) . c) <= (h . c) * ((1_minus f) . c)
by XREAL_1:66;
then
(g . c) * (1 - (f . c)) <= (h . c) * ((1_minus f) . c)
by FUZZY_1:def 6;
then
(g . c) * (1 - (f . c)) <= (h . c) * (1 - (f . c))
by FUZZY_1:def 6;
then A4:
(((g . c) * 1) - ((g . c) * (f . c))) + (f . c) <= ((h . c) * (1 - (f . c))) + (f . c)
by XREAL_1:8;
A5:
(f ++ (min g,h)) . c = ((f . c) + (g . c)) - ((f . c) * (g . c))
by A2, A3, FUZZY_1:6;
((f . c) + (g . c)) - ((f . c) * (g . c)) =
min (((f . c) + (g . c)) - ((f . c) * (g . c))),
(((f . c) + (h . c)) - ((f . c) * (h . c)))
by A4, XXREAL_0:def 9
.=
min ((f ++ g) . c),
(((f . c) + (h . c)) - ((f . c) * (h . c)))
by Def3
.=
min ((f ++ g) . c),
((f ++ h) . c)
by Def3
;
hence
(f ++ (min g,h)) . c = (min (f ++ g),(f ++ h)) . c
by A5, FUZZY_1:6;
:: thesis: verum
end; hence
(
c in C implies
(f ++ (min g,h)) . c = (min (f ++ g),(f ++ h)) . c )
;
:: thesis: verum end; suppose A6:
min (g . c),
(h . c) = h . c
;
:: thesis: ( c in C implies (f ++ (min g,h)) . c = (min (f ++ g),(f ++ h)) . c )
(f ++ (min g,h)) . c = (min (f ++ g),(f ++ h)) . c
proof
(
h . c <= g . c &
(1_minus f) . c >= 0 )
by A6, Th1, XXREAL_0:def 9;
then
(h . c) * ((1_minus f) . c) <= (g . c) * ((1_minus f) . c)
by XREAL_1:66;
then
(h . c) * (1 - (f . c)) <= (g . c) * ((1_minus f) . c)
by FUZZY_1:def 6;
then
(h . c) * (1 - (f . c)) <= (g . c) * (1 - (f . c))
by FUZZY_1:def 6;
then A7:
(((h . c) * 1) - ((h . c) * (f . c))) + (f . c) <= ((g . c) * (1 - (f . c))) + (f . c)
by XREAL_1:8;
A8:
(f ++ (min g,h)) . c = ((f . c) + (h . c)) - ((f . c) * (h . c))
by A2, A6, FUZZY_1:6;
((f . c) + (h . c)) - ((f . c) * (h . c)) =
min (((f . c) + (g . c)) - ((f . c) * (g . c))),
(((f . c) + (h . c)) - ((f . c) * (h . c)))
by A7, XXREAL_0:def 9
.=
min ((f ++ g) . c),
(((f . c) + (h . c)) - ((f . c) * (h . c)))
by Def3
.=
min ((f ++ g) . c),
((f ++ h) . c)
by Def3
;
hence
(f ++ (min g,h)) . c = (min (f ++ g),(f ++ h)) . c
by A8, FUZZY_1:6;
:: thesis: verum
end; hence
(
c in C implies
(f ++ (min g,h)) . c = (min (f ++ g),(f ++ h)) . c )
;
:: thesis: verum end;
hence
(
c in C implies
(f ++ (min g,h)) . c = (min (f ++ g),(f ++ h)) . c )
;
:: thesis: verum
end;
hence
f ++ (min g,h) = min (f ++ g),(f ++ h)
by A1, PARTFUN1:34; :: thesis: verum