Definition df-scaf 20861

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 20859	. 2 class ·sf
2		vg	. . 3 setvar 𝑔
3		cvv 3480	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5		vy	. . . 4 setvar 𝑦
6	2	cv 1539	. . . . . 6 class 𝑔
7		csca 17300	. . . . . 6 class Scalar
8	6, 7	cfv 6561	. . . . 5 class (Scalar‘𝑔)
9		cbs 17247	. . . . 5 class Base
10	8, 9	cfv 6561	. . . 4 class (Base‘(Scalar‘𝑔))
11	6, 9	cfv 6561	. . . 4 class (Base‘𝑔)
12	4	cv 1539	. . . . 5 class 𝑥
13	5	cv 1539	. . . . 5 class 𝑦
14		cvsca 17301	. . . . . 6 class ·𝑠
15	6, 14	cfv 6561	. . . . 5 class ( ·𝑠 ‘𝑔)
16	12, 13, 15	co 7431	. . . 4 class (𝑥( ·𝑠 ‘𝑔)𝑦)
17	4, 5, 10, 11, 16	cmpo 7433	. . 3 class (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠 ‘𝑔)𝑦))
18	2, 3, 17	cmpt 5225	. 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠 ‘𝑔)𝑦)))
19	1, 18	wceq 1540	1 wff ·sf = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠 ‘𝑔)𝑦)))

This definition is referenced by:  scaffval  20878