Definition df-scaf 14599

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 14597	. 2 class .sf
2		vg	. . 3 setvar g
3		cvv 2821	. . 3 class _V
4		vx	. . . 4 setvar x
5		vy	. . . 4 setvar y
6	2	cv 1401	. . . . . 6 class g
7		csca 13411	. . . . . 6 class Scalar
8	6, 7	cfv 5372	. . . . 5 class (Scalar ` g )
9		cbs 13330	. . . . 5 class Base
10	8, 9	cfv 5372	. . . 4 class ( Base ` (Scalar ` g ) )
11	6, 9	cfv 5372	. . . 4 class ( Base ` g )
12	4	cv 1401	. . . . 5 class x
13	5	cv 1401	. . . . 5 class y
14		cvsca 13412	. . . . . 6 class .s
15	6, 14	cfv 5372	. . . . 5 class ( .s ` g )
16	12, 13, 15	co 6075	. . . 4 class ( x ( .s ` g ) y )
17	4, 5, 10, 11, 16	cmpo 6077	. . 3 class ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) )
18	2, 3, 17	cmpt 4187	. 2 class ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
19	1, 18	wceq 1402	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  14615