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 = ( 𝑟 ∈ V , 𝑖 ∈ V ↦ ( ( Scalar ‘ 𝑟 ) Xs ( 𝑖 × { 𝑟 } ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpws	⊢ ↑s
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		vi	⊢ 𝑖
4		csca	⊢ Scalar
5	1	cv	⊢ 𝑟
6	5 4	cfv	⊢ ( Scalar ‘ 𝑟 )
7		cprds	⊢ Xs
8	3	cv	⊢ 𝑖
9	5	csn	⊢ { 𝑟 }
10	8 9	cxp	⊢ ( 𝑖 × { 𝑟 } )
11	6 10 7	co	⊢ ( ( Scalar ‘ 𝑟 ) Xs ( 𝑖 × { 𝑟 } ) )
12	1 3 2 2 11	cmpo	⊢ ( 𝑟 ∈ V , 𝑖 ∈ V ↦ ( ( Scalar ‘ 𝑟 ) Xs ( 𝑖 × { 𝑟 } ) ) )
13	0 12	wceq	⊢ ↑s = ( 𝑟 ∈ V , 𝑖 ∈ V ↦ ( ( Scalar ‘ 𝑟 ) Xs ( 𝑖 × { 𝑟 } ) ) )