let I be non empty set ; for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete Heyting LATTICE ) holds
( product J is complete & product J is Heyting )
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; ( ( for i being Element of I holds J . i is complete Heyting LATTICE ) implies ( product J is complete & product J is Heyting ) )
assume A1:
for i being Element of I holds J . i is complete Heyting LATTICE
; ( product J is complete & product J is Heyting )
A2:
for i being Element of I holds J . i is complete LATTICE
by A1;
set H = product J;
reconsider H = product J as complete LATTICE by A2, WAYBEL_3:31;
H = H
;
hence
( product J is complete & product J is LATTICE )
; WAYBEL_1:def 19 for b1 being Element of the carrier of (product J) holds b1 "/\" is lower_adjoint
let f be Element of (product J); f "/\" is lower_adjoint
reconsider g = f as Element of H ;
reconsider F = f "/\" as Function of H,H ;
A3:
for i being Element of I holds J . i is Semilattice
by A1;
F is sups-preserving
proof
let X be
Subset of
H;
WAYBEL_0:def 33 F preserves_sup_of X
reconsider Y =
F .: X,
X9 =
X as
Subset of
(product J) ;
reconsider sX =
sup X as
Element of
(product J) ;
assume
ex_sup_of X,
H
;
WAYBEL_0:def 31 ( ex_sup_of F .: X,H & "\/" ((F .: X),H) = F . ("\/" (X,H)) )
thus
ex_sup_of F .: X,
H
by YELLOW_0:17;
"\/" ((F .: X),H) = F . ("\/" (X,H))
reconsider f1 =
sup (F .: X),
f2 =
F . (sup X) as
Element of
(product J) ;
A4:
now for x being object st x in dom f1 holds
f1 . x = f2 . xlet x be
object ;
( x in dom f1 implies f1 . x = f2 . x )assume
x in dom f1
;
f1 . x = f2 . xthen reconsider i =
x as
Element of
I by WAYBEL_3:27;
A5:
J . i is
complete Heyting LATTICE
by A1;
then A6:
ex_sup_of pi (
X9,
i),
J . i
by YELLOW_0:17;
A7:
((f . i) "/\") .: (pi (X9,i)) c= pi (
Y,
i)
proof
let b be
object ;
TARSKI:def 3 ( not b in ((f . i) "/\") .: (pi (X9,i)) or b in pi (Y,i) )
assume
b in ((f . i) "/\") .: (pi (X9,i))
;
b in pi (Y,i)
then consider f4 being
object such that
f4 in dom ((f . i) "/\")
and A8:
f4 in pi (
X9,
i)
and A9:
b = ((f . i) "/\") . f4
by FUNCT_1:def 6;
consider f5 being
Function such that A10:
f5 in X9
and A11:
f4 = f5 . i
by A8, CARD_3:def 6;
reconsider f5 =
f5 as
Element of
(product J) by A10;
f "/\" f5 = (f "/\") . f5
by WAYBEL_1:def 18;
then A12:
f "/\" f5 in (f "/\") .: X
by A10, FUNCT_2:35;
((f . i) "/\") . f4 =
(f . i) "/\" (f5 . i)
by A11, WAYBEL_1:def 18
.=
(f "/\" f5) . i
by A3, Th11
;
hence
b in pi (
Y,
i)
by A9, A12, CARD_3:def 6;
verum
end;
pi (
Y,
i)
c= ((f . i) "/\") .: (pi (X9,i))
proof
let a be
object ;
TARSKI:def 3 ( not a in pi (Y,i) or a in ((f . i) "/\") .: (pi (X9,i)) )
assume
a in pi (
Y,
i)
;
a in ((f . i) "/\") .: (pi (X9,i))
then consider f3 being
Function such that A13:
f3 in Y
and A14:
a = f3 . i
by CARD_3:def 6;
reconsider f3 =
f3 as
Element of
(product J) by A13;
consider h being
object such that A15:
h in dom F
and A16:
h in X
and A17:
f3 = F . h
by A13, FUNCT_1:def 6;
reconsider h =
h as
Element of
(product J) by A15;
A18:
h . i in pi (
X9,
i)
by A16, CARD_3:def 6;
f3 . i =
(f "/\" h) . i
by A17, WAYBEL_1:def 18
.=
(f . i) "/\" (h . i)
by A3, Th11
.=
((f . i) "/\") . (h . i)
by WAYBEL_1:def 18
;
hence
a in ((f . i) "/\") .: (pi (X9,i))
by A14, A18, FUNCT_2:35;
verum
end; then A19:
pi (
Y,
i)
= ((f . i) "/\") .: (pi (X9,i))
by A7;
(f . i) "/\" is
lower_adjoint
by A5, WAYBEL_1:def 19;
then A20:
(f . i) "/\" preserves_sup_of pi (
X9,
i)
by A5, WAYBEL_0:def 33;
f2 = g "/\" (sup X)
by WAYBEL_1:def 18;
then f2 . i =
(f . i) "/\" (sX . i)
by A3, Th11
.=
(f . i) "/\" (sup (pi (X9,i)))
by A2, WAYBEL_3:32
.=
((f . i) "/\") . (sup (pi (X9,i)))
by WAYBEL_1:def 18
.=
sup (((f . i) "/\") .: (pi (X9,i)))
by A20, A6
;
hence
f1 . x = f2 . x
by A2, A19, WAYBEL_3:32;
verum end;
(
dom f1 = I &
dom f2 = I )
by WAYBEL_3:27;
hence
"\/" (
(F .: X),
H)
= F . ("\/" (X,H))
by A4, FUNCT_1:2;
verum
end;
hence
f "/\" is lower_adjoint
by WAYBEL_1:17; verum