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

Definition df-vc 21102
Description: Define the class of all complex vector spaces. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-vc  |-  CVec OLD  =  { <. g ,  s
>.  |  ( g  e.  AbelOp  /\  s :
( CC  X.  ran  g ) --> ran  g  /\  A. x  e.  ran  g ( ( 1 s x )  =  x  /\  A. y  e.  CC  ( A. z  e.  ran  g ( y s ( x g z ) )  =  ( ( y s x ) g ( y s z ) )  /\  A. z  e.  CC  ( ( ( y  +  z ) s x )  =  ( ( y s x ) g ( z s x ) )  /\  ( ( y  x.  z ) s x )  =  ( y s ( z s x ) ) ) ) ) ) }
Distinct variable group:    g, s, x, y, z

Detailed syntax breakdown of Definition df-vc
StepHypRef Expression
1 cvc 21101 . 2  class  CVec OLD
2 vg . . . . . 6  set  g
32cv 1622 . . . . 5  class  g
4 cablo 20948 . . . . 5  class  AbelOp
53, 4wcel 1684 . . . 4  wff  g  e. 
AbelOp
6 cc 8735 . . . . . 6  class  CC
73crn 4690 . . . . . 6  class  ran  g
86, 7cxp 4687 . . . . 5  class  ( CC 
X.  ran  g )
9 vs . . . . . 6  set  s
109cv 1622 . . . . 5  class  s
118, 7, 10wf 5251 . . . 4  wff  s : ( CC  X.  ran  g ) --> ran  g
12 c1 8738 . . . . . . . 8  class  1
13 vx . . . . . . . . 9  set  x
1413cv 1622 . . . . . . . 8  class  x
1512, 14, 10co 5858 . . . . . . 7  class  ( 1 s x )
1615, 14wceq 1623 . . . . . 6  wff  ( 1 s x )  =  x
17 vy . . . . . . . . . . . 12  set  y
1817cv 1622 . . . . . . . . . . 11  class  y
19 vz . . . . . . . . . . . . 13  set  z
2019cv 1622 . . . . . . . . . . . 12  class  z
2114, 20, 3co 5858 . . . . . . . . . . 11  class  ( x g z )
2218, 21, 10co 5858 . . . . . . . . . 10  class  ( y s ( x g z ) )
2318, 14, 10co 5858 . . . . . . . . . . 11  class  ( y s x )
2418, 20, 10co 5858 . . . . . . . . . . 11  class  ( y s z )
2523, 24, 3co 5858 . . . . . . . . . 10  class  ( ( y s x ) g ( y s z ) )
2622, 25wceq 1623 . . . . . . . . 9  wff  ( y s ( x g z ) )  =  ( ( y s x ) g ( y s z ) )
2726, 19, 7wral 2543 . . . . . . . 8  wff  A. z  e.  ran  g ( y s ( x g z ) )  =  ( ( y s x ) g ( y s z ) )
28 caddc 8740 . . . . . . . . . . . . 13  class  +
2918, 20, 28co 5858 . . . . . . . . . . . 12  class  ( y  +  z )
3029, 14, 10co 5858 . . . . . . . . . . 11  class  ( ( y  +  z ) s x )
3120, 14, 10co 5858 . . . . . . . . . . . 12  class  ( z s x )
3223, 31, 3co 5858 . . . . . . . . . . 11  class  ( ( y s x ) g ( z s x ) )
3330, 32wceq 1623 . . . . . . . . . 10  wff  ( ( y  +  z ) s x )  =  ( ( y s x ) g ( z s x ) )
34 cmul 8742 . . . . . . . . . . . . 13  class  x.
3518, 20, 34co 5858 . . . . . . . . . . . 12  class  ( y  x.  z )
3635, 14, 10co 5858 . . . . . . . . . . 11  class  ( ( y  x.  z ) s x )
3718, 31, 10co 5858 . . . . . . . . . . 11  class  ( y s ( z s x ) )
3836, 37wceq 1623 . . . . . . . . . 10  wff  ( ( y  x.  z ) s x )  =  ( y s ( z s x ) )
3933, 38wa 358 . . . . . . . . 9  wff  ( ( ( y  +  z ) s x )  =  ( ( y s x ) g ( z s x ) )  /\  (
( y  x.  z
) s x )  =  ( y s ( z s x ) ) )
4039, 19, 6wral 2543 . . . . . . . 8  wff  A. z  e.  CC  ( ( ( y  +  z ) s x )  =  ( ( y s x ) g ( z s x ) )  /\  ( ( y  x.  z ) s x )  =  ( y s ( z s x ) ) )
4127, 40wa 358 . . . . . . 7  wff  ( A. z  e.  ran  g ( y s ( x g z ) )  =  ( ( y s x ) g ( y s z ) )  /\  A. z  e.  CC  (
( ( y  +  z ) s x )  =  ( ( y s x ) g ( z s x ) )  /\  ( ( y  x.  z ) s x )  =  ( y s ( z s x ) ) ) )
4241, 17, 6wral 2543 . . . . . 6  wff  A. y  e.  CC  ( A. z  e.  ran  g ( y s ( x g z ) )  =  ( ( y s x ) g ( y s z ) )  /\  A. z  e.  CC  ( ( ( y  +  z ) s x )  =  ( ( y s x ) g ( z s x ) )  /\  ( ( y  x.  z ) s x )  =  ( y s ( z s x ) ) ) )
4316, 42wa 358 . . . . 5  wff  ( ( 1 s x )  =  x  /\  A. y  e.  CC  ( A. z  e.  ran  g ( y s ( x g z ) )  =  ( ( y s x ) g ( y s z ) )  /\  A. z  e.  CC  ( ( ( y  +  z ) s x )  =  ( ( y s x ) g ( z s x ) )  /\  ( ( y  x.  z ) s x )  =  ( y s ( z s x ) ) ) ) )
4443, 13, 7wral 2543 . . . 4  wff  A. x  e.  ran  g ( ( 1 s x )  =  x  /\  A. y  e.  CC  ( A. z  e.  ran  g ( y s ( x g z ) )  =  ( ( y s x ) g ( y s z ) )  /\  A. z  e.  CC  ( ( ( y  +  z ) s x )  =  ( ( y s x ) g ( z s x ) )  /\  ( ( y  x.  z ) s x )  =  ( y s ( z s x ) ) ) ) )
455, 11, 44w3a 934 . . 3  wff  ( g  e.  AbelOp  /\  s :
( CC  X.  ran  g ) --> ran  g  /\  A. x  e.  ran  g ( ( 1 s x )  =  x  /\  A. y  e.  CC  ( A. z  e.  ran  g ( y s ( x g z ) )  =  ( ( y s x ) g ( y s z ) )  /\  A. z  e.  CC  ( ( ( y  +  z ) s x )  =  ( ( y s x ) g ( z s x ) )  /\  ( ( y  x.  z ) s x )  =  ( y s ( z s x ) ) ) ) ) )
4645, 2, 9copab 4076 . 2  class  { <. g ,  s >.  |  ( g  e.  AbelOp  /\  s : ( CC  X.  ran  g ) --> ran  g  /\  A. x  e.  ran  g ( ( 1 s x )  =  x  /\  A. y  e.  CC  ( A. z  e.  ran  g ( y s ( x g z ) )  =  ( ( y s x ) g ( y s z ) )  /\  A. z  e.  CC  ( ( ( y  +  z ) s x )  =  ( ( y s x ) g ( z s x ) )  /\  ( ( y  x.  z ) s x )  =  ( y s ( z s x ) ) ) ) ) ) }
471, 46wceq 1623 1  wff  CVec OLD  =  { <. g ,  s
>.  |  ( g  e.  AbelOp  /\  s :
( CC  X.  ran  g ) --> ran  g  /\  A. x  e.  ran  g ( ( 1 s x )  =  x  /\  A. y  e.  CC  ( A. z  e.  ran  g ( y s ( x g z ) )  =  ( ( y s x ) g ( y s z ) )  /\  A. z  e.  CC  ( ( ( y  +  z ) s x )  =  ( ( y s x ) g ( z s x ) )  /\  ( ( y  x.  z ) s x )  =  ( y s ( z s x ) ) ) ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  vcrel  21103  vci  21104  isvclem  21133
  Copyright terms: Public domain W3C validator