Definition df-scaf

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)

	Ref	Expression
Assertion	df-scaf	⊢ ·sf = ( 𝑔 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) , 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑥 ( ·𝑠 ‘ 𝑔 ) 𝑦 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cscaf	⊢ ·sf
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		cbs	⊢ Base
5		csca	⊢ Scalar
6	1	cv	⊢ 𝑔
7	6 5	cfv	⊢ ( Scalar ‘ 𝑔 )
8	7 4	cfv	⊢ ( Base ‘ ( Scalar ‘ 𝑔 ) )
9		vy	⊢ 𝑦
10	6 4	cfv	⊢ ( Base ‘ 𝑔 )
11	3	cv	⊢ 𝑥
12		cvsca	⊢ ·𝑠
13	6 12	cfv	⊢ ( ·𝑠 ‘ 𝑔 )
14	9	cv	⊢ 𝑦
15	11 14 13	co	⊢ ( 𝑥 ( ·𝑠 ‘ 𝑔 ) 𝑦 )
16	3 9 8 10 15	cmpo	⊢ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) , 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑥 ( ·𝑠 ‘ 𝑔 ) 𝑦 ) )
17	1 2 16	cmpt	⊢ ( 𝑔 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) , 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑥 ( ·𝑠 ‘ 𝑔 ) 𝑦 ) ) )
18	0 17	wceq	⊢ ·sf = ( 𝑔 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑔 ) ) , 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑥 ( ·𝑠 ‘ 𝑔 ) 𝑦 ) ) )