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
for X being Subset of (product J)
for i being Element of I holds (inf X) . i = inf (pi (X,i))
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 for X being Subset of (product J)
for i being Element of I holds (inf X) . i = inf (pi (X,i)) )
assume A1: for i being Element of I holds J . i is complete LATTICE ; :: thesis: for X being Subset of (product J)
for i being Element of I holds (inf X) . i = inf (pi (X,i))
then reconsider L = product J as complete LATTICE by WAYBEL_3:31;
let X be Subset of (product J); :: thesis: for i being Element of I holds (inf X) . i = inf (pi (X,i))
let i be Element of I; :: thesis: (inf X) . i = inf (pi (X,i))
A2: L is complete ;
then A3: inf X is_<=_than X by YELLOW_0:33;
A4: (inf X) . i is_<=_than pi (X,i)
proof
let a be Element of (J . i); :: according to LATTICE3:def 8 :: thesis: ( not a in pi (X,i) or (inf X) . i <= a )
assume a in pi (X,i) ; :: thesis: (inf X) . i <= a
then consider f being Function such that
A5: f in X and
A6: a = f . i by CARD_3:def 6;
reconsider f = f as Element of (product J) by A5;
inf X <= f by A3, A5;
hence (inf X) . i <= a by A6, WAYBEL_3:28; :: thesis: verum
end;
A7: now :: thesis: for a being Element of (J . i) st a is_<=_than pi (X,i) holds
(inf X) . i >= a
let a be Element of (J . i); :: thesis: ( a is_<=_than pi (X,i) implies (inf X) . i >= a )
set f = (inf X) +* (i,a);
A8: dom ((inf X) +* (i,a)) = dom (inf X) by FUNCT_7:30;
A9: dom (inf X) = I by WAYBEL_3:27;
now :: thesis: for j being Element of I holds ((inf X) +* (i,a)) . j is Element of (J . j)
let j be Element of I; :: thesis: ((inf X) +* (i,a)) . j is Element of (J . j)
( j = i or j <> i ) ;
then ( ((inf X) +* (i,a)) . j = (inf X) . j or ( ((inf X) +* (i,a)) . j = a & j = i ) ) by A9, FUNCT_7:31, FUNCT_7:32;
hence ((inf X) +* (i,a)) . j is Element of (J . j) ; :: thesis: verum
end;
then reconsider f = (inf X) +* (i,a) as Element of (product J) by A8, WAYBEL_3:27;
assume A10: a is_<=_than pi (X,i) ; :: thesis: (inf X) . i >= a
f is_<=_than X
proof
let g be Element of (product J); :: according to LATTICE3:def 8 :: thesis: ( not g in X or f <= g )
assume g in X ; :: thesis: f <= g
then A11: ( g >= inf X & g . i in pi (X,i) ) by A2, CARD_3:def 6, YELLOW_2:22;
now :: thesis: for j being Element of I holds f . j <= g . j
let j be Element of I; :: thesis: f . j <= g . j
( j = i or j <> i ) ;
then ( f . j = (inf X) . j or ( f . j = a & j = i ) ) by A9, FUNCT_7:31, FUNCT_7:32;
hence f . j <= g . j by A10, A11, WAYBEL_3:28; :: thesis: verum
end;
hence f <= g by WAYBEL_3:28; :: thesis: verum
end;
then A12: f <= inf X by A2, YELLOW_0:33;
f . i = a by A9, FUNCT_7:31;
hence (inf X) . i >= a by A12, WAYBEL_3:28; :: thesis: verum
end;
J . i is complete LATTICE by A1;
hence (inf X) . i = inf (pi (X,i)) by A4, A7, YELLOW_0:33; :: thesis: verum