Definition df-scaf 14438

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 14436	. 2 class .sf
2		vg	. . 3 setvar g
3		cvv 2813	. . 3 class _V
4		vx	. . . 4 setvar x
5		vy	. . . 4 setvar y
6	2	cv 1397	. . . . . 6 class g
7		csca 13293	. . . . . 6 class Scalar
8	6, 7	cfv 5352	. . . . 5 class (Scalar ` g )
9		cbs 13212	. . . . 5 class Base
10	8, 9	cfv 5352	. . . 4 class ( Base ` (Scalar ` g ) )
11	6, 9	cfv 5352	. . . 4 class ( Base ` g )
12	4	cv 1397	. . . . 5 class x
13	5	cv 1397	. . . . 5 class y
14		cvsca 13294	. . . . . 6 class .s
15	6, 14	cfv 5352	. . . . 5 class ( .s ` g )
16	12, 13, 15	co 6050	. . . 4 class ( x ( .s ` g ) y )
17	4, 5, 10, 11, 16	cmpo 6052	. . 3 class ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) )
18	2, 3, 17	cmpt 4171	. 2 class ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
19	1, 18	wceq 1398	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  14454