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

Definition df-act 25551
Description: Definition of an action law. The action is the function ( k ^m ( v ^m v ). Definitions equivalent through currying. (Contributed by FL, 24-Dec-2013.)
Assertion
Ref Expression
df-act  |-  Action  =  {
f  |  E. k E. v E. s ( ( k  =  (
Base `  (Scalar `  f
) )  /\  v  =  ( Base `  f
)  /\  s  =  ( .s `  f ) )  /\  A. r  e.  k  A. w  e.  v  ( r
s w )  e.  v ) }
Distinct variable group:    f, k, v, s, r, w

Detailed syntax breakdown of Definition df-act
StepHypRef Expression
1 cact 25550 . 2  class  Action
2 vk . . . . . . . . . 10  set  k
32cv 1631 . . . . . . . . 9  class  k
4 vf . . . . . . . . . . . 12  set  f
54cv 1631 . . . . . . . . . . 11  class  f
6 csca 13227 . . . . . . . . . . 11  class Scalar
75, 6cfv 5271 . . . . . . . . . 10  class  (Scalar `  f )
8 cbs 13164 . . . . . . . . . 10  class  Base
97, 8cfv 5271 . . . . . . . . 9  class  ( Base `  (Scalar `  f )
)
103, 9wceq 1632 . . . . . . . 8  wff  k  =  ( Base `  (Scalar `  f ) )
11 vv . . . . . . . . . 10  set  v
1211cv 1631 . . . . . . . . 9  class  v
135, 8cfv 5271 . . . . . . . . 9  class  ( Base `  f )
1412, 13wceq 1632 . . . . . . . 8  wff  v  =  ( Base `  f
)
15 vs . . . . . . . . . 10  set  s
1615cv 1631 . . . . . . . . 9  class  s
17 cvsca 13228 . . . . . . . . . 10  class  .s
185, 17cfv 5271 . . . . . . . . 9  class  ( .s
`  f )
1916, 18wceq 1632 . . . . . . . 8  wff  s  =  ( .s `  f
)
2010, 14, 19w3a 934 . . . . . . 7  wff  ( k  =  ( Base `  (Scalar `  f ) )  /\  v  =  ( Base `  f )  /\  s  =  ( .s `  f ) )
21 vr . . . . . . . . . . . 12  set  r
2221cv 1631 . . . . . . . . . . 11  class  r
23 vw . . . . . . . . . . . 12  set  w
2423cv 1631 . . . . . . . . . . 11  class  w
2522, 24, 16co 5874 . . . . . . . . . 10  class  ( r s w )
2625, 12wcel 1696 . . . . . . . . 9  wff  ( r s w )  e.  v
2726, 23, 12wral 2556 . . . . . . . 8  wff  A. w  e.  v  ( r
s w )  e.  v
2827, 21, 3wral 2556 . . . . . . 7  wff  A. r  e.  k  A. w  e.  v  ( r
s w )  e.  v
2920, 28wa 358 . . . . . 6  wff  ( ( k  =  ( Base `  (Scalar `  f )
)  /\  v  =  ( Base `  f )  /\  s  =  ( .s `  f ) )  /\  A. r  e.  k  A. w  e.  v  ( r s w )  e.  v )
3029, 15wex 1531 . . . . 5  wff  E. s
( ( k  =  ( Base `  (Scalar `  f ) )  /\  v  =  ( Base `  f )  /\  s  =  ( .s `  f ) )  /\  A. r  e.  k  A. w  e.  v  (
r s w )  e.  v )
3130, 11wex 1531 . . . 4  wff  E. v E. s ( ( k  =  ( Base `  (Scalar `  f ) )  /\  v  =  ( Base `  f )  /\  s  =  ( .s `  f ) )  /\  A. r  e.  k  A. w  e.  v  (
r s w )  e.  v )
3231, 2wex 1531 . . 3  wff  E. k E. v E. s ( ( k  =  (
Base `  (Scalar `  f
) )  /\  v  =  ( Base `  f
)  /\  s  =  ( .s `  f ) )  /\  A. r  e.  k  A. w  e.  v  ( r
s w )  e.  v )
3332, 4cab 2282 . 2  class  { f  |  E. k E. v E. s ( ( k  =  (
Base `  (Scalar `  f
) )  /\  v  =  ( Base `  f
)  /\  s  =  ( .s `  f ) )  /\  A. r  e.  k  A. w  e.  v  ( r
s w )  e.  v ) }
341, 33wceq 1632 1  wff  Action  =  {
f  |  E. k E. v E. s ( ( k  =  (
Base `  (Scalar `  f
) )  /\  v  =  ( Base `  f
)  /\  s  =  ( .s `  f ) )  /\  A. r  e.  k  A. w  e.  v  ( r
s w )  e.  v ) }
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator