Definition df-ssp 28985

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

Assertion

Ref	Expression
df-ssp	⊢ SubSp = (𝑢 ∈ NrmCVec ↦ {𝑤 ∈ NrmCVec ∣ (( +𝑣 ‘𝑤) ⊆ ( +𝑣 ‘𝑢) ∧ ( ·𝑠OLD ‘𝑤) ⊆ ( ·𝑠OLD ‘𝑢) ∧ (normCV‘𝑤) ⊆ (normCV‘𝑢))})

Distinct variable group:   𝑤,𝑢

Detailed syntax breakdown of Definition df-ssp

Step	Hyp	Ref	Expression
1		css 28984	. 2 class SubSp
2		vu	. . 3 setvar 𝑢
3		cnv 28847	. . 3 class NrmCVec
4		vw	. . . . . . . 8 setvar 𝑤
5	4	cv 1538	. . . . . . 7 class 𝑤
6		cpv 28848	. . . . . . 7 class +𝑣
7	5, 6	cfv 6418	. . . . . 6 class ( +𝑣 ‘𝑤)
8	2	cv 1538	. . . . . . 7 class 𝑢
9	8, 6	cfv 6418	. . . . . 6 class ( +𝑣 ‘𝑢)
10	7, 9	wss 3883	. . . . 5 wff ( +𝑣 ‘𝑤) ⊆ ( +𝑣 ‘𝑢)
11		cns 28850	. . . . . . 7 class ·𝑠OLD
12	5, 11	cfv 6418	. . . . . 6 class ( ·𝑠OLD ‘𝑤)
13	8, 11	cfv 6418	. . . . . 6 class ( ·𝑠OLD ‘𝑢)
14	12, 13	wss 3883	. . . . 5 wff ( ·𝑠OLD ‘𝑤) ⊆ ( ·𝑠OLD ‘𝑢)
15		cnmcv 28853	. . . . . . 7 class normCV
16	5, 15	cfv 6418	. . . . . 6 class (normCV‘𝑤)
17	8, 15	cfv 6418	. . . . . 6 class (normCV‘𝑢)
18	16, 17	wss 3883	. . . . 5 wff (normCV‘𝑤) ⊆ (normCV‘𝑢)
19	10, 14, 18	w3a 1085	. . . 4 wff (( +𝑣 ‘𝑤) ⊆ ( +𝑣 ‘𝑢) ∧ ( ·𝑠OLD ‘𝑤) ⊆ ( ·𝑠OLD ‘𝑢) ∧ (normCV‘𝑤) ⊆ (normCV‘𝑢))
20	19, 4, 3	crab 3067	. . 3 class {𝑤 ∈ NrmCVec ∣ (( +𝑣 ‘𝑤) ⊆ ( +𝑣 ‘𝑢) ∧ ( ·𝑠OLD ‘𝑤) ⊆ ( ·𝑠OLD ‘𝑢) ∧ (normCV‘𝑤) ⊆ (normCV‘𝑢))}
21	2, 3, 20	cmpt 5153	. 2 class (𝑢 ∈ NrmCVec ↦ {𝑤 ∈ NrmCVec ∣ (( +𝑣 ‘𝑤) ⊆ ( +𝑣 ‘𝑢) ∧ ( ·𝑠OLD ‘𝑤) ⊆ ( ·𝑠OLD ‘𝑢) ∧ (normCV‘𝑤) ⊆ (normCV‘𝑢))})
22	1, 21	wceq 1539	1 wff SubSp = (𝑢 ∈ NrmCVec ↦ {𝑤 ∈ NrmCVec ∣ (( +𝑣 ‘𝑤) ⊆ ( +𝑣 ‘𝑢) ∧ ( ·𝑠OLD ‘𝑤) ⊆ ( ·𝑠OLD ‘𝑢) ∧ (normCV‘𝑤) ⊆ (normCV‘𝑢))})

This definition is referenced by:  sspval  28986