Definition df-pws 13375

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 13351	. 2 class ^s
2		vr	. . 3 setvar r
3		vi	. . 3 setvar i
4		cvv 2802	. . 3 class _V
5	2	cv 1396	. . . . 5 class r
6		csca 13165	. . . . 5 class Scalar
7	5, 6	cfv 5326	. . . 4 class (Scalar ` r )
8	3	cv 1396	. . . . 5 class i
9	5	csn 3669	. . . . 5 class { r }
10	8, 9	cxp 4723	. . . 4 class ( i X. { r } )
11		cprds 13350	. . . 4 class X_s
12	7, 10, 11	co 6018	. . 3 class ( (Scalar ` r ) X_s ( i X. { r } ) )
13	2, 3, 4, 4, 12	cmpo 6020	. 2 class ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
14	1, 13	wceq 1397	1 wff ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )

This definition is referenced by:  pwsval  13376