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 = { <. <. g , s >. , n >. | ( <. g , s >. e. CVecOLD /\ n : ran g --> RR /\ A. x e. ran g ( ( ( n ` x ) = 0 -> x = ( GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnv 
 |-  NrmCVec
1 vg 
 |-  g
2 vs 
 |-  s
3 vn 
 |-  n
4 1 cv 
 |-  g
5 2 cv 
 |-  s
6 4 5 cop 
 |-  <. g , s >.
7 cvc 
 |-  CVecOLD
8 6 7 wcel 
 |-  <. g , s >. e. CVecOLD
9 3 cv 
 |-  n
10 4 crn 
 |-  ran g
11 cr 
 |-  RR
12 10 11 9 wf 
 |-  n : ran g --> RR
13 vx 
 |-  x
14 13 cv 
 |-  x
15 14 9 cfv 
 |-  ( n ` x )
16 cc0 
 |-  0
17 15 16 wceq 
 |-  ( n ` x ) = 0
18 cgi 
 |-  GId
19 4 18 cfv 
 |-  ( GId ` g )
20 14 19 wceq 
 |-  x = ( GId ` g )
21 17 20 wi 
 |-  ( ( n ` x ) = 0 -> x = ( GId ` g ) )
22 vy 
 |-  y
23 cc 
 |-  CC
24 22 cv 
 |-  y
25 24 14 5 co 
 |-  ( y s x )
26 25 9 cfv 
 |-  ( n ` ( y s x ) )
27 cabs 
 |-  abs
28 24 27 cfv 
 |-  ( abs ` y )
29 cmul 
 |-  x.
30 28 15 29 co 
 |-  ( ( abs ` y ) x. ( n ` x ) )
31 26 30 wceq 
 |-  ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) )
32 31 22 23 wral 
 |-  A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) )
33 14 24 4 co 
 |-  ( x g y )
34 33 9 cfv 
 |-  ( n ` ( x g y ) )
35 cle 
 |-  <_
36 caddc 
 |-  +
37 24 9 cfv 
 |-  ( n ` y )
38 15 37 36 co 
 |-  ( ( n ` x ) + ( n ` y ) )
39 34 38 35 wbr 
 |-  ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) )
40 39 22 10 wral 
 |-  A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) )
41 21 32 40 w3a 
 |-  ( ( ( n ` x ) = 0 -> x = ( GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) )
42 41 13 10 wral 
 |-  A. x e. ran g ( ( ( n ` x ) = 0 -> x = ( GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) )
43 8 12 42 w3a 
 |-  ( <. g , s >. e. CVecOLD /\ n : ran g --> RR /\ A. x e. ran g ( ( ( n ` x ) = 0 -> x = ( GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) )
44 43 1 2 3 coprab 
 |-  { <. <. g , s >. , n >. | ( <. g , s >. e. CVecOLD /\ n : ran g --> RR /\ A. x e. ran g ( ( ( n ` x ) = 0 -> x = ( GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) }
45 0 44 wceq 
 |-  NrmCVec = { <. <. g , s >. , n >. | ( <. g , s >. e. CVecOLD /\ n : ran g --> RR /\ A. x e. ran g ( ( ( n ` x ) = 0 -> x = ( GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) }