Definition df-scaf 19258

Description: Define the functionalization of the ·_𝑠 operator. This restricts the value of ·_𝑠 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 = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠 ‘𝑔)𝑦)))

Distinct variable group:   𝑥,𝑔,𝑦

Detailed syntax breakdown of Definition df-scaf

Step	Hyp	Ref	Expression
1		cscaf 19256	. 2 class ·sf
2		vg	. . 3 setvar 𝑔
3		cvv 3398	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5		vy	. . . 4 setvar 𝑦
6	2	cv 1600	. . . . . 6 class 𝑔
7		csca 16341	. . . . . 6 class Scalar
8	6, 7	cfv 6135	. . . . 5 class (Scalar‘𝑔)
9		cbs 16255	. . . . 5 class Base
10	8, 9	cfv 6135	. . . 4 class (Base‘(Scalar‘𝑔))
11	6, 9	cfv 6135	. . . 4 class (Base‘𝑔)
12	4	cv 1600	. . . . 5 class 𝑥
13	5	cv 1600	. . . . 5 class 𝑦
14		cvsca 16342	. . . . . 6 class ·𝑠
15	6, 14	cfv 6135	. . . . 5 class ( ·𝑠 ‘𝑔)
16	12, 13, 15	co 6922	. . . 4 class (𝑥( ·𝑠 ‘𝑔)𝑦)
17	4, 5, 10, 11, 16	cmpt2 6924	. . 3 class (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠 ‘𝑔)𝑦))
18	2, 3, 17	cmpt 4965	. 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠 ‘𝑔)𝑦)))
19	1, 18	wceq 1601	1 wff ·sf = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠 ‘𝑔)𝑦)))

This definition is referenced by:  scaffval  19273