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	$⊢ SubSp = (u \in NrmCVec ⟼ \{w \in NrmCVec \| (+_{v} (w) \subseteq +_{v} (u) \land \cdot_{𝑠OLD} (w) \subseteq \cdot_{𝑠OLD} (u) \land {norm}_{CV} (w) \subseteq {norm}_{CV} (u))\})$

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

Metamath Proof Explorer