let L, T be complete continuous LATTICE; for g being CLHomomorphism of L,T
for S being Subset of [:L,L:] st S = [:g,g:] " (id the carrier of T) holds
subrelstr S is CLSubFrame of [:L,L:]
let g be CLHomomorphism of L,T; for S being Subset of [:L,L:] st S = [:g,g:] " (id the carrier of T) holds
subrelstr S is CLSubFrame of [:L,L:]
let SL be Subset of [:L,L:]; ( SL = [:g,g:] " (id the carrier of T) implies subrelstr SL is CLSubFrame of [:L,L:] )
assume A1:
SL = [:g,g:] " (id the carrier of T)
; subrelstr SL is CLSubFrame of [:L,L:]
set x = the Element of L;
A2:
dom g = the carrier of L
by FUNCT_2:def 1;
then A3:
[ the Element of L, the Element of L] in [:(dom g),(dom g):]
by ZFMISC_1:87;
[(g . the Element of L),(g . the Element of L)] in id the carrier of T
by RELAT_1:def 10;
then
( dom [:g,g:] = [:(dom g),(dom g):] & [:g,g:] . ( the Element of L, the Element of L) in id the carrier of T )
by A2, FUNCT_3:def 8;
then reconsider nSL = SL as non empty Subset of [:L,L:] by A1, A3, FUNCT_1:def 7;
set pL = [:L,L:];
set pg = [:g,g:];
A4:
( g is infs-preserving & g is directed-sups-preserving )
by WAYBEL16:def 1;
A5:
the carrier of [:L,L:] = [: the carrier of L, the carrier of L:]
by YELLOW_3:def 2;
A6:
not subrelstr nSL is empty
;
A7:
subrelstr SL is directed-sups-inheriting
proof
let X be
directed Subset of
(subrelstr SL);
WAYBEL_0:def 4 ( X = {} or not ex_sup_of X,[:L,L:] or "\/" (X,[:L,L:]) in the carrier of (subrelstr SL) )
assume that A8:
X <> {}
and A9:
ex_sup_of X,
[:L,L:]
;
"\/" (X,[:L,L:]) in the carrier of (subrelstr SL)
reconsider X9 =
X as non
empty directed Subset of
[:L,L:] by A6, A8, YELLOW_2:7;
[:g,g:] is
directed-sups-preserving
by A4, Th12;
then
[:g,g:] preserves_sup_of X9
;
then A10:
sup ([:g,g:] .: X9) = [:g,g:] . (sup X9)
by A9;
X c= the
carrier of
(subrelstr SL)
;
then
X c= SL
by YELLOW_0:def 15;
then A11:
[:g,g:] .: X c= [:g,g:] .: SL
by RELAT_1:123;
(
[:g,g:] .: SL c= id the
carrier of
T &
ex_sup_of [:g,g:] .: X9,
[:T,T:] )
by A1, FUNCT_1:75, YELLOW_0:17;
then A12:
sup ([:g,g:] .: X9) in id the
carrier of
T
by A11, Th14, XBOOLE_1:1;
consider x,
y being
object such that A13:
(
x in the
carrier of
L &
y in the
carrier of
L )
and A14:
sup X9 = [x,y]
by A5, ZFMISC_1:def 2;
[x,y] in [:(dom g),(dom g):]
by A2, A13, ZFMISC_1:87;
then
[x,y] in dom [:g,g:]
by FUNCT_3:def 8;
then
[x,y] in [:g,g:] " (id the carrier of T)
by A14, A10, A12, FUNCT_1:def 7;
hence
"\/" (
X,
[:L,L:])
in the
carrier of
(subrelstr SL)
by A1, A14, YELLOW_0:def 15;
verum
end;
subrelstr SL is infs-inheriting
proof
let X be
Subset of
(subrelstr SL);
YELLOW_0:def 18 ( not ex_inf_of X,[:L,L:] or "/\" (X,[:L,L:]) in the carrier of (subrelstr SL) )
assume A15:
ex_inf_of X,
[:L,L:]
;
"/\" (X,[:L,L:]) in the carrier of (subrelstr SL)
X c= the
carrier of
(subrelstr SL)
;
then A16:
X c= SL
by YELLOW_0:def 15;
then reconsider X9 =
X as
Subset of
[:L,L:] by XBOOLE_1:1;
A17:
(
[:g,g:] .: SL c= id the
carrier of
T &
ex_inf_of [:g,g:] .: X9,
[:T,T:] )
by A1, FUNCT_1:75, YELLOW_0:17;
[:g,g:] is
infs-preserving
by A4, Th9;
then
[:g,g:] preserves_inf_of X9
;
then A18:
inf ([:g,g:] .: X9) = [:g,g:] . (inf X9)
by A15;
[:g,g:] .: X c= [:g,g:] .: SL
by A16, RELAT_1:123;
then A19:
inf ([:g,g:] .: X9) in id the
carrier of
T
by A17, Th13, XBOOLE_1:1;
consider x,
y being
object such that A20:
(
x in the
carrier of
L &
y in the
carrier of
L )
and A21:
inf X9 = [x,y]
by A5, ZFMISC_1:def 2;
[x,y] in [:(dom g),(dom g):]
by A2, A20, ZFMISC_1:87;
then
[x,y] in dom [:g,g:]
by FUNCT_3:def 8;
then
[x,y] in [:g,g:] " (id the carrier of T)
by A21, A18, A19, FUNCT_1:def 7;
hence
"/\" (
X,
[:L,L:])
in the
carrier of
(subrelstr SL)
by A1, A21, YELLOW_0:def 15;
verum
end;
hence
subrelstr SL is CLSubFrame of [:L,L:]
by A7; verum