Metamath Proof Explorer


Theorem prdstset

Description: Structure product topology. (Contributed by Mario Carneiro, 15-Aug-2015) (Revised by Thierry Arnoux, 16-Jun-2019) (Revised by Zhi Wang, 18-Aug-2024)

Ref Expression
Hypotheses prdsbas.p P = S 𝑠 R
prdsbas.s φ S V
prdsbas.r φ R W
prdsbas.b B = Base P
prdsbas.i φ dom R = I
prdstset.l O = TopSet P
Assertion prdstset φ O = 𝑡 TopOpen R

Proof

Step Hyp Ref Expression
1 prdsbas.p P = S 𝑠 R
2 prdsbas.s φ S V
3 prdsbas.r φ R W
4 prdsbas.b B = Base P
5 prdsbas.i φ dom R = I
6 prdstset.l O = TopSet P
7 eqid Base S = Base S
8 1 2 3 4 5 prdsbas φ B = x I Base R x
9 eqid + P = + P
10 1 2 3 4 5 9 prdsplusg φ + P = f B , g B x I f x + R x g x
11 eqid P = P
12 1 2 3 4 5 11 prdsmulr φ P = f B , g B x I f x R x g x
13 eqid P = P
14 1 2 3 4 5 7 13 prdsvsca φ P = f Base S , g B x I f R x g x
15 eqidd φ f B , g B S x I f x 𝑖 R x g x = f B , g B S x I f x 𝑖 R x g x
16 eqidd φ 𝑡 TopOpen R = 𝑡 TopOpen R
17 eqid P = P
18 1 2 3 4 5 17 prdsle φ P = f g | f g B x I f x R x g x
19 eqid dist P = dist P
20 1 2 3 4 5 19 prdsds φ dist P = f B , g B sup ran x I f x dist R x g x 0 * <
21 eqidd φ f B , g B x I f x Hom R x g x = f B , g B x I f x Hom R x g x
22 eqidd φ a B × B , c B d 2 nd a f B , g B x I f x Hom R x g x c , e f B , g B x I f x Hom R x g x a x I d x 1 st a x 2 nd a x comp R x c x e x = a B × B , c B d 2 nd a f B , g B x I f x Hom R x g x c , e f B , g B x I f x Hom R x g x a x I d x 1 st a x 2 nd a x comp R x c x e x
23 1 7 5 8 10 12 14 15 16 18 20 21 22 2 3 prdsval φ P = Base ndx B + ndx + P ndx P Scalar ndx S ndx P 𝑖 ndx f B , g B S x I f x 𝑖 R x g x TopSet ndx 𝑡 TopOpen R ndx P dist ndx dist P Hom ndx f B , g B x I f x Hom R x g x comp ndx a B × B , c B d 2 nd a f B , g B x I f x Hom R x g x c , e f B , g B x I f x Hom R x g x a x I d x 1 st a x 2 nd a x comp R x c x e x
24 tsetid TopSet = Slot TopSet ndx
25 fvexd φ 𝑡 TopOpen R V
26 snsstp1 TopSet ndx 𝑡 TopOpen R TopSet ndx 𝑡 TopOpen R ndx P dist ndx dist P
27 ssun1 TopSet ndx 𝑡 TopOpen R ndx P dist ndx dist P TopSet ndx 𝑡 TopOpen R ndx P dist ndx dist P Hom ndx f B , g B x I f x Hom R x g x comp ndx a B × B , c B d 2 nd a f B , g B x I f x Hom R x g x c , e f B , g B x I f x Hom R x g x a x I d x 1 st a x 2 nd a x comp R x c x e x
28 26 27 sstri TopSet ndx 𝑡 TopOpen R TopSet ndx 𝑡 TopOpen R ndx P dist ndx dist P Hom ndx f B , g B x I f x Hom R x g x comp ndx a B × B , c B d 2 nd a f B , g B x I f x Hom R x g x c , e f B , g B x I f x Hom R x g x a x I d x 1 st a x 2 nd a x comp R x c x e x
29 ssun2 TopSet ndx 𝑡 TopOpen R ndx P dist ndx dist P Hom ndx f B , g B x I f x Hom R x g x comp ndx a B × B , c B d 2 nd a f B , g B x I f x Hom R x g x c , e f B , g B x I f x Hom R x g x a x I d x 1 st a x 2 nd a x comp R x c x e x Base ndx B + ndx + P ndx P Scalar ndx S ndx P 𝑖 ndx f B , g B S x I f x 𝑖 R x g x TopSet ndx 𝑡 TopOpen R ndx P dist ndx dist P Hom ndx f B , g B x I f x Hom R x g x comp ndx a B × B , c B d 2 nd a f B , g B x I f x Hom R x g x c , e f B , g B x I f x Hom R x g x a x I d x 1 st a x 2 nd a x comp R x c x e x
30 28 29 sstri TopSet ndx 𝑡 TopOpen R Base ndx B + ndx + P ndx P Scalar ndx S ndx P 𝑖 ndx f B , g B S x I f x 𝑖 R x g x TopSet ndx 𝑡 TopOpen R ndx P dist ndx dist P Hom ndx f B , g B x I f x Hom R x g x comp ndx a B × B , c B d 2 nd a f B , g B x I f x Hom R x g x c , e f B , g B x I f x Hom R x g x a x I d x 1 st a x 2 nd a x comp R x c x e x
31 23 6 24 25 30 prdsbaslem φ O = 𝑡 TopOpen R