This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Detailed syntax breakdown

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