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 20341
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 20339 . 2 class Β·sf
2 vg . . 3 setvar 𝑔
3 cvv 3448 . . 3 class V
4 vx . . . 4 setvar π‘₯
5 vy . . . 4 setvar 𝑦
62cv 1541 . . . . . 6 class 𝑔
7 csca 17143 . . . . . 6 class Scalar
86, 7cfv 6501 . . . . 5 class (Scalarβ€˜π‘”)
9 cbs 17090 . . . . 5 class Base
108, 9cfv 6501 . . . 4 class (Baseβ€˜(Scalarβ€˜π‘”))
116, 9cfv 6501 . . . 4 class (Baseβ€˜π‘”)
124cv 1541 . . . . 5 class π‘₯
135cv 1541 . . . . 5 class 𝑦
14 cvsca 17144 . . . . . 6 class ·𝑠
156, 14cfv 6501 . . . . 5 class ( ·𝑠 β€˜π‘”)
1612, 13, 15co 7362 . . . 4 class (π‘₯( ·𝑠 β€˜π‘”)𝑦)
174, 5, 10, 11, 16cmpo 7364 . . 3 class (π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘”)), 𝑦 ∈ (Baseβ€˜π‘”) ↦ (π‘₯( ·𝑠 β€˜π‘”)𝑦))
182, 3, 17cmpt 5193 . 2 class (𝑔 ∈ V ↦ (π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘”)), 𝑦 ∈ (Baseβ€˜π‘”) ↦ (π‘₯( ·𝑠 β€˜π‘”)𝑦)))
191, 18wceq 1542 1 wff Β·sf = (𝑔 ∈ V ↦ (π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘”)), 𝑦 ∈ (Baseβ€˜π‘”) ↦ (π‘₯( ·𝑠 β€˜π‘”)𝑦)))
Colors of variables: wff setvar class
This definition is referenced by:  scaffval  20356
  Copyright terms: Public domain W3C validator