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

Definition df-scaf 15881
Description: Define the functionalization of the  .s operator. This restricts the value of  .s to the stated domain, which is necessary when working with restricted structures, whose operations may be defined on a larger set than the true base. (Contributed by Mario Carneiro, 5-Oct-2015.)
Assertion
Ref Expression
df-scaf  |-  .s f  =  ( g  e. 
_V  |->  ( x  e.  ( Base `  (Scalar `  g ) ) ,  y  e.  ( Base `  g )  |->  ( x ( .s `  g
) y ) ) )
Distinct variable group:    x, g, y

Detailed syntax breakdown of Definition df-scaf
StepHypRef Expression
1 cscaf 15879 . 2  class  .s f
2 vg . . 3  set  g
3 cvv 2900 . . 3  class  _V
4 vx . . . 4  set  x
5 vy . . . 4  set  y
62cv 1648 . . . . . 6  class  g
7 csca 13460 . . . . . 6  class Scalar
86, 7cfv 5395 . . . . 5  class  (Scalar `  g )
9 cbs 13397 . . . . 5  class  Base
108, 9cfv 5395 . . . 4  class  ( Base `  (Scalar `  g )
)
116, 9cfv 5395 . . . 4  class  ( Base `  g )
124cv 1648 . . . . 5  class  x
135cv 1648 . . . . 5  class  y
14 cvsca 13461 . . . . . 6  class  .s
156, 14cfv 5395 . . . . 5  class  ( .s
`  g )
1612, 13, 15co 6021 . . . 4  class  ( x ( .s `  g
) y )
174, 5, 10, 11, 16cmpt2 6023 . . 3  class  ( x  e.  ( Base `  (Scalar `  g ) ) ,  y  e.  ( Base `  g )  |->  ( x ( .s `  g
) y ) )
182, 3, 17cmpt 4208 . 2  class  ( g  e.  _V  |->  ( x  e.  ( Base `  (Scalar `  g ) ) ,  y  e.  ( Base `  g )  |->  ( x ( .s `  g
) y ) ) )
191, 18wceq 1649 1  wff  .s f  =  ( g  e. 
_V  |->  ( x  e.  ( Base `  (Scalar `  g ) ) ,  y  e.  ( Base `  g )  |->  ( x ( .s `  g
) y ) ) )
Colors of variables: wff set class
This definition is referenced by:  scaffval  15896
  Copyright terms: Public domain W3C validator