Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-nv Unicode version

Definition df-nv 22024
 Description: Define the class of all normed complex vector spaces. (Contributed by NM, 11-Nov-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-nv GId
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-nv
StepHypRef Expression
1 cnv 22016 . 2
2 vg . . . . . . 7
32cv 1648 . . . . . 6
4 vs . . . . . . 7
54cv 1648 . . . . . 6
63, 5cop 3777 . . . . 5
7 cvc 21977 . . . . 5
86, 7wcel 1721 . . . 4
93crn 4838 . . . . 5
10 cr 8945 . . . . 5
11 vn . . . . . 6
1211cv 1648 . . . . 5
139, 10, 12wf 5409 . . . 4
14 vx . . . . . . . . . 10
1514cv 1648 . . . . . . . . 9
1615, 12cfv 5413 . . . . . . . 8
17 cc0 8946 . . . . . . . 8
1816, 17wceq 1649 . . . . . . 7
19 cgi 21728 . . . . . . . . 9 GId
203, 19cfv 5413 . . . . . . . 8 GId
2115, 20wceq 1649 . . . . . . 7 GId
2218, 21wi 4 . . . . . 6 GId
23 vy . . . . . . . . . . 11
2423cv 1648 . . . . . . . . . 10
2524, 15, 5co 6040 . . . . . . . . 9
2625, 12cfv 5413 . . . . . . . 8
27 cabs 11994 . . . . . . . . . 10
2824, 27cfv 5413 . . . . . . . . 9
29 cmul 8951 . . . . . . . . 9
3028, 16, 29co 6040 . . . . . . . 8
3126, 30wceq 1649 . . . . . . 7
32 cc 8944 . . . . . . 7
3331, 23, 32wral 2666 . . . . . 6
3415, 24, 3co 6040 . . . . . . . . 9
3534, 12cfv 5413 . . . . . . . 8
3624, 12cfv 5413 . . . . . . . . 9
37 caddc 8949 . . . . . . . . 9
3816, 36, 37co 6040 . . . . . . . 8
39 cle 9077 . . . . . . . 8
4035, 38, 39wbr 4172 . . . . . . 7
4140, 23, 9wral 2666 . . . . . 6
4222, 33, 41w3a 936 . . . . 5 GId
4342, 14, 9wral 2666 . . . 4 GId
448, 13, 43w3a 936 . . 3 GId
4544, 2, 4, 11coprab 6041 . 2 GId
461, 45wceq 1649 1 GId
 Colors of variables: wff set class This definition is referenced by:  nvss  22025  isnvlem  22042
 Copyright terms: Public domain W3C validator