# Metamath Proof Explorer

## Theorem prdshom

Description: Structure product hom-sets. (Contributed by Mario Carneiro, 7-Jan-2017) (Revised by Thierry Arnoux, 16-Jun-2019)

Ref Expression
Hypotheses prdsbas.p ${⊢}{P}={S}{⨉}_{𝑠}{R}$
prdsbas.s ${⊢}{\phi }\to {S}\in {V}$
prdsbas.r ${⊢}{\phi }\to {R}\in {W}$
prdsbas.b ${⊢}{B}={\mathrm{Base}}_{{P}}$
prdsbas.i ${⊢}{\phi }\to \mathrm{dom}{R}={I}$
prdshom.h ${⊢}{H}=\mathrm{Hom}\left({P}\right)$
Assertion prdshom ${⊢}{\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)$

### Proof

Step Hyp Ref Expression
1 prdsbas.p ${⊢}{P}={S}{⨉}_{𝑠}{R}$
2 prdsbas.s ${⊢}{\phi }\to {S}\in {V}$
3 prdsbas.r ${⊢}{\phi }\to {R}\in {W}$
4 prdsbas.b ${⊢}{B}={\mathrm{Base}}_{{P}}$
5 prdsbas.i ${⊢}{\phi }\to \mathrm{dom}{R}={I}$
6 prdshom.h ${⊢}{H}=\mathrm{Hom}\left({P}\right)$
7 eqid ${⊢}{\mathrm{Base}}_{{S}}={\mathrm{Base}}_{{S}}$
8 1 2 3 4 5 prdsbas ${⊢}{\phi }\to {B}=\underset{{x}\in {I}}{⨉}{\mathrm{Base}}_{{R}\left({x}\right)}$
9 eqid ${⊢}{+}_{{P}}={+}_{{P}}$
10 1 2 3 4 5 9 prdsplusg ${⊢}{\phi }\to {+}_{{P}}=\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)$
11 eqid ${⊢}{\cdot }_{{P}}={\cdot }_{{P}}$
12 1 2 3 4 5 11 prdsmulr ${⊢}{\phi }\to {\cdot }_{{P}}=\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)$
13 eqid ${⊢}{\cdot }_{{P}}={\cdot }_{{P}}$
14 1 2 3 4 5 7 13 prdsvsca ${⊢}{\phi }\to {\cdot }_{{P}}=\left({f}\in {\mathrm{Base}}_{{S}},{g}\in {B}⟼\left({x}\in {I}⟼{f}{\cdot }_{{R}\left({x}\right)}{g}\left({x}\right)\right)\right)$
15 eqidd ${⊢}{\phi }\to \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)=\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)$
16 eqid ${⊢}\mathrm{TopSet}\left({P}\right)=\mathrm{TopSet}\left({P}\right)$
17 1 2 3 4 5 16 prdstset ${⊢}{\phi }\to \mathrm{TopSet}\left({P}\right)={\prod }_{𝑡}\left(\mathrm{TopOpen}\circ {R}\right)$
18 eqid ${⊢}{\le }_{{P}}={\le }_{{P}}$
19 1 2 3 4 5 18 prdsle ${⊢}{\phi }\to {\le }_{{P}}=\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\}$
20 eqid ${⊢}\mathrm{dist}\left({P}\right)=\mathrm{dist}\left({P}\right)$
21 1 2 3 4 5 20 prdsds ${⊢}{\phi }\to \mathrm{dist}\left({P}\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)$
22 eqidd ${⊢}{\phi }\to \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)=\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)$
23 eqidd ${⊢}{\phi }\to \left({a}\in \left({B}×{B}\right),{c}\in {B}⟼\left({d}\in \left({c}\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){2}^{nd}\left({a}\right)\right),{e}\in \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)\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)=\left({a}\in \left({B}×{B}\right),{c}\in {B}⟼\left({d}\in \left({c}\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){2}^{nd}\left({a}\right)\right),{e}\in \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)\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)$
24 1 7 5 8 10 12 14 15 17 19 21 22 23 2 3 prdsval ${⊢}{\phi }\to {P}=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{B}⟩,⟨{+}_{\mathrm{ndx}},{+}_{{P}}⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_{{P}}⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{S}⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_{{P}}⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\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)⟩\right\}\right)\cup \left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left({P}\right)⟩,⟨{\le }_{\mathrm{ndx}},{\le }_{{P}}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{dist}\left({P}\right)⟩\right\}\cup \left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\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)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left({a}\in \left({B}×{B}\right),{c}\in {B}⟼\left({d}\in \left({c}\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){2}^{nd}\left({a}\right)\right),{e}\in \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)\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)⟩\right\}\right)$
25 homid ${⊢}\mathrm{Hom}=\mathrm{Slot}\mathrm{Hom}\left(\mathrm{ndx}\right)$
26 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)$
27 25 strfvss ${⊢}\mathrm{Hom}\left({R}\left({x}\right)\right)\subseteq \bigcup \mathrm{ran}{R}\left({x}\right)$
28 fvssunirn ${⊢}{R}\left({x}\right)\subseteq \bigcup \mathrm{ran}{R}$
29 rnss ${⊢}{R}\left({x}\right)\subseteq \bigcup \mathrm{ran}{R}\to \mathrm{ran}{R}\left({x}\right)\subseteq \mathrm{ran}\bigcup \mathrm{ran}{R}$
30 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}$
31 28 29 30 mp2b ${⊢}\bigcup \mathrm{ran}{R}\left({x}\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}{R}$
32 27 31 sstri ${⊢}\mathrm{Hom}\left({R}\left({x}\right)\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}{R}$
33 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}$
34 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}$
35 32 33 34 mp2b ${⊢}\bigcup \mathrm{ran}\mathrm{Hom}\left({R}\left({x}\right)\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{R}$
36 26 35 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}$
37 36 rgenw ${⊢}\forall {x}\in {I}\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}$
38 ss2ixp ${⊢}\forall {x}\in {I}\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 {I}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\subseteq \underset{{x}\in {I}}{⨉}\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{R}$
39 37 38 ax-mp ${⊢}\underset{{x}\in {I}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({R}\left({x}\right)\right){g}\left({x}\right)\right)\subseteq \underset{{x}\in {I}}{⨉}\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{R}$
40 3 dmexd ${⊢}{\phi }\to \mathrm{dom}{R}\in \mathrm{V}$
41 5 40 eqeltrrd ${⊢}{\phi }\to {I}\in \mathrm{V}$
42 rnexg ${⊢}{R}\in {W}\to \mathrm{ran}{R}\in \mathrm{V}$
43 uniexg ${⊢}\mathrm{ran}{R}\in \mathrm{V}\to \bigcup \mathrm{ran}{R}\in \mathrm{V}$
44 3 42 43 3syl ${⊢}{\phi }\to \bigcup \mathrm{ran}{R}\in \mathrm{V}$
45 rnexg ${⊢}\bigcup \mathrm{ran}{R}\in \mathrm{V}\to \mathrm{ran}\bigcup \mathrm{ran}{R}\in \mathrm{V}$
46 uniexg ${⊢}\mathrm{ran}\bigcup \mathrm{ran}{R}\in \mathrm{V}\to \bigcup \mathrm{ran}\bigcup \mathrm{ran}{R}\in \mathrm{V}$
47 44 45 46 3syl ${⊢}{\phi }\to \bigcup \mathrm{ran}\bigcup \mathrm{ran}{R}\in \mathrm{V}$
48 rnexg ${⊢}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{R}\in \mathrm{V}\to \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{R}\in \mathrm{V}$
49 uniexg ${⊢}\mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{R}\in \mathrm{V}\to \bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{R}\in \mathrm{V}$
50 47 48 49 3syl ${⊢}{\phi }\to \bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{R}\in \mathrm{V}$
51 ixpconstg ${⊢}\left({I}\in \mathrm{V}\wedge \bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{R}\in \mathrm{V}\right)\to \underset{{x}\in {I}}{⨉}\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{R}={\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{R}}^{{I}}$
52 41 50 51 syl2anc ${⊢}{\phi }\to \underset{{x}\in {I}}{⨉}\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{R}={\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{R}}^{{I}}$
53 39 52 sseqtrid ${⊢}{\phi }\to \underset{{x}\in {I}}{⨉}\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}}^{{I}}$
54 ovex ${⊢}{\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{R}}^{{I}}\in \mathrm{V}$
55 54 elpw2 ${⊢}\underset{{x}\in {I}}{⨉}\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}}^{{I}}\right)↔\underset{{x}\in {I}}{⨉}\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}}^{{I}}$
56 53 55 sylibr ${⊢}{\phi }\to \underset{{x}\in {I}}{⨉}\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}}^{{I}}\right)$
57 56 ralrimivw ${⊢}{\phi }\to \forall {g}\in {B}\phantom{\rule{.4em}{0ex}}\underset{{x}\in {I}}{⨉}\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}}^{{I}}\right)$
58 57 ralrimivw ${⊢}{\phi }\to \forall {f}\in {B}\phantom{\rule{.4em}{0ex}}\forall {g}\in {B}\phantom{\rule{.4em}{0ex}}\underset{{x}\in {I}}{⨉}\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}}^{{I}}\right)$
59 eqid ${⊢}\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)=\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)$
60 59 fmpo ${⊢}\forall {f}\in {B}\phantom{\rule{.4em}{0ex}}\forall {g}\in {B}\phantom{\rule{.4em}{0ex}}\underset{{x}\in {I}}{⨉}\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}}^{{I}}\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):{B}×{B}⟶𝒫\left({\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{R}}^{{I}}\right)$
61 58 60 sylib ${⊢}{\phi }\to \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):{B}×{B}⟶𝒫\left({\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{R}}^{{I}}\right)$
62 4 fvexi ${⊢}{B}\in \mathrm{V}$
63 62 62 xpex ${⊢}{B}×{B}\in \mathrm{V}$
64 63 a1i ${⊢}{\phi }\to {B}×{B}\in \mathrm{V}$
65 54 pwex ${⊢}𝒫\left({\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{R}}^{{I}}\right)\in \mathrm{V}$
66 65 a1i ${⊢}{\phi }\to 𝒫\left({\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{R}}^{{I}}\right)\in \mathrm{V}$
67 fex2 ${⊢}\left(\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):{B}×{B}⟶𝒫\left({\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{R}}^{{I}}\right)\wedge {B}×{B}\in \mathrm{V}\wedge 𝒫\left({\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}{R}}^{{I}}\right)\in \mathrm{V}\right)\to \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)\in \mathrm{V}$
68 61 64 66 67 syl3anc ${⊢}{\phi }\to \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)\in \mathrm{V}$
69 snsspr1 ${⊢}\left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\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)⟩\right\}\subseteq \left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\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)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left({a}\in \left({B}×{B}\right),{c}\in {B}⟼\left({d}\in \left({c}\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){2}^{nd}\left({a}\right)\right),{e}\in \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)\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)⟩\right\}$
70 ssun2 ${⊢}\left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\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)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left({a}\in \left({B}×{B}\right),{c}\in {B}⟼\left({d}\in \left({c}\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){2}^{nd}\left({a}\right)\right),{e}\in \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)\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)⟩\right\}\subseteq \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left({P}\right)⟩,⟨{\le }_{\mathrm{ndx}},{\le }_{{P}}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{dist}\left({P}\right)⟩\right\}\cup \left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\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)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left({a}\in \left({B}×{B}\right),{c}\in {B}⟼\left({d}\in \left({c}\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){2}^{nd}\left({a}\right)\right),{e}\in \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)\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)⟩\right\}$
71 69 70 sstri ${⊢}\left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\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)⟩\right\}\subseteq \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left({P}\right)⟩,⟨{\le }_{\mathrm{ndx}},{\le }_{{P}}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{dist}\left({P}\right)⟩\right\}\cup \left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\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)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left({a}\in \left({B}×{B}\right),{c}\in {B}⟼\left({d}\in \left({c}\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){2}^{nd}\left({a}\right)\right),{e}\in \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)\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)⟩\right\}$
72 ssun2 ${⊢}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left({P}\right)⟩,⟨{\le }_{\mathrm{ndx}},{\le }_{{P}}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{dist}\left({P}\right)⟩\right\}\cup \left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\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)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left({a}\in \left({B}×{B}\right),{c}\in {B}⟼\left({d}\in \left({c}\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){2}^{nd}\left({a}\right)\right),{e}\in \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)\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)⟩\right\}\subseteq \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{B}⟩,⟨{+}_{\mathrm{ndx}},{+}_{{P}}⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_{{P}}⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{S}⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_{{P}}⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\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)⟩\right\}\right)\cup \left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left({P}\right)⟩,⟨{\le }_{\mathrm{ndx}},{\le }_{{P}}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{dist}\left({P}\right)⟩\right\}\cup \left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\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)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left({a}\in \left({B}×{B}\right),{c}\in {B}⟼\left({d}\in \left({c}\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){2}^{nd}\left({a}\right)\right),{e}\in \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)\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)⟩\right\}\right)$
73 71 72 sstri ${⊢}\left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\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)⟩\right\}\subseteq \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{B}⟩,⟨{+}_{\mathrm{ndx}},{+}_{{P}}⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_{{P}}⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{S}⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_{{P}}⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\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)⟩\right\}\right)\cup \left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left({P}\right)⟩,⟨{\le }_{\mathrm{ndx}},{\le }_{{P}}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{dist}\left({P}\right)⟩\right\}\cup \left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\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)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left({a}\in \left({B}×{B}\right),{c}\in {B}⟼\left({d}\in \left({c}\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){2}^{nd}\left({a}\right)\right),{e}\in \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)\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)⟩\right\}\right)$
74 24 6 25 68 73 prdsvallem ${⊢}{\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)$