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 ↑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 ( 𝑖 × { 𝑟 } ) ) )