let I be non empty set ; for J1, J2 being non-Empty TopSpace-yielding ManySortedSet of I st ( for i being Element of I holds J1 . i is SubSpace of J2 . i ) holds
product J1 is SubSpace of product J2
let J1, J2 be non-Empty TopSpace-yielding ManySortedSet of I; ( ( for i being Element of I holds J1 . i is SubSpace of J2 . i ) implies product J1 is SubSpace of product J2 )
assume A1:
for i being Element of I holds J1 . i is SubSpace of J2 . i
; product J1 is SubSpace of product J2
ex K1 being prebasis of (product J1) ex K2 being prebasis of (product J2) st
( [#] (product J1) in K1 & K1 = INTERSECTION (K2,{([#] (product J1))}) )
proof
reconsider K1 =
product_prebasis J1 as
prebasis of
(product J1) by WAYBEL18:def 3;
reconsider K2 =
product_prebasis J2 as
prebasis of
(product J2) by WAYBEL18:def 3;
take
K1
;
ex K2 being prebasis of (product J2) st
( [#] (product J1) in K1 & K1 = INTERSECTION (K2,{([#] (product J1))}) )
take
K2
;
( [#] (product J1) in K1 & K1 = INTERSECTION (K2,{([#] (product J1))}) )
A2:
[#] (product J1) =
the
carrier of
(product J1)
by STRUCT_0:def 3
.=
product (Carrier J1)
by WAYBEL18:def 3
;
then
[#] (product J1) = [#] (product (Carrier J1))
by SUBSET_1:def 3;
then reconsider P =
[#] (product J1) as
Subset of
(product (Carrier J1)) ;
ex
i being
set ex
T being
TopStruct ex
V being
Subset of
T st
(
i in I &
V is
open &
T = J1 . i &
P = product ((Carrier J1) +* (i,V)) )
hence
[#] (product J1) in K1
by WAYBEL18:def 2;
K1 = INTERSECTION (K2,{([#] (product J1))})
for
U being
set holds
(
U in K1 iff ex
A,
P0 being
set st
(
A in K2 &
P0 in {([#] (product J1))} &
U = A /\ P0 ) )
proof
let U be
set ;
( U in K1 iff ex A, P0 being set st
( A in K2 & P0 in {([#] (product J1))} & U = A /\ P0 ) )
A3:
for
i being
Element of
I for
V being
Subset of
(J1 . i) for
W being
Subset of
(J2 . i) st
V = W /\ ([#] (J1 . i)) holds
(Carrier J1) +* (
i,
V)
= ((Carrier J2) +* (i,W)) (/\) (Carrier J1)
proof
let i be
Element of
I;
for V being Subset of (J1 . i)
for W being Subset of (J2 . i) st V = W /\ ([#] (J1 . i)) holds
(Carrier J1) +* (i,V) = ((Carrier J2) +* (i,W)) (/\) (Carrier J1)let V be
Subset of
(J1 . i);
for W being Subset of (J2 . i) st V = W /\ ([#] (J1 . i)) holds
(Carrier J1) +* (i,V) = ((Carrier J2) +* (i,W)) (/\) (Carrier J1)let W be
Subset of
(J2 . i);
( V = W /\ ([#] (J1 . i)) implies (Carrier J1) +* (i,V) = ((Carrier J2) +* (i,W)) (/\) (Carrier J1) )
assume A4:
V = W /\ ([#] (J1 . i))
;
(Carrier J1) +* (i,V) = ((Carrier J2) +* (i,W)) (/\) (Carrier J1)
A5:
dom ((Carrier J1) +* (i,V)) =
I
by PARTFUN1:def 2
.=
dom (((Carrier J2) +* (i,W)) (/\) (Carrier J1))
by PARTFUN1:def 2
;
for
x being
object st
x in dom ((Carrier J1) +* (i,V)) holds
((Carrier J1) +* (i,V)) . x = (((Carrier J2) +* (i,W)) (/\) (Carrier J1)) . x
hence
(Carrier J1) +* (
i,
V)
= ((Carrier J2) +* (i,W)) (/\) (Carrier J1)
by A5, FUNCT_1:2;
verum
end;
thus
(
U in K1 implies ex
A,
P0 being
set st
(
A in K2 &
P0 in {([#] (product J1))} &
U = A /\ P0 ) )
( ex A, P0 being set st
( A in K2 & P0 in {([#] (product J1))} & U = A /\ P0 ) implies U in K1 )proof
assume
U in K1
;
ex A, P0 being set st
( A in K2 & P0 in {([#] (product J1))} & U = A /\ P0 )
then consider i being
set ,
T being
TopStruct ,
V being
Subset of
T such that A13:
(
i in I &
V is
open &
T = J1 . i )
and A14:
U = product ((Carrier J1) +* (i,V))
by WAYBEL18:def 2;
reconsider i =
i as
Element of
I by A13;
A15:
V in the
topology of
(J1 . i)
by A13, PRE_TOPC:def 2;
reconsider V =
V as
Subset of
(J1 . i) by A13;
J1 . i is
SubSpace of
J2 . i
by A1;
then consider W being
Subset of
(J2 . i) such that A16:
(
W in the
topology of
(J2 . i) &
V = W /\ ([#] (J1 . i)) )
by A15, PRE_TOPC:def 4;
set A =
product ((Carrier J2) +* (i,W));
take
product ((Carrier J2) +* (i,W))
;
ex P0 being set st
( product ((Carrier J2) +* (i,W)) in K2 & P0 in {([#] (product J1))} & U = (product ((Carrier J2) +* (i,W))) /\ P0 )
take
P
;
( product ((Carrier J2) +* (i,W)) in K2 & P in {([#] (product J1))} & U = (product ((Carrier J2) +* (i,W))) /\ P )
(Carrier J2) . i =
[#] (J2 . i)
by PENCIL_3:7
.=
the
carrier of
(J2 . i)
by STRUCT_0:def 3
;
then
(
i in dom (Carrier J2) &
W c= (Carrier J2) . i )
by A13, PARTFUN1:def 2;
then A17:
product ((Carrier J2) +* (i,W)) is
Subset of
(product (Carrier J2))
by Th39;
ex
i9 being
set ex
T9 being
TopStruct ex
V9 being
Subset of
T9 st
(
i9 in I &
V9 is
open &
T9 = J2 . i9 &
product ((Carrier J2) +* (i,W)) = product ((Carrier J2) +* (i9,V9)) )
by A16, PRE_TOPC:def 2;
hence
product ((Carrier J2) +* (i,W)) in K2
by A17, WAYBEL18:def 2;
( P in {([#] (product J1))} & U = (product ((Carrier J2) +* (i,W))) /\ P )
thus
P in {([#] (product J1))}
by TARSKI:def 1;
U = (product ((Carrier J2) +* (i,W))) /\ P
thus U =
product (((Carrier J2) +* (i,W)) (/\) (Carrier J1))
by A14, A16, A3
.=
(product ((Carrier J2) +* (i,W))) /\ P
by A2, Th33
;
verum
end;
given A,
P0 being
set such that A18:
(
A in K2 &
P0 in {([#] (product J1))} &
U = A /\ P0 )
;
U in K1
consider i being
set ,
T being
TopStruct ,
W being
Subset of
T such that A19:
(
i in I &
W is
open &
T = J2 . i )
and A20:
A = product ((Carrier J2) +* (i,W))
by A18, WAYBEL18:def 2;
reconsider i =
i as
Element of
I by A19;
A21:
W in the
topology of
(J2 . i)
by A19, PRE_TOPC:def 2;
reconsider W =
W as
Subset of
(J2 . i) by A19;
set V =
W /\ ([#] (J1 . i));
A22:
W /\ ([#] (J1 . i)) c= [#] (J1 . i)
by XBOOLE_1:17;
reconsider V =
W /\ ([#] (J1 . i)) as
Subset of
(J1 . i) ;
P0 = product (Carrier J1)
by A2, A18, TARSKI:def 1;
then A23:
U =
product (((Carrier J2) +* (i,W)) (/\) (Carrier J1))
by A18, A20, Th33
.=
product ((Carrier J1) +* (i,V))
by A3
;
A24:
i in dom (Carrier J1)
by A19, PARTFUN1:def 2;
V c= (Carrier J1) . i
by A22, PENCIL_3:7;
then A25:
U c= product (Carrier J1)
by A23, A24, Th39;
ex
i9 being
set ex
T9 being
TopStruct ex
V9 being
Subset of
T9 st
(
i9 in I &
V9 is
open &
T9 = J1 . i9 &
U = product ((Carrier J1) +* (i9,V9)) )
hence
U in K1
by A25, WAYBEL18:def 2;
verum
end;
hence
K1 = INTERSECTION (
K2,
{([#] (product J1))})
by SETFAM_1:def 5;
verum
end;
hence
product J1 is SubSpace of product J2
by Th51; verum