Definition df-scaf 13603

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 13601	. 2 class ·sf
2		vg	. . 3 setvar 𝑔
3		cvv 2752	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5		vy	. . . 4 setvar 𝑦
6	2	cv 1363	. . . . . 6 class 𝑔
7		csca 12589	. . . . . 6 class Scalar
8	6, 7	cfv 5235	. . . . 5 class (Scalar‘𝑔)
9		cbs 12511	. . . . 5 class Base
10	8, 9	cfv 5235	. . . 4 class (Base‘(Scalar‘𝑔))
11	6, 9	cfv 5235	. . . 4 class (Base‘𝑔)
12	4	cv 1363	. . . . 5 class 𝑥
13	5	cv 1363	. . . . 5 class 𝑦
14		cvsca 12590	. . . . . 6 class ·𝑠
15	6, 14	cfv 5235	. . . . 5 class ( ·𝑠 ‘𝑔)
16	12, 13, 15	co 5895	. . . 4 class (𝑥( ·𝑠 ‘𝑔)𝑦)
17	4, 5, 10, 11, 16	cmpo 5897	. . 3 class (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠 ‘𝑔)𝑦))
18	2, 3, 17	cmpt 4079	. 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠 ‘𝑔)𝑦)))
19	1, 18	wceq 1364	1 wff ·sf = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠 ‘𝑔)𝑦)))

This definition is referenced by:  scaffvalg  13619