Definition df-pws 17169

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

Step	Hyp	Ref	Expression
1		cpws 17166	. 2 class ↑s
2		vr	. . 3 setvar 𝑟
3		vi	. . 3 setvar 𝑖
4		cvv 3433	. . 3 class V
5	2	cv 1538	. . . . 5 class 𝑟
6		csca 16974	. . . . 5 class Scalar
7	5, 6	cfv 6437	. . . 4 class (Scalar‘𝑟)
8	3	cv 1538	. . . . 5 class 𝑖
9	5	csn 4562	. . . . 5 class {𝑟}
10	8, 9	cxp 5588	. . . 4 class (𝑖 × {𝑟})
11		cprds 17165	. . . 4 class Xs
12	7, 10, 11	co 7284	. . 3 class ((Scalar‘𝑟)Xs(𝑖 × {𝑟}))
13	2, 3, 4, 4, 12	cmpo 7286	. 2 class (𝑟 ∈ V, 𝑖 ∈ V ↦ ((Scalar‘𝑟)Xs(𝑖 × {𝑟})))
14	1, 13	wceq 1539	1 wff ↑s = (𝑟 ∈ V, 𝑖 ∈ V ↦ ((Scalar‘𝑟)Xs(𝑖 × {𝑟})))

This definition is referenced by:  pwsval  17206