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 𝑃 = ( 𝑆 Xs 𝑅 )
prdsbas.s ( 𝜑𝑆𝑉 )
prdsbas.r ( 𝜑𝑅𝑊 )
prdsbas.b 𝐵 = ( Base ‘ 𝑃 )
prdsbas.i ( 𝜑 → dom 𝑅 = 𝐼 )
prdstset.l 𝑂 = ( TopSet ‘ 𝑃 )
Assertion prdstset ( 𝜑𝑂 = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 prdsbas.p 𝑃 = ( 𝑆 Xs 𝑅 )
2 prdsbas.s ( 𝜑𝑆𝑉 )
3 prdsbas.r ( 𝜑𝑅𝑊 )
4 prdsbas.b 𝐵 = ( Base ‘ 𝑃 )
5 prdsbas.i ( 𝜑 → dom 𝑅 = 𝐼 )
6 prdstset.l 𝑂 = ( TopSet ‘ 𝑃 )
7 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
8 1 2 3 4 5 prdsbas ( 𝜑𝐵 = X 𝑥𝐼 ( Base ‘ ( 𝑅𝑥 ) ) )
9 eqid ( +g𝑃 ) = ( +g𝑃 )
10 1 2 3 4 5 9 prdsplusg ( 𝜑 → ( +g𝑃 ) = ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( +g ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) )
11 eqid ( .r𝑃 ) = ( .r𝑃 )
12 1 2 3 4 5 11 prdsmulr ( 𝜑 → ( .r𝑃 ) = ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( .r ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) )
13 eqid ( ·𝑠𝑃 ) = ( ·𝑠𝑃 )
14 1 2 3 4 5 7 13 prdsvsca ( 𝜑 → ( ·𝑠𝑃 ) = ( 𝑓 ∈ ( Base ‘ 𝑆 ) , 𝑔𝐵 ↦ ( 𝑥𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) )
15 eqidd ( 𝜑 → ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑆 Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) = ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑆 Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) )
16 eqidd ( 𝜑 → ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )
17 eqid ( le ‘ 𝑃 ) = ( le ‘ 𝑃 )
18 1 2 3 4 5 17 prdsle ( 𝜑 → ( le ‘ 𝑃 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥𝐼 ( 𝑓𝑥 ) ( le ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) } )
19 eqid ( dist ‘ 𝑃 ) = ( dist ‘ 𝑃 )
20 1 2 3 4 5 19 prdsds ( 𝜑 → ( dist ‘ 𝑃 ) = ( 𝑓𝐵 , 𝑔𝐵 ↦ sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) )
21 eqidd ( 𝜑 → ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) = ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) )
22 eqidd ( 𝜑 → ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐𝐵 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥𝐼 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) = ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐𝐵 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥𝐼 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) )
23 1 7 5 8 10 12 14 15 16 18 20 21 22 2 3 prdsval ( 𝜑𝑃 = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g𝑃 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r𝑃 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠𝑃 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑆 Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( le ‘ 𝑃 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑃 ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐𝐵 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥𝐼 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) ⟩ } ) ) )
24 tsetid TopSet = Slot ( TopSet ‘ ndx )
25 fvexd ( 𝜑 → ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ∈ V )
26 snsstp1 { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ⟩ } ⊆ { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( le ‘ 𝑃 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑃 ) ⟩ }
27 ssun1 { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( le ‘ 𝑃 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑃 ) ⟩ } ⊆ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( le ‘ 𝑃 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑃 ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐𝐵 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥𝐼 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) ⟩ } )
28 26 27 sstri { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ⟩ } ⊆ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( le ‘ 𝑃 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑃 ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐𝐵 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥𝐼 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) ⟩ } )
29 ssun2 ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( le ‘ 𝑃 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑃 ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐𝐵 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥𝐼 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) ⟩ } ) ⊆ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g𝑃 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r𝑃 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠𝑃 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑆 Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( le ‘ 𝑃 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑃 ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐𝐵 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥𝐼 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) ⟩ } ) )
30 28 29 sstri { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ⟩ } ⊆ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g𝑃 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r𝑃 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠𝑃 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑆 Σg ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( le ‘ 𝑃 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑃 ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐𝐵 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓𝐵 , 𝑔𝐵X 𝑥𝐼 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥𝐼 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) ⟩ } ) )
31 23 6 24 25 30 prdsbaslem ( 𝜑𝑂 = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )