This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑢 ) ) } )