Definition df-scaf 13385

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 13383	. 2 class .sf
2		vg	. . 3 setvar g
3		cvv 2739	. . 3 class _V
4		vx	. . . 4 setvar x
5		vy	. . . 4 setvar y
6	2	cv 1352	. . . . . 6 class g
7		csca 12541	. . . . . 6 class Scalar
8	6, 7	cfv 5218	. . . . 5 class (Scalar ` g )
9		cbs 12464	. . . . 5 class Base
10	8, 9	cfv 5218	. . . 4 class ( Base ` (Scalar ` g ) )
11	6, 9	cfv 5218	. . . 4 class ( Base ` g )
12	4	cv 1352	. . . . 5 class x
13	5	cv 1352	. . . . 5 class y
14		cvsca 12542	. . . . . 6 class .s
15	6, 14	cfv 5218	. . . . 5 class ( .s ` g )
16	12, 13, 15	co 5877	. . . 4 class ( x ( .s ` g ) y )
17	4, 5, 10, 11, 16	cmpo 5879	. . 3 class ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) )
18	2, 3, 17	cmpt 4066	. 2 class ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
19	1, 18	wceq 1353	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  13401