Theorem pwsval

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

	Ref	Expression
Hypotheses	pwsval.y	$$⊢Y=R{\uparrow }_{𝑠}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\times \left\{R\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		pwsval.y	$$⊢Y=R{\uparrow }_{𝑠}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	eqtr4di	$$⊢\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\times \left\{r\right\}=I\times \left\{R\right\}$$
11	8 9 10	syl2anr	$$⊢\left(r=R\wedge i=I\right)\to i\times \left\{r\right\}=I\times \left\{R\right\}$$
12	7 11	oveq12d	$$⊢\left(r=R\wedge i=I\right)\to \mathrm{Scalar}\left(r\right){⨉}_{𝑠}\left(i\times \left\{r\right\}\right)=F{⨉}_{𝑠}\left(I\times \left\{R\right\}\right)$$
13		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)$$
14		ovex	$$⊢F{⨉}_{𝑠}\left(I\times \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{\uparrow }_{𝑠}I=F{⨉}_{𝑠}\left(I\times \left\{R\right\}\right)$$
16	3 4 15	syl2an	$$⊢\left(R\in V\wedge I\in W\right)\to R{\uparrow }_{𝑠}I=F{⨉}_{𝑠}\left(I\times \left\{R\right\}\right)$$
17	1 16	syl5eq	$$⊢\left(R\in V\wedge I\in W\right)\to Y=F{⨉}_{𝑠}\left(I\times \left\{R\right\}\right)$$