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 lower-bounded algebraic LATTICE ) holds
product J is lower-bounded algebraic LATTICE
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; :: thesis: ( ( for i being Element of I holds J . i is lower-bounded algebraic LATTICE ) implies product J is lower-bounded algebraic LATTICE )
assume A1: for i being Element of I holds J . i is lower-bounded algebraic LATTICE ; :: thesis: product J is lower-bounded algebraic LATTICE
then A2: for i being Element of I holds J . i is complete LATTICE ;
then reconsider L = product J as non empty lower-bounded LATTICE by WAYBEL_3:31;
for i being Element of I holds J . i is antisymmetric by A1;
then A3: product J is antisymmetric by WAYBEL_3:30;
now :: thesis: for x being Element of (product J) holds x = sup (compactbelow x)
let x be Element of (product J); :: thesis: x = sup (compactbelow x)
A4: for i being Element of I holds sup (compactbelow (x . i)) = (sup (compactbelow x)) . i
proof
let i be Element of I; :: thesis: sup (compactbelow (x . i)) = (sup (compactbelow x)) . i
A5: compactbelow (x . i) c= pi ((compactbelow x),i)
proof
deffunc H1( Element of I) -> Element of the carrier of (J . $1) = Bottom (J . $1);
defpred S1[ set ] means $1 = i;
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in compactbelow (x . i) or v in pi ((compactbelow x),i) )
assume v in compactbelow (x . i) ; :: thesis: v in pi ((compactbelow x),i)
then v in { y where y is Element of (J . i) : ( x . i >= y & y is compact ) } by WAYBEL_8:def 2;
then consider v1 being Element of (J . i) such that
A6: v1 = v and
A7: x . i >= v1 and
A8: v1 is compact ;
deffunc H2( set ) -> Element of (J . i) = v1;
consider f being Function such that
A9: dom f = I and
A10: for j being Element of I holds
( ( S1[j] implies f . j = H2(j) ) & ( not S1[j] implies f . j = H1(j) ) ) from PARTFUN1:sch 4();
 A11: f . i = v1 by A10;
