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 28519
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 28511 . 2 class NrmCVec
2 vg . . . . . . 7 setvar 𝑔
32cv 1541 . . . . . 6 class 𝑔
4 vs . . . . . . 7 setvar 𝑠
54cv 1541 . . . . . 6 class 𝑠
63, 5cop 4519 . . . . 5 class 𝑔, 𝑠
7 cvc 28485 . . . . 5 class CVecOLD
86, 7wcel 2113 . . . 4 wff 𝑔, 𝑠⟩ ∈ CVecOLD
93crn 5520 . . . . 5 class ran 𝑔
10 cr 10607 . . . . 5 class
11 vn . . . . . 6 setvar 𝑛
1211cv 1541 . . . . 5 class 𝑛
139, 10, 12wf 6329 . . . 4 wff 𝑛:ran 𝑔⟶ℝ
14 vx . . . . . . . . . 10 setvar 𝑥
1514cv 1541 . . . . . . . . 9 class 𝑥
1615, 12cfv 6333 . . . . . . . 8 class (𝑛𝑥)
17 cc0 10608 . . . . . . . 8 class 0
1816, 17wceq 1542 . . . . . . 7 wff (𝑛𝑥) = 0
19 cgi 28417 . . . . . . . . 9 class GId
203, 19cfv 6333 . . . . . . . 8 class (GId‘𝑔)
2115, 20wceq 1542 . . . . . . 7 wff 𝑥 = (GId‘𝑔)
2218, 21wi 4 . . . . . 6 wff ((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔))
23 vy . . . . . . . . . . 11 setvar 𝑦
2423cv 1541 . . . . . . . . . 10 class 𝑦
2524, 15, 5co 7164 . . . . . . . . 9 class (𝑦𝑠𝑥)
2625, 12cfv 6333 . . . . . . . 8 class (𝑛‘(𝑦𝑠𝑥))
27 cabs 14676 . . . . . . . . . 10 class abs
2824, 27cfv 6333 . . . . . . . . 9 class (abs‘𝑦)
29 cmul 10613 . . . . . . . . 9 class ·
3028, 16, 29co 7164 . . . . . . . 8 class ((abs‘𝑦) · (𝑛𝑥))
3126, 30wceq 1542 . . . . . . 7 wff (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥))
32 cc 10606 . . . . . . 7 class
3331, 23, 32wral 3053 . . . . . 6 wff 𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥))
3415, 24, 3co 7164 . . . . . . . . 9 class (𝑥𝑔𝑦)
3534, 12cfv 6333 . . . . . . . 8 class (𝑛‘(𝑥𝑔𝑦))
3624, 12cfv 6333 . . . . . . . . 9 class (𝑛𝑦)
37 caddc 10611 . . . . . . . . 9 class +
3816, 36, 37co 7164 . . . . . . . 8 class ((𝑛𝑥) + (𝑛𝑦))
39 cle 10747 . . . . . . . 8 class
4035, 38, 39wbr 5027 . . . . . . 7 wff (𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))
4140, 23, 9wral 3053 . . . . . 6 wff 𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))
4222, 33, 41w3a 1088 . . . . 5 wff (((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))
4342, 14, 9wral 3053 . . . 4 wff 𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))
448, 13, 43w3a 1088 . . 3 wff (⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))
4544, 2, 4, 11coprab 7165 . 2 class {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ (⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))}
461, 45wceq 1542 1 wff NrmCVec = {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ (⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))}
Colors of variables: wff setvar class
This definition is referenced by:  nvss  28520  isnvlem  28537
  Copyright terms: Public domain W3C validator