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

Definition df-pws 15882
Description: Define a structure power, which is just a structure product where all the factors are the same. (Contributed by Mario Carneiro, 11-Jan-2015.)
Assertion
Ref Expression
df-pws s = (𝑟 ∈ V, 𝑖 ∈ V ↦ ((Scalar‘𝑟)Xs(𝑖 × {𝑟})))
Distinct variable group:   𝑖,𝑟

Detailed syntax breakdown of Definition df-pws
StepHypRef Expression
1 cpws 15879 . 2 class s
2 vr . . 3 setvar 𝑟
3 vi . . 3 setvar 𝑖
4 cvv 3172 . . 3 class V
52cv 1473 . . . . 5 class 𝑟
6 csca 15720 . . . . 5 class Scalar
75, 6cfv 5790 . . . 4 class (Scalar‘𝑟)
83cv 1473 . . . . 5 class 𝑖
95csn 4124 . . . . 5 class {𝑟}
108, 9cxp 5026 . . . 4 class (𝑖 × {𝑟})
11 cprds 15878 . . . 4 class Xs
127, 10, 11co 6527 . . 3 class ((Scalar‘𝑟)Xs(𝑖 × {𝑟}))
132, 3, 4, 4, 12cmpt2 6529 . 2 class (𝑟 ∈ V, 𝑖 ∈ V ↦ ((Scalar‘𝑟)Xs(𝑖 × {𝑟})))
141, 13wceq 1474 1 wff s = (𝑟 ∈ V, 𝑖 ∈ V ↦ ((Scalar‘𝑟)Xs(𝑖 × {𝑟})))
Colors of variables: wff setvar class
This definition is referenced by:  pwsval  15918
  Copyright terms: Public domain W3C validator