let L be lower-bounded continuous sup-Semilattice; :: thesis: for B being with_bottom CLbasis of L holds [(supMap (subrelstr B)),(baseMap B)] is Galois

let B be with_bottom CLbasis of L; :: thesis: [(supMap (subrelstr B)),(baseMap B)] is Galois

let B be with_bottom CLbasis of L; :: thesis: [(supMap (subrelstr B)),(baseMap B)] is Galois

now :: thesis: for x being Element of L

for y being Element of (InclPoset (Ids (subrelstr B))) holds

( ( x <= (supMap (subrelstr B)) . y implies (baseMap B) . x <= y ) & ( (baseMap B) . x <= y implies x <= (supMap (subrelstr B)) . y ) )

hence
[(supMap (subrelstr B)),(baseMap B)] is Galois
by WAYBEL_1:8; :: thesis: verumfor y being Element of (InclPoset (Ids (subrelstr B))) holds

( ( x <= (supMap (subrelstr B)) . y implies (baseMap B) . x <= y ) & ( (baseMap B) . x <= y implies x <= (supMap (subrelstr B)) . y ) )

let x be Element of L; :: thesis: for y being Element of (InclPoset (Ids (subrelstr B))) holds

( ( x <= (supMap (subrelstr B)) . y implies (baseMap B) . x <= y ) & ( (baseMap B) . x <= y implies x <= (supMap (subrelstr B)) . y ) )

let y be Element of (InclPoset (Ids (subrelstr B))); :: thesis: ( ( x <= (supMap (subrelstr B)) . y implies (baseMap B) . x <= y ) & ( (baseMap B) . x <= y implies x <= (supMap (subrelstr B)) . y ) )

reconsider I = y as Ideal of (subrelstr B) by YELLOW_2:41;

reconsider J = I as non empty directed Subset of L by YELLOW_2:7;

A1: ex_sup_of (waybelow x) /\ B,L by YELLOW_0:17;

thus ( x <= (supMap (subrelstr B)) . y implies (baseMap B) . x <= y ) :: thesis: ( (baseMap B) . x <= y implies x <= (supMap (subrelstr B)) . y )

thus ( (baseMap B) . x <= y implies x <= (supMap (subrelstr B)) . y ) :: thesis: verum

end;( ( x <= (supMap (subrelstr B)) . y implies (baseMap B) . x <= y ) & ( (baseMap B) . x <= y implies x <= (supMap (subrelstr B)) . y ) )

let y be Element of (InclPoset (Ids (subrelstr B))); :: thesis: ( ( x <= (supMap (subrelstr B)) . y implies (baseMap B) . x <= y ) & ( (baseMap B) . x <= y implies x <= (supMap (subrelstr B)) . y ) )

reconsider I = y as Ideal of (subrelstr B) by YELLOW_2:41;

reconsider J = I as non empty directed Subset of L by YELLOW_2:7;

A1: ex_sup_of (waybelow x) /\ B,L by YELLOW_0:17;

thus ( x <= (supMap (subrelstr B)) . y implies (baseMap B) . x <= y ) :: thesis: ( (baseMap B) . x <= y implies x <= (supMap (subrelstr B)) . y )

proof

A8:
ex_sup_of J,L
by YELLOW_0:17;
A2:
(downarrow J) /\ B c= J

then x <= "\/" (I,L) by Def10;

then A6: x <= sup (downarrow J) by WAYBEL_0:33, YELLOW_0:17;

waybelow x c= downarrow J

then (waybelow x) /\ B c= y by A2;

then (baseMap B) . x c= y by Def12;

hence (baseMap B) . x <= y by YELLOW_1:3; :: thesis: verum

end;proof

assume
x <= (supMap (subrelstr B)) . y
; :: thesis: (baseMap B) . x <= y
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in (downarrow J) /\ B or z in J )

assume A3: z in (downarrow J) /\ B ; :: thesis: z in J

then reconsider z1 = z as Element of L ;

z in B by A3, XBOOLE_0:def 4;

then reconsider z2 = z as Element of (subrelstr B) by YELLOW_0:def 15;

z in downarrow J by A3, XBOOLE_0:def 4;

then consider v1 being Element of L such that

A4: v1 >= z1 and

A5: v1 in J by WAYBEL_0:def 15;

reconsider v2 = v1 as Element of (subrelstr B) by A5;

z2 <= v2 by A4, YELLOW_0:60;

hence z in J by A5, WAYBEL_0:def 19; :: thesis: verum

end;assume A3: z in (downarrow J) /\ B ; :: thesis: z in J

then reconsider z1 = z as Element of L ;

z in B by A3, XBOOLE_0:def 4;

then reconsider z2 = z as Element of (subrelstr B) by YELLOW_0:def 15;

z in downarrow J by A3, XBOOLE_0:def 4;

then consider v1 being Element of L such that

A4: v1 >= z1 and

A5: v1 in J by WAYBEL_0:def 15;

reconsider v2 = v1 as Element of (subrelstr B) by A5;

z2 <= v2 by A4, YELLOW_0:60;

hence z in J by A5, WAYBEL_0:def 19; :: thesis: verum

then x <= "\/" (I,L) by Def10;

then A6: x <= sup (downarrow J) by WAYBEL_0:33, YELLOW_0:17;

waybelow x c= downarrow J

proof

then
(waybelow x) /\ B c= (downarrow J) /\ B
by XBOOLE_1:26;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in waybelow x or z in downarrow J )

assume A7: z in waybelow x ; :: thesis: z in downarrow J

then reconsider z1 = z as Element of L ;

z1 << x by A7, WAYBEL_3:7;

hence z in downarrow J by A6, WAYBEL_3:20; :: thesis: verum

end;assume A7: z in waybelow x ; :: thesis: z in downarrow J

then reconsider z1 = z as Element of L ;

z1 << x by A7, WAYBEL_3:7;

hence z in downarrow J by A6, WAYBEL_3:20; :: thesis: verum

then (waybelow x) /\ B c= y by A2;

then (baseMap B) . x c= y by Def12;

hence (baseMap B) . x <= y by YELLOW_1:3; :: thesis: verum

thus ( (baseMap B) . x <= y implies x <= (supMap (subrelstr B)) . y ) :: thesis: verum

proof

assume
(baseMap B) . x <= y
; :: thesis: x <= (supMap (subrelstr B)) . y

then (baseMap B) . x c= y by YELLOW_1:3;

then (waybelow x) /\ B c= y by Def12;

then sup ((waybelow x) /\ B) <= sup J by A8, A1, YELLOW_0:34;

then x <= "\/" (I,L) by Def7;

hence x <= (supMap (subrelstr B)) . y by Def10; :: thesis: verum

end;then (baseMap B) . x c= y by YELLOW_1:3;

then (waybelow x) /\ B c= y by Def12;

then sup ((waybelow x) /\ B) <= sup J by A8, A1, YELLOW_0:34;

then x <= "\/" (I,L) by Def7;

hence x <= (supMap (subrelstr B)) . y by Def10; :: thesis: verum