Definition df-scaf 14254

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 14252	. 2 class .sf
2		vg	. . 3 setvar g
3		cvv 2799	. . 3 class _V
4		vx	. . . 4 setvar x
5		vy	. . . 4 setvar y
6	2	cv 1394	. . . . . 6 class g
7		csca 13113	. . . . . 6 class Scalar
8	6, 7	cfv 5318	. . . . 5 class (Scalar ` g )
9		cbs 13032	. . . . 5 class Base
10	8, 9	cfv 5318	. . . 4 class ( Base ` (Scalar ` g ) )
11	6, 9	cfv 5318	. . . 4 class ( Base ` g )
12	4	cv 1394	. . . . 5 class x
13	5	cv 1394	. . . . 5 class y
14		cvsca 13114	. . . . . 6 class .s
15	6, 14	cfv 5318	. . . . 5 class ( .s ` g )
16	12, 13, 15	co 6001	. . . 4 class ( x ( .s ` g ) y )
17	4, 5, 10, 11, 16	cmpo 6003	. . 3 class ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) )
18	2, 3, 17	cmpt 4145	. 2 class ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
19	1, 18	wceq 1395	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  14270