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

Definition df-nv 22071
 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 22063 . 2
2 vg . . . . . . 7
32cv 1651 . . . . . 6
4 vs . . . . . . 7
54cv 1651 . . . . . 6
63, 5cop 3817 . . . . 5
7 cvc 22024 . . . . 5
86, 7wcel 1725 . . . 4
93crn 4879 . . . . 5
10 cr 8989 . . . . 5
11 vn . . . . . 6
1211cv 1651 . . . . 5
139, 10, 12wf 5450 . . . 4
14 vx . . . . . . . . . 10
1514cv 1651 . . . . . . . . 9
1615, 12cfv 5454 . . . . . . . 8
17 cc0 8990 . . . . . . . 8
1816, 17wceq 1652 . . . . . . 7
19 cgi 21775 . . . . . . . . 9 GId
203, 19cfv 5454 . . . . . . . 8 GId
2115, 20wceq 1652 . . . . . . 7 GId
2218, 21wi 4 . . . . . 6 GId
23 vy . . . . . . . . . . 11
2423cv 1651 . . . . . . . . . 10
2524, 15, 5co 6081 . . . . . . . . 9
2625, 12cfv 5454 . . . . . . . 8
27 cabs 12039 . . . . . . . . . 10
2824, 27cfv 5454 . . . . . . . . 9
29 cmul 8995 . . . . . . . . 9
3028, 16, 29co 6081 . . . . . . . 8
3126, 30wceq 1652 . . . . . . 7
32 cc 8988 . . . . . . 7
3331, 23, 32wral 2705 . . . . . 6
3415, 24, 3co 6081 . . . . . . . . 9
3534, 12cfv 5454 . . . . . . . 8
3624, 12cfv 5454 . . . . . . . . 9
37 caddc 8993 . . . . . . . . 9
3816, 36, 37co 6081 . . . . . . . 8
39 cle 9121 . . . . . . . 8
4035, 38, 39wbr 4212 . . . . . . 7
4140, 23, 9wral 2705 . . . . . 6
4222, 33, 41w3a 936 . . . . 5 GId
4342, 14, 9wral 2705 . . . 4 GId
448, 13, 43w3a 936 . . 3 GId
4544, 2, 4, 11coprab 6082 . 2 GId
461, 45wceq 1652 1 GId
 Colors of variables: wff set class This definition is referenced by:  nvss  22072  isnvlem  22089
 Copyright terms: Public domain W3C validator