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 19076
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 19074 . 2 class ·sf
2 vg . . 3 setvar 𝑔
3 cvv 3351 . . 3 class V
4 vx . . . 4 setvar 𝑥
5 vy . . . 4 setvar 𝑦
62cv 1630 . . . . . 6 class 𝑔
7 csca 16152 . . . . . 6 class Scalar
86, 7cfv 6031 . . . . 5 class (Scalar‘𝑔)
9 cbs 16064 . . . . 5 class Base
108, 9cfv 6031 . . . 4 class (Base‘(Scalar‘𝑔))
116, 9cfv 6031 . . . 4 class (Base‘𝑔)
124cv 1630 . . . . 5 class 𝑥
135cv 1630 . . . . 5 class 𝑦
14 cvsca 16153 . . . . . 6 class ·𝑠
156, 14cfv 6031 . . . . 5 class ( ·𝑠𝑔)
1612, 13, 15co 6793 . . . 4 class (𝑥( ·𝑠𝑔)𝑦)
174, 5, 10, 11, 16cmpt2 6795 . . 3 class (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠𝑔)𝑦))
182, 3, 17cmpt 4863 . 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠𝑔)𝑦)))
191, 18wceq 1631 1 wff ·sf = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠𝑔)𝑦)))
Colors of variables: wff setvar class
This definition is referenced by:  scaffval  19091
  Copyright terms: Public domain W3C validator