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

Definition df-scaf 15630
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 15628 . 2  class  .s f
2 vg . . 3  set  g
3 cvv 2788 . . 3  class  _V
4 vx . . . 4  set  x
5 vy . . . 4  set  y
62cv 1622 . . . . . 6  class  g
7 csca 13211 . . . . . 6  class Scalar
86, 7cfv 5255 . . . . 5  class  (Scalar `  g )
9 cbs 13148 . . . . 5  class  Base
108, 9cfv 5255 . . . 4  class  ( Base `  (Scalar `  g )
)
116, 9cfv 5255 . . . 4  class  ( Base `  g )
124cv 1622 . . . . 5  class  x
135cv 1622 . . . . 5  class  y
14 cvsca 13212 . . . . . 6  class  .s
156, 14cfv 5255 . . . . 5  class  ( .s
`  g )
1612, 13, 15co 5858 . . . 4  class  ( x ( .s `  g
) y )
174, 5, 10, 11, 16cmpt2 5860 . . 3  class  ( x  e.  ( Base `  (Scalar `  g ) ) ,  y  e.  ( Base `  g )  |->  ( x ( .s `  g
) y ) )
182, 3, 17cmpt 4077 . 2  class  ( g  e.  _V  |->  ( x  e.  ( Base `  (Scalar `  g ) ) ,  y  e.  ( Base `  g )  |->  ( x ( .s `  g
) y ) ) )
191, 18wceq 1623 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  15645
  Copyright terms: Public domain W3C validator