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 28649
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 28648 . 2 class SubSp
2 vu . . 3 setvar 𝑢
3 cnv 28511 . . 3 class NrmCVec
4 vw . . . . . . . 8 setvar 𝑤
54cv 1541 . . . . . . 7 class 𝑤
6 cpv 28512 . . . . . . 7 class +𝑣
75, 6cfv 6333 . . . . . 6 class ( +𝑣𝑤)
82cv 1541 . . . . . . 7 class 𝑢
98, 6cfv 6333 . . . . . 6 class ( +𝑣𝑢)
107, 9wss 3841 . . . . 5 wff ( +𝑣𝑤) ⊆ ( +𝑣𝑢)
11 cns 28514 . . . . . . 7 class ·𝑠OLD
125, 11cfv 6333 . . . . . 6 class ( ·𝑠OLD𝑤)
138, 11cfv 6333 . . . . . 6 class ( ·𝑠OLD𝑢)
1412, 13wss 3841 . . . . 5 wff ( ·𝑠OLD𝑤) ⊆ ( ·𝑠OLD𝑢)
15 cnmcv 28517 . . . . . . 7 class normCV
165, 15cfv 6333 . . . . . 6 class (normCV𝑤)
178, 15cfv 6333 . . . . . 6 class (normCV𝑢)
1816, 17wss 3841 . . . . 5 wff (normCV𝑤) ⊆ (normCV𝑢)
1910, 14, 18w3a 1088 . . . 4 wff (( +𝑣𝑤) ⊆ ( +𝑣𝑢) ∧ ( ·𝑠OLD𝑤) ⊆ ( ·𝑠OLD𝑢) ∧ (normCV𝑤) ⊆ (normCV𝑢))
2019, 4, 3crab 3057 . . 3 class {𝑤 ∈ NrmCVec ∣ (( +𝑣𝑤) ⊆ ( +𝑣𝑢) ∧ ( ·𝑠OLD𝑤) ⊆ ( ·𝑠OLD𝑢) ∧ (normCV𝑤) ⊆ (normCV𝑢))}
212, 3, 20cmpt 5107 . 2 class (𝑢 ∈ NrmCVec ↦ {𝑤 ∈ NrmCVec ∣ (( +𝑣𝑤) ⊆ ( +𝑣𝑢) ∧ ( ·𝑠OLD𝑤) ⊆ ( ·𝑠OLD𝑢) ∧ (normCV𝑤) ⊆ (normCV𝑢))})
221, 21wceq 1542 1 wff SubSp = (𝑢 ∈ NrmCVec ↦ {𝑤 ∈ NrmCVec ∣ (( +𝑣𝑤) ⊆ ( +𝑣𝑢) ∧ ( ·𝑠OLD𝑤) ⊆ ( ·𝑠OLD𝑢) ∧ (normCV𝑤) ⊆ (normCV𝑢))})
Colors of variables: wff setvar class
This definition is referenced by:  sspval  28650
  Copyright terms: Public domain W3C validator