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

Definition df-scaf 17386
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  |-  .sf 
=  ( 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 17384 . 2  class  .sf
2 vg . . 3  setvar  g
3 cvv 3118 . . 3  class  _V
4 vx . . . 4  setvar  x
5 vy . . . 4  setvar  y
62cv 1378 . . . . . 6  class  g
7 csca 14575 . . . . . 6  class Scalar
86, 7cfv 5594 . . . . 5  class  (Scalar `  g )
9 cbs 14507 . . . . 5  class  Base
108, 9cfv 5594 . . . 4  class  ( Base `  (Scalar `  g )
)
116, 9cfv 5594 . . . 4  class  ( Base `  g )
124cv 1378 . . . . 5  class  x
135cv 1378 . . . . 5  class  y
14 cvsca 14576 . . . . . 6  class  .s
156, 14cfv 5594 . . . . 5  class  ( .s
`  g )
1612, 13, 15co 6295 . . . 4  class  ( x ( .s `  g
) y )
174, 5, 10, 11, 16cmpt2 6297 . . 3  class  ( x  e.  ( Base `  (Scalar `  g ) ) ,  y  e.  ( Base `  g )  |->  ( x ( .s `  g
) y ) )
182, 3, 17cmpt 4511 . 2  class  ( g  e.  _V  |->  ( x  e.  ( Base `  (Scalar `  g ) ) ,  y  e.  ( Base `  g )  |->  ( x ( .s `  g
) y ) ) )
191, 18wceq 1379 1  wff  .sf 
=  ( g  e. 
_V  |->  ( x  e.  ( Base `  (Scalar `  g ) ) ,  y  e.  ( Base `  g )  |->  ( x ( .s `  g
) y ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  scaffval  17401
  Copyright terms: Public domain W3C validator