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	⊢ SubSp = ( 𝑢 ∈ NrmCVec ↦ { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣 ‘ 𝑤 ) ⊆ ( +𝑣 ‘ 𝑢 ) ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ ( ·𝑠OLD ‘ 𝑢 ) ∧ ( normCV ‘ 𝑤 ) ⊆ ( normCV ‘ 𝑢 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		css	⊢ SubSp
1		vu	⊢ 𝑢
2		cnv	⊢ NrmCVec
3		vw	⊢ 𝑤
4		cpv	⊢ +𝑣
5	3	cv	⊢ 𝑤
6	5 4	cfv	⊢ ( +𝑣 ‘ 𝑤 )
7	1	cv	⊢ 𝑢
8	7 4	cfv	⊢ ( +𝑣 ‘ 𝑢 )
9	6 8	wss	⊢ ( +𝑣 ‘ 𝑤 ) ⊆ ( +𝑣 ‘ 𝑢 )
10		cns	⊢ ·𝑠OLD
11	5 10	cfv	⊢ ( ·𝑠OLD ‘ 𝑤 )
12	7 10	cfv	⊢ ( ·𝑠OLD ‘ 𝑢 )
13	11 12	wss	⊢ ( ·𝑠OLD ‘ 𝑤 ) ⊆ ( ·𝑠OLD ‘ 𝑢 )
14		cnmcv	⊢ normCV
15	5 14	cfv	⊢ ( normCV ‘ 𝑤 )
16	7 14	cfv	⊢ ( normCV ‘ 𝑢 )
17	15 16	wss	⊢ ( normCV ‘ 𝑤 ) ⊆ ( normCV ‘ 𝑢 )
18	9 13 17	w3a	⊢ ( ( +𝑣 ‘ 𝑤 ) ⊆ ( +𝑣 ‘ 𝑢 ) ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ ( ·𝑠OLD ‘ 𝑢 ) ∧ ( normCV ‘ 𝑤 ) ⊆ ( normCV ‘ 𝑢 ) )
19	18 3 2	crab	⊢ { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣 ‘ 𝑤 ) ⊆ ( +𝑣 ‘ 𝑢 ) ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ ( ·𝑠OLD ‘ 𝑢 ) ∧ ( normCV ‘ 𝑤 ) ⊆ ( normCV ‘ 𝑢 ) ) }
20	1 2 19	cmpt	⊢ ( 𝑢 ∈ NrmCVec ↦ { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣 ‘ 𝑤 ) ⊆ ( +𝑣 ‘ 𝑢 ) ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ ( ·𝑠OLD ‘ 𝑢 ) ∧ ( normCV ‘ 𝑤 ) ⊆ ( normCV ‘ 𝑢 ) ) } )
21	0 20	wceq	⊢ SubSp = ( 𝑢 ∈ NrmCVec ↦ { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣 ‘ 𝑤 ) ⊆ ( +𝑣 ‘ 𝑢 ) ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ ( ·𝑠OLD ‘ 𝑢 ) ∧ ( normCV ‘ 𝑤 ) ⊆ ( normCV ‘ 𝑢 ) ) } )