Definition df-scaf 13631

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 13629	. 2 class .sf
2		vg	. . 3 setvar g
3		cvv 2752	. . 3 class _V
4		vx	. . . 4 setvar x
5		vy	. . . 4 setvar y
6	2	cv 1363	. . . . . 6 class g
7		csca 12603	. . . . . 6 class Scalar
8	6, 7	cfv 5238	. . . . 5 class (Scalar ` g )
9		cbs 12523	. . . . 5 class Base
10	8, 9	cfv 5238	. . . 4 class ( Base ` (Scalar ` g ) )
11	6, 9	cfv 5238	. . . 4 class ( Base ` g )
12	4	cv 1363	. . . . 5 class x
13	5	cv 1363	. . . . 5 class y
14		cvsca 12604	. . . . . 6 class .s
15	6, 14	cfv 5238	. . . . 5 class ( .s ` g )
16	12, 13, 15	co 5900	. . . 4 class ( x ( .s ` g ) y )
17	4, 5, 10, 11, 16	cmpo 5902	. . 3 class ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) )
18	2, 3, 17	cmpt 4082	. 2 class ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
19	1, 18	wceq 1364	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  13647