Definition df-nv 28369

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

Step	Hyp	Ref	Expression
1		cnv 28361	. 2 class NrmCVec
2		vg	. . . . . . 7 setvar 𝑔
3	2	cv 1536	. . . . . 6 class 𝑔
4		vs	. . . . . . 7 setvar 𝑠
5	4	cv 1536	. . . . . 6 class 𝑠
6	3, 5	cop 4573	. . . . 5 class ⟨𝑔, 𝑠⟩
7		cvc 28335	. . . . 5 class CVecOLD
8	6, 7	wcel 2114	. . . 4 wff ⟨𝑔, 𝑠⟩ ∈ CVecOLD
9	3	crn 5556	. . . . 5 class ran 𝑔
10		cr 10536	. . . . 5 class ℝ
11		vn	. . . . . 6 setvar 𝑛
12	11	cv 1536	. . . . 5 class 𝑛
13	9, 10, 12	wf 6351	. . . 4 wff 𝑛:ran 𝑔⟶ℝ
14		vx	. . . . . . . . . 10 setvar 𝑥
15	14	cv 1536	. . . . . . . . 9 class 𝑥
16	15, 12	cfv 6355	. . . . . . . 8 class (𝑛‘𝑥)
17		cc0 10537	. . . . . . . 8 class 0
18	16, 17	wceq 1537	. . . . . . 7 wff (𝑛‘𝑥) = 0
19		cgi 28267	. . . . . . . . 9 class GId
20	3, 19	cfv 6355	. . . . . . . 8 class (GId‘𝑔)
21	15, 20	wceq 1537	. . . . . . 7 wff 𝑥 = (GId‘𝑔)
22	18, 21	wi 4	. . . . . 6 wff ((𝑛‘𝑥) = 0 → 𝑥 = (GId‘𝑔))
23		vy	. . . . . . . . . . 11 setvar 𝑦
24	23	cv 1536	. . . . . . . . . 10 class 𝑦
25	24, 15, 5	co 7156	. . . . . . . . 9 class (𝑦𝑠𝑥)
26	25, 12	cfv 6355	. . . . . . . 8 class (𝑛‘(𝑦𝑠𝑥))
27		cabs 14593	. . . . . . . . . 10 class abs
28	24, 27	cfv 6355	. . . . . . . . 9 class (abs‘𝑦)
29		cmul 10542	. . . . . . . . 9 class ·
30	28, 16, 29	co 7156	. . . . . . . 8 class ((abs‘𝑦) · (𝑛‘𝑥))
31	26, 30	wceq 1537	. . . . . . 7 wff (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛‘𝑥))
32		cc 10535	. . . . . . 7 class ℂ
33	31, 23, 32	wral 3138	. . . . . 6 wff ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛‘𝑥))
34	15, 24, 3	co 7156	. . . . . . . . 9 class (𝑥𝑔𝑦)
35	34, 12	cfv 6355	. . . . . . . 8 class (𝑛‘(𝑥𝑔𝑦))
36	24, 12	cfv 6355	. . . . . . . . 9 class (𝑛‘𝑦)
37		caddc 10540	. . . . . . . . 9 class +
38	16, 36, 37	co 7156	. . . . . . . 8 class ((𝑛‘𝑥) + (𝑛‘𝑦))
39		cle 10676	. . . . . . . 8 class ≤
40	35, 38, 39	wbr 5066	. . . . . . 7 wff (𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛‘𝑥) + (𝑛‘𝑦))
41	40, 23, 9	wral 3138	. . . . . 6 wff ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛‘𝑥) + (𝑛‘𝑦))
42	22, 33, 41	w3a 1083	. . . . 5 wff (((𝑛‘𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛‘𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛‘𝑥) + (𝑛‘𝑦)))
43	42, 14, 9	wral 3138	. . . 4 wff ∀𝑥 ∈ ran 𝑔(((𝑛‘𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛‘𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛‘𝑥) + (𝑛‘𝑦)))
44	8, 13, 43	w3a 1083	. . 3 wff (⟨𝑔, 𝑠⟩ ∈ CVecOLD ∧ 𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛‘𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛‘𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛‘𝑥) + (𝑛‘𝑦))))
45	44, 2, 4, 11	coprab 7157	. 2 class {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ (⟨𝑔, 𝑠⟩ ∈ CVecOLD ∧ 𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛‘𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛‘𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛‘𝑥) + (𝑛‘𝑦))))}
46	1, 45	wceq 1537	1 wff NrmCVec = {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ (⟨𝑔, 𝑠⟩ ∈ CVecOLD ∧ 𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛‘𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛‘𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛‘𝑥) + (𝑛‘𝑦))))}

This definition is referenced by:  nvss  28370  isnvlem  28387