now :: thesis: for k being Element of I holds f . k is Element of (J . k)
let k be Element of I; :: thesis: f . k is Element of (J . k)
now :: thesis: f . k is Element of (J . k)
per cases ( k = i or k <> i ) ;
suppose k = i ; :: thesis: f . k is Element of (J . k)
hence f . k is Element of (J . k) by A10; :: thesis: verum
end;
suppose k <> i ; :: thesis: f . k is Element of (J . k)
then f . k = Bottom (J . k) by A10;
hence f . k is Element of (J . k) ; :: thesis: verum
end;
end;
end;
hence f . k is Element of (J . k) ; :: thesis: verum
end;
then reconsider f = f as Element of (product J) by A9, WAYBEL_3:27;
now :: thesis: for k being Element of I holds f . k <= x . k
let k be Element of I; :: thesis: f . k <= x . k
A12: J . k is lower-bounded algebraic LATTICE by A1;
now :: thesis: f . k <= x . k
per cases ( k = i or k <> i ) ;
suppose k = i ; :: thesis: f . k <= x . k
hence f . k <= x . k by A7, A10; :: thesis: verum
end;
suppose k <> i ; :: thesis: f . k <= x . k
then f . k = Bottom (J . k) by A10;
hence f . k <= x . k by A12, YELLOW_0:44; :: thesis: verum
end;
end;
end;
hence f . k <= x . k ; :: thesis: verum
end;
then A13: f <= x by WAYBEL_3:28;
A14: now :: thesis: for k being Element of I holds f . k << f . k
let k be Element of I; :: thesis: f . k << f . k
A15: J . k is lower-bounded algebraic LATTICE by A1;
now :: thesis: f . k << f . k
per cases ( k = i or k <> i ) ;
suppose A16: k = i ; :: thesis: f . k << f . k
then f . k = v1 by A10;
hence f . k << f . k by A8, A16, WAYBEL_3:def 2; :: thesis: verum
end;
end;
end;
hence f . k << f . k ; :: thesis: verum
end;
ex K being finite Subset of I st
for k being Element of I st not k in K holds
f . k = Bottom (J . k)
proof
take K = {i}; :: thesis: for k being Element of I st not k in K holds
f . k = Bottom (J . k)
let k be Element of I; :: thesis: ( not k in K implies f . k = Bottom (J . k) )
assume not k in K ; :: thesis: f . k = Bottom (J . k)
then k <> i by TARSKI:def 1;
hence f . k = Bottom (J . k) by A10; :: thesis: verum
end;
then f << f by A2, A14, WAYBEL_3:33;
then f is compact by WAYBEL_3:def 2;
then f in compactbelow x by A13, WAYBEL_8:4;
hence v in pi ((compactbelow x),i) by A6, A11, CARD_3:def 6; :: thesis: verum
end;
pi ((compactbelow x),i) c= compactbelow (x . i)
proof
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in pi ((compactbelow x),i) or v in compactbelow (x . i) )
assume v in pi ((compactbelow x),i) ; :: thesis: v in compactbelow (x . i)
then consider f being Function such that
A17: f in compactbelow x and
A18: v = f . i by CARD_3:def 6;
f in { y where y is Element of (product J) : ( x >= y & y is compact ) } by A17, WAYBEL_8:def 2;
then consider f1 being Element of (product J) such that
A19: f1 = f and
A20: x >= f1 and
A21: f1 is compact ;
f1 << f1 by A21, WAYBEL_3:def 2;
then f1 . i << f1 . i by A2, WAYBEL_3:33;
then A22: f1 . i is compact by WAYBEL_3:def 2;
f1 . i <= x . i by A20, WAYBEL_3:28;
hence v in compactbelow (x . i) by A18, A19, A22, WAYBEL_8:4; :: thesis: verum
end;
hence sup (compactbelow (x . i)) = sup (pi ((compactbelow x),i)) by A5, XBOOLE_0:def 10
.= (sup (compactbelow x)) . i by A2, WAYBEL_3:32 ;
:: thesis: verum
end;
now :: thesis: for i being Element of I holds (sup (compactbelow x)) . i <= x . i
let i be Element of I; :: thesis: (sup (compactbelow x)) . i <= x . i
J . i is satisfying_axiom_K by A1;
then x . i = sup (compactbelow (x . i)) by WAYBEL_8:def 3;
hence (sup (compactbelow x)) . i <= x . i by A4; :: thesis: verum
end;
then A23: sup (compactbelow x) <= x by WAYBEL_3:28;
now :: thesis: for i being Element of I holds x . i <= (sup (compactbelow x)) . i
let i be Element of I; :: thesis: x . i <= (sup (compactbelow x)) . i
J . i is satisfying_axiom_K by A1;
then x . i = sup (compactbelow (x . i)) by WAYBEL_8:def 3;
hence x . i <= (sup (compactbelow x)) . i by A4; :: thesis: verum
end;
then x <= sup (compactbelow x) by WAYBEL_3:28;
hence x = sup (compactbelow x) by A3, A23, YELLOW_0:def 3; :: thesis: verum
end;
then A24: product J is satisfying_axiom_K by WAYBEL_8:def 3;
A25: for x being Element of L holds
( not compactbelow x is empty & compactbelow x is directed )
proof
let x be Element of L; :: thesis: ( not compactbelow x is empty & compactbelow x is directed )
now :: thesis: for c, d being Element of L st c in compactbelow x & d in compactbelow x holds
ex e being Element of the carrier of L st
( e in compactbelow x & c <= e & d <= e )
let c, d be Element of L; :: thesis: ( c in compactbelow x & d in compactbelow x implies ex e being Element of the carrier of L st
( e in compactbelow x & c <= e & d <= e ) )
assume that
A26: c in compactbelow x and
A27: d in compactbelow x ; :: thesis: ex e being Element of the carrier of L st
( e in compactbelow x & c <= e & d <= e )
d is compact by A27, WAYBEL_8:4;
then ( d <= c "\/" d & d << d ) by WAYBEL_3:def 2, YELLOW_0:22;
then A28: d << c "\/" d by WAYBEL_3:2;
c is compact by A26, WAYBEL_8:4;
then ( c <= c "\/" d & c << c ) by WAYBEL_3:def 2, YELLOW_0:22;
then c << c "\/" d by WAYBEL_3:2;
then c "\/" d << c "\/" d by A28, WAYBEL_3:3;
then A29: c "\/" d is compact by WAYBEL_3:def 2;
take e = c "\/" d; :: thesis: ( e in compactbelow x & c <= e & d <= e )
( c <= x & d <= x ) by A26, A27, WAYBEL_8:4;
then c "\/" d <= x by YELLOW_0:22;
hence e in compactbelow x by A29, WAYBEL_8:4; :: thesis: ( c <= e & d <= e )
thus ( c <= e & d <= e ) by YELLOW_0:22; :: thesis: verum
end;
hence ( not compactbelow x is empty & compactbelow x is directed ) by WAYBEL_0:def 1; :: thesis: verum
end;
L is up-complete by A2, WAYBEL_3:31;
hence product J is lower-bounded algebraic LATTICE by A25, A24, WAYBEL_8:def 4; :: thesis: verum