Definition df-ssp 29963

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 29962	. 2 class SubSp
2		vu	. . 3 setvar 𝑢
3		cnv 29825	. . 3 class NrmCVec
4		vw	. . . . . . . 8 setvar 𝑤
5	4	cv 1541	. . . . . . 7 class 𝑤
6		cpv 29826	. . . . . . 7 class +𝑣
7	5, 6	cfv 6541	. . . . . 6 class ( +𝑣 ‘𝑤)
8	2	cv 1541	. . . . . . 7 class 𝑢
9	8, 6	cfv 6541	. . . . . 6 class ( +𝑣 ‘𝑢)
10	7, 9	wss 3948	. . . . 5 wff ( +𝑣 ‘𝑤) ⊆ ( +𝑣 ‘𝑢)
11		cns 29828	. . . . . . 7 class ·𝑠OLD
12	5, 11	cfv 6541	. . . . . 6 class ( ·𝑠OLD ‘𝑤)
13	8, 11	cfv 6541	. . . . . 6 class ( ·𝑠OLD ‘𝑢)
14	12, 13	wss 3948	. . . . 5 wff ( ·𝑠OLD ‘𝑤) ⊆ ( ·𝑠OLD ‘𝑢)
15		cnmcv 29831	. . . . . . 7 class normCV
16	5, 15	cfv 6541	. . . . . 6 class (normCV‘𝑤)
17	8, 15	cfv 6541	. . . . . 6 class (normCV‘𝑢)
18	16, 17	wss 3948	. . . . 5 wff (normCV‘𝑤) ⊆ (normCV‘𝑢)
19	10, 14, 18	w3a 1088	. . . 4 wff (( +𝑣 ‘𝑤) ⊆ ( +𝑣 ‘𝑢) ∧ ( ·𝑠OLD ‘𝑤) ⊆ ( ·𝑠OLD ‘𝑢) ∧ (normCV‘𝑤) ⊆ (normCV‘𝑢))
20	19, 4, 3	crab 3433	. . 3 class {𝑤 ∈ NrmCVec ∣ (( +𝑣 ‘𝑤) ⊆ ( +𝑣 ‘𝑢) ∧ ( ·𝑠OLD ‘𝑤) ⊆ ( ·𝑠OLD ‘𝑢) ∧ (normCV‘𝑤) ⊆ (normCV‘𝑢))}
21	2, 3, 20	cmpt 5231	. 2 class (𝑢 ∈ NrmCVec ↦ {𝑤 ∈ NrmCVec ∣ (( +𝑣 ‘𝑤) ⊆ ( +𝑣 ‘𝑢) ∧ ( ·𝑠OLD ‘𝑤) ⊆ ( ·𝑠OLD ‘𝑢) ∧ (normCV‘𝑤) ⊆ (normCV‘𝑢))})
22	1, 21	wceq 1542	1 wff SubSp = (𝑢 ∈ NrmCVec ↦ {𝑤 ∈ NrmCVec ∣ (( +𝑣 ‘𝑤) ⊆ ( +𝑣 ‘𝑢) ∧ ( ·𝑠OLD ‘𝑤) ⊆ ( ·𝑠OLD ‘𝑢) ∧ (normCV‘𝑤) ⊆ (normCV‘𝑢))})

This definition is referenced by:  sspval  29964