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

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
StepHypRef 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 𝑦
62cv 1539 . . . . . 6 class 𝑔
7 csca 17300 . . . . . 6 class Scalar
86, 7cfv 6561 . . . . 5 class (Scalar‘𝑔)
9 cbs 17247 . . . . 5 class Base
108, 9cfv 6561 . . . 4 class (Base‘(Scalar‘𝑔))
116, 9cfv 6561 . . . 4 class (Base‘𝑔)
124cv 1539 . . . . 5 class 𝑥
135cv 1539 . . . . 5 class 𝑦
14 cvsca 17301 . . . . . 6 class ·𝑠
156, 14cfv 6561 . . . . 5 class ( ·𝑠𝑔)
1612, 13, 15co 7431 . . . 4 class (𝑥( ·𝑠𝑔)𝑦)
174, 5, 10, 11, 16cmpo 7433 . . 3 class (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠𝑔)𝑦))
182, 3, 17cmpt 5225 . 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠𝑔)𝑦)))
191, 18wceq 1540 1 wff ·sf = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠𝑔)𝑦)))
Colors of variables: wff setvar class
This definition is referenced by:  scaffval  20878
  Copyright terms: Public domain W3C validator