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 let x be
set ;
( 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
set ;
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
set such that
f4 in dom ((f . i) "/\" )
and A8:
f4 in pi X9,
i
and A9:
b = ((f . i) "/\" ) . f4
by FUNCT_1:def 12;
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:43;
((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
set ;
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
set such that A15:
h in dom F
and A16:
h in X
and A17:
f3 = F . h
by A13, FUNCT_1:def 12;
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:43;
verum
end; then A19:
pi Y,
i = ((f . i) "/\" ) .: (pi X9,i)
by A7, XBOOLE_0:def 10;
(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, WAYBEL_0:def 31
;
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:9;
verum
end;
hence
f "/\" is lower_adjoint
by WAYBEL_1:18; verum