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

Step	Hyp	Ref	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
6	2	cv 1372	. . . . . 6 class g
7		csca 12912	. . . . . 6 class Scalar
8	6, 7	cfv 5271	. . . . 5 class (Scalar ` g )
9		cbs 12832	. . . . 5 class Base
10	8, 9	cfv 5271	. . . 4 class ( Base ` (Scalar ` g ) )
11	6, 9	cfv 5271	. . . 4 class ( Base ` g )
12	4	cv 1372	. . . . 5 class x
13	5	cv 1372	. . . . 5 class y
14		cvsca 12913	. . . . . 6 class .s
15	6, 14	cfv 5271	. . . . 5 class ( .s ` g )
16	12, 13, 15	co 5944	. . . 4 class ( x ( .s ` g ) y )
17	4, 5, 10, 11, 16	cmpo 5946	. . 3 class ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) )
18	2, 3, 17	cmpt 4105	. 2 class ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
19	1, 18	wceq 1373	1 wff .sf = ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )

This definition is referenced by:  scaffvalg  14068