MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ssp Structured version   Visualization version   GIF version

Definition df-ssp 26761
Description: Define the class of all subspaces of complex normed 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
StepHypRef Expression
1 css 26760 . 2 class SubSp
2 vu . . 3 setvar 𝑢
3 cnv 26603 . . 3 class NrmCVec
4 vw . . . . . . . 8 setvar 𝑤
54cv 1473 . . . . . . 7 class 𝑤
6 cpv 26604 . . . . . . 7 class +𝑣
75, 6cfv 5786 . . . . . 6 class ( +𝑣𝑤)
82cv 1473 . . . . . . 7 class 𝑢
98, 6cfv 5786 . . . . . 6 class ( +𝑣𝑢)
107, 9wss 3535 . . . . 5 wff ( +𝑣𝑤) ⊆ ( +𝑣𝑢)
11 cns 26606 . . . . . . 7 class ·𝑠OLD
125, 11cfv 5786 . . . . . 6 class ( ·𝑠OLD𝑤)
138, 11cfv 5786 . . . . . 6 class ( ·𝑠OLD𝑢)
1412, 13wss 3535 . . . . 5 wff ( ·𝑠OLD𝑤) ⊆ ( ·𝑠OLD𝑢)
15 cnmcv 26609 . . . . . . 7 class normCV
165, 15cfv 5786 . . . . . 6 class (normCV𝑤)
178, 15cfv 5786 . . . . . 6 class (normCV𝑢)
1816, 17wss 3535 . . . . 5 wff (normCV𝑤) ⊆ (normCV𝑢)
1910, 14, 18w3a 1030 . . . 4 wff (( +𝑣𝑤) ⊆ ( +𝑣𝑢) ∧ ( ·𝑠OLD𝑤) ⊆ ( ·𝑠OLD𝑢) ∧ (normCV𝑤) ⊆ (normCV𝑢))
2019, 4, 3crab 2895 . . 3 class {𝑤 ∈ NrmCVec ∣ (( +𝑣𝑤) ⊆ ( +𝑣𝑢) ∧ ( ·𝑠OLD𝑤) ⊆ ( ·𝑠OLD𝑢) ∧ (normCV𝑤) ⊆ (normCV𝑢))}
212, 3, 20cmpt 4633 . 2 class (𝑢 ∈ NrmCVec ↦ {𝑤 ∈ NrmCVec ∣ (( +𝑣𝑤) ⊆ ( +𝑣𝑢) ∧ ( ·𝑠OLD𝑤) ⊆ ( ·𝑠OLD𝑢) ∧ (normCV𝑤) ⊆ (normCV𝑢))})
221, 21wceq 1474 1 wff SubSp = (𝑢 ∈ NrmCVec ↦ {𝑤 ∈ NrmCVec ∣ (( +𝑣𝑤) ⊆ ( +𝑣𝑢) ∧ ( ·𝑠OLD𝑤) ⊆ ( ·𝑠OLD𝑢) ∧ (normCV𝑤) ⊆ (normCV𝑢))})
Colors of variables: wff setvar class
This definition is referenced by:  sspval  26762
  Copyright terms: Public domain W3C validator