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 = u ∈ NrmCVec ⟼ w ∈ NrmCVec | + v ⁡ w ⊆ + v ⁡ u ∧ ⋅ 𝑠OLD ⁡ w ⊆ ⋅ 𝑠OLD ⁡ u ∧ norm CV ⁡ w ⊆ norm CV ⁡ u

Detailed syntax breakdown

Step Hyp Ref Expression
0 css class SubSp
1 vu setvar u
2 cnv class NrmCVec
3 vw setvar w
4 cpv class + v
5 3 cv setvar w
6 5 4 cfv class + v ⁡ w
7 1 cv setvar u
8 7 4 cfv class + v ⁡ u
9 6 8 wss wff + v ⁡ w ⊆ + v ⁡ u
10 cns class ⋅ 𝑠OLD
11 5 10 cfv class ⋅ 𝑠OLD ⁡ w
12 7 10 cfv class ⋅ 𝑠OLD ⁡ u
13 11 12 wss wff ⋅ 𝑠OLD ⁡ w ⊆ ⋅ 𝑠OLD ⁡ u
14 cnmcv class norm CV
15 5 14 cfv class norm CV ⁡ w
16 7 14 cfv class norm CV ⁡ u
17 15 16 wss wff norm CV ⁡ w ⊆ norm CV ⁡ u
18 9 13 17 w3a wff + v ⁡ w ⊆ + v ⁡ u ∧ ⋅ 𝑠OLD ⁡ w ⊆ ⋅ 𝑠OLD ⁡ u ∧ norm CV ⁡ w ⊆ norm CV ⁡ u
19 18 3 2 crab class w ∈ NrmCVec | + v ⁡ w ⊆ + v ⁡ u ∧ ⋅ 𝑠OLD ⁡ w ⊆ ⋅ 𝑠OLD ⁡ u ∧ norm CV ⁡ w ⊆ norm CV ⁡ u
20 1 2 19 cmpt class u ∈ NrmCVec ⟼ w ∈ NrmCVec | + v ⁡ w ⊆ + v ⁡ u ∧ ⋅ 𝑠OLD ⁡ w ⊆ ⋅ 𝑠OLD ⁡ u ∧ norm CV ⁡ w ⊆ norm CV ⁡ u
21 0 20 wceq wff SubSp = u ∈ NrmCVec ⟼ w ∈ NrmCVec | + v ⁡ w ⊆ + v ⁡ u ∧ ⋅ 𝑠OLD ⁡ w ⊆ ⋅ 𝑠OLD ⁡ u ∧ norm CV ⁡ w ⊆ norm CV ⁡ u