Definition 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 = { ⟨ ⟨ 𝑔 , 𝑠 ⟩ , 𝑛 ⟩ ∣ ( ⟨ 𝑔 , 𝑠 ⟩ ∈ CVecOLD ∧ 𝑛 : ran 𝑔 ⟶ ℝ ∧ ∀ 𝑥 ∈ ran 𝑔 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnv	⊢ NrmCVec
1		vg	⊢ 𝑔
2		vs	⊢ 𝑠
3		vn	⊢ 𝑛
4	1	cv	⊢ 𝑔
5	2	cv	⊢ 𝑠
6	4 5	cop	⊢ ⟨ 𝑔 , 𝑠 ⟩
7		cvc	⊢ CVecOLD
8	6 7	wcel	⊢ ⟨ 𝑔 , 𝑠 ⟩ ∈ CVecOLD
9	3	cv	⊢ 𝑛
10	4	crn	⊢ ran 𝑔
11		cr	⊢ ℝ
12	10 11 9	wf	⊢ 𝑛 : ran 𝑔 ⟶ ℝ
13		vx	⊢ 𝑥
14	13	cv	⊢ 𝑥
15	14 9	cfv	⊢ ( 𝑛 ‘ 𝑥 )
16		cc0	⊢ 0
17	15 16	wceq	⊢ ( 𝑛 ‘ 𝑥 ) = 0
18		cgi	⊢ GId
19	4 18	cfv	⊢ ( GId ‘ 𝑔 )
20	14 19	wceq	⊢ 𝑥 = ( GId ‘ 𝑔 )
21	17 20	wi	⊢ ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) )
22		vy	⊢ 𝑦
23		cc	⊢ ℂ
24	22	cv	⊢ 𝑦
25	24 14 5	co	⊢ ( 𝑦 𝑠 𝑥 )
26	25 9	cfv	⊢ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) )
27		cabs	⊢ abs
28	24 27	cfv	⊢ ( abs ‘ 𝑦 )
29		cmul	⊢ ·
30	28 15 29	co	⊢ ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) )
31	26 30	wceq	⊢ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) )
32	31 22 23	wral	⊢ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) )
33	14 24 4	co	⊢ ( 𝑥 𝑔 𝑦 )
34	33 9	cfv	⊢ ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) )
35		cle	⊢ ≤
36		caddc	⊢ +
37	24 9	cfv	⊢ ( 𝑛 ‘ 𝑦 )
38	15 37 36	co	⊢ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) )
39	34 38 35	wbr	⊢ ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) )
40	39 22 10	wral	⊢ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) )
41	21 32 40	w3a	⊢ ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) )
42	41 13 10	wral	⊢ ∀ 𝑥 ∈ ran 𝑔 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) )
43	8 12 42	w3a	⊢ ( ⟨ 𝑔 , 𝑠 ⟩ ∈ CVecOLD ∧ 𝑛 : ran 𝑔 ⟶ ℝ ∧ ∀ 𝑥 ∈ ran 𝑔 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) )
44	43 1 2 3	coprab	⊢ { ⟨ ⟨ 𝑔 , 𝑠 ⟩ , 𝑛 ⟩ ∣ ( ⟨ 𝑔 , 𝑠 ⟩ ∈ CVecOLD ∧ 𝑛 : ran 𝑔 ⟶ ℝ ∧ ∀ 𝑥 ∈ ran 𝑔 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) }
45	0 44	wceq	⊢ NrmCVec = { ⟨ ⟨ 𝑔 , 𝑠 ⟩ , 𝑛 ⟩ ∣ ( ⟨ 𝑔 , 𝑠 ⟩ ∈ CVecOLD ∧ 𝑛 : ran 𝑔 ⟶ ℝ ∧ ∀ 𝑥 ∈ ran 𝑔 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) }