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