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 ) ) ) ) }