Definition df-pws 12701

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 12698	. 2 class ^s
2		vr	. . 3 setvar r
3		vi	. . 3 setvar i
4		cvv 2737	. . 3 class _V
5	2	cv 1352	. . . . 5 class r
6		csca 12529	. . . . 5 class Scalar
7	5, 6	cfv 5213	. . . 4 class (Scalar ` r )
8	3	cv 1352	. . . . 5 class i
9	5	csn 3592	. . . . 5 class { r }
10	8, 9	cxp 4622	. . . 4 class ( i X. { r } )
11		cprds 12697	. . . 4 class X_s
12	7, 10, 11	co 5870	. . 3 class ( (Scalar ` r ) X_s ( i X. { r } ) )
13	2, 3, 4, 4, 12	cmpo 5872	. 2 class ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
14	1, 13	wceq 1353	1 wff ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )

This definition is referenced by: (None)