let Y be non empty set ; for a, b being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y holds B_INF (a '&' b),PA = (B_INF a,PA) '&' (B_INF b,PA)
let a, b be Element of Funcs Y,BOOLEAN ; for PA being a_partition of Y holds B_INF (a '&' b),PA = (B_INF a,PA) '&' (B_INF b,PA)
let PA be a_partition of Y; B_INF (a '&' b),PA = (B_INF a,PA) '&' (B_INF b,PA)
consider k3 being Function such that
A1:
B_INF (a '&' b),PA = k3
and
A2:
dom k3 = Y
and
rng k3 c= BOOLEAN
by FUNCT_2:def 2;
consider k4 being Function such that
A3:
(B_INF a,PA) '&' (B_INF b,PA) = k4
and
A4:
dom k4 = Y
and
rng k4 c= BOOLEAN
by FUNCT_2:def 2;
for y being Element of Y holds (B_INF (a '&' b),PA) . y = ((B_INF a,PA) '&' (B_INF b,PA)) . y
proof
let y be
Element of
Y;
(B_INF (a '&' b),PA) . y = ((B_INF a,PA) '&' (B_INF b,PA)) . y
A5:
now assume that
for
x being
Element of
Y st
x in EqClass y,
PA holds
a . x = TRUE
and A6:
ex
x being
Element of
Y st
(
x in EqClass y,
PA & not
b . x = TRUE )
;
(B_INF (a '&' b),PA) . y = ((B_INF a,PA) '&' (B_INF b,PA)) . y
(B_INF b,PA) . y = FALSE
by A6, Def19;
then
((B_INF a,PA) . y) '&' ((B_INF b,PA) . y) = FALSE
;
then A7:
((B_INF a,PA) '&' (B_INF b,PA)) . y = FALSE
by MARGREL1:def 21;
consider x1 being
Element of
Y such that A8:
x1 in EqClass y,
PA
and A9:
b . x1 <> TRUE
by A6;
b . x1 = FALSE
by A9, XBOOLEAN:def 3;
then
(a . x1) '&' (b . x1) = FALSE
;
then
(a '&' b) . x1 <> TRUE
by MARGREL1:def 21;
hence
(B_INF (a '&' b),PA) . y = ((B_INF a,PA) '&' (B_INF b,PA)) . y
by A8, A7, Def19;
verum end;
A10:
now assume that A11:
ex
x being
Element of
Y st
(
x in EqClass y,
PA & not
a . x = TRUE )
and A12:
ex
x being
Element of
Y st
(
x in EqClass y,
PA & not
b . x = TRUE )
;
(B_INF (a '&' b),PA) . y = ((B_INF a,PA) '&' (B_INF b,PA)) . y
(B_INF b,PA) . y = FALSE
by A12, Def19;
then
((B_INF a,PA) . y) '&' ((B_INF b,PA) . y) = FALSE
;
then A13:
((B_INF a,PA) '&' (B_INF b,PA)) . y = FALSE
by MARGREL1:def 21;
consider xa being
Element of
Y such that A14:
xa in EqClass y,
PA
and A15:
a . xa <> TRUE
by A11;
a . xa = FALSE
by A15, XBOOLEAN:def 3;
then
(a . xa) '&' (b . xa) = FALSE
;
then
(a '&' b) . xa <> TRUE
by MARGREL1:def 21;
hence
(B_INF (a '&' b),PA) . y = ((B_INF a,PA) '&' (B_INF b,PA)) . y
by A14, A13, Def19;
verum end;
A16:
now assume that A17:
for
x being
Element of
Y st
x in EqClass y,
PA holds
a . x = TRUE
and A18:
for
x being
Element of
Y st
x in EqClass y,
PA holds
b . x = TRUE
;
(B_INF (a '&' b),PA) . y = ((B_INF a,PA) '&' (B_INF b,PA)) . yA19:
for
x being
Element of
Y st
x in EqClass y,
PA holds
(a '&' b) . x = TRUE
(B_INF b,PA) . y = TRUE
by A18, Def19;
then
((B_INF a,PA) . y) '&' ((B_INF b,PA) . y) = TRUE '&' TRUE
by A17, Def19;
then
((B_INF a,PA) '&' (B_INF b,PA)) . y = TRUE
by MARGREL1:def 21;
hence
(B_INF (a '&' b),PA) . y = ((B_INF a,PA) '&' (B_INF b,PA)) . y
by A19, Def19;
verum end;
now assume that A21:
ex
x being
Element of
Y st
(
x in EqClass y,
PA & not
a . x = TRUE )
and A22:
for
x being
Element of
Y st
x in EqClass y,
PA holds
b . x = TRUE
;
(B_INF (a '&' b),PA) . y = ((B_INF a,PA) '&' (B_INF b,PA)) . y
(B_INF b,PA) . y = TRUE
by A22, Def19;
then
((B_INF a,PA) . y) '&' ((B_INF b,PA) . y) = FALSE '&' TRUE
by A21, Def19;
then A23:
((B_INF a,PA) '&' (B_INF b,PA)) . y = FALSE
by MARGREL1:def 21;
consider x1 being
Element of
Y such that A24:
x1 in EqClass y,
PA
and A25:
a . x1 <> TRUE
by A21;
a . x1 = FALSE
by A25, XBOOLEAN:def 3;
then
(a . x1) '&' (b . x1) = FALSE
;
then
(a '&' b) . x1 <> TRUE
by MARGREL1:def 21;
hence
(B_INF (a '&' b),PA) . y = ((B_INF a,PA) '&' (B_INF b,PA)) . y
by A24, A23, Def19;
verum end;
hence
(B_INF (a '&' b),PA) . y = ((B_INF a,PA) '&' (B_INF b,PA)) . y
by A16, A5, A10;
verum
end;
then
for u being set st u in Y holds
k3 . u = k4 . u
by A1, A3;
hence
B_INF (a '&' b),PA = (B_INF a,PA) '&' (B_INF b,PA)
by A1, A2, A3, A4, FUNCT_1:9; verum