Definition df-scaf 18866

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 18864	. 2 class .sf
2		vg	. . 3 setvar g
3		cvv 3200	. . 3 class _V
4		vx	. . . 4 setvar x
5		vy	. . . 4 setvar y
6	2	cv 1482	. . . . . 6 class g
7		csca 15944	. . . . . 6 class Scalar
8	6, 7	cfv 5888	. . . . 5 class (Scalar ` g )
9		cbs 15857	. . . . 5 class Base
10	8, 9	cfv 5888	. . . 4 class ( Base ` (Scalar ` g ) )
11	6, 9	cfv 5888	. . . 4 class ( Base ` g )
12	4	cv 1482	. . . . 5 class x
13	5	cv 1482	. . . . 5 class y
14		cvsca 15945	. . . . . 6 class .s
15	6, 14	cfv 5888	. . . . 5 class ( .s ` g )
16	12, 13, 15	co 6650	. . . 4 class ( x ( .s ` g ) y )
17	4, 5, 10, 11, 16	cmpt2 6652	. . 3 class ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) )
18	2, 3, 17	cmpt 4729	. 2 class ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
19	1, 18	wceq 1483	1 wff .sf = ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )

This definition is referenced by:  scaffval  18881