Theorem pwssca

Description: The ring of scalars of a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Hypotheses	pwssca.y	$$⊢Y=R{\uparrow }_{𝑠}I$$
	pwssca.s	$$⊢S=\mathrm{Scalar}\left(R\right)$$
Assertion	pwssca	$$⊢\left(R\in V\wedge I\in W\right)\to S=\mathrm{Scalar}\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		pwssca.y	$$⊢Y=R{\uparrow }_{𝑠}I$$
2		pwssca.s	$$⊢S=\mathrm{Scalar}\left(R\right)$$
3		eqid	$$⊢S{⨉}_{𝑠}\left(I\times \left\{R\right\}\right)=S{⨉}_{𝑠}\left(I\times \left\{R\right\}\right)$$
4	2	fvexi	$$⊢S\in \mathrm{V}$$
5	4	a1i	$$⊢\left(R\in V\wedge I\in W\right)\to S\in \mathrm{V}$$
6		simpr	$$⊢\left(R\in V\wedge I\in W\right)\to I\in W$$
7		snex	$$⊢\left\{R\right\}\in \mathrm{V}$$
8		xpexg	$$⊢\left(I\in W\wedge \left\{R\right\}\in \mathrm{V}\right)\to I\times \left\{R\right\}\in \mathrm{V}$$
9	6 7 8	sylancl	$$⊢\left(R\in V\wedge I\in W\right)\to I\times \left\{R\right\}\in \mathrm{V}$$
10	3 5 9	prdssca	$$⊢\left(R\in V\wedge I\in W\right)\to S=\mathrm{Scalar}\left(S{⨉}_{𝑠}\left(I\times \left\{R\right\}\right)\right)$$
11	1 2	pwsval	$$⊢\left(R\in V\wedge I\in W\right)\to Y=S{⨉}_{𝑠}\left(I\times \left\{R\right\}\right)$$
12	11	fveq2d	$$⊢\left(R\in V\wedge I\in W\right)\to \mathrm{Scalar}\left(Y\right)=\mathrm{Scalar}\left(S{⨉}_{𝑠}\left(I\times \left\{R\right\}\right)\right)$$
13	10 12	eqtr4d	$$⊢\left(R\in V\wedge I\in W\right)\to S=\mathrm{Scalar}\left(Y\right)$$