let L be LATTICE; :: thesis: for l being Element of L holds
( l is prime iff for x being set
for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds
( f . p = {} iff p <= l ) ) holds
( f is meet-preserving & f is join-preserving ) )
let l be Element of L; :: thesis: ( l is prime iff for x being set
for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds
( f . p = {} iff p <= l ) ) holds
( f is meet-preserving & f is join-preserving ) )
thus
( l is prime implies for x being set
for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds
( f . p = {} iff p <= l ) ) holds
( f is meet-preserving & f is join-preserving ) )
:: thesis: ( ( for x being set
for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds
( f . p = {} iff p <= l ) ) holds
( f is meet-preserving & f is join-preserving ) ) implies l is prime )proof
assume A1:
l is
prime
;
:: thesis: for x being set
for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds
( f . p = {} iff p <= l ) ) holds
( f is meet-preserving & f is join-preserving )
let x be
set ;
:: thesis: for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds
( f . p = {} iff p <= l ) ) holds
( f is meet-preserving & f is join-preserving )let f be
Function of
L,
(BoolePoset {x});
:: thesis: ( ( for p being Element of L holds
( f . p = {} iff p <= l ) ) implies ( f is meet-preserving & f is join-preserving ) )
assume A2:
for
p being
Element of
L holds
(
f . p = {} iff
p <= l )
;
:: thesis: ( f is meet-preserving & f is join-preserving )
A3:
(
dom f = the
carrier of
L &
rng f c= the
carrier of
(BoolePoset {x}) )
by FUNCT_2:def 1;
A4: the
carrier of
(BoolePoset {x}) =
the
carrier of
(InclPoset (bool {x}))
by YELLOW_1:4
.=
bool {x}
by YELLOW_1:1
.=
{{} ,{x}}
by ZFMISC_1:30
;
for
z,
y being
Element of
L holds
f preserves_inf_of {z,y}
proof
let z,
y be
Element of
L;
:: thesis: f preserves_inf_of {z,y}
A5:
f .: {z,y} = {(f . z),(f . y)}
by A3, FUNCT_1:118;
then A6:
(
ex_inf_of {z,y},
L implies
ex_inf_of f .: {z,y},
BoolePoset {x} )
by YELLOW_0:21;
inf (f .: {z,y}) =
(f . z) "/\" (f . y)
by A5, YELLOW_0:40
.=
f . (inf {z,y})
by A7, YELLOW_0:40
;
hence
f preserves_inf_of {z,y}
by A6, WAYBEL_0:def 30;
:: thesis: verum
end;
hence
f is
meet-preserving
by WAYBEL_0:def 34;
:: thesis: f is join-preserving
for
z,
y being
Element of
L holds
f preserves_sup_of {z,y}
proof
let z,
y be
Element of
L;
:: thesis: f preserves_sup_of {z,y}
A16:
f .: {z,y} = {(f . z),(f . y)}
by A3, FUNCT_1:118;
then A17:
(
ex_sup_of {z,y},
L implies
ex_sup_of f .: {z,y},
BoolePoset {x} )
by YELLOW_0:20;
sup (f .: {z,y}) =
(f . z) "\/" (f . y)
by A16, YELLOW_0:41
.=
f . (sup {z,y})
by A18, YELLOW_0:41
;
hence
f preserves_sup_of {z,y}
by A17, WAYBEL_0:def 31;
:: thesis: verum
end;
hence
f is
join-preserving
by WAYBEL_0:def 35;
:: thesis: verum
end;
thus
( ( for x being set
for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds
( f . p = {} iff p <= l ) ) holds
( f is meet-preserving & f is join-preserving ) ) implies l is prime )
:: thesis: verumproof
assume A27:
for
x being
set for
f being
Function of
L,
(BoolePoset {x}) st ( for
p being
Element of
L holds
(
f . p = {} iff
p <= l ) ) holds
(
f is
meet-preserving &
f is
join-preserving )
;
:: thesis: l is prime
let z,
y be
Element of
L;
:: according to WAYBEL_6:def 6 :: thesis: ( not z "/\" y <= l or z <= l or y <= l )
assume A28:
z "/\" y <= l
;
:: thesis: ( z <= l or y <= l )
A29: the
carrier of
(BoolePoset {{} }) =
the
carrier of
(InclPoset (bool {{} }))
by YELLOW_1:4
.=
bool {{} }
by YELLOW_1:1
.=
{{} ,{{} }}
by ZFMISC_1:30
;
defpred S1[
Element of
L,
set ]
means ( $1
<= l iff $2
= {} );
A30:
for
a being
Element of
L ex
b being
Element of
(BoolePoset {{} }) st
S1[
a,
b]
consider f being
Function of
L,
(BoolePoset {{} }) such that A33:
for
p being
Element of
L holds
S1[
p,
f . p]
from FUNCT_2:sch 10(A30);
(
dom f = the
carrier of
L &
rng f c= the
carrier of
(BoolePoset {{} }) )
by FUNCT_2:def 1;
then A34:
f .: {z,y} = {(f . z),(f . y)}
by FUNCT_1:118;
A35:
ex_inf_of {z,y},
L
by YELLOW_0:21;
f is
meet-preserving
by A27, A33;
then A36:
f preserves_inf_of {z,y}
by WAYBEL_0:def 34;
A37:
{} =
f . (z "/\" y)
by A28, A33
.=
f . (inf {z,y})
by YELLOW_0:40
.=
inf {(f . z),(f . y)}
by A34, A35, A36, WAYBEL_0:def 30
.=
(f . z) "/\" (f . y)
by YELLOW_0:40
.=
(f . z) /\ (f . y)
by YELLOW_1:17
;
hence
(
z <= l or
y <= l )
by A33;
:: thesis: verum
end;