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

Definition df-scaf 15646
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 15644 . 2  class  .s f
2 vg . . 3  set  g
3 cvv 2801 . . 3  class  _V
4 vx . . . 4  set  x
5 vy . . . 4  set  y
62cv 1631 . . . . . 6  class  g
7 csca 13227 . . . . . 6  class Scalar
86, 7cfv 5271 . . . . 5  class  (Scalar `  g )
9 cbs 13164 . . . . 5  class  Base
108, 9cfv 5271 . . . 4  class  ( Base `  (Scalar `  g )
)
116, 9cfv 5271 . . . 4  class  ( Base `  g )
124cv 1631 . . . . 5  class  x
135cv 1631 . . . . 5  class  y
14 cvsca 13228 . . . . . 6  class  .s
156, 14cfv 5271 . . . . 5  class  ( .s
`  g )
1612, 13, 15co 5874 . . . 4  class  ( x ( .s `  g
) y )
174, 5, 10, 11, 16cmpt2 5876 . . 3  class  ( x  e.  ( Base `  (Scalar `  g ) ) ,  y  e.  ( Base `  g )  |->  ( x ( .s `  g
) y ) )
182, 3, 17cmpt 4093 . 2  class  ( g  e.  _V  |->  ( x  e.  ( Base `  (Scalar `  g ) ) ,  y  e.  ( Base `  g )  |->  ( x ( .s `  g
) y ) ) )
191, 18wceq 1632 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  15661
  Copyright terms: Public domain W3C validator