Definition df-scaf 14303

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 14301	. 2 class .sf
2		vg	. . 3 setvar g
3		cvv 2802	. . 3 class _V
4		vx	. . . 4 setvar x
5		vy	. . . 4 setvar y
6	2	cv 1396	. . . . . 6 class g
7		csca 13162	. . . . . 6 class Scalar
8	6, 7	cfv 5326	. . . . 5 class (Scalar ` g )
9		cbs 13081	. . . . 5 class Base
10	8, 9	cfv 5326	. . . 4 class ( Base ` (Scalar ` g ) )
11	6, 9	cfv 5326	. . . 4 class ( Base ` g )
12	4	cv 1396	. . . . 5 class x
13	5	cv 1396	. . . . 5 class y
14		cvsca 13163	. . . . . 6 class .s
15	6, 14	cfv 5326	. . . . 5 class ( .s ` g )
16	12, 13, 15	co 6017	. . . 4 class ( x ( .s ` g ) y )
17	4, 5, 10, 11, 16	cmpo 6019	. . 3 class ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) )
18	2, 3, 17	cmpt 4150	. 2 class ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
19	1, 18	wceq 1397	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  14319