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 18787
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 18785 . 2 class ·sf
2 vg . . 3 setvar 𝑔
3 cvv 3186 . . 3 class V
4 vx . . . 4 setvar 𝑥
5 vy . . . 4 setvar 𝑦
62cv 1479 . . . . . 6 class 𝑔
7 csca 15865 . . . . . 6 class Scalar
86, 7cfv 5847 . . . . 5 class (Scalar‘𝑔)
9 cbs 15781 . . . . 5 class Base
108, 9cfv 5847 . . . 4 class (Base‘(Scalar‘𝑔))
116, 9cfv 5847 . . . 4 class (Base‘𝑔)
124cv 1479 . . . . 5 class 𝑥
135cv 1479 . . . . 5 class 𝑦
14 cvsca 15866 . . . . . 6 class ·𝑠
156, 14cfv 5847 . . . . 5 class ( ·𝑠𝑔)
1612, 13, 15co 6604 . . . 4 class (𝑥( ·𝑠𝑔)𝑦)
174, 5, 10, 11, 16cmpt2 6606 . . 3 class (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠𝑔)𝑦))
182, 3, 17cmpt 4673 . 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠𝑔)𝑦)))
191, 18wceq 1480 1 wff ·sf = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠𝑔)𝑦)))
Colors of variables: wff setvar class
This definition is referenced by:  scaffval  18802
  Copyright terms: Public domain W3C validator