Metamath Proof Explorer

Theorem prdsval

Description: Value of the structure product. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by Mario Carneiro, 7-Jan-2017) (Revised by Thierry Arnoux, 16-Jun-2019) (Revised by Zhi Wang, 18-Aug-2024)

Ref Expression
Hypotheses prdsval.p ⊢ 𝑃 = ( 𝑆 Xs 𝑅 )
prdsval.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
prdsval.i ⊢ ( 𝜑 → dom 𝑅 = 𝐼 )
prdsval.b ⊢ ( 𝜑 → 𝐵 = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
prdsval.a ⊢ ( 𝜑 → + = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
prdsval.t ⊢ ( 𝜑 → × = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
prdsval.m ⊢ ( 𝜑 → · = ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
prdsval.j ⊢ ( 𝜑 → , = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑆 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
prdsval.o ⊢ ( 𝜑 → 𝑂 = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )
prdsval.l ⊢ ( 𝜑 → ≤ = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } )
prdsval.d ⊢ ( 𝜑 → 𝐷 = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) )
prdsval.h ⊢ ( 𝜑 → 𝐻 = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
prdsval.x ⊢ ( 𝜑 → ∙ = ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) )
prdsval.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
prdsval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
Assertion prdsval ( 𝜑 → 𝑃 = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ) )

Proof

Step Hyp Ref Expression
1 prdsval.p ⊢ 𝑃 = ( 𝑆 Xs 𝑅 )
2 prdsval.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
3 prdsval.i ⊢ ( 𝜑 → dom 𝑅 = 𝐼 )
4 prdsval.b ⊢ ( 𝜑 → 𝐵 = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
5 prdsval.a ⊢ ( 𝜑 → + = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
6 prdsval.t ⊢ ( 𝜑 → × = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
7 prdsval.m ⊢ ( 𝜑 → · = ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
8 prdsval.j ⊢ ( 𝜑 → , = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑆 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
9 prdsval.o ⊢ ( 𝜑 → 𝑂 = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )
10 prdsval.l ⊢ ( 𝜑 → ≤ = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } )
11 prdsval.d ⊢ ( 𝜑 → 𝐷 = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) )
12 prdsval.h ⊢ ( 𝜑 → 𝐻 = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
13 prdsval.x ⊢ ( 𝜑 → ∙ = ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) )
14 prdsval.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
15 prdsval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
16 df-prds ⊢ Xs = ( 𝑠 ∈ V , 𝑟 ∈ V ↦ ⦋ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) / 𝑣 ⦌ ⦋ ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) / ℎ ⦌ ( ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ℎ ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) ℎ 𝑐 ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ) )
17 16 a1i ⊢ ( 𝜑 → Xs = ( 𝑠 ∈ V , 𝑟 ∈ V ↦ ⦋ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) / 𝑣 ⦌ ⦋ ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) / ℎ ⦌ ( ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ℎ ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) ℎ 𝑐 ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ) ) )
18 vex ⊢ 𝑟 ∈ V
19 18 rnex ⊢ ran 𝑟 ∈ V
20 19 uniex ⊢ ∪ ran 𝑟 ∈ V
21 20 rnex ⊢ ran ∪ ran 𝑟 ∈ V
22 21 uniex ⊢ ∪ ran ∪ ran 𝑟 ∈ V
23 baseid ⊢ Base = Slot ( Base ‘ ndx )
24 23 strfvss ⊢ ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ∪ ran ( 𝑟 ‘ 𝑥 )
25 fvssunirn ⊢ ( 𝑟 ‘ 𝑥 ) ⊆ ∪ ran 𝑟
26 rnss ⊢ ( ( 𝑟 ‘ 𝑥 ) ⊆ ∪ ran 𝑟 → ran ( 𝑟 ‘ 𝑥 ) ⊆ ran ∪ ran 𝑟 )
27 uniss ⊢ ( ran ( 𝑟 ‘ 𝑥 ) ⊆ ran ∪ ran 𝑟 → ∪ ran ( 𝑟 ‘ 𝑥 ) ⊆ ∪ ran ∪ ran 𝑟 )
28 25 26 27 mp2b ⊢ ∪ ran ( 𝑟 ‘ 𝑥 ) ⊆ ∪ ran ∪ ran 𝑟
29 24 28 sstri ⊢ ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran 𝑟
30 29 rgenw ⊢ ∀ 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran 𝑟
31 iunss ⊢ ( ∪ 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran 𝑟 ↔ ∀ 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran 𝑟 )
32 30 31 mpbir ⊢ ∪ 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran 𝑟
33 22 32 ssexi ⊢ ∪ 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ∈ V
34 ixpssmap2g ⊢ ( ∪ 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ∈ V → X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ( ∪ 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ↑m dom 𝑟 ) )
35 33 34 ax-mp ⊢ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ( ∪ 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ↑m dom 𝑟 )
36 ovex ⊢ ( ∪ 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ↑m dom 𝑟 ) ∈ V
37 36 ssex ⊢ ( X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ( ∪ 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ↑m dom 𝑟 ) → X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ∈ V )
38 35 37 mp1i ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ∈ V )
39 simpr ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → 𝑟 = 𝑅 )
40 39 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( 𝑟 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑥 ) )
41 40 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) = ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
42 41 ixpeq2dv ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
43 39 dmeqd ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → dom 𝑟 = dom 𝑅 )
44 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → dom 𝑅 = 𝐼 )
45 43 44 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → dom 𝑟 = 𝐼 )
46 45 ixpeq1d ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) )
47 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → 𝐵 = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
48 42 46 47 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) = 𝐵 )
49 prdsvallem ⊢ ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∈ V
50 49 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∈ V )
51 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → 𝑣 = 𝐵 )
52 45 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → dom 𝑟 = 𝐼 )
53 52 ixpeq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
54 40 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) = ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) )
55 54 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
56 55 ixpeq2dv ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
57 56 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
58 53 57 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
59 51 51 58 mpoeq123dv ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
60 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → 𝐻 = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
61 59 60 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = 𝐻 )
62 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → 𝑣 = 𝐵 )
63 62 opeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ = ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ )
64 40 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( +g ‘ ( 𝑟 ‘ 𝑥 ) ) = ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) )
65 64 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
66 45 65 mpteq12dv ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
67 66 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
68 51 51 67 mpoeq123dv ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
69 68 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
70 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → + = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
71 69 70 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = + )
72 71 opeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ = ⟨ ( +g ‘ ndx ) , + ⟩ )
73 40 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( .r ‘ ( 𝑟 ‘ 𝑥 ) ) = ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) )
74 73 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
75 45 74 mpteq12dv ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
76 75 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
77 51 51 76 mpoeq123dv ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
78 77 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
79 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → × = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
80 78 79 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = × )
81 80 opeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ = ⟨ ( .r ‘ ndx ) , × ⟩ )
82 63 72 81 tpeq123d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } )
83 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → 𝑠 = 𝑆 )
84 83 opeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ = ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ )
85 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → 𝑠 = 𝑆 )
86 85 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( Base ‘ 𝑠 ) = ( Base ‘ 𝑆 ) )
87 86 2 eqtr4di ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( Base ‘ 𝑠 ) = 𝐾 )
88 40 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ·𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) = ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) )
89 88 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( 𝑓 ( ·𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
90 45 89 mpteq12dv ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
91 90 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
92 87 51 91 mpoeq123dv ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
93 92 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
94 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → · = ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
95 93 94 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = · )
96 95 opeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ = ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ )
97 40 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) = ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) )
98 97 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
99 45 98 mpteq12dv ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
100 99 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
101 85 100 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑆 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
102 51 51 101 mpoeq123dv ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑆 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
103 102 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑆 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
104 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → , = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑆 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
105 103 104 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) = , )
106 105 opeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ = ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ )
107 84 96 106 tpeq123d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → { ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } = { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } )
108 82 107 uneq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) )
109 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → 𝑟 = 𝑅 )
110 109 coeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( TopOpen ∘ 𝑟 ) = ( TopOpen ∘ 𝑅 ) )
111 110 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( ∏t ‘ ( TopOpen ∘ 𝑟 ) ) = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )
112 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → 𝑂 = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )
113 111 112 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( ∏t ‘ ( TopOpen ∘ 𝑟 ) ) = 𝑂 )
114 113 opeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ = ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ )
115 51 sseq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( { 𝑓 , 𝑔 } ⊆ 𝑣 ↔ { 𝑓 , 𝑔 } ⊆ 𝐵 ) )
116 40 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( le ‘ ( 𝑟 ‘ 𝑥 ) ) = ( le ‘ ( 𝑅 ‘ 𝑥 ) ) )
117 116 breqd ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ↔ ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
118 45 117 raleqbidv ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
119 118 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
120 115 119 anbi12d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ↔ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
121 120 opabbidv ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } )
122 121 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } )
123 10 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ≤ = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } )
124 122 123 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } = ≤ )
125 124 opeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ = ⟨ ( le ‘ ndx ) , ≤ ⟩ )
126 40 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) = ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) )
127 126 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
128 45 127 mpteq12dv ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
129 128 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
130 129 rneqd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
131 130 uneq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) = ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) )
132 131 supeq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
133 51 51 132 mpoeq123dv ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) )
134 133 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) )
135 11 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → 𝐷 = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) )
136 134 135 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) = 𝐷 )
137 136 opeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ = ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ )
138 114 125 137 tpeq123d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } = { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } )
139 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ℎ = 𝐻 )
140 139 opeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( Hom ‘ ndx ) , ℎ ⟩ = ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ )
141 62 sqxpeqd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑣 × 𝑣 ) = ( 𝐵 × 𝐵 ) )
142 139 oveqd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( ( 2nd ‘ 𝑎 ) ℎ 𝑐 ) = ( ( 2nd ‘ 𝑎 ) 𝐻 𝑐 ) )
143 139 fveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( ℎ ‘ 𝑎 ) = ( 𝐻 ‘ 𝑎 ) )
144 40 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) = ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) )
145 144 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) = ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) )
146 145 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) = ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) )
147 45 146 mpteq12dv ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) )
148 147 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) )
149 142 143 148 mpoeq123dv ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) ℎ 𝑐 ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) = ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) )
150 141 62 149 mpoeq123dv ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) ℎ 𝑐 ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) = ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) )
151 13 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ∙ = ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) )
152 150 151 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) ℎ 𝑐 ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) = ∙ )
153 152 opeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) ℎ 𝑐 ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ = ⟨ ( comp ‘ ndx ) , ∙ ⟩ )
154 140 153 preq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → { ⟨ ( Hom ‘ ndx ) , ℎ ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) ℎ 𝑐 ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } = { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } )
155 138 154 uneq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ℎ ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) ℎ 𝑐 ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ) = ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) )
156 108 155 uneq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ℎ ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) ℎ 𝑐 ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ) = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ) )
157 50 61 156 csbied2 ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ⦋ ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) / ℎ ⦌ ( ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ℎ ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) ℎ 𝑐 ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ) = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ) )
158 38 48 157 csbied2 ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ⦋ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) / 𝑣 ⦌ ⦋ ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) / ℎ ⦌ ( ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ℎ ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) ℎ 𝑐 ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ) = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ) )
159 158 anasss ⊢ ( ( 𝜑 ∧ ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) ) → ⦋ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) / 𝑣 ⦌ ⦋ ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) / ℎ ⦌ ( ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ℎ ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) ℎ 𝑐 ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ) = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ) )
160 14 elexd ⊢ ( 𝜑 → 𝑆 ∈ V )
161 15 elexd ⊢ ( 𝜑 → 𝑅 ∈ V )
162 tpex ⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∈ V
163 tpex ⊢ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ∈ V
164 162 163 unex ⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ∈ V
165 tpex ⊢ { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∈ V
166 prex ⊢ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ∈ V
167 165 166 unex ⊢ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ∈ V
168 164 167 unex ⊢ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ) ∈ V
169 168 a1i ⊢ ( 𝜑 → ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ) ∈ V )
170 17 159 160 161 169 ovmpod ⊢ ( 𝜑 → ( 𝑆 Xs 𝑅 ) = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ) )
171 1 170 syl5eq ⊢ ( 𝜑 → 𝑃 = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ) )