This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ⋅ 𝑠𝑓 = g ∈ V ⟼ x ∈ Base Scalar ⁡ g , y ∈ Base g ⟼ x ⋅ g y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cscaf class ⋅ 𝑠𝑓
1 vg setvar g
2 cvv class V
3 vx setvar x
4 cbs class Base
5 csca class Scalar
6 1 cv setvar g
7 6 5 cfv class Scalar ⁡ g
8 7 4 cfv class Base Scalar ⁡ g
9 vy setvar y
10 6 4 cfv class Base g
11 3 cv setvar x
12 cvsca class ⋅ 𝑠
13 6 12 cfv class ⋅ g
14 9 cv setvar y
15 11 14 13 co class x ⋅ g y
16 3 9 8 10 15 cmpo class x ∈ Base Scalar ⁡ g , y ∈ Base g ⟼ x ⋅ g y
17 1 2 16 cmpt class g ∈ V ⟼ x ∈ Base Scalar ⁡ g , y ∈ Base g ⟼ x ⋅ g y
18 0 17 wceq wff ⋅ 𝑠𝑓 = g ∈ V ⟼ x ∈ Base Scalar ⁡ g , y ∈ Base g ⟼ x ⋅ g y