ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-scaf Unicode version

Definition df-scaf 14052
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 14050 . 2  class  .sf
2 vg . . 3  setvar  g
3 cvv 2772 . . 3  class  _V
4 vx . . . 4  setvar  x
5 vy . . . 4  setvar  y
62cv 1372 . . . . . 6  class  g
7 csca 12912 . . . . . 6  class Scalar
86, 7cfv 5271 . . . . 5  class  (Scalar `  g )
9 cbs 12832 . . . . 5  class  Base
108, 9cfv 5271 . . . 4  class  ( Base `  (Scalar `  g )
)
116, 9cfv 5271 . . . 4  class  ( Base `  g )
124cv 1372 . . . . 5  class  x
135cv 1372 . . . . 5  class  y
14 cvsca 12913 . . . . . 6  class  .s
156, 14cfv 5271 . . . . 5  class  ( .s
`  g )
1612, 13, 15co 5944 . . . 4  class  ( x ( .s `  g
) y )
174, 5, 10, 11, 16cmpo 5946 . . 3  class  ( x  e.  ( Base `  (Scalar `  g ) ) ,  y  e.  ( Base `  g )  |->  ( x ( .s `  g
) y ) )
182, 3, 17cmpt 4105 . 2  class  ( g  e.  _V  |->  ( x  e.  ( Base `  (Scalar `  g ) ) ,  y  e.  ( Base `  g )  |->  ( x ( .s `  g
) y ) ) )
191, 18wceq 1373 1  wff  .sf 
=  ( 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:  scaffvalg  14068
  Copyright terms: Public domain W3C validator