# Metamath Proof Explorer

## Definition df-lno

Description: Define the class of linear operators between two normed complex vector spaces. In the literature, an operator may be a partial function, i.e. the domain of an operator is not necessarily the entire vector space. However, since the domain of a linear operator is a vector subspace, we define it with a complete function for convenience and will use subset relations to specify the partial function case. (Contributed by NM, 6-Nov-2007) (New usage is discouraged.)

Ref Expression
Assertion df-lno ${⊢}\mathrm{LnOp}=\left({u}\in \mathrm{NrmCVec},{w}\in \mathrm{NrmCVec}⟼\left\{{t}\in \left({\mathrm{BaseSet}\left({w}\right)}^{\mathrm{BaseSet}\left({u}\right)}\right)|\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{BaseSet}\left({u}\right)\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{BaseSet}\left({u}\right)\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({u}\right){y}\right){+}_{v}\left({u}\right){z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)\right){+}_{v}\left({w}\right){t}\left({z}\right)\right\}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 clno ${class}\mathrm{LnOp}$
1 vu ${setvar}{u}$
2 cnv ${class}\mathrm{NrmCVec}$
3 vw ${setvar}{w}$
4 vt ${setvar}{t}$
5 cba ${class}\mathrm{BaseSet}$
6 3 cv ${setvar}{w}$
7 6 5 cfv ${class}\mathrm{BaseSet}\left({w}\right)$
8 cmap ${class}{↑}_{𝑚}$
9 1 cv ${setvar}{u}$
10 9 5 cfv ${class}\mathrm{BaseSet}\left({u}\right)$
11 7 10 8 co ${class}\left({\mathrm{BaseSet}\left({w}\right)}^{\mathrm{BaseSet}\left({u}\right)}\right)$
12 vx ${setvar}{x}$
13 cc ${class}ℂ$
14 vy ${setvar}{y}$
15 vz ${setvar}{z}$
16 4 cv ${setvar}{t}$
17 12 cv ${setvar}{x}$
18 cns ${class}{\cdot }_{\mathrm{𝑠OLD}}$
19 9 18 cfv ${class}{\cdot }_{\mathrm{𝑠OLD}}\left({u}\right)$
20 14 cv ${setvar}{y}$
21 17 20 19 co ${class}\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({u}\right){y}\right)$
22 cpv ${class}{+}_{v}$
23 9 22 cfv ${class}{+}_{v}\left({u}\right)$
24 15 cv ${setvar}{z}$
25 21 24 23 co ${class}\left(\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({u}\right){y}\right){+}_{v}\left({u}\right){z}\right)$
26 25 16 cfv ${class}{t}\left(\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({u}\right){y}\right){+}_{v}\left({u}\right){z}\right)$
27 6 18 cfv ${class}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right)$
28 20 16 cfv ${class}{t}\left({y}\right)$
29 17 28 27 co ${class}\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)\right)$
30 6 22 cfv ${class}{+}_{v}\left({w}\right)$
31 24 16 cfv ${class}{t}\left({z}\right)$
32 29 31 30 co ${class}\left(\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)\right){+}_{v}\left({w}\right){t}\left({z}\right)\right)$
33 26 32 wceq ${wff}{t}\left(\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({u}\right){y}\right){+}_{v}\left({u}\right){z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)\right){+}_{v}\left({w}\right){t}\left({z}\right)$
34 33 15 10 wral ${wff}\forall {z}\in \mathrm{BaseSet}\left({u}\right)\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({u}\right){y}\right){+}_{v}\left({u}\right){z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)\right){+}_{v}\left({w}\right){t}\left({z}\right)$
35 34 14 10 wral ${wff}\forall {y}\in \mathrm{BaseSet}\left({u}\right)\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{BaseSet}\left({u}\right)\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({u}\right){y}\right){+}_{v}\left({u}\right){z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)\right){+}_{v}\left({w}\right){t}\left({z}\right)$
36 35 12 13 wral ${wff}\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{BaseSet}\left({u}\right)\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{BaseSet}\left({u}\right)\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({u}\right){y}\right){+}_{v}\left({u}\right){z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)\right){+}_{v}\left({w}\right){t}\left({z}\right)$
37 36 4 11 crab ${class}\left\{{t}\in \left({\mathrm{BaseSet}\left({w}\right)}^{\mathrm{BaseSet}\left({u}\right)}\right)|\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{BaseSet}\left({u}\right)\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{BaseSet}\left({u}\right)\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({u}\right){y}\right){+}_{v}\left({u}\right){z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)\right){+}_{v}\left({w}\right){t}\left({z}\right)\right\}$
38 1 3 2 2 37 cmpo ${class}\left({u}\in \mathrm{NrmCVec},{w}\in \mathrm{NrmCVec}⟼\left\{{t}\in \left({\mathrm{BaseSet}\left({w}\right)}^{\mathrm{BaseSet}\left({u}\right)}\right)|\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{BaseSet}\left({u}\right)\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{BaseSet}\left({u}\right)\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({u}\right){y}\right){+}_{v}\left({u}\right){z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)\right){+}_{v}\left({w}\right){t}\left({z}\right)\right\}\right)$
39 0 38 wceq ${wff}\mathrm{LnOp}=\left({u}\in \mathrm{NrmCVec},{w}\in \mathrm{NrmCVec}⟼\left\{{t}\in \left({\mathrm{BaseSet}\left({w}\right)}^{\mathrm{BaseSet}\left({u}\right)}\right)|\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{BaseSet}\left({u}\right)\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{BaseSet}\left({u}\right)\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({u}\right){y}\right){+}_{v}\left({u}\right){z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)\right){+}_{v}\left({w}\right){t}\left({z}\right)\right\}\right)$