# Metamath Proof Explorer

## Definition df-ssp

Description: Define the class of all subspaces of normed complex vector spaces. (Contributed by NM, 26-Jan-2008) (New usage is discouraged.)

Ref Expression
Assertion df-ssp ${⊢}\mathrm{SubSp}=\left({u}\in \mathrm{NrmCVec}⟼\left\{{w}\in \mathrm{NrmCVec}|\left({+}_{v}\left({w}\right)\subseteq {+}_{v}\left({u}\right)\wedge {\cdot }_{\mathrm{𝑠OLD}}\left({w}\right)\subseteq {\cdot }_{\mathrm{𝑠OLD}}\left({u}\right)\wedge {norm}_{CV}\left({w}\right)\subseteq {norm}_{CV}\left({u}\right)\right)\right\}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 css ${class}\mathrm{SubSp}$
1 vu ${setvar}{u}$
2 cnv ${class}\mathrm{NrmCVec}$
3 vw ${setvar}{w}$
4 cpv ${class}{+}_{v}$
5 3 cv ${setvar}{w}$
6 5 4 cfv ${class}{+}_{v}\left({w}\right)$
7 1 cv ${setvar}{u}$
8 7 4 cfv ${class}{+}_{v}\left({u}\right)$
9 6 8 wss ${wff}{+}_{v}\left({w}\right)\subseteq {+}_{v}\left({u}\right)$
10 cns ${class}{\cdot }_{\mathrm{𝑠OLD}}$
11 5 10 cfv ${class}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right)$
12 7 10 cfv ${class}{\cdot }_{\mathrm{𝑠OLD}}\left({u}\right)$
13 11 12 wss ${wff}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right)\subseteq {\cdot }_{\mathrm{𝑠OLD}}\left({u}\right)$
14 cnmcv ${class}{norm}_{CV}$
15 5 14 cfv ${class}{norm}_{CV}\left({w}\right)$
16 7 14 cfv ${class}{norm}_{CV}\left({u}\right)$
17 15 16 wss ${wff}{norm}_{CV}\left({w}\right)\subseteq {norm}_{CV}\left({u}\right)$
18 9 13 17 w3a ${wff}\left({+}_{v}\left({w}\right)\subseteq {+}_{v}\left({u}\right)\wedge {\cdot }_{\mathrm{𝑠OLD}}\left({w}\right)\subseteq {\cdot }_{\mathrm{𝑠OLD}}\left({u}\right)\wedge {norm}_{CV}\left({w}\right)\subseteq {norm}_{CV}\left({u}\right)\right)$
19 18 3 2 crab ${class}\left\{{w}\in \mathrm{NrmCVec}|\left({+}_{v}\left({w}\right)\subseteq {+}_{v}\left({u}\right)\wedge {\cdot }_{\mathrm{𝑠OLD}}\left({w}\right)\subseteq {\cdot }_{\mathrm{𝑠OLD}}\left({u}\right)\wedge {norm}_{CV}\left({w}\right)\subseteq {norm}_{CV}\left({u}\right)\right)\right\}$
20 1 2 19 cmpt ${class}\left({u}\in \mathrm{NrmCVec}⟼\left\{{w}\in \mathrm{NrmCVec}|\left({+}_{v}\left({w}\right)\subseteq {+}_{v}\left({u}\right)\wedge {\cdot }_{\mathrm{𝑠OLD}}\left({w}\right)\subseteq {\cdot }_{\mathrm{𝑠OLD}}\left({u}\right)\wedge {norm}_{CV}\left({w}\right)\subseteq {norm}_{CV}\left({u}\right)\right)\right\}\right)$
21 0 20 wceq ${wff}\mathrm{SubSp}=\left({u}\in \mathrm{NrmCVec}⟼\left\{{w}\in \mathrm{NrmCVec}|\left({+}_{v}\left({w}\right)\subseteq {+}_{v}\left({u}\right)\wedge {\cdot }_{\mathrm{𝑠OLD}}\left({w}\right)\subseteq {\cdot }_{\mathrm{𝑠OLD}}\left({u}\right)\wedge {norm}_{CV}\left({w}\right)\subseteq {norm}_{CV}\left({u}\right)\right)\right\}\right)$