Definition df-pws 16110

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 16107	. 2 class ^s
2		vr	. . 3 setvar r
3		vi	. . 3 setvar i
4		cvv 3200	. . 3 class _V
5	2	cv 1482	. . . . 5 class r
6		csca 15944	. . . . 5 class Scalar
7	5, 6	cfv 5888	. . . 4 class (Scalar ` r )
8	3	cv 1482	. . . . 5 class i
9	5	csn 4177	. . . . 5 class { r }
10	8, 9	cxp 5112	. . . 4 class ( i X. { r } )
11		cprds 16106	. . . 4 class X_s
12	7, 10, 11	co 6650	. . 3 class ( (Scalar ` r ) X_s ( i X. { r } ) )
13	2, 3, 4, 4, 12	cmpt2 6652	. 2 class ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
14	1, 13	wceq 1483	1 wff ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )

This definition is referenced by:  pwsval  16146