let Y be non empty set ; for G being Subset of (PARTITIONS Y)
for u, a being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex (u '&' a),PA,G = u '&' (Ex a,PA,G)
let G be Subset of (PARTITIONS Y); for u, a being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex (u '&' a),PA,G = u '&' (Ex a,PA,G)
let u, a be Element of Funcs Y,BOOLEAN ; for PA being a_partition of Y st u is_independent_of PA,G holds
Ex (u '&' a),PA,G = u '&' (Ex a,PA,G)
let PA be a_partition of Y; ( u is_independent_of PA,G implies Ex (u '&' a),PA,G = u '&' (Ex a,PA,G) )
assume
u is_independent_of PA,G
; Ex (u '&' a),PA,G = u '&' (Ex a,PA,G)
then A1:
u is_dependent_of CompF PA,G
by Def8;
A2:
Ex (u '&' a),PA,G '<' u '&' (Ex a,PA,G)
proof
let z be
Element of
Y;
BVFUNC_1:def 15 ( not (Ex (u '&' a),PA,G) . z = TRUE or (u '&' (Ex a,PA,G)) . z = TRUE )
assume
(Ex (u '&' a),PA,G) . z = TRUE
;
(u '&' (Ex a,PA,G)) . z = TRUE
then consider x1 being
Element of
Y such that A3:
x1 in EqClass z,
(CompF PA,G)
and A4:
(u '&' a) . x1 = TRUE
by BVFUNC_1:def 20;
A5:
(u . x1) '&' (a . x1) = TRUE
by A4, MARGREL1:def 21;
then
a . x1 = TRUE
by MARGREL1:45;
then A6:
(Ex a,PA,G) . z = TRUE
by A3, BVFUNC_1:def 20;
z in EqClass z,
(CompF PA,G)
by EQREL_1:def 8;
then A7:
u . z = u . x1
by A1, A3, BVFUNC_1:def 18;
u . x1 = TRUE
by A5, MARGREL1:45;
then (u '&' (Ex a,PA,G)) . z =
TRUE '&' TRUE
by A6, A7, MARGREL1:def 21
.=
TRUE
;
hence
(u '&' (Ex a,PA,G)) . z = TRUE
;
verum
end;
u '&' (Ex a,PA,G) '<' Ex (u '&' a),PA,G
proof
let z be
Element of
Y;
BVFUNC_1:def 15 ( not (u '&' (Ex a,PA,G)) . z = TRUE or (Ex (u '&' a),PA,G) . z = TRUE )
assume
(u '&' (Ex a,PA,G)) . z = TRUE
;
(Ex (u '&' a),PA,G) . z = TRUE
then A8:
(u . z) '&' ((Ex a,PA,G) . z) = TRUE
by MARGREL1:def 21;
then A9:
u . z = TRUE
by MARGREL1:45;
(Ex a,PA,G) . z = TRUE
by A8, MARGREL1:45;
then consider x1 being
Element of
Y such that A10:
x1 in EqClass z,
(CompF PA,G)
and A11:
a . x1 = TRUE
by BVFUNC_1:def 20;
z in EqClass z,
(CompF PA,G)
by EQREL_1:def 8;
then
u . x1 = u . z
by A1, A10, BVFUNC_1:def 18;
then (u '&' a) . x1 =
TRUE '&' TRUE
by A9, A11, MARGREL1:def 21
.=
TRUE
;
hence
(Ex (u '&' a),PA,G) . z = TRUE
by A10, BVFUNC_1:def 20;
verum
end;
hence
Ex (u '&' a),PA,G = u '&' (Ex a,PA,G)
by A2, BVFUNC_1:18; verum