Definition df-pws 12992

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 12968	. 2 class ^s
2		vr	. . 3 setvar r
3		vi	. . 3 setvar i
4		cvv 2763	. . 3 class _V
5	2	cv 1363	. . . . 5 class r
6		csca 12783	. . . . 5 class Scalar
7	5, 6	cfv 5259	. . . 4 class (Scalar ` r )
8	3	cv 1363	. . . . 5 class i
9	5	csn 3623	. . . . 5 class { r }
10	8, 9	cxp 4662	. . . 4 class ( i X. { r } )
11		cprds 12967	. . . 4 class X_s
12	7, 10, 11	co 5925	. . 3 class ( (Scalar ` r ) X_s ( i X. { r } ) )
13	2, 3, 4, 4, 12	cmpo 5927	. 2 class ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
14	1, 13	wceq 1364	1 wff ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )

This definition is referenced by:  pwsval  12993