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

Definition df-ssp 27705
 Description: Define the class of all subspaces of normed complex 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 27704 . 2 class SubSp
2 vu . . 3 setvar 𝑢
3 cnv 27567 . . 3 class NrmCVec
4 vw . . . . . . . 8 setvar 𝑤
54cv 1522 . . . . . . 7 class 𝑤
6 cpv 27568 . . . . . . 7 class +𝑣
75, 6cfv 5926 . . . . . 6 class ( +𝑣𝑤)
82cv 1522 . . . . . . 7 class 𝑢
98, 6cfv 5926 . . . . . 6 class ( +𝑣𝑢)
107, 9wss 3607 . . . . 5 wff ( +𝑣𝑤) ⊆ ( +𝑣𝑢)
11 cns 27570 . . . . . . 7 class ·𝑠OLD
125, 11cfv 5926 . . . . . 6 class ( ·𝑠OLD𝑤)
138, 11cfv 5926 . . . . . 6 class ( ·𝑠OLD𝑢)
1412, 13wss 3607 . . . . 5 wff ( ·𝑠OLD𝑤) ⊆ ( ·𝑠OLD𝑢)
15 cnmcv 27573 . . . . . . 7 class normCV
165, 15cfv 5926 . . . . . 6 class (normCV𝑤)
178, 15cfv 5926 . . . . . 6 class (normCV𝑢)
1816, 17wss 3607 . . . . 5 wff (normCV𝑤) ⊆ (normCV𝑢)
1910, 14, 18w3a 1054 . . . 4 wff (( +𝑣𝑤) ⊆ ( +𝑣𝑢) ∧ ( ·𝑠OLD𝑤) ⊆ ( ·𝑠OLD𝑢) ∧ (normCV𝑤) ⊆ (normCV𝑢))
2019, 4, 3crab 2945 . . 3 class {𝑤 ∈ NrmCVec ∣ (( +𝑣𝑤) ⊆ ( +𝑣𝑢) ∧ ( ·𝑠OLD𝑤) ⊆ ( ·𝑠OLD𝑢) ∧ (normCV𝑤) ⊆ (normCV𝑢))}
212, 3, 20cmpt 4762 . 2 class (𝑢 ∈ NrmCVec ↦ {𝑤 ∈ NrmCVec ∣ (( +𝑣𝑤) ⊆ ( +𝑣𝑢) ∧ ( ·𝑠OLD𝑤) ⊆ ( ·𝑠OLD𝑢) ∧ (normCV𝑤) ⊆ (normCV𝑢))})
221, 21wceq 1523 1 wff SubSp = (𝑢 ∈ NrmCVec ↦ {𝑤 ∈ NrmCVec ∣ (( +𝑣𝑤) ⊆ ( +𝑣𝑢) ∧ ( ·𝑠OLD𝑤) ⊆ ( ·𝑠OLD𝑢) ∧ (normCV𝑤) ⊆ (normCV𝑢))})
 Colors of variables: wff setvar class This definition is referenced by:  sspval  27706
 Copyright terms: Public domain W3C validator