# Metamath Proof Explorer

## Definition df-prds

Description: Define a structure product. This can be a product of groups, rings, modules, or ordered topological fields; any unused components will have garbage in them but this is usually not relevant for the purpose of inheriting the structures present in the factors. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by Thierry Arnoux, 15-Jun-2019)

Ref Expression
Assertion df-prds

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cprds ${class}{⨉}_{𝑠}$
1 vs ${setvar}{s}$
2 cvv ${class}\mathrm{V}$
3 vr ${setvar}{r}$
4 vx ${setvar}{x}$
5 3 cv ${setvar}{r}$
6 5 cdm ${class}\mathrm{dom}{r}$
7 cbs ${class}\mathrm{Base}$
8 4 cv ${setvar}{x}$
9 8 5 cfv ${class}{r}\left({x}\right)$
10 9 7 cfv ${class}{\mathrm{Base}}_{{r}\left({x}\right)}$
11 4 6 10 cixp ${class}\underset{{x}\in \mathrm{dom}{r}}{⨉}{\mathrm{Base}}_{{r}\left({x}\right)}$
12 vv ${setvar}{v}$
13 vf ${setvar}{f}$
14 12 cv ${setvar}{v}$
15 vg ${setvar}{g}$
16 13 cv ${setvar}{f}$
17 8 16 cfv ${class}{f}\left({x}\right)$
18 chom ${class}\mathrm{Hom}$
19 9 18 cfv ${class}\mathrm{Hom}\left({r}\left({x}\right)\right)$
20 15 cv ${setvar}{g}$
21 8 20 cfv ${class}{g}\left({x}\right)$
22 17 21 19 co ${class}\left({f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)$
23 4 6 22 cixp ${class}\underset{{x}\in \mathrm{dom}{r}}{⨉}\left({f}\left({x}\right)\mathrm{Hom}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)$
24 13 15 14 14 23 cmpo ${class}\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)$
25 vh ${setvar}{h}$
26 cnx ${class}\mathrm{ndx}$
27 26 7 cfv ${class}{\mathrm{Base}}_{\mathrm{ndx}}$
28 27 14 cop ${class}⟨{\mathrm{Base}}_{\mathrm{ndx}},{v}⟩$
29 cplusg ${class}{+}_{𝑔}$
30 26 29 cfv ${class}{+}_{\mathrm{ndx}}$
31 9 29 cfv ${class}{+}_{{r}\left({x}\right)}$
32 17 21 31 co ${class}\left({f}\left({x}\right){+}_{{r}\left({x}\right)}{g}\left({x}\right)\right)$
33 4 6 32 cmpt ${class}\left({x}\in \mathrm{dom}{r}⟼{f}\left({x}\right){+}_{{r}\left({x}\right)}{g}\left({x}\right)\right)$
34 13 15 14 14 33 cmpo ${class}\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)$
35 30 34 cop ${class}⟨{+}_{\mathrm{ndx}},\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)⟩$
36 cmulr ${class}{\cdot }_{𝑟}$
37 26 36 cfv ${class}{\cdot }_{\mathrm{ndx}}$
38 9 36 cfv ${class}{\cdot }_{{r}\left({x}\right)}$
39 17 21 38 co ${class}\left({f}\left({x}\right){\cdot }_{{r}\left({x}\right)}{g}\left({x}\right)\right)$
40 4 6 39 cmpt ${class}\left({x}\in \mathrm{dom}{r}⟼{f}\left({x}\right){\cdot }_{{r}\left({x}\right)}{g}\left({x}\right)\right)$
41 13 15 14 14 40 cmpo ${class}\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)$
42 37 41 cop ${class}⟨{\cdot }_{\mathrm{ndx}},\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)⟩$
43 28 35 42 ctp ${class}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{v}⟩,⟨{+}_{\mathrm{ndx}},\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)⟩,⟨{\cdot }_{\mathrm{ndx}},\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)⟩\right\}$
44 csca ${class}\mathrm{Scalar}$
45 26 44 cfv ${class}\mathrm{Scalar}\left(\mathrm{ndx}\right)$
46 1 cv ${setvar}{s}$
47 45 46 cop ${class}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{s}⟩$
48 cvsca ${class}{\cdot }_{𝑠}$
49 26 48 cfv ${class}{\cdot }_{\mathrm{ndx}}$
50 46 7 cfv ${class}{\mathrm{Base}}_{{s}}$
51 9 48 cfv ${class}{\cdot }_{{r}\left({x}\right)}$
52 16 21 51 co ${class}\left({f}{\cdot }_{{r}\left({x}\right)}{g}\left({x}\right)\right)$
53 4 6 52 cmpt ${class}\left({x}\in \mathrm{dom}{r}⟼{f}{\cdot }_{{r}\left({x}\right)}{g}\left({x}\right)\right)$
54 13 15 50 14 53 cmpo ${class}\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)$
55 49 54 cop ${class}⟨{\cdot }_{\mathrm{ndx}},\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)⟩$
56 cip ${class}{\cdot }_{𝑖}$
57 26 56 cfv ${class}{\cdot }_{𝑖}\left(\mathrm{ndx}\right)$
58 cgsu ${class}{\Sigma }_{𝑔}$
59 9 56 cfv ${class}{\cdot }_{𝑖}\left({r}\left({x}\right)\right)$
60 17 21 59 co ${class}\left({f}\left({x}\right){\cdot }_{𝑖}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)$
61 4 6 60 cmpt ${class}\left({x}\in \mathrm{dom}{r}⟼{f}\left({x}\right){\cdot }_{𝑖}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)$
62 46 61 58 co ${class}\left(\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)$
63 13 15 14 14 62 cmpo ${class}\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)$
64 57 63 cop ${class}⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\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)⟩$
65 47 55 64 ctp ${class}\left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{s}⟩,⟨{\cdot }_{\mathrm{ndx}},\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)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\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)⟩\right\}$
66 43 65 cun ${class}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{v}⟩,⟨{+}_{\mathrm{ndx}},\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)⟩,⟨{\cdot }_{\mathrm{ndx}},\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)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{s}⟩,⟨{\cdot }_{\mathrm{ndx}},\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)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\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)⟩\right\}\right)$
67 cts ${class}\mathrm{TopSet}$
68 26 67 cfv ${class}\mathrm{TopSet}\left(\mathrm{ndx}\right)$
69 cpt ${class}{\prod }_{𝑡}$
70 ctopn ${class}\mathrm{TopOpen}$
71 70 5 ccom ${class}\left(\mathrm{TopOpen}\circ {r}\right)$
72 71 69 cfv ${class}{\prod }_{𝑡}\left(\mathrm{TopOpen}\circ {r}\right)$
73 68 72 cop ${class}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(\mathrm{TopOpen}\circ {r}\right)⟩$
74 cple ${class}\mathrm{le}$
75 26 74 cfv ${class}{\le }_{\mathrm{ndx}}$
76 16 20 cpr ${class}\left\{{f},{g}\right\}$
77 76 14 wss ${wff}\left\{{f},{g}\right\}\subseteq {v}$
78 9 74 cfv ${class}{\le }_{{r}\left({x}\right)}$
79 17 21 78 wbr ${wff}{f}\left({x}\right){\le }_{{r}\left({x}\right)}{g}\left({x}\right)$
80 79 4 6 wral ${wff}\forall {x}\in \mathrm{dom}{r}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){\le }_{{r}\left({x}\right)}{g}\left({x}\right)$
81 77 80 wa ${wff}\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)$
82 81 13 15 copab ${class}\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\}$
83 75 82 cop ${class}⟨{\le }_{\mathrm{ndx}},\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\}⟩$
84 cds ${class}\mathrm{dist}$
85 26 84 cfv ${class}\mathrm{dist}\left(\mathrm{ndx}\right)$
86 9 84 cfv ${class}\mathrm{dist}\left({r}\left({x}\right)\right)$
87 17 21 86 co ${class}\left({f}\left({x}\right)\mathrm{dist}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)$
88 4 6 87 cmpt ${class}\left({x}\in \mathrm{dom}{r}⟼{f}\left({x}\right)\mathrm{dist}\left({r}\left({x}\right)\right){g}\left({x}\right)\right)$
89 88 crn ${class}\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)$
90 cc0 ${class}0$
91 90 csn ${class}\left\{0\right\}$
92 89 91 cun ${class}\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)$
93 cxr ${class}{ℝ}^{*}$
94 clt ${class}<$
95 92 93 94 csup ${class}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)$
96 13 15 14 14 95 cmpo ${class}\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)$
97 85 96 cop ${class}⟨\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)⟩$
98 73 83 97 ctp ${class}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(\mathrm{TopOpen}\circ {r}\right)⟩,⟨{\le }_{\mathrm{ndx}},\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\}⟩,⟨\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)⟩\right\}$
99 26 18 cfv ${class}\mathrm{Hom}\left(\mathrm{ndx}\right)$
100 25 cv ${setvar}{h}$
101 99 100 cop ${class}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{h}⟩$
102 cco ${class}\mathrm{comp}$
103 26 102 cfv ${class}\mathrm{comp}\left(\mathrm{ndx}\right)$
104 va ${setvar}{a}$
105 14 14 cxp ${class}\left({v}×{v}\right)$
106 vc ${setvar}{c}$
107 vd ${setvar}{d}$
108 106 cv ${setvar}{c}$
109 c2nd ${class}{2}^{nd}$
110 104 cv ${setvar}{a}$
111 110 109 cfv ${class}{2}^{nd}\left({a}\right)$
112 108 111 100 co ${class}\left({c}{h}{2}^{nd}\left({a}\right)\right)$
113 ve ${setvar}{e}$
114 110 100 cfv ${class}{h}\left({a}\right)$
115 107 cv ${setvar}{d}$
116 8 115 cfv ${class}{d}\left({x}\right)$
117 c1st ${class}{1}^{st}$
118 110 117 cfv ${class}{1}^{st}\left({a}\right)$
119 8 118 cfv ${class}{1}^{st}\left({a}\right)\left({x}\right)$
120 8 111 cfv ${class}{2}^{nd}\left({a}\right)\left({x}\right)$
121 119 120 cop ${class}⟨{1}^{st}\left({a}\right)\left({x}\right),{2}^{nd}\left({a}\right)\left({x}\right)⟩$
122 9 102 cfv ${class}\mathrm{comp}\left({r}\left({x}\right)\right)$
123 8 108 cfv ${class}{c}\left({x}\right)$
124 121 123 122 co ${class}\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)$
125 113 cv ${setvar}{e}$
126 8 125 cfv ${class}{e}\left({x}\right)$
127 116 126 124 co ${class}\left({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)$
128 4 6 127 cmpt ${class}\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)$
129 107 113 112 114 128 cmpo ${class}\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)$
130 104 106 105 14 129 cmpo ${class}\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)$
131 103 130 cop ${class}⟨\mathrm{comp}\left(\mathrm{ndx}\right),\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)⟩$
132 101 131 cpr ${class}\left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{h}⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\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)⟩\right\}$
133 98 132 cun ${class}\left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(\mathrm{TopOpen}\circ {r}\right)⟩,⟨{\le }_{\mathrm{ndx}},\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\}⟩,⟨\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)⟩\right\}\cup \left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{h}⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\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)⟩\right\}\right)$
134 66 133 cun ${class}\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{v}⟩,⟨{+}_{\mathrm{ndx}},\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)⟩,⟨{\cdot }_{\mathrm{ndx}},\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)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{s}⟩,⟨{\cdot }_{\mathrm{ndx}},\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)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\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)⟩\right\}\right)\cup \left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(\mathrm{TopOpen}\circ {r}\right)⟩,⟨{\le }_{\mathrm{ndx}},\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\}⟩,⟨\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)⟩\right\}\cup \left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{h}⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\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)⟩\right\}\right)\right)$
135 25 24 134 csb
136 12 11 135 csb
137 1 3 2 2 136 cmpo
138 0 137 wceq