df-nv

Description: Define the class of all normed complex vector spaces. (Contributed by NM, 11-Nov-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	df-nv	$⊢ NrmCVec = \{⟨⟨g, s⟩, n⟩ \| (⟨g, s⟩ \in {CVec}_{OLD} \land n : ran g ⟶ ℝ \land \forall x \in ran g ((n (x) = 0 \to x = GId (g)) \land \forall y \in ℂ n (y s x) = \|y\| n (x) \land \forall y \in ran g n (x g y) \leq n (x) + n (y)))\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnv	$class NrmCVec$
1		vg	$setvar g$
2		vs	$setvar s$
3		vn	$setvar n$
4	1	cv	$setvar g$
5	2	cv	$setvar s$
6	4 5	cop	$class ⟨g, s⟩$
7		cvc	$class {CVec}_{OLD}$
8	6 7	wcel	$wff ⟨g, s⟩ \in {CVec}_{OLD}$
9	3	cv	$setvar n$
10	4	crn	$class ran g$
11		cr	$class ℝ$
12	10 11 9	wf	$wff n : ran g ⟶ ℝ$
13		vx	$setvar x$
14	13	cv	$setvar x$
15	14 9	cfv	$class n (x)$
16		cc0	$class 0$
17	15 16	wceq	$wff n (x) = 0$
18		cgi	$class GId$
19	4 18	cfv	$class GId (g)$
20	14 19	wceq	$wff x = GId (g)$
21	17 20	wi	$wff (n (x) = 0 \to x = GId (g))$
22		vy	$setvar y$
23		cc	$class ℂ$
24	22	cv	$setvar y$
25	24 14 5	co	$class (y s x)$
26	25 9	cfv	$class n (y s x)$
27		cabs	$class abs$
28	24 27	cfv	$class \|y\|$
29		cmul	$class \times$
30	28 15 29	co	$class \|y\| n (x)$
31	26 30	wceq	$wff n (y s x) = \|y\| n (x)$
32	31 22 23	wral	$wff \forall y \in ℂ n (y s x) = \|y\| n (x)$
33	14 24 4	co	$class (x g y)$
34	33 9	cfv	$class n (x g y)$
35		cle	$class \leq$
36		caddc	$class +$
37	24 9	cfv	$class n (y)$
38	15 37 36	co	$class (n (x) + n (y))$
39	34 38 35	wbr	$wff n (x g y) \leq n (x) + n (y)$
40	39 22 10	wral	$wff \forall y \in ran g n (x g y) \leq n (x) + n (y)$
41	21 32 40	w3a	$wff ((n (x) = 0 \to x = GId (g)) \land \forall y \in ℂ n (y s x) = \|y\| n (x) \land \forall y \in ran g n (x g y) \leq n (x) + n (y))$
42	41 13 10	wral	$wff \forall x \in ran g ((n (x) = 0 \to x = GId (g)) \land \forall y \in ℂ n (y s x) = \|y\| n (x) \land \forall y \in ran g n (x g y) \leq n (x) + n (y))$
43	8 12 42	w3a	$wff (⟨g, s⟩ \in {CVec}_{OLD} \land n : ran g ⟶ ℝ \land \forall x \in ran g ((n (x) = 0 \to x = GId (g)) \land \forall y \in ℂ n (y s x) = \|y\| n (x) \land \forall y \in ran g n (x g y) \leq n (x) + n (y)))$
44	43 1 2 3	coprab	$class \{⟨⟨g, s⟩, n⟩ \| (⟨g, s⟩ \in {CVec}_{OLD} \land n : ran g ⟶ ℝ \land \forall x \in ran g ((n (x) = 0 \to x = GId (g)) \land \forall y \in ℂ n (y s x) = \|y\| n (x) \land \forall y \in ran g n (x g y) \leq n (x) + n (y)))\}$
45	0 44	wceq	$wff NrmCVec = \{⟨⟨g, s⟩, n⟩ \| (⟨g, s⟩ \in {CVec}_{OLD} \land n : ran g ⟶ ℝ \land \forall x \in ran g ((n (x) = 0 \to x = GId (g)) \land \forall y \in ℂ n (y s x) = \|y\| n (x) \land \forall y \in ran g n (x g y) \leq n (x) + n (y)))\}$

Metamath Proof Explorer

Definition df-nv

Detailed syntax breakdown