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

Definition df-nv 26831
Description: Define the class of all normed complex vector spaces. (Contributed by NM, 11-Nov-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-nv NrmCVec = {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ (⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))}
Distinct variable group:   𝑔,𝑠,𝑛,𝑥,𝑦

Detailed syntax breakdown of Definition df-nv
StepHypRef Expression
1 cnv 26823 . 2 class NrmCVec
2 vg . . . . . . 7 setvar 𝑔
32cv 1474 . . . . . 6 class 𝑔
4 vs . . . . . . 7 setvar 𝑠
54cv 1474 . . . . . 6 class 𝑠
63, 5cop 4131 . . . . 5 class 𝑔, 𝑠
7 cvc 26797 . . . . 5 class CVecOLD
86, 7wcel 1977 . . . 4 wff 𝑔, 𝑠⟩ ∈ CVecOLD
93crn 5039 . . . . 5 class ran 𝑔
10 cr 9814 . . . . 5 class
11 vn . . . . . 6 setvar 𝑛
1211cv 1474 . . . . 5 class 𝑛
139, 10, 12wf 5800 . . . 4 wff 𝑛:ran 𝑔⟶ℝ
14 vx . . . . . . . . . 10 setvar 𝑥
1514cv 1474 . . . . . . . . 9 class 𝑥
1615, 12cfv 5804 . . . . . . . 8 class (𝑛𝑥)
17 cc0 9815 . . . . . . . 8 class 0
1816, 17wceq 1475 . . . . . . 7 wff (𝑛𝑥) = 0
19 cgi 26728 . . . . . . . . 9 class GId
203, 19cfv 5804 . . . . . . . 8 class (GId‘𝑔)
2115, 20wceq 1475 . . . . . . 7 wff 𝑥 = (GId‘𝑔)
2218, 21wi 4 . . . . . 6 wff ((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔))
23 vy . . . . . . . . . . 11 setvar 𝑦
2423cv 1474 . . . . . . . . . 10 class 𝑦
2524, 15, 5co 6549 . . . . . . . . 9 class (𝑦𝑠𝑥)
2625, 12cfv 5804 . . . . . . . 8 class (𝑛‘(𝑦𝑠𝑥))
27 cabs 13822 . . . . . . . . . 10 class abs
2824, 27cfv 5804 . . . . . . . . 9 class (abs‘𝑦)
29 cmul 9820 . . . . . . . . 9 class ·
3028, 16, 29co 6549 . . . . . . . 8 class ((abs‘𝑦) · (𝑛𝑥))
3126, 30wceq 1475 . . . . . . 7 wff (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥))
32 cc 9813 . . . . . . 7 class
3331, 23, 32wral 2896 . . . . . 6 wff 𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥))
3415, 24, 3co 6549 . . . . . . . . 9 class (𝑥𝑔𝑦)
3534, 12cfv 5804 . . . . . . . 8 class (𝑛‘(𝑥𝑔𝑦))
3624, 12cfv 5804 . . . . . . . . 9 class (𝑛𝑦)
37 caddc 9818 . . . . . . . . 9 class +
3816, 36, 37co 6549 . . . . . . . 8 class ((𝑛𝑥) + (𝑛𝑦))
39 cle 9954 . . . . . . . 8 class
4035, 38, 39wbr 4583 . . . . . . 7 wff (𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))
4140, 23, 9wral 2896 . . . . . 6 wff 𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))
4222, 33, 41w3a 1031 . . . . 5 wff (((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))
4342, 14, 9wral 2896 . . . 4 wff 𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))
448, 13, 43w3a 1031 . . 3 wff (⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))
4544, 2, 4, 11coprab 6550 . 2 class {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ (⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))}
461, 45wceq 1475 1 wff NrmCVec = {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ (⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))}
Colors of variables: wff setvar class
This definition is referenced by:  nvss  26832  isnvlem  26849
  Copyright terms: Public domain W3C validator