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)

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 ovex ⊢ ( ∪ ran ∪ ran ∪ ran 𝑟 ↑m dom 𝑟 ) ∈ V
50 ovssunirn ⊢ ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ⊆ ∪ ran ( Hom ‘ ( 𝑟 ‘ 𝑥 ) )
51 df-hom ⊢ Hom = Slot 1 4
52 51 strfvss ⊢ ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ∪ ran ( 𝑟 ‘ 𝑥 )
53 52 28 sstri ⊢ ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran 𝑟
54 rnss ⊢ ( ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran 𝑟 → ran ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ran ∪ ran ∪ ran 𝑟 )
55 uniss ⊢ ( ran ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ran ∪ ran ∪ ran 𝑟 → ∪ ran ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran ∪ ran 𝑟 )
56 53 54 55 mp2b ⊢ ∪ ran ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran ∪ ran 𝑟
57 50 56 sstri ⊢ ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran ∪ ran 𝑟
58 57 rgenw ⊢ ∀ 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran ∪ ran 𝑟
59 ss2ixp ⊢ ( ∀ 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran ∪ ran 𝑟 → X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ⊆ X 𝑥 ∈ dom 𝑟 ∪ ran ∪ ran ∪ ran 𝑟 )
60 58 59 ax-mp ⊢ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ⊆ X 𝑥 ∈ dom 𝑟 ∪ ran ∪ ran ∪ ran 𝑟
61 18 dmex ⊢ dom 𝑟 ∈ V
62 22 rnex ⊢ ran ∪ ran ∪ ran 𝑟 ∈ V
63 62 uniex ⊢ ∪ ran ∪ ran ∪ ran 𝑟 ∈ V
64 61 63 ixpconst ⊢ X 𝑥 ∈ dom 𝑟 ∪ ran ∪ ran ∪ ran 𝑟 = ( ∪ ran ∪ ran ∪ ran 𝑟 ↑m dom 𝑟 )
65 60 64 sseqtri ⊢ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ⊆ ( ∪ ran ∪ ran ∪ ran 𝑟 ↑m dom 𝑟 )
66 49 65 elpwi2 ⊢ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ∈ 𝒫 ( ∪ ran ∪ ran ∪ ran 𝑟 ↑m dom 𝑟 )
67 66 rgen2w ⊢ ∀ 𝑓 ∈ 𝑣 ∀ 𝑔 ∈ 𝑣 X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ∈ 𝒫 ( ∪ ran ∪ ran ∪ ran 𝑟 ↑m dom 𝑟 )
68 eqid ⊢ ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
69 68 fmpo ⊢ ( ∀ 𝑓 ∈ 𝑣 ∀ 𝑔 ∈ 𝑣 X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ∈ 𝒫 ( ∪ ran ∪ ran ∪ ran 𝑟 ↑m dom 𝑟 ) ↔ ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) : ( 𝑣 × 𝑣 ) ⟶ 𝒫 ( ∪ ran ∪ ran ∪ ran 𝑟 ↑m dom 𝑟 ) )
70 67 69 mpbi ⊢ ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) : ( 𝑣 × 𝑣 ) ⟶ 𝒫 ( ∪ ran ∪ ran ∪ ran 𝑟 ↑m dom 𝑟 )
71 vex ⊢ 𝑣 ∈ V
72 71 71 xpex ⊢ ( 𝑣 × 𝑣 ) ∈ V
73 49 pwex ⊢ 𝒫 ( ∪ ran ∪ ran ∪ ran 𝑟 ↑m dom 𝑟 ) ∈ V
74 fex2 ⊢ ( ( ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) : ( 𝑣 × 𝑣 ) ⟶ 𝒫 ( ∪ ran ∪ ran ∪ ran 𝑟 ↑m dom 𝑟 ) ∧ ( 𝑣 × 𝑣 ) ∈ V ∧ 𝒫 ( ∪ ran ∪ ran ∪ ran 𝑟 ↑m dom 𝑟 ) ∈ V ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∈ V )
75 70 72 73 74 mp3an ⊢ ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∈ V
76 75 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∈ V )
77 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → 𝑣 = 𝐵 )
78 45 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → dom 𝑟 = 𝐼 )
79 78 ixpeq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
80 40 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) = ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) )
81 80 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
82 81 ixpeq2dv ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
83 82 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
84 79 83 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
85 77 77 84 mpoeq123dv ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
86 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → 𝐻 = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
87 85 86 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = 𝐻 )
88 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → 𝑣 = 𝐵 )
89 88 opeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ = ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ )
90 40 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( +g ‘ ( 𝑟 ‘ 𝑥 ) ) = ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) )
91 90 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
92 45 91 mpteq12dv ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
93 92 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
94 77 77 93 mpoeq123dv ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
95 94 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
96 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → + = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
97 95 96 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = + )
98 97 opeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ = ⟨ ( +g ‘ ndx ) , + ⟩ )
99 40 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( .r ‘ ( 𝑟 ‘ 𝑥 ) ) = ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) )
100 99 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
101 45 100 mpteq12dv ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
102 101 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
103 77 77 102 mpoeq123dv ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
104 103 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
105 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → × = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
106 104 105 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = × )
107 106 opeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ = ⟨ ( .r ‘ ndx ) , × ⟩ )
108 89 98 107 tpeq123d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } )
109 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → 𝑠 = 𝑆 )
110 109 opeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ = ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ )
111 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → 𝑠 = 𝑆 )
112 111 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( Base ‘ 𝑠 ) = ( Base ‘ 𝑆 ) )
113 112 2 syl6eqr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( Base ‘ 𝑠 ) = 𝐾 )
114 40 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ·𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) = ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) )
115 114 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( 𝑓 ( ·𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
116 45 115 mpteq12dv ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
117 116 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
118 113 77 117 mpoeq123dv ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
119 118 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
120 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → · = ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
121 119 120 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = · )
122 121 opeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ = ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ )
123 40 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) = ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) )
124 123 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
125 45 124 mpteq12dv ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
126 125 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
127 111 126 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑆 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
128 77 77 127 mpoeq123dv ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑆 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
129 128 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑆 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
130 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → , = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑆 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
131 129 130 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) = , )
132 131 opeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ = ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ )
133 110 122 132 tpeq123d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → { ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } = { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } )
134 108 133 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 ) , , ⟩ } ) )
135 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → 𝑟 = 𝑅 )
136 135 coeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( TopOpen ∘ 𝑟 ) = ( TopOpen ∘ 𝑅 ) )
137 136 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( ∏t ‘ ( TopOpen ∘ 𝑟 ) ) = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )
138 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → 𝑂 = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )
139 137 138 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( ∏t ‘ ( TopOpen ∘ 𝑟 ) ) = 𝑂 )
140 139 opeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ = ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ )
141 77 sseq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( { 𝑓 , 𝑔 } ⊆ 𝑣 ↔ { 𝑓 , 𝑔 } ⊆ 𝐵 ) )
142 40 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( le ‘ ( 𝑟 ‘ 𝑥 ) ) = ( le ‘ ( 𝑅 ‘ 𝑥 ) ) )
143 142 breqd ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ↔ ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
144 45 143 raleqbidv ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
145 144 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
146 141 145 anbi12d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ↔ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
147 146 opabbidv ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } )
148 147 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } )
149 10 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ≤ = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } )
150 148 149 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } = ≤ )
151 150 opeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ = ⟨ ( le ‘ ndx ) , ≤ ⟩ )
152 40 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) = ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) )
153 152 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
154 45 153 mpteq12dv ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
155 154 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
156 155 rneqd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
157 156 uneq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) = ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) )
158 157 supeq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
159 77 77 158 mpoeq123dv ⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) )
160 159 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) )
161 11 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → 𝐷 = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) )
162 160 161 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) = 𝐷 )
163 162 opeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ = ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ )
164 140 151 163 tpeq123d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } = { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } )
165 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ℎ = 𝐻 )
166 165 opeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( Hom ‘ ndx ) , ℎ ⟩ = ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ )
167 88 sqxpeqd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑣 × 𝑣 ) = ( 𝐵 × 𝐵 ) )
168 165 oveqd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑐 ℎ ( 2nd ‘ 𝑎 ) ) = ( 𝑐 𝐻 ( 2nd ‘ 𝑎 ) ) )
169 165 fveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( ℎ ‘ 𝑎 ) = ( 𝐻 ‘ 𝑎 ) )
170 40 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) = ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) )
171 170 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) = ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) )
172 171 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) = ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) )
173 45 172 mpteq12dv ⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) )
174 173 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) )
175 168 169 174 mpoeq123dv ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑑 ∈ ( 𝑐 ℎ ( 2nd ‘ 𝑎 ) ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) = ( 𝑑 ∈ ( 𝑐 𝐻 ( 2nd ‘ 𝑎 ) ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) )
176 167 88 175 mpoeq123dv ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( 𝑐 ℎ ( 2nd ‘ 𝑎 ) ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) = ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( 𝑐 𝐻 ( 2nd ‘ 𝑎 ) ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) )
177 13 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ∙ = ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( 𝑐 𝐻 ( 2nd ‘ 𝑎 ) ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) )
178 176 177 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( 𝑐 ℎ ( 2nd ‘ 𝑎 ) ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) = ∙ )
179 178 opeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( 𝑐 ℎ ( 2nd ‘ 𝑎 ) ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ = ⟨ ( comp ‘ ndx ) , ∙ ⟩ )
180 166 179 preq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → { ⟨ ( Hom ‘ ndx ) , ℎ ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( 𝑐 ℎ ( 2nd ‘ 𝑎 ) ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } = { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } )
181 164 180 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 ) , ∙ ⟩ } ) )
182 134 181 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 ) , ∙ ⟩ } ) ) )
183 76 87 182 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 ) , ∙ ⟩ } ) ) )
184 38 48 183 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 ) , ∙ ⟩ } ) ) )
185 184 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 ) , ∙ ⟩ } ) ) )
186 14 elexd ⊢ ( 𝜑 → 𝑆 ∈ V )
187 15 elexd ⊢ ( 𝜑 → 𝑅 ∈ V )
188 tpex ⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∈ V
189 tpex ⊢ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ∈ V
190 188 189 unex ⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ∈ V
191 tpex ⊢ { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∈ V
192 prex ⊢ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ∈ V
193 191 192 unex ⊢ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ∈ V
194 190 193 unex ⊢ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ) ∈ V
195 194 a1i ⊢ ( 𝜑 → ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ) ∈ V )
196 17 185 186 187 195 ovmpod ⊢ ( 𝜑 → ( 𝑆 Xs 𝑅 ) = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ) )
197 1 196 syl5eq ⊢ ( 𝜑 → 𝑃 = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ) )