let I be non empty set ; :: thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete LATTICE ) holds
product J is complete LATTICE
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; :: thesis: ( ( for i being Element of I holds J . i is complete LATTICE ) implies product J is complete LATTICE )
assume A1: for i being Element of I holds J . i is complete LATTICE ; :: thesis: product J is complete LATTICE
then A2: for i being Element of I holds J . i is transitive ;
for i being Element of I holds J . i is antisymmetric by A1;
then reconsider L = product J as non empty Poset by A2, Th29, Th30;
now :: thesis: for X being Subset of (product J) holds ex_sup_of X, product J
let X be Subset of (product J); :: thesis: ex_sup_of X, product J
deffunc H1( Element of I) -> Element of the carrier of (J . $1) = sup (pi (X,$1));
consider f being ManySortedSet of I such that
A3: for i being Element of I holds f . i = H1(i) from PBOOLE:sch 5();
A4: dom f = I by PARTFUN1:def 2;
now :: thesis: for i being Element of I holds f . i is Element of (J . i)
let i be Element of I; :: thesis: f . i is Element of (J . i)
f . i = sup (pi (X,i)) by A3;
hence f . i is Element of (J . i) ; :: thesis: verum
end;
then reconsider f = f as Element of (product J) by A4, Th27;
A5: f is_>=_than X
proof
let x be Element of (product J); :: according to LATTICE3:def 9 :: thesis: ( not x in X or x <= f )
assume A6: x in X ; :: thesis: x <= f
now :: thesis: for i being Element of I holds x . i <= f . i
let i be Element of I; :: thesis: x . i <= f . i
A7: x . i in pi (X,i) by A6, CARD_3:def 6;
A8: J . i is complete LATTICE by A1;
f . i = sup (pi (X,i)) by A3;
hence x . i <= f . i by A7, A8, YELLOW_2:22; :: thesis: verum
end;
hence x <= f by Th28; :: thesis: verum
end;
now :: thesis: for g being Element of (product J) st X is_<=_than g holds
f <= g
let g be Element of (product J); :: thesis: ( X is_<=_than g implies f <= g )
assume A9: X is_<=_than g ; :: thesis: f <= g
now :: thesis: ( L = L & ( for i being Element of I holds f . i <= g . i ) )
thus L = L ; :: thesis: for i being Element of I holds f . i <= g . i
let i be Element of I; :: thesis: f . i <= g . i
A10: f . i = sup (pi (X,i)) by A3;
A11: J . i is complete LATTICE by A1;
g . i is_>=_than pi (X,i)
proof
let a be Element of (J . i); :: according to LATTICE3:def 9 :: thesis: ( not a in pi (X,i) or a <= g . i )
assume a in pi (X,i) ; :: thesis: a <= g . i
then consider h being Function such that
A12: h in X and
A13: a = h . i by CARD_3:def 6;
reconsider h = h as Element of (product J) by A12;
h <= g by A9, A12;
hence a <= g . i by A13, Th28; :: thesis: verum
end;
hence f . i <= g . i by A10, A11, YELLOW_0:32; :: thesis: verum
end;
hence f <= g by Th28; :: thesis: verum
end;
then ex_sup_of X,L by A5, YELLOW_0:15;
hence ex_sup_of X, product J ; :: thesis: verum
end;
then L is non empty complete Poset by YELLOW_0:53;
hence product J is complete LATTICE ; :: thesis: verum