# 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 ${⊢}{P}={S}{⨉}_{𝑠}{R}$
prdsval.k ${⊢}{K}={\mathrm{Base}}_{{S}}$
prdsval.i ${⊢}{\phi }\to \mathrm{dom}{R}={I}$
prdsval.b ${⊢}{\phi }\to {B}=\underset{{x}\in {I}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}$
prdsval.a
prdsval.t
prdsval.m
prdsval.j
prdsval.o ${⊢}{\phi }\to {O}={\prod }_{𝑡}\left(\mathrm{TopOpen}\circ {R}\right)$
prdsval.l
prdsval.d ${⊢}{\phi }\to {D}=\left({f}\in {B},{g}\in {B}⟼sup\left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right)\mathrm{dist}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\right)$
prdsval.h ${⊢}{\phi }\to {H}=\left({f}\in {B},{g}\in {B}⟼\underset{{x}\in {I}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right)$
prdsval.x
prdsval.s ${⊢}{\phi }\to {S}\in {W}$
prdsval.r ${⊢}{\phi }\to {R}\in {Z}$
Assertion prdsval

### Proof

Step Hyp Ref Expression
1 prdsval.p ${⊢}{P}={S}{⨉}_{𝑠}{R}$
2 prdsval.k ${⊢}{K}={\mathrm{Base}}_{{S}}$
3 prdsval.i ${⊢}{\phi }\to \mathrm{dom}{R}={I}$
4 prdsval.b ${⊢}{\phi }\to {B}=\underset{{x}\in {I}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}$
5 prdsval.a
6 prdsval.t
7 prdsval.m
8 prdsval.j
9 prdsval.o ${⊢}{\phi }\to {O}={\prod }_{𝑡}\left(\mathrm{TopOpen}\circ {R}\right)$
10 prdsval.l
11 prdsval.d ${⊢}{\phi }\to {D}=\left({f}\in {B},{g}\in {B}⟼sup\left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right)\mathrm{dist}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\right)$
12 prdsval.h ${⊢}{\phi }\to {H}=\left({f}\in {B},{g}\in {B}⟼\underset{{x}\in {I}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right)$
13 prdsval.x
14 prdsval.s ${⊢}{\phi }\to {S}\in {W}$
15 prdsval.r ${⊢}{\phi }\to {R}\in {Z}$
16 df-prds
17 16 a1i
18 vex ${⊢}{r}\in \mathrm{V}$
19 18 rnex ${⊢}\mathrm{ran}{r}\in \mathrm{V}$
20 19 uniex ${⊢}\bigcup \mathrm{ran}{r}\in \mathrm{V}$
21 20 rnex ${⊢}\mathrm{ran}\bigcup \mathrm{ran}{r}\in \mathrm{V}$
22 21 uniex ${⊢}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}\in \mathrm{V}$
23 baseid ${⊢}\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$
24 23 strfvss ${⊢}{\mathrm{Base}}_{{r}\left({x}\right)}\subseteq \bigcup \mathrm{ran}{r}\left({x}\right)$
25 fvssunirn ${⊢}{r}\left({x}\right)\subseteq \bigcup \mathrm{ran}{r}$
26 rnss ${⊢}{r}\left({x}\right)\subseteq \bigcup \mathrm{ran}{r}\to \mathrm{ran}{r}\left({x}\right)\subseteq \mathrm{ran}\bigcup \mathrm{ran}{r}$
27 uniss ${⊢}\mathrm{ran}{r}\left({x}\right)\subseteq \mathrm{ran}\bigcup \mathrm{ran}{r}\to \bigcup \mathrm{ran}{r}\left({x}\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}$
28 25 26 27 mp2b ${⊢}\bigcup \mathrm{ran}{r}\left({x}\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}$
29 24 28 sstri ${⊢}{\mathrm{Base}}_{{r}\left({x}\right)}\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}$
30 29 rgenw ${⊢}\forall {x}\in \mathrm{dom}{r}\phantom{\rule{.4em}{0ex}}{\mathrm{Base}}_{{r}\left({x}\right)}\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}$
31 iunss ${⊢}\bigcup _{{x}\in \mathrm{dom}{r}}{\mathrm{Base}}_{{r}\left({x}\right)}\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}↔\forall {x}\in \mathrm{dom}{r}\phantom{\rule{.4em}{0ex}}{\mathrm{Base}}_{{r}\left({x}\right)}\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}$
32 30 31 mpbir ${⊢}\bigcup _{{x}\in \mathrm{dom}{r}}{\mathrm{Base}}_{{r}\left({x}\right)}\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}$
33 22 32 ssexi ${⊢}\bigcup _{{x}\in \mathrm{dom}{r}}{\mathrm{Base}}_{{r}\left({x}\right)}\in \mathrm{V}$
34 ixpssmap2g ${⊢}\bigcup _{{x}\in \mathrm{dom}{r}}{\mathrm{Base}}_{{r}\left({x}\right)}\in \mathrm{V}\to \underset{{x}\in \mathrm{dom}{r}}{⨉}{\mathrm{Base}}_{{r}\left({x}\right)}\subseteq {\bigcup _{{x}\in \mathrm{dom}{r}}{\mathrm{Base}}_{{r}\left({x}\right)}}^{\mathrm{dom}{r}}$
35 33 34 ax-mp ${⊢}\underset{{x}\in \mathrm{dom}{r}}{⨉}{\mathrm{Base}}_{{r}\left({x}\right)}\subseteq {\bigcup _{{x}\in \mathrm{dom}{r}}{\mathrm{Base}}_{{r}\left({x}\right)}}^{\mathrm{dom}{r}}$
36 ovex ${⊢}{\bigcup _{{x}\in \mathrm{dom}{r}}{\mathrm{Base}}_{{r}\left({x}\right)}}^{\mathrm{dom}{r}}\in \mathrm{V}$
37 36 ssex ${⊢}\underset{{x}\in \mathrm{dom}{r}}{⨉}{\mathrm{Base}}_{{r}\left({x}\right)}\subseteq {\bigcup _{{x}\in \mathrm{dom}{r}}{\mathrm{Base}}_{{r}\left({x}\right)}}^{\mathrm{dom}{r}}\to \underset{{x}\in \mathrm{dom}{r}}{⨉}{\mathrm{Base}}_{{r}\left({x}\right)}\in \mathrm{V}$
38 35 37 mp1i ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to \underset{{x}\in \mathrm{dom}{r}}{⨉}{\mathrm{Base}}_{{r}\left({x}\right)}\in \mathrm{V}$
39 simpr ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to {r}={R}$
40 39 fveq1d ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to {r}\left({x}\right)={R}\left({x}\right)$
41 40 fveq2d ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to {\mathrm{Base}}_{{r}\left({x}\right)}={\mathrm{Base}}_{{R}\left({x}\right)}$
42 41 ixpeq2dv ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to \underset{{x}\in {I}}{⨉}{\mathrm{Base}}_{{r}\left({x}\right)}=\underset{{x}\in {I}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}$
43 39 dmeqd ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to \mathrm{dom}{r}=\mathrm{dom}{R}$
44 3 ad2antrr ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to \mathrm{dom}{R}={I}$
45 43 44 eqtrd ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to \mathrm{dom}{r}={I}$
46 45 ixpeq1d ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to \underset{{x}\in \mathrm{dom}{r}}{⨉}{\mathrm{Base}}_{{r}\left({x}\right)}=\underset{{x}\in {I}}{⨉}{\mathrm{Base}}_{{r}\left({x}\right)}$
47 4 ad2antrr ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to {B}=\underset{{x}\in {I}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}$
48 42 46 47 3eqtr4d ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to \underset{{x}\in \mathrm{dom}{r}}{⨉}{\mathrm{Base}}_{{r}\left({x}\right)}={B}$
49 ovex ${⊢}{\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}}^{\mathrm{dom}{r}}\in \mathrm{V}$
50 ovssunirn ${⊢}{f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\subseteq \bigcup \mathrm{ran}\mathrm{Hom}\left({r}\left({x}\right)\right)$
51 df-hom ${⊢}\mathrm{Hom}=\mathrm{Slot}14$
52 51 strfvss ${⊢}\mathrm{Hom}\left({r}\left({x}\right)\right)\subseteq \bigcup \mathrm{ran}{r}\left({x}\right)$
53 52 28 sstri ${⊢}\mathrm{Hom}\left({r}\left({x}\right)\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}$
54 rnss ${⊢}\mathrm{Hom}\left({r}\left({x}\right)\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}\to \mathrm{ran}\mathrm{Hom}\left({r}\left({x}\right)\right)\subseteq \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}$
55 uniss ${⊢}\mathrm{ran}\mathrm{Hom}\left({r}\left({x}\right)\right)\subseteq \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}\to \bigcup \mathrm{ran}\mathrm{Hom}\left({r}\left({x}\right)\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}$
56 53 54 55 mp2b ${⊢}\bigcup \mathrm{ran}\mathrm{Hom}\left({r}\left({x}\right)\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}$
57 50 56 sstri ${⊢}{f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}$
58 57 rgenw ${⊢}\forall {x}\in \mathrm{dom}{r}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}$
59 ss2ixp ${⊢}\forall {x}\in \mathrm{dom}{r}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}\to \underset{{x}\in \mathrm{dom}{r}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)\subseteq \underset{{x}\in \mathrm{dom}{r}}{⨉}\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}$
60 58 59 ax-mp ${⊢}\underset{{x}\in \mathrm{dom}{r}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)\subseteq \underset{{x}\in \mathrm{dom}{r}}{⨉}\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}$
61 18 dmex ${⊢}\mathrm{dom}{r}\in \mathrm{V}$
62 22 rnex ${⊢}\mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}\in \mathrm{V}$
63 62 uniex ${⊢}\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}\in \mathrm{V}$
64 61 63 ixpconst ${⊢}\underset{{x}\in \mathrm{dom}{r}}{⨉}\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}={\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}}^{\mathrm{dom}{r}}$
65 60 64 sseqtri ${⊢}\underset{{x}\in \mathrm{dom}{r}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)\subseteq {\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}}^{\mathrm{dom}{r}}$
66 49 65 elpwi2 ${⊢}\underset{{x}\in \mathrm{dom}{r}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)\in 𝒫\left({\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}}^{\mathrm{dom}{r}}\right)$
67 66 rgen2w ${⊢}\forall {f}\in {v}\phantom{\rule{.4em}{0ex}}\forall {g}\in {v}\phantom{\rule{.4em}{0ex}}\underset{{x}\in \mathrm{dom}{r}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)\in 𝒫\left({\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}}^{\mathrm{dom}{r}}\right)$
68 eqid ${⊢}\left({f}\in {v},{g}\in {v}⟼\underset{{x}\in \mathrm{dom}{r}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)\right)=\left({f}\in {v},{g}\in {v}⟼\underset{{x}\in \mathrm{dom}{r}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)\right)$
69 68 fmpo ${⊢}\forall {f}\in {v}\phantom{\rule{.4em}{0ex}}\forall {g}\in {v}\phantom{\rule{.4em}{0ex}}\underset{{x}\in \mathrm{dom}{r}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)\in 𝒫\left({\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}}^{\mathrm{dom}{r}}\right)↔\left({f}\in {v},{g}\in {v}⟼\underset{{x}\in \mathrm{dom}{r}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)\right):{v}×{v}⟶𝒫\left({\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}}^{\mathrm{dom}{r}}\right)$
70 67 69 mpbi ${⊢}\left({f}\in {v},{g}\in {v}⟼\underset{{x}\in \mathrm{dom}{r}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)\right):{v}×{v}⟶𝒫\left({\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}}^{\mathrm{dom}{r}}\right)$
71 vex ${⊢}{v}\in \mathrm{V}$
72 71 71 xpex ${⊢}{v}×{v}\in \mathrm{V}$
73 49 pwex ${⊢}𝒫\left({\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}}^{\mathrm{dom}{r}}\right)\in \mathrm{V}$
74 fex2 ${⊢}\left(\left({f}\in {v},{g}\in {v}⟼\underset{{x}\in \mathrm{dom}{r}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)\right):{v}×{v}⟶𝒫\left({\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}}^{\mathrm{dom}{r}}\right)\wedge {v}×{v}\in \mathrm{V}\wedge 𝒫\left({\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{r}}^{\mathrm{dom}{r}}\right)\in \mathrm{V}\right)\to \left({f}\in {v},{g}\in {v}⟼\underset{{x}\in \mathrm{dom}{r}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)\right)\in \mathrm{V}$
75 70 72 73 74 mp3an ${⊢}\left({f}\in {v},{g}\in {v}⟼\underset{{x}\in \mathrm{dom}{r}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)\right)\in \mathrm{V}$
76 75 a1i ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to \left({f}\in {v},{g}\in {v}⟼\underset{{x}\in \mathrm{dom}{r}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)\right)\in \mathrm{V}$
77 simpr ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to {v}={B}$
78 45 adantr ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to \mathrm{dom}{r}={I}$
79 78 ixpeq1d ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to \underset{{x}\in \mathrm{dom}{r}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)=\underset{{x}\in {I}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)$
80 40 fveq2d ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to \mathrm{Hom}\left({r}\left({x}\right)\right)=\mathrm{Hom}\left({R}\left({x}\right)\right)$
81 80 oveqd ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to {f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)={f}\left({x}\right)\mathrm{Hom}\left({R}\left({x}\right)\right){g}\left({x}\right)$
82 81 ixpeq2dv ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to \underset{{x}\in {I}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)=\underset{{x}\in {I}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)$
83 82 adantr ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to \underset{{x}\in {I}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)=\underset{{x}\in {I}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)$
84 79 83 eqtrd ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to \underset{{x}\in \mathrm{dom}{r}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)=\underset{{x}\in {I}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)$
85 77 77 84 mpoeq123dv ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to \left({f}\in {v},{g}\in {v}⟼\underset{{x}\in \mathrm{dom}{r}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)\right)=\left({f}\in {B},{g}\in {B}⟼\underset{{x}\in {I}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right)$
86 12 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to {H}=\left({f}\in {B},{g}\in {B}⟼\underset{{x}\in {I}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right)$
87 85 86 eqtr4d ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to \left({f}\in {v},{g}\in {v}⟼\underset{{x}\in \mathrm{dom}{r}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)\right)={H}$
88 simplr ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to {v}={B}$
89 88 opeq2d ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},{v}⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},{B}⟩$
90 40 fveq2d ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to {+}_{{r}\left({x}\right)}={+}_{{R}\left({x}\right)}$
91 90 oveqd ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to {f}\left({x}\right){+}_{{r}\left({x}\right)}{g}\left({x}\right)={f}\left({x}\right){+}_{{R}\left({x}\right)}{g}\left({x}\right)$
92 45 91 mpteq12dv ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to \left({x}\in \mathrm{dom}{r}⟼{f}\left({x}\right){+}_{{r}\left({x}\right)}{g}\left({x}\right)\right)=\left({x}\in {I}⟼{f}\left({x}\right){+}_{{R}\left({x}\right)}{g}\left({x}\right)\right)$
93 92 adantr ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to \left({x}\in \mathrm{dom}{r}⟼{f}\left({x}\right){+}_{{r}\left({x}\right)}{g}\left({x}\right)\right)=\left({x}\in {I}⟼{f}\left({x}\right){+}_{{R}\left({x}\right)}{g}\left({x}\right)\right)$
94 77 77 93 mpoeq123dv ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to \left({f}\in {v},{g}\in {v}⟼\left({x}\in \mathrm{dom}{r}⟼{f}\left({x}\right){+}_{{r}\left({x}\right)}{g}\left({x}\right)\right)\right)=\left({f}\in {B},{g}\in {B}⟼\left({x}\in {I}⟼{f}\left({x}\right){+}_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)$
95 94 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to \left({f}\in {v},{g}\in {v}⟼\left({x}\in \mathrm{dom}{r}⟼{f}\left({x}\right){+}_{{r}\left({x}\right)}{g}\left({x}\right)\right)\right)=\left({f}\in {B},{g}\in {B}⟼\left({x}\in {I}⟼{f}\left({x}\right){+}_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)$
96 5 ad4antr
97 95 96 eqtr4d
98 97 opeq2d
99 40 fveq2d ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to {\cdot }_{{r}\left({x}\right)}={\cdot }_{{R}\left({x}\right)}$
100 99 oveqd ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to {f}\left({x}\right){\cdot }_{{r}\left({x}\right)}{g}\left({x}\right)={f}\left({x}\right){\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)$
101 45 100 mpteq12dv ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to \left({x}\in \mathrm{dom}{r}⟼{f}\left({x}\right){\cdot }_{{r}\left({x}\right)}{g}\left({x}\right)\right)=\left({x}\in {I}⟼{f}\left({x}\right){\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)$
102 101 adantr ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to \left({x}\in \mathrm{dom}{r}⟼{f}\left({x}\right){\cdot }_{{r}\left({x}\right)}{g}\left({x}\right)\right)=\left({x}\in {I}⟼{f}\left({x}\right){\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)$
103 77 77 102 mpoeq123dv ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to \left({f}\in {v},{g}\in {v}⟼\left({x}\in \mathrm{dom}{r}⟼{f}\left({x}\right){\cdot }_{{r}\left({x}\right)}{g}\left({x}\right)\right)\right)=\left({f}\in {B},{g}\in {B}⟼\left({x}\in {I}⟼{f}\left({x}\right){\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)$
104 103 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to \left({f}\in {v},{g}\in {v}⟼\left({x}\in \mathrm{dom}{r}⟼{f}\left({x}\right){\cdot }_{{r}\left({x}\right)}{g}\left({x}\right)\right)\right)=\left({f}\in {B},{g}\in {B}⟼\left({x}\in {I}⟼{f}\left({x}\right){\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)$
105 6 ad4antr
106 104 105 eqtr4d
107 106 opeq2d
108 89 98 107 tpeq123d
109 simp-4r ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to {s}={S}$
110 109 opeq2d ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to ⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{s}⟩=⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{S}⟩$
111 simpllr ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to {s}={S}$
112 111 fveq2d ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to {\mathrm{Base}}_{{s}}={\mathrm{Base}}_{{S}}$
113 112 2 syl6eqr ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to {\mathrm{Base}}_{{s}}={K}$
114 40 fveq2d ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to {\cdot }_{{r}\left({x}\right)}={\cdot }_{{R}\left({x}\right)}$
115 114 oveqd ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to {f}{\cdot }_{{r}\left({x}\right)}{g}\left({x}\right)={f}{\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)$
116 45 115 mpteq12dv ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to \left({x}\in \mathrm{dom}{r}⟼{f}{\cdot }_{{r}\left({x}\right)}{g}\left({x}\right)\right)=\left({x}\in {I}⟼{f}{\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)$
117 116 adantr ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to \left({x}\in \mathrm{dom}{r}⟼{f}{\cdot }_{{r}\left({x}\right)}{g}\left({x}\right)\right)=\left({x}\in {I}⟼{f}{\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)$
118 113 77 117 mpoeq123dv ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to \left({f}\in {\mathrm{Base}}_{{s}},{g}\in {v}⟼\left({x}\in \mathrm{dom}{r}⟼{f}{\cdot }_{{r}\left({x}\right)}{g}\left({x}\right)\right)\right)=\left({f}\in {K},{g}\in {B}⟼\left({x}\in {I}⟼{f}{\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)$
119 118 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to \left({f}\in {\mathrm{Base}}_{{s}},{g}\in {v}⟼\left({x}\in \mathrm{dom}{r}⟼{f}{\cdot }_{{r}\left({x}\right)}{g}\left({x}\right)\right)\right)=\left({f}\in {K},{g}\in {B}⟼\left({x}\in {I}⟼{f}{\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)$
120 7 ad4antr
121 119 120 eqtr4d
122 121 opeq2d
123 40 fveq2d ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to {\cdot }_{𝑖}\left({r}\left({x}\right)\right)={\cdot }_{𝑖}\left({R}\left({x}\right)\right)$
124 123 oveqd ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to {f}\left({x}\right){\cdot }_{𝑖}\left({r}\left({x}\right)\right){g}\left({x}\right)={f}\left({x}\right){\cdot }_{𝑖}\left({R}\left({x}\right)\right){g}\left({x}\right)$
125 45 124 mpteq12dv ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to \left({x}\in \mathrm{dom}{r}⟼{f}\left({x}\right){\cdot }_{𝑖}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)=\left({x}\in {I}⟼{f}\left({x}\right){\cdot }_{𝑖}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)$
126 125 adantr ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to \left({x}\in \mathrm{dom}{r}⟼{f}\left({x}\right){\cdot }_{𝑖}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)=\left({x}\in {I}⟼{f}\left({x}\right){\cdot }_{𝑖}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)$
127 111 126 oveq12d ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to \underset{{x}\in \mathrm{dom}{r}}{{\sum }_{{s}}}\left({f}\left({x}\right){\cdot }_{𝑖}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)=\underset{{x}\in {I}}{{\sum }_{{S}}}\left({f}\left({x}\right){\cdot }_{𝑖}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)$
128 77 77 127 mpoeq123dv ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to \left({f}\in {v},{g}\in {v}⟼\underset{{x}\in \mathrm{dom}{r}}{{\sum }_{{s}}}\left({f}\left({x}\right){\cdot }_{𝑖}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)\right)=\left({f}\in {B},{g}\in {B}⟼\underset{{x}\in {I}}{{\sum }_{{S}}}\left({f}\left({x}\right){\cdot }_{𝑖}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right)$
129 128 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to \left({f}\in {v},{g}\in {v}⟼\underset{{x}\in \mathrm{dom}{r}}{{\sum }_{{s}}}\left({f}\left({x}\right){\cdot }_{𝑖}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)\right)=\left({f}\in {B},{g}\in {B}⟼\underset{{x}\in {I}}{{\sum }_{{S}}}\left({f}\left({x}\right){\cdot }_{𝑖}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\right)$
130 8 ad4antr
131 129 130 eqtr4d
132 131 opeq2d
133 110 122 132 tpeq123d
134 108 133 uneq12d
135 simpllr ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to {r}={R}$
136 135 coeq2d ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to \mathrm{TopOpen}\circ {r}=\mathrm{TopOpen}\circ {R}$
137 136 fveq2d ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to {\prod }_{𝑡}\left(\mathrm{TopOpen}\circ {r}\right)={\prod }_{𝑡}\left(\mathrm{TopOpen}\circ {R}\right)$
138 9 ad4antr ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to {O}={\prod }_{𝑡}\left(\mathrm{TopOpen}\circ {R}\right)$
139 137 138 eqtr4d ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to {\prod }_{𝑡}\left(\mathrm{TopOpen}\circ {r}\right)={O}$
140 139 opeq2d ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to ⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(\mathrm{TopOpen}\circ {r}\right)⟩=⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{O}⟩$
141 77 sseq2d ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to \left(\left\{{f},{g}\right\}\subseteq {v}↔\left\{{f},{g}\right\}\subseteq {B}\right)$
142 40 fveq2d ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to {\le }_{{r}\left({x}\right)}={\le }_{{R}\left({x}\right)}$
143 142 breqd ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to \left({f}\left({x}\right){\le }_{{r}\left({x}\right)}{g}\left({x}\right)↔{f}\left({x}\right){\le }_{{R}\left({x}\right)}{g}\left({x}\right)\right)$
144 45 143 raleqbidv ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to \left(\forall {x}\in \mathrm{dom}{r}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){\le }_{{r}\left({x}\right)}{g}\left({x}\right)↔\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){\le }_{{R}\left({x}\right)}{g}\left({x}\right)\right)$
145 144 adantr ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to \left(\forall {x}\in \mathrm{dom}{r}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){\le }_{{r}\left({x}\right)}{g}\left({x}\right)↔\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){\le }_{{R}\left({x}\right)}{g}\left({x}\right)\right)$
146 141 145 anbi12d ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to \left(\left(\left\{{f},{g}\right\}\subseteq {v}\wedge \forall {x}\in \mathrm{dom}{r}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){\le }_{{r}\left({x}\right)}{g}\left({x}\right)\right)↔\left(\left\{{f},{g}\right\}\subseteq {B}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){\le }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)$
147 146 opabbidv ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to \left\{⟨{f},{g}⟩|\left(\left\{{f},{g}\right\}\subseteq {v}\wedge \forall {x}\in \mathrm{dom}{r}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){\le }_{{r}\left({x}\right)}{g}\left({x}\right)\right)\right\}=\left\{⟨{f},{g}⟩|\left(\left\{{f},{g}\right\}\subseteq {B}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){\le }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right\}$
148 147 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to \left\{⟨{f},{g}⟩|\left(\left\{{f},{g}\right\}\subseteq {v}\wedge \forall {x}\in \mathrm{dom}{r}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){\le }_{{r}\left({x}\right)}{g}\left({x}\right)\right)\right\}=\left\{⟨{f},{g}⟩|\left(\left\{{f},{g}\right\}\subseteq {B}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){\le }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right\}$
149 10 ad4antr
150 148 149 eqtr4d
151 150 opeq2d
152 40 fveq2d ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to \mathrm{dist}\left({r}\left({x}\right)\right)=\mathrm{dist}\left({R}\left({x}\right)\right)$
153 152 oveqd ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to {f}\left({x}\right)\mathrm{dist}\left({r}\left({x}\right)\right){g}\left({x}\right)={f}\left({x}\right)\mathrm{dist}\left({R}\left({x}\right)\right){g}\left({x}\right)$
154 45 153 mpteq12dv ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to \left({x}\in \mathrm{dom}{r}⟼{f}\left({x}\right)\mathrm{dist}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)=\left({x}\in {I}⟼{f}\left({x}\right)\mathrm{dist}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)$
155 154 adantr ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to \left({x}\in \mathrm{dom}{r}⟼{f}\left({x}\right)\mathrm{dist}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)=\left({x}\in {I}⟼{f}\left({x}\right)\mathrm{dist}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)$
156 155 rneqd ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to \mathrm{ran}\left({x}\in \mathrm{dom}{r}⟼{f}\left({x}\right)\mathrm{dist}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)=\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right)\mathrm{dist}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)$
157 156 uneq1d ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to \mathrm{ran}\left({x}\in \mathrm{dom}{r}⟼{f}\left({x}\right)\mathrm{dist}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)\cup \left\{0\right\}=\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right)\mathrm{dist}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\cup \left\{0\right\}$
158 157 supeq1d ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to sup\left(\mathrm{ran}\left({x}\in \mathrm{dom}{r}⟼{f}\left({x}\right)\mathrm{dist}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)=sup\left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right)\mathrm{dist}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)$
159 77 77 158 mpoeq123dv ${⊢}\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\to \left({f}\in {v},{g}\in {v}⟼sup\left(\mathrm{ran}\left({x}\in \mathrm{dom}{r}⟼{f}\left({x}\right)\mathrm{dist}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\right)=\left({f}\in {B},{g}\in {B}⟼sup\left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right)\mathrm{dist}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\right)$
160 159 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to \left({f}\in {v},{g}\in {v}⟼sup\left(\mathrm{ran}\left({x}\in \mathrm{dom}{r}⟼{f}\left({x}\right)\mathrm{dist}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\right)=\left({f}\in {B},{g}\in {B}⟼sup\left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right)\mathrm{dist}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\right)$
161 11 ad4antr ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to {D}=\left({f}\in {B},{g}\in {B}⟼sup\left(\mathrm{ran}\left({x}\in {I}⟼{f}\left({x}\right)\mathrm{dist}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\right)$
162 160 161 eqtr4d ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to \left({f}\in {v},{g}\in {v}⟼sup\left(\mathrm{ran}\left({x}\in \mathrm{dom}{r}⟼{f}\left({x}\right)\mathrm{dist}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\right)={D}$
163 162 opeq2d ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to ⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left({f}\in {v},{g}\in {v}⟼sup\left(\mathrm{ran}\left({x}\in \mathrm{dom}{r}⟼{f}\left({x}\right)\mathrm{dist}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\right)⟩=⟨\mathrm{dist}\left(\mathrm{ndx}\right),{D}⟩$
164 140 151 163 tpeq123d
165 simpr ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to {h}={H}$
166 165 opeq2d ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to ⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{h}⟩=⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩$
167 88 sqxpeqd ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to {v}×{v}={B}×{B}$
168 165 oveqd ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to {c}{h}{2}^{nd}\left({a}\right)={c}{H}{2}^{nd}\left({a}\right)$
169 165 fveq1d ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to {h}\left({a}\right)={H}\left({a}\right)$
170 40 fveq2d ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to \mathrm{comp}\left({r}\left({x}\right)\right)=\mathrm{comp}\left({R}\left({x}\right)\right)$
171 170 oveqd ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to ⟨{1}^{st}\left({a}\right)\left({x}\right),{2}^{nd}\left({a}\right)\left({x}\right)⟩\mathrm{comp}\left({r}\left({x}\right)\right){c}\left({x}\right)=⟨{1}^{st}\left({a}\right)\left({x}\right),{2}^{nd}\left({a}\right)\left({x}\right)⟩\mathrm{comp}\left({R}\left({x}\right)\right){c}\left({x}\right)$
172 171 oveqd ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to {d}\left({x}\right)\left(⟨{1}^{st}\left({a}\right)\left({x}\right),{2}^{nd}\left({a}\right)\left({x}\right)⟩\mathrm{comp}\left({r}\left({x}\right)\right){c}\left({x}\right)\right){e}\left({x}\right)={d}\left({x}\right)\left(⟨{1}^{st}\left({a}\right)\left({x}\right),{2}^{nd}\left({a}\right)\left({x}\right)⟩\mathrm{comp}\left({R}\left({x}\right)\right){c}\left({x}\right)\right){e}\left({x}\right)$
173 45 172 mpteq12dv ${⊢}\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\to \left({x}\in \mathrm{dom}{r}⟼{d}\left({x}\right)\left(⟨{1}^{st}\left({a}\right)\left({x}\right),{2}^{nd}\left({a}\right)\left({x}\right)⟩\mathrm{comp}\left({r}\left({x}\right)\right){c}\left({x}\right)\right){e}\left({x}\right)\right)=\left({x}\in {I}⟼{d}\left({x}\right)\left(⟨{1}^{st}\left({a}\right)\left({x}\right),{2}^{nd}\left({a}\right)\left({x}\right)⟩\mathrm{comp}\left({R}\left({x}\right)\right){c}\left({x}\right)\right){e}\left({x}\right)\right)$
174 173 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to \left({x}\in \mathrm{dom}{r}⟼{d}\left({x}\right)\left(⟨{1}^{st}\left({a}\right)\left({x}\right),{2}^{nd}\left({a}\right)\left({x}\right)⟩\mathrm{comp}\left({r}\left({x}\right)\right){c}\left({x}\right)\right){e}\left({x}\right)\right)=\left({x}\in {I}⟼{d}\left({x}\right)\left(⟨{1}^{st}\left({a}\right)\left({x}\right),{2}^{nd}\left({a}\right)\left({x}\right)⟩\mathrm{comp}\left({R}\left({x}\right)\right){c}\left({x}\right)\right){e}\left({x}\right)\right)$
175 168 169 174 mpoeq123dv ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to \left({d}\in \left({c}{h}{2}^{nd}\left({a}\right)\right),{e}\in {h}\left({a}\right)⟼\left({x}\in \mathrm{dom}{r}⟼{d}\left({x}\right)\left(⟨{1}^{st}\left({a}\right)\left({x}\right),{2}^{nd}\left({a}\right)\left({x}\right)⟩\mathrm{comp}\left({r}\left({x}\right)\right){c}\left({x}\right)\right){e}\left({x}\right)\right)\right)=\left({d}\in \left({c}{H}{2}^{nd}\left({a}\right)\right),{e}\in {H}\left({a}\right)⟼\left({x}\in {I}⟼{d}\left({x}\right)\left(⟨{1}^{st}\left({a}\right)\left({x}\right),{2}^{nd}\left({a}\right)\left({x}\right)⟩\mathrm{comp}\left({R}\left({x}\right)\right){c}\left({x}\right)\right){e}\left({x}\right)\right)\right)$
176 167 88 175 mpoeq123dv ${⊢}\left(\left(\left(\left({\phi }\wedge {s}={S}\right)\wedge {r}={R}\right)\wedge {v}={B}\right)\wedge {h}={H}\right)\to \left({a}\in \left({v}×{v}\right),{c}\in {v}⟼\left({d}\in \left({c}{h}{2}^{nd}\left({a}\right)\right),{e}\in {h}\left({a}\right)⟼\left({x}\in \mathrm{dom}{r}⟼{d}\left({x}\right)\left(⟨{1}^{st}\left({a}\right)\left({x}\right),{2}^{nd}\left({a}\right)\left({x}\right)⟩\mathrm{comp}\left({r}\left({x}\right)\right){c}\left({x}\right)\right){e}\left({x}\right)\right)\right)\right)=\left({a}\in \left({B}×{B}\right),{c}\in {B}⟼\left({d}\in \left({c}{H}{2}^{nd}\left({a}\right)\right),{e}\in {H}\left({a}\right)⟼\left({x}\in {I}⟼{d}\left({x}\right)\left(⟨{1}^{st}\left({a}\right)\left({x}\right),{2}^{nd}\left({a}\right)\left({x}\right)⟩\mathrm{comp}\left({R}\left({x}\right)\right){c}\left({x}\right)\right){e}\left({x}\right)\right)\right)\right)$
177 13 ad4antr
178 176 177 eqtr4d
179 178 opeq2d
180 166 179 preq12d
181 164 180 uneq12d
182 134 181 uneq12d
183 76 87 182 csbied2
184 38 48 183 csbied2
185 184 anasss
186 14 elexd ${⊢}{\phi }\to {S}\in \mathrm{V}$
187 15 elexd ${⊢}{\phi }\to {R}\in \mathrm{V}$
188 tpex
189 tpex
190 188 189 unex
191 tpex
192 prex
193 191 192 unex
194 190 193 unex
195 194 a1i
196 17 185 186 187 195 ovmpod
197 1 196 syl5eq