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

Definition df-ssp 26961
 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 26960 . 2 class SubSp
2 vu . . 3 setvar 𝑢
3 cnv 26823 . . 3 class NrmCVec
4 vw . . . . . . . 8 setvar 𝑤
54cv 1474 . . . . . . 7 class 𝑤
6 cpv 26824 . . . . . . 7 class +𝑣
75, 6cfv 5804 . . . . . 6 class ( +𝑣𝑤)
82cv 1474 . . . . . . 7 class 𝑢
98, 6cfv 5804 . . . . . 6 class ( +𝑣𝑢)
107, 9wss 3540 . . . . 5 wff ( +𝑣𝑤) ⊆ ( +𝑣𝑢)
11 cns 26826 . . . . . . 7 class ·𝑠OLD
125, 11cfv 5804 . . . . . 6 class ( ·𝑠OLD𝑤)
138, 11cfv 5804 . . . . . 6 class ( ·𝑠OLD𝑢)
1412, 13wss 3540 . . . . 5 wff ( ·𝑠OLD𝑤) ⊆ ( ·𝑠OLD𝑢)
15 cnmcv 26829 . . . . . . 7 class normCV
165, 15cfv 5804 . . . . . 6 class (normCV𝑤)
178, 15cfv 5804 . . . . . 6 class (normCV𝑢)
1816, 17wss 3540 . . . . 5 wff (normCV𝑤) ⊆ (normCV𝑢)
1910, 14, 18w3a 1031 . . . 4 wff (( +𝑣𝑤) ⊆ ( +𝑣𝑢) ∧ ( ·𝑠OLD𝑤) ⊆ ( ·𝑠OLD𝑢) ∧ (normCV𝑤) ⊆ (normCV𝑢))
2019, 4, 3crab 2900 . . 3 class {𝑤 ∈ NrmCVec ∣ (( +𝑣𝑤) ⊆ ( +𝑣𝑢) ∧ ( ·𝑠OLD𝑤) ⊆ ( ·𝑠OLD𝑢) ∧ (normCV𝑤) ⊆ (normCV𝑢))}
212, 3, 20cmpt 4643 . 2 class (𝑢 ∈ NrmCVec ↦ {𝑤 ∈ NrmCVec ∣ (( +𝑣𝑤) ⊆ ( +𝑣𝑢) ∧ ( ·𝑠OLD𝑤) ⊆ ( ·𝑠OLD𝑢) ∧ (normCV𝑤) ⊆ (normCV𝑢))})
221, 21wceq 1475 1 wff SubSp = (𝑢 ∈ NrmCVec ↦ {𝑤 ∈ NrmCVec ∣ (( +𝑣𝑤) ⊆ ( +𝑣𝑢) ∧ ( ·𝑠OLD𝑤) ⊆ ( ·𝑠OLD𝑢) ∧ (normCV𝑤) ⊆ (normCV𝑢))})
 Colors of variables: wff setvar class This definition is referenced by:  sspval  26962
 Copyright terms: Public domain W3C validator