This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) }