let I be non empty set ; :: thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of 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 ; :: 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 ;
for i being Element of I holds J . i is antisymmetric by A1;
then A3: product J is antisymmetric by WAYBEL_3:30;
reconsider L = product J as non empty lower-bounded LATTICE by A2, WAYBEL_3:31;
A4: 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

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 ( c in compactbelow x & d in compactbelow x ) ; :: thesis: ex e being Element of the carrier of L st
( e in compactbelow x & c <= e & d <= e )
then A5: ( c <= x & c is compact & d <= x & d is compact ) by WAYBEL_8:4;
take e = c "\/" d; :: thesis: ( e in compactbelow x & c <= e & d <= e )
A6: ( c <= c "\/" d & d <= c "\/" d ) by YELLOW_0:22;
c << c by A5, WAYBEL_3:def 2;
then A7: c << c "\/" d by A6, WAYBEL_3:2;
d << d by A5, WAYBEL_3:def 2;
then d << c "\/" d by A6, WAYBEL_3:2;
then c "\/" d << c "\/" d by A7, WAYBEL_3:3;
then A8: c "\/" d is compact by WAYBEL_3:def 2;
c "\/" d <= x by A5, YELLOW_0:22;
hence e in compactbelow x by A8, 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;

A9: L is up-complete by A2, WAYBEL_3:31;

now

let x be Element of (product J); :: thesis: x = sup (compactbelow x)
A10: 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
A11: pi (compactbelow x),i c= compactbelow (x . i)

proof

let v be set ; :: 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
A12: f in compactbelow x and
A13: v = f . i by CARD_3:def 6;
f in { y where y is Element of (product J) : ( x >= y & y is compact ) } by A12, WAYBEL_8:def 2;
then consider f1 being Element of (product J) such that
A14: f1 = f and
A15: x >= f1 and
A16: f1 is compact ;
f1 << f1 by A16, WAYBEL_3:def 2;
then f1 . i << f1 . i by A2, WAYBEL_3:33;
then A17: f1 . i is compact by WAYBEL_3:def 2;
f1 . i <= x . i by A15, WAYBEL_3:28;
hence v in compactbelow (x . i) by A13, A14, A17, WAYBEL_8:4; :: thesis: verum

end;

compactbelow (x . i) c= pi (compactbelow x),i

proof

let v be set ; :: 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
A18: v1 = v and
A19: x . i >= v1 and
A20: v1 is compact ;
defpred S₁[ set ] means $1 = i;
deffunc H₁( set ) -> Element of (J . i) = v1;
deffunc H₂( Element of I) -> Element of the carrier of (J . $1) = Bottom (J . $1);
consider f being Function such that
A21: dom f = I and
A22: for j being Element of I holds
( ( S₁[j] implies f . j = H₁(j) ) & ( not S₁[j] implies f . j = H₂(j) ) ) from PARTFUN1:sch 4();
A23: f . i = v1 by A22;

now

let k be Element of I; :: thesis: f . k is Element of (J . k)

now

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 A22; :: thesis: verum

end;

suppose k <> i ; :: thesis: f . k is Element of (J . k)

then f . k = Bottom (J . k) by A22;
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 A21, WAYBEL_3:27;

now

let k be Element of I; :: thesis: f . k <= x . k
A24: J . k is lower-bounded algebraic LATTICE by A1;

now

per cases ( k = i or k <> i ) ;

suppose k = i ; :: thesis: f . k <= x . k

hence f . k <= x . k by A19, A22; :: thesis: verum

end;

suppose k <> i ; :: thesis: f . k <= x . k

then f . k = Bottom (J . k) by A22;
hence f . k <= x . k by A24, YELLOW_0:44; :: thesis: verum

end;

end;

end;

hence f . k <= x . k ; :: thesis: verum

end;

then A25: f <= x by WAYBEL_3:28;
A26: 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 A22; :: thesis: verum

end;

now

let k be Element of I; :: thesis: f . k << f . k
A27: J . k is lower-bounded algebraic LATTICE by A1;

now

per cases ( k = i or k <> i ) ;

suppose A28: k = i ; :: thesis: f . k << f . k

then f . k = v1 by A22;
hence f . k << f . k by A20, A28, WAYBEL_3:def 2; :: thesis: verum

end;

suppose k <> i ; :: thesis: f . k << f . k

then f . k = Bottom (J . k) by A22;
then f . k is compact by A27, WAYBEL_3:15;
hence f . k << f . k by WAYBEL_3:def 2; :: thesis: verum

end;

end;

end;

hence f . k << f . k ; :: thesis: verum

end;

then f << f by A2, A26, WAYBEL_3:33;
then f is compact by WAYBEL_3:def 2;
then f in compactbelow x by A25, WAYBEL_8:4;
hence v in pi (compactbelow x),i by A18, A23, CARD_3:def 6; :: thesis: verum

end;

hence sup (compactbelow (x . i)) = sup (pi (compactbelow x),i) by A11, XBOOLE_0:def 10
.= (sup (compactbelow x)) . i by A2, WAYBEL_3:32 ;
:: thesis: verum

end;

now

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 A10; :: thesis: verum

end;

then A29: x <= sup (compactbelow x) by WAYBEL_3:28;

now

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 A10; :: thesis: verum

end;

then sup (compactbelow x) <= x by WAYBEL_3:28;
hence x = sup (compactbelow x) by A3, A29, YELLOW_0:def 3; :: thesis: verum

end;

then product J is satisfying_axiom_K by WAYBEL_8:def 3;
hence product J is lower-bounded algebraic LATTICE by A4, A9, WAYBEL_8:def 4; :: thesis: verum