let Y be non empty set ; :: thesis: 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); :: thesis: 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 ; :: thesis: 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; :: thesis: ( u is_independent_of PA,G implies Ex (u '&' a),PA,G = u '&' (Ex a,PA,G) )
assume
u is_independent_of PA,G
; :: thesis: 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;
:: according to BVFUNC_1:def 15 :: thesis: ( not (Ex (u '&' a),PA,G) . z = TRUE or (u '&' (Ex a,PA,G)) . z = TRUE )
assume
(Ex (u '&' a),PA,G) . z = TRUE
;
:: thesis: (u '&' (Ex a,PA,G)) . z = TRUE
then consider x1 being
Element of
Y such that A3:
(
x1 in EqClass z,
(CompF PA,G) &
(u '&' a) . x1 = TRUE )
by BVFUNC_1:def 20;
(u . x1) '&' (a . x1) = TRUE
by A3, MARGREL1:def 21;
then A4:
(
u . x1 = TRUE &
a . x1 = TRUE )
by MARGREL1:45;
A5:
(
z in EqClass z,
(CompF PA,G) &
EqClass z,
(CompF PA,G) in CompF PA,
G )
by EQREL_1:def 8;
A6:
(Ex a,PA,G) . z = TRUE
by A3, A4, BVFUNC_1:def 20;
u . z = u . x1
by A1, A3, A5, BVFUNC_1:def 18;
then (u '&' (Ex a,PA,G)) . z =
TRUE '&' TRUE
by A4, A6, MARGREL1:def 21
.=
TRUE
;
hence
(u '&' (Ex a,PA,G)) . z = TRUE
;
:: thesis: verum
end;
u '&' (Ex a,PA,G) '<' Ex (u '&' a),PA,G
proof
let z be
Element of
Y;
:: according to BVFUNC_1:def 15 :: thesis: ( not (u '&' (Ex a,PA,G)) . z = TRUE or (Ex (u '&' a),PA,G) . z = TRUE )
assume
(u '&' (Ex a,PA,G)) . z = TRUE
;
:: thesis: (Ex (u '&' a),PA,G) . z = TRUE
then
(u . z) '&' ((Ex a,PA,G) . z) = TRUE
by MARGREL1:def 21;
then A7:
(
u . z = TRUE &
(Ex a,PA,G) . z = TRUE )
by MARGREL1:45;
A8:
(
z in EqClass z,
(CompF PA,G) &
EqClass z,
(CompF PA,G) in CompF PA,
G )
by EQREL_1:def 8;
consider x1 being
Element of
Y such that A9:
(
x1 in EqClass z,
(CompF PA,G) &
a . x1 = TRUE )
by A7, BVFUNC_1:def 20;
u . x1 = u . z
by A1, A8, A9, BVFUNC_1:def 18;
then (u '&' a) . x1 =
TRUE '&' TRUE
by A7, A9, MARGREL1:def 21
.=
TRUE
;
hence
(Ex (u '&' a),PA,G) . z = TRUE
by A9, BVFUNC_1:def 20;
:: thesis: verum
end;
hence
Ex (u '&' a),PA,G = u '&' (Ex a,PA,G)
by A2, BVFUNC_1:18; :: thesis: verum