# Metamath Proof Explorer

## Theorem pwsval

Description: Value of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015)

Ref Expression
Hypotheses pwsval.y ${⊢}{Y}={R}{↑}_{𝑠}{I}$
pwsval.f ${⊢}{F}=\mathrm{Scalar}\left({R}\right)$
Assertion pwsval ${⊢}\left({R}\in {V}\wedge {I}\in {W}\right)\to {Y}={F}{⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)$

### Proof

Step Hyp Ref Expression
1 pwsval.y ${⊢}{Y}={R}{↑}_{𝑠}{I}$
2 pwsval.f ${⊢}{F}=\mathrm{Scalar}\left({R}\right)$
3 elex ${⊢}{R}\in {V}\to {R}\in \mathrm{V}$
4 elex ${⊢}{I}\in {W}\to {I}\in \mathrm{V}$
5 simpl ${⊢}\left({r}={R}\wedge {i}={I}\right)\to {r}={R}$
6 5 fveq2d ${⊢}\left({r}={R}\wedge {i}={I}\right)\to \mathrm{Scalar}\left({r}\right)=\mathrm{Scalar}\left({R}\right)$
7 6 2 syl6eqr ${⊢}\left({r}={R}\wedge {i}={I}\right)\to \mathrm{Scalar}\left({r}\right)={F}$
8 id ${⊢}{i}={I}\to {i}={I}$
9 sneq ${⊢}{r}={R}\to \left\{{r}\right\}=\left\{{R}\right\}$
10 xpeq12 ${⊢}\left({i}={I}\wedge \left\{{r}\right\}=\left\{{R}\right\}\right)\to {i}×\left\{{r}\right\}={I}×\left\{{R}\right\}$
11 8 9 10 syl2anr ${⊢}\left({r}={R}\wedge {i}={I}\right)\to {i}×\left\{{r}\right\}={I}×\left\{{R}\right\}$
12 7 11 oveq12d ${⊢}\left({r}={R}\wedge {i}={I}\right)\to \mathrm{Scalar}\left({r}\right){⨉}_{𝑠}\left({i}×\left\{{r}\right\}\right)={F}{⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)$
13 df-pws ${⊢}{↑}_{𝑠}=\left({r}\in \mathrm{V},{i}\in \mathrm{V}⟼\mathrm{Scalar}\left({r}\right){⨉}_{𝑠}\left({i}×\left\{{r}\right\}\right)\right)$
14 ovex ${⊢}{F}{⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)\in \mathrm{V}$
15 12 13 14 ovmpoa ${⊢}\left({R}\in \mathrm{V}\wedge {I}\in \mathrm{V}\right)\to {R}{↑}_{𝑠}{I}={F}{⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)$
16 3 4 15 syl2an ${⊢}\left({R}\in {V}\wedge {I}\in {W}\right)\to {R}{↑}_{𝑠}{I}={F}{⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)$
17 1 16 syl5eq ${⊢}\left({R}\in {V}\wedge {I}\in {W}\right)\to {Y}={F}{⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)$