Definition df-pws 13155

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 = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )

Distinct variable group:   i, r

Detailed syntax breakdown of Definition df-pws

Step	Hyp	Ref	Expression
1		cpws 13131	. 2 class ^s
2		vr	. . 3 setvar r
3		vi	. . 3 setvar i
4		cvv 2772	. . 3 class _V
5	2	cv 1372	. . . . 5 class r
6		csca 12945	. . . . 5 class Scalar
7	5, 6	cfv 5272	. . . 4 class (Scalar ` r )
8	3	cv 1372	. . . . 5 class i
9	5	csn 3633	. . . . 5 class { r }
10	8, 9	cxp 4674	. . . 4 class ( i X. { r } )
11		cprds 13130	. . . 4 class X_s
12	7, 10, 11	co 5946	. . 3 class ( (Scalar ` r ) X_s ( i X. { r } ) )
13	2, 3, 4, 4, 12	cmpo 5948	. 2 class ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
14	1, 13	wceq 1373	1 wff ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )

This definition is referenced by:  pwsval  13156