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

Definition df-scaf 15945
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 15943 . 2  class  .s f
2 vg . . 3  set  g
3 cvv 2948 . . 3  class  _V
4 vx . . . 4  set  x
5 vy . . . 4  set  y
62cv 1651 . . . . . 6  class  g
7 csca 13524 . . . . . 6  class Scalar
86, 7cfv 5446 . . . . 5  class  (Scalar `  g )
9 cbs 13461 . . . . 5  class  Base
108, 9cfv 5446 . . . 4  class  ( Base `  (Scalar `  g )
)
116, 9cfv 5446 . . . 4  class  ( Base `  g )
124cv 1651 . . . . 5  class  x
135cv 1651 . . . . 5  class  y
14 cvsca 13525 . . . . . 6  class  .s
156, 14cfv 5446 . . . . 5  class  ( .s
`  g )
1612, 13, 15co 6073 . . . 4  class  ( x ( .s `  g
) y )
174, 5, 10, 11, 16cmpt2 6075 . . 3  class  ( x  e.  ( Base `  (Scalar `  g ) ) ,  y  e.  ( Base `  g )  |->  ( x ( .s `  g
) y ) )
182, 3, 17cmpt 4258 . 2  class  ( g  e.  _V  |->  ( x  e.  ( Base `  (Scalar `  g ) ) ,  y  e.  ( Base `  g )  |->  ( x ( .s `  g
) y ) ) )
191, 18wceq 1652 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  15960
  Copyright terms: Public domain W3C validator