let X be non empty set ; :: thesis: for S, T being non empty Poset ex F being Function of (UPS S,(T |^ X)),((UPS S,T) |^ X) st
( F is commuting & F is isomorphic )
let S, T be non empty Poset; :: thesis: ex F being Function of (UPS S,(T |^ X)),((UPS S,T) |^ X) st
( F is commuting & F is isomorphic )
deffunc H1( Function) -> set = commute $1;
consider F being ManySortedSet of such that
A1:
for f being Element of (UPS S,(T |^ X)) holds F . f = H1(f)
from PBOOLE:sch 5();
A2:
dom F = the carrier of (UPS S,(T |^ X))
by PARTFUN1:def 4;
A3:
rng F c= the carrier of ((UPS S,T) |^ X)
proof
let g be
set ;
:: according to TARSKI:def 3 :: thesis: ( not g in rng F or g in the carrier of ((UPS S,T) |^ X) )
assume
g in rng F
;
:: thesis: g in the carrier of ((UPS S,T) |^ X)
then consider f being
set such that A4:
(
f in dom F &
g = F . f )
by FUNCT_1:def 5;
reconsider f =
f as
directed-sups-preserving Function of
S,
(T |^ X) by A2, A4, Def4;
g = commute f
by A1, A2, A4;
then reconsider g =
g as
Function of
X,the
carrier of
(UPS S,T) by Th39;
(
dom g = X &
rng g c= the
carrier of
(UPS S,T) )
by FUNCT_2:def 1;
then
g in Funcs X,the
carrier of
(UPS S,T)
by FUNCT_2:def 2;
hence
g in the
carrier of
((UPS S,T) |^ X)
by YELLOW_1:28;
:: thesis: verum
end;
then reconsider F = F as Function of (UPS S,(T |^ X)),((UPS S,T) |^ X) by A2, FUNCT_2:4;
consider G being ManySortedSet of such that
A5:
for f being Element of ((UPS S,T) |^ X) holds G . f = H1(f)
from PBOOLE:sch 5();
A6:
dom G = the carrier of ((UPS S,T) |^ X)
by PARTFUN1:def 4;
A7:
rng G c= the carrier of (UPS S,(T |^ X))
proof
let g be
set ;
:: according to TARSKI:def 3 :: thesis: ( not g in rng G or g in the carrier of (UPS S,(T |^ X)) )
assume
g in rng G
;
:: thesis: g in the carrier of (UPS S,(T |^ X))
then consider f being
set such that A8:
(
f in dom G &
g = G . f )
by FUNCT_1:def 5;
the
carrier of
((UPS S,T) |^ X) = Funcs X,the
carrier of
(UPS S,T)
by YELLOW_1:28;
then reconsider f =
f as
Function of
X,the
carrier of
(UPS S,T) by A6, A8, FUNCT_2:121;
g = commute f
by A5, A6, A8;
then
g is
directed-sups-preserving Function of
S,
(T |^ X)
by Th40;
hence
g in the
carrier of
(UPS S,(T |^ X))
by Def4;
:: thesis: verum
end;
then reconsider G = G as Function of ((UPS S,T) |^ X),(UPS S,(T |^ X)) by A6, FUNCT_2:4;
take
F
; :: thesis: ( F is commuting & F is isomorphic )
thus A9:
F is commuting
:: thesis: F is isomorphic
A10:
G is commuting
UPS S,T is full SubRelStr of T |^ the carrier of S
by Def4;
then A11:
(UPS S,T) |^ X is full SubRelStr of (T |^ the carrier of S) |^ X
by YELLOW16:41;
A12:
UPS S,(T |^ X) is full SubRelStr of (T |^ X) |^ the carrier of S
by Def4;
then A13:
F is monotone
by A9, A11, Th19;
A14:
G is monotone
by A10, A11, A12, Th19;
A15:
the carrier of (T |^ X) = Funcs X,the carrier of T
by YELLOW_1:28;
the carrier of ((UPS S,T) |^ X) = Funcs X,the carrier of (UPS S,T)
by YELLOW_1:28;
then A16:
the carrier of ((UPS S,T) |^ X) c= Funcs X,(Funcs the carrier of S,the carrier of T)
by Th22, FUNCT_5:63;
the carrier of (UPS S,(T |^ X)) c= Funcs the carrier of S,the carrier of (T |^ X)
by Th22;
then
( F * G = id ((UPS S,T) |^ X) & G * F = id (UPS S,(T |^ X)) )
by A2, A3, A6, A7, A9, A10, A15, A16, Th3;
hence
F is isomorphic
by A13, A14, YELLOW16:17; :: thesis: verum