Definition df-pws

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)

	Ref	Expression
Assertion	df-pws	|- ^s = ( r e. _V , i e. _V |-> ( ( Scalar ` r ) Xs_ ( i X. { r } ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpws	|- ^s
1		vr	|- r
2		cvv	|- _V
3		vi	|- i
4		csca	|- Scalar
5	1	cv	|- r
6	5 4	cfv	|- ( Scalar ` r )
7		cprds	|- Xs_
8	3	cv	|- i
9	5	csn	|- { r }
10	8 9	cxp	|- ( i X. { r } )
11	6 10 7	co	|- ( ( Scalar ` r ) Xs_ ( i X. { r } ) )
12	1 3 2 2 11	cmpo	|- ( r e. _V , i e. _V |-> ( ( Scalar ` r ) Xs_ ( i X. { r } ) ) )
13	0 12	wceq	|- ^s = ( r e. _V , i e. _V |-> ( ( Scalar ` r ) Xs_ ( i X. { r } ) ) )