Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-vec Unicode version

Definition df-vec 25450
Description: Definition of a vector space ( <. g ,  h >. is a field ), or of a module ( <. g ,  h >. is a ring ). (Contributed by FL, 12-Jul-2010.)
Assertion
Ref Expression
df-vec  |-  Vec  =  { z  |  E. g E. h E. a E. b ( z  = 
<. <. g ,  h >. ,  <. a ,  b
>. >.  /\  ( a  e.  AbelOp  /\  b :
( ran  g  X.  ran  a ) --> ran  a  /\  A. u  e.  ran  a ( ( (GId
`  h ) b u )  =  u  /\  A. x  e. 
ran  g ( A. v  e.  ran  a ( x b ( u a v ) )  =  ( ( x b u ) a ( x b v ) )  /\  A. y  e.  ran  g ( ( ( x g y ) b u )  =  ( ( x b u ) a ( y b u ) )  /\  ( ( x h y ) b u )  =  ( x b ( y b u ) ) ) ) ) ) ) }
Distinct variable group:    g, h, a, b, u, x, v, y, z

Detailed syntax breakdown of Definition df-vec
StepHypRef Expression
1 cvec 25449 . 2  class  Vec
2 vz . . . . . . . . . 10  set  z
32cv 1622 . . . . . . . . 9  class  z
4 vg . . . . . . . . . . . 12  set  g
54cv 1622 . . . . . . . . . . 11  class  g
6 vh . . . . . . . . . . . 12  set  h
76cv 1622 . . . . . . . . . . 11  class  h
85, 7cop 3643 . . . . . . . . . 10  class  <. g ,  h >.
9 va . . . . . . . . . . . 12  set  a
109cv 1622 . . . . . . . . . . 11  class  a
11 vb . . . . . . . . . . . 12  set  b
1211cv 1622 . . . . . . . . . . 11  class  b
1310, 12cop 3643 . . . . . . . . . 10  class  <. a ,  b >.
148, 13cop 3643 . . . . . . . . 9  class  <. <. g ,  h >. ,  <. a ,  b >. >.
153, 14wceq 1623 . . . . . . . 8  wff  z  = 
<. <. g ,  h >. ,  <. a ,  b
>. >.
16 cablo 20948 . . . . . . . . . 10  class  AbelOp
1710, 16wcel 1684 . . . . . . . . 9  wff  a  e. 
AbelOp
185crn 4690 . . . . . . . . . . 11  class  ran  g
1910crn 4690 . . . . . . . . . . 11  class  ran  a
2018, 19cxp 4687 . . . . . . . . . 10  class  ( ran  g  X.  ran  a
)
2120, 19, 12wf 5251 . . . . . . . . 9  wff  b : ( ran  g  X. 
ran  a ) --> ran  a
22 cgi 20854 . . . . . . . . . . . . . 14  class GId
237, 22cfv 5255 . . . . . . . . . . . . 13  class  (GId `  h )
24 vu . . . . . . . . . . . . . 14  set  u
2524cv 1622 . . . . . . . . . . . . 13  class  u
2623, 25, 12co 5858 . . . . . . . . . . . 12  class  ( (GId
`  h ) b u )
2726, 25wceq 1623 . . . . . . . . . . 11  wff  ( (GId
`  h ) b u )  =  u
28 vx . . . . . . . . . . . . . . . . 17  set  x
2928cv 1622 . . . . . . . . . . . . . . . 16  class  x
30 vv . . . . . . . . . . . . . . . . . 18  set  v
3130cv 1622 . . . . . . . . . . . . . . . . 17  class  v
3225, 31, 10co 5858 . . . . . . . . . . . . . . . 16  class  ( u a v )
3329, 32, 12co 5858 . . . . . . . . . . . . . . 15  class  ( x b ( u a v ) )
3429, 25, 12co 5858 . . . . . . . . . . . . . . . 16  class  ( x b u )
3529, 31, 12co 5858 . . . . . . . . . . . . . . . 16  class  ( x b v )
3634, 35, 10co 5858 . . . . . . . . . . . . . . 15  class  ( ( x b u ) a ( x b v ) )
3733, 36wceq 1623 . . . . . . . . . . . . . 14  wff  ( x b ( u a v ) )  =  ( ( x b u ) a ( x b v ) )
3837, 30, 19wral 2543 . . . . . . . . . . . . 13  wff  A. v  e.  ran  a ( x b ( u a v ) )  =  ( ( x b u ) a ( x b v ) )
39 vy . . . . . . . . . . . . . . . . . . 19  set  y
4039cv 1622 . . . . . . . . . . . . . . . . . 18  class  y
4129, 40, 5co 5858 . . . . . . . . . . . . . . . . 17  class  ( x g y )
4241, 25, 12co 5858 . . . . . . . . . . . . . . . 16  class  ( ( x g y ) b u )
4340, 25, 12co 5858 . . . . . . . . . . . . . . . . 17  class  ( y b u )
4434, 43, 10co 5858 . . . . . . . . . . . . . . . 16  class  ( ( x b u ) a ( y b u ) )
4542, 44wceq 1623 . . . . . . . . . . . . . . 15  wff  ( ( x g y ) b u )  =  ( ( x b u ) a ( y b u ) )
4629, 40, 7co 5858 . . . . . . . . . . . . . . . . 17  class  ( x h y )
4746, 25, 12co 5858 . . . . . . . . . . . . . . . 16  class  ( ( x h y ) b u )
4829, 43, 12co 5858 . . . . . . . . . . . . . . . 16  class  ( x b ( y b u ) )
4947, 48wceq 1623 . . . . . . . . . . . . . . 15  wff  ( ( x h y ) b u )  =  ( x b ( y b u ) )
5045, 49wa 358 . . . . . . . . . . . . . 14  wff  ( ( ( x g y ) b u )  =  ( ( x b u ) a ( y b u ) )  /\  (
( x h y ) b u )  =  ( x b ( y b u ) ) )
5150, 39, 18wral 2543 . . . . . . . . . . . . 13  wff  A. y  e.  ran  g ( ( ( x g y ) b u )  =  ( ( x b u ) a ( y b u ) )  /\  (
( x h y ) b u )  =  ( x b ( y b u ) ) )
5238, 51wa 358 . . . . . . . . . . . 12  wff  ( A. v  e.  ran  a ( x b ( u a v ) )  =  ( ( x b u ) a ( x b v ) )  /\  A. y  e.  ran  g ( ( ( x g y ) b u )  =  ( ( x b u ) a ( y b u ) )  /\  ( ( x h y ) b u )  =  ( x b ( y b u ) ) ) )
5352, 28, 18wral 2543 . . . . . . . . . . 11  wff  A. x  e.  ran  g ( A. v  e.  ran  a ( x b ( u a v ) )  =  ( ( x b u ) a ( x b v ) )  /\  A. y  e.  ran  g ( ( ( x g y ) b u )  =  ( ( x b u ) a ( y b u ) )  /\  ( ( x h y ) b u )  =  ( x b ( y b u ) ) ) )
5427, 53wa 358 . . . . . . . . . 10  wff  ( ( (GId `  h )
b u )  =  u  /\  A. x  e.  ran  g ( A. v  e.  ran  a ( x b ( u a v ) )  =  ( ( x b u ) a ( x b v ) )  /\  A. y  e.  ran  g ( ( ( x g y ) b u )  =  ( ( x b u ) a ( y b u ) )  /\  ( ( x h y ) b u )  =  ( x b ( y b u ) ) ) ) )
5554, 24, 19wral 2543 . . . . . . . . 9  wff  A. u  e.  ran  a ( ( (GId `  h )
b u )  =  u  /\  A. x  e.  ran  g ( A. v  e.  ran  a ( x b ( u a v ) )  =  ( ( x b u ) a ( x b v ) )  /\  A. y  e.  ran  g ( ( ( x g y ) b u )  =  ( ( x b u ) a ( y b u ) )  /\  ( ( x h y ) b u )  =  ( x b ( y b u ) ) ) ) )
5617, 21, 55w3a 934 . . . . . . . 8  wff  ( a  e.  AbelOp  /\  b :
( ran  g  X.  ran  a ) --> ran  a  /\  A. u  e.  ran  a ( ( (GId
`  h ) b u )  =  u  /\  A. x  e. 
ran  g ( A. v  e.  ran  a ( x b ( u a v ) )  =  ( ( x b u ) a ( x b v ) )  /\  A. y  e.  ran  g ( ( ( x g y ) b u )  =  ( ( x b u ) a ( y b u ) )  /\  ( ( x h y ) b u )  =  ( x b ( y b u ) ) ) ) ) )
5715, 56wa 358 . . . . . . 7  wff  ( z  =  <. <. g ,  h >. ,  <. a ,  b
>. >.  /\  ( a  e.  AbelOp  /\  b :
( ran  g  X.  ran  a ) --> ran  a  /\  A. u  e.  ran  a ( ( (GId
`  h ) b u )  =  u  /\  A. x  e. 
ran  g ( A. v  e.  ran  a ( x b ( u a v ) )  =  ( ( x b u ) a ( x b v ) )  /\  A. y  e.  ran  g ( ( ( x g y ) b u )  =  ( ( x b u ) a ( y b u ) )  /\  ( ( x h y ) b u )  =  ( x b ( y b u ) ) ) ) ) ) )
5857, 11wex 1528 . . . . . 6  wff  E. b
( z  =  <. <.
g ,  h >. , 
<. a ,  b >. >.  /\  ( a  e. 
AbelOp  /\  b : ( ran  g  X.  ran  a ) --> ran  a  /\  A. u  e.  ran  a ( ( (GId
`  h ) b u )  =  u  /\  A. x  e. 
ran  g ( A. v  e.  ran  a ( x b ( u a v ) )  =  ( ( x b u ) a ( x b v ) )  /\  A. y  e.  ran  g ( ( ( x g y ) b u )  =  ( ( x b u ) a ( y b u ) )  /\  ( ( x h y ) b u )  =  ( x b ( y b u ) ) ) ) ) ) )
5958, 9wex 1528 . . . . 5  wff  E. a E. b ( z  = 
<. <. g ,  h >. ,  <. a ,  b
>. >.  /\  ( a  e.  AbelOp  /\  b :
( ran  g  X.  ran  a ) --> ran  a  /\  A. u  e.  ran  a ( ( (GId
`  h ) b u )  =  u  /\  A. x  e. 
ran  g ( A. v  e.  ran  a ( x b ( u a v ) )  =  ( ( x b u ) a ( x b v ) )  /\  A. y  e.  ran  g ( ( ( x g y ) b u )  =  ( ( x b u ) a ( y b u ) )  /\  ( ( x h y ) b u )  =  ( x b ( y b u ) ) ) ) ) ) )
6059, 6wex 1528 . . . 4  wff  E. h E. a E. b ( z  =  <. <. g ,  h >. ,  <. a ,  b >. >.  /\  (
a  e.  AbelOp  /\  b : ( ran  g  X.  ran  a ) --> ran  a  /\  A. u  e.  ran  a ( ( (GId `  h )
b u )  =  u  /\  A. x  e.  ran  g ( A. v  e.  ran  a ( x b ( u a v ) )  =  ( ( x b u ) a ( x b v ) )  /\  A. y  e.  ran  g ( ( ( x g y ) b u )  =  ( ( x b u ) a ( y b u ) )  /\  ( ( x h y ) b u )  =  ( x b ( y b u ) ) ) ) ) ) )
6160, 4wex 1528 . . 3  wff  E. g E. h E. a E. b ( z  = 
<. <. g ,  h >. ,  <. a ,  b
>. >.  /\  ( a  e.  AbelOp  /\  b :
( ran  g  X.  ran  a ) --> ran  a  /\  A. u  e.  ran  a ( ( (GId
`  h ) b u )  =  u  /\  A. x  e. 
ran  g ( A. v  e.  ran  a ( x b ( u a v ) )  =  ( ( x b u ) a ( x b v ) )  /\  A. y  e.  ran  g ( ( ( x g y ) b u )  =  ( ( x b u ) a ( y b u ) )  /\  ( ( x h y ) b u )  =  ( x b ( y b u ) ) ) ) ) ) )
6261, 2cab 2269 . 2  class  { z  |  E. g E. h E. a E. b ( z  = 
<. <. g ,  h >. ,  <. a ,  b
>. >.  /\  ( a  e.  AbelOp  /\  b :
( ran  g  X.  ran  a ) --> ran  a  /\  A. u  e.  ran  a ( ( (GId
`  h ) b u )  =  u  /\  A. x  e. 
ran  g ( A. v  e.  ran  a ( x b ( u a v ) )  =  ( ( x b u ) a ( x b v ) )  /\  A. y  e.  ran  g ( ( ( x g y ) b u )  =  ( ( x b u ) a ( y b u ) )  /\  ( ( x h y ) b u )  =  ( x b ( y b u ) ) ) ) ) ) ) }
631, 62wceq 1623 1  wff  Vec  =  { z  |  E. g E. h E. a E. b ( z  = 
<. <. g ,  h >. ,  <. a ,  b
>. >.  /\  ( a  e.  AbelOp  /\  b :
( ran  g  X.  ran  a ) --> ran  a  /\  A. u  e.  ran  a ( ( (GId
`  h ) b u )  =  u  /\  A. x  e. 
ran  g ( A. v  e.  ran  a ( x b ( u a v ) )  =  ( ( x b u ) a ( x b v ) )  /\  A. y  e.  ran  g ( ( ( x g y ) b u )  =  ( ( x b u ) a ( y b u ) )  /\  ( ( x h y ) b u )  =  ( x b ( y b u ) ) ) ) ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  vecval1b  25451  vecval3b  25452
  Copyright terms: Public domain W3C validator