let L, T be complete continuous LATTICE; :: thesis: 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; :: thesis: 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:]; :: thesis: ( 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)
; :: thesis: subrelstr SL is CLSubFrame of [:L,L:]
A2:
( g is infs-preserving & g is directed-sups-preserving )
by WAYBEL16:def 1;
set pL = [:L,L:];
set pg = [:g,g:];
set pT = [:T,T:];
consider x being Element of L;
A3:
dom g = the carrier of L
by FUNCT_2:def 1;
then A4:
[x,x] in [:(dom g),(dom g):]
by ZFMISC_1:106;
A5:
dom [:g,g:] = [:(dom g),(dom g):]
by FUNCT_3:def 9;
[(g . x),(g . x)] in id the carrier of T
by RELAT_1:def 10;
then
[:g,g:] . x,x in id the carrier of T
by A3, FUNCT_3:def 9;
then reconsider nSL = SL as non empty Subset of [:L,L:] by A1, A4, A5, FUNCT_1:def 13;
A6:
not subrelstr nSL is empty
;
A7:
the carrier of [:L,L:] = [:the carrier of L,the carrier of L:]
by YELLOW_3:def 2;
A8:
subrelstr SL is infs-inheriting
proof
let X be
Subset of
(subrelstr SL);
:: according to YELLOW_0:def 18 :: thesis: ( not ex_inf_of X,[:L,L:] or "/\" X,[:L,L:] in the carrier of (subrelstr SL) )
assume A9:
ex_inf_of X,
[:L,L:]
;
:: thesis: "/\" X,[:L,L:] in the carrier of (subrelstr SL)
X c= the
carrier of
(subrelstr SL)
;
then A10:
X c= SL
by YELLOW_0:def 15;
then reconsider X' =
X as
Subset of
[:L,L:] by XBOOLE_1:1;
consider x,
y being
set such that A11:
(
x in the
carrier of
L &
y in the
carrier of
L )
and A12:
inf X' = [x,y]
by A7, ZFMISC_1:def 2;
[:g,g:] is
infs-preserving
by A2, Th9;
then
[:g,g:] preserves_inf_of X'
by WAYBEL_0:def 32;
then A13:
(
ex_inf_of [:g,g:] .: X',
[:T,T:] &
inf ([:g,g:] .: X') = [:g,g:] . (inf X') )
by A9, WAYBEL_0:def 30;
A14:
[:g,g:] .: X c= [:g,g:] .: SL
by A10, RELAT_1:156;
A15:
[:g,g:] .: SL c= id the
carrier of
T
by A1, FUNCT_1:145;
ex_inf_of [:g,g:] .: X',
[:T,T:]
by YELLOW_0:17;
then A16:
inf ([:g,g:] .: X') in id the
carrier of
T
by A14, A15, Th13, XBOOLE_1:1;
[x,y] in [:(dom g),(dom g):]
by A3, A11, ZFMISC_1:106;
then
[x,y] in dom [:g,g:]
by FUNCT_3:def 9;
then
[x,y] in [:g,g:] " (id the carrier of T)
by A12, A13, A16, FUNCT_1:def 13;
hence
"/\" X,
[:L,L:] in the
carrier of
(subrelstr SL)
by A1, A12, YELLOW_0:def 15;
:: thesis: verum
end;
subrelstr SL is directed-sups-inheriting
proof
let X be
directed Subset of
(subrelstr SL);
:: according to WAYBEL_0:def 4 :: thesis: ( X = {} or not ex_sup_of X,[:L,L:] or "\/" X,[:L,L:] in the carrier of (subrelstr SL) )
assume that A17:
X <> {}
and A18:
ex_sup_of X,
[:L,L:]
;
:: thesis: "\/" X,[:L,L:] in the carrier of (subrelstr SL)
X c= the
carrier of
(subrelstr SL)
;
then A19:
X c= SL
by YELLOW_0:def 15;
reconsider X' =
X as non
empty directed Subset of
[:L,L:] by A6, A17, YELLOW_2:7;
consider x,
y being
set such that A20:
(
x in the
carrier of
L &
y in the
carrier of
L )
and A21:
sup X' = [x,y]
by A7, ZFMISC_1:def 2;
[:g,g:] is
directed-sups-preserving
by A2, Th12;
then
[:g,g:] preserves_sup_of X'
by WAYBEL_0:def 37;
then A22:
(
ex_sup_of [:g,g:] .: X',
[:T,T:] &
sup ([:g,g:] .: X') = [:g,g:] . (sup X') )
by A18, WAYBEL_0:def 31;
A23:
[:g,g:] .: X c= [:g,g:] .: SL
by A19, RELAT_1:156;
A24:
[:g,g:] .: SL c= id the
carrier of
T
by A1, FUNCT_1:145;
ex_sup_of [:g,g:] .: X',
[:T,T:]
by YELLOW_0:17;
then A25:
sup ([:g,g:] .: X') in id the
carrier of
T
by A23, A24, Th14, XBOOLE_1:1;
[x,y] in [:(dom g),(dom g):]
by A3, A20, ZFMISC_1:106;
then
[x,y] in dom [:g,g:]
by FUNCT_3:def 9;
then
[x,y] in [:g,g:] " (id the carrier of T)
by A21, A22, A25, FUNCT_1:def 13;
hence
"\/" X,
[:L,L:] in the
carrier of
(subrelstr SL)
by A1, A21, YELLOW_0:def 15;
:: thesis: verum
end;
hence
subrelstr SL is CLSubFrame of [:L,L:]
by A8; :: thesis: verum