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 20;
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 20;
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 20;
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 20;
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 20;
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 20;
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 20;
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:2; verum