df-ssp - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Definition df-ssp 8381

Description: Define the class of all subspaces of complex normed vector spaces.

**Assertion**
Ref	Expression
df-ssp	SubSp NrmCVec $/\$ NrmCVec $/\$ $/\$

**Detailed syntax breakdown of Definition df-ssp**
Step	Hyp	Ref	Expression
1		css 8380	. 2 SubSp
2		vu	. . . . . 6
3	2	cv 955	. . . . 5
4		cnv 8203	. . . . 5 NrmCVec
5	3, 4	wcel 958	. . . 4 NrmCVec
6		vs	. . . . . 6
7	6	cv 955	. . . . 5
8		vw	. . . . . . . . . 10
9	8	cv 955	. . . . . . . . 9
10		cpv 8204	. . . . . . . . 9
11	9, 10	cfv 3182	. . . . . . . 8
12	3, 10	cfv 3182	. . . . . . . 8
13	11, 12	wss 2047	. . . . . . 7
14		cns 8206	. . . . . . . . 9
15	9, 14	cfv 3182	. . . . . . . 8
16	3, 14	cfv 3182	. . . . . . . 8
17	15, 16	wss 2047	. . . . . . 7
18		cnm 8209	. . . . . . . . 9
19	9, 18	cfv 3182	. . . . . . . 8
20	3, 18	cfv 3182	. . . . . . . 8
21	19, 20	wss 2047	. . . . . . 7
22	13, 17, 21	w3a 775	. . . . . 6 $/\$ $/\$
23	22, 8, 4	crab 1648	. . . . 5 NrmCVec $/\$ $/\$
24	7, 23	wceq 956	. . . 4 NrmCVec $/\$ $/\$
25	5, 24	wa 223	. . 3 NrmCVec $/\$ NrmCVec $/\$ $/\$
26	25, 2, 6	copab 2666	. 2 NrmCVec $/\$ NrmCVec $/\$ $/\$
27	1, 26	wceq 956	1 SubSp NrmCVec $/\$ NrmCVec $/\$ $/\$

Colors of variables: wff set class

This definition is referenced by: sspval 8382