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 eqtr4di ( ( ( ( 𝜑𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 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 ) , ⟩ } ) ) )