Definition df-scaf 14023

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 14021	. 2 class .sf
2		vg	. . 3 setvar g
3		cvv 2771	. . 3 class _V
4		vx	. . . 4 setvar x
5		vy	. . . 4 setvar y
6	2	cv 1371	. . . . . 6 class g
7		csca 12883	. . . . . 6 class Scalar
8	6, 7	cfv 5270	. . . . 5 class (Scalar ` g )
9		cbs 12803	. . . . 5 class Base
10	8, 9	cfv 5270	. . . 4 class ( Base ` (Scalar ` g ) )
11	6, 9	cfv 5270	. . . 4 class ( Base ` g )
12	4	cv 1371	. . . . 5 class x
13	5	cv 1371	. . . . 5 class y
14		cvsca 12884	. . . . . 6 class .s
15	6, 14	cfv 5270	. . . . 5 class ( .s ` g )
16	12, 13, 15	co 5943	. . . 4 class ( x ( .s ` g ) y )
17	4, 5, 10, 11, 16	cmpo 5945	. . 3 class ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) )
18	2, 3, 17	cmpt 4104	. 2 class ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
19	1, 18	wceq 1372	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  14039