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

Definition df-nv 27575
 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 27567 . 2 class NrmCVec
2 vg . . . . . . 7 setvar 𝑔
32cv 1522 . . . . . 6 class 𝑔
4 vs . . . . . . 7 setvar 𝑠
54cv 1522 . . . . . 6 class 𝑠
63, 5cop 4216 . . . . 5 class 𝑔, 𝑠
7 cvc 27541 . . . . 5 class CVecOLD
86, 7wcel 2030 . . . 4 wff 𝑔, 𝑠⟩ ∈ CVecOLD
93crn 5144 . . . . 5 class ran 𝑔
10 cr 9973 . . . . 5 class
11 vn . . . . . 6 setvar 𝑛
1211cv 1522 . . . . 5 class 𝑛
139, 10, 12wf 5922 . . . 4 wff 𝑛:ran 𝑔⟶ℝ
14 vx . . . . . . . . . 10 setvar 𝑥
1514cv 1522 . . . . . . . . 9 class 𝑥
1615, 12cfv 5926 . . . . . . . 8 class (𝑛𝑥)
17 cc0 9974 . . . . . . . 8 class 0
1816, 17wceq 1523 . . . . . . 7 wff (𝑛𝑥) = 0
19 cgi 27472 . . . . . . . . 9 class GId
203, 19cfv 5926 . . . . . . . 8 class (GId‘𝑔)
2115, 20wceq 1523 . . . . . . 7 wff 𝑥 = (GId‘𝑔)
2218, 21wi 4 . . . . . 6 wff ((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔))
23 vy . . . . . . . . . . 11 setvar 𝑦
2423cv 1522 . . . . . . . . . 10 class 𝑦
2524, 15, 5co 6690 . . . . . . . . 9 class (𝑦𝑠𝑥)
2625, 12cfv 5926 . . . . . . . 8 class (𝑛‘(𝑦𝑠𝑥))
27 cabs 14018 . . . . . . . . . 10 class abs
2824, 27cfv 5926 . . . . . . . . 9 class (abs‘𝑦)
29 cmul 9979 . . . . . . . . 9 class ·
3028, 16, 29co 6690 . . . . . . . 8 class ((abs‘𝑦) · (𝑛𝑥))
3126, 30wceq 1523 . . . . . . 7 wff (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥))
32 cc 9972 . . . . . . 7 class
3331, 23, 32wral 2941 . . . . . 6 wff 𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥))
3415, 24, 3co 6690 . . . . . . . . 9 class (𝑥𝑔𝑦)
3534, 12cfv 5926 . . . . . . . 8 class (𝑛‘(𝑥𝑔𝑦))
3624, 12cfv 5926 . . . . . . . . 9 class (𝑛𝑦)
37 caddc 9977 . . . . . . . . 9 class +
3816, 36, 37co 6690 . . . . . . . 8 class ((𝑛𝑥) + (𝑛𝑦))
39 cle 10113 . . . . . . . 8 class
4035, 38, 39wbr 4685 . . . . . . 7 wff (𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))
4140, 23, 9wral 2941 . . . . . 6 wff 𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))
4222, 33, 41w3a 1054 . . . . 5 wff (((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))
4342, 14, 9wral 2941 . . . 4 wff 𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))
448, 13, 43w3a 1054 . . 3 wff (⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))
4544, 2, 4, 11coprab 6691 . 2 class {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ (⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))}
461, 45wceq 1523 1 wff NrmCVec = {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ (⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))}
 Colors of variables: wff setvar class This definition is referenced by:  nvss  27576  isnvlem  27593
 Copyright terms: Public domain W3C validator