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 ) , ⟩ } ) ) )