Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-scaf Structured version   Visualization version   GIF version

Definition df-scaf 19629
 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
StepHypRef Expression
1 cscaf 19627 . 2 class ·sf
2 vg . . 3 setvar 𝑔
3 cvv 3493 . . 3 class V
4 vx . . . 4 setvar 𝑥
5 vy . . . 4 setvar 𝑦
62cv 1529 . . . . . 6 class 𝑔
7 csca 16560 . . . . . 6 class Scalar
86, 7cfv 6348 . . . . 5 class (Scalar‘𝑔)
9 cbs 16475 . . . . 5 class Base
108, 9cfv 6348 . . . 4 class (Base‘(Scalar‘𝑔))
116, 9cfv 6348 . . . 4 class (Base‘𝑔)
124cv 1529 . . . . 5 class 𝑥
135cv 1529 . . . . 5 class 𝑦
14 cvsca 16561 . . . . . 6 class ·𝑠
156, 14cfv 6348 . . . . 5 class ( ·𝑠𝑔)
1612, 13, 15co 7148 . . . 4 class (𝑥( ·𝑠𝑔)𝑦)
174, 5, 10, 11, 16cmpo 7150 . . 3 class (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠𝑔)𝑦))
182, 3, 17cmpt 5137 . 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠𝑔)𝑦)))
191, 18wceq 1530 1 wff ·sf = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠𝑔)𝑦)))
 Colors of variables: wff setvar class This definition is referenced by:  scaffval  19644
 Copyright terms: Public domain W3C validator