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	$$⊢{\uparrow }_{𝑠}=\left(r\in \mathrm{V},i\in \mathrm{V}⟼\mathrm{Scalar}\left(r\right){⨉}_{𝑠}\left(i\times \left\{r\right\}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpws	$$class{\uparrow }_{𝑠}$$
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		vi	$$setvari$$
4		csca	$$class\mathrm{Scalar}$$
5	1	cv	$$setvarr$$
6	5 4	cfv	$$class\mathrm{Scalar}\left(r\right)$$
7		cprds	$$class{⨉}_{𝑠}$$
8	3	cv	$$setvari$$
9	5	csn	$$class\left\{r\right\}$$
10	8 9	cxp	$$class\left(i\times \left\{r\right\}\right)$$
11	6 10 7	co	$$class\left(\mathrm{Scalar}\left(r\right){⨉}_{𝑠}\left(i\times \left\{r\right\}\right)\right)$$
12	1 3 2 2 11	cmpo	$$class\left(r\in \mathrm{V},i\in \mathrm{V}⟼\mathrm{Scalar}\left(r\right){⨉}_{𝑠}\left(i\times \left\{r\right\}\right)\right)$$
13	0 12	wceq	$$wff{\uparrow }_{𝑠}=\left(r\in \mathrm{V},i\in \mathrm{V}⟼\mathrm{Scalar}\left(r\right){⨉}_{𝑠}\left(i\times \left\{r\right\}\right)\right)$$