Theorem smfval

Description: Value of the function for the scalar multiplication operation on a normed complex vector space. (Contributed by NM, 24-Apr-2007) (New usage is discouraged.)

	Ref	Expression
Hypothesis	smfval.4	$$⊢S={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
Assertion	smfval	$$⊢S=2^{nd}\left(1^{st}\left(U\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		smfval.4	$$⊢S={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
2		df-sm	$$⊢{\cdot }_{\mathrm{𝑠OLD}}=2^{nd}\circ 1^{st}$$
3	2	fveq1i	$$⊢{\cdot }_{\mathrm{𝑠OLD}}\left(U\right)=\left(2^{nd}\circ 1^{st}\right)\left(U\right)$$
4		fo1st	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$
5		fof	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to 1^{st}:\mathrm{V}⟶\mathrm{V}$$
6	4 5	ax-mp	$$⊢1^{st}:\mathrm{V}⟶\mathrm{V}$$
7		fvco3	$$⊢\left(1^{st}:\mathrm{V}⟶\mathrm{V}\wedge U\in \mathrm{V}\right)\to \left(2^{nd}\circ 1^{st}\right)\left(U\right)=2^{nd}\left(1^{st}\left(U\right)\right)$$
8	6 7	mpan	$$⊢U\in \mathrm{V}\to \left(2^{nd}\circ 1^{st}\right)\left(U\right)=2^{nd}\left(1^{st}\left(U\right)\right)$$
9	3 8	syl5eq	$$⊢U\in \mathrm{V}\to {\cdot }_{\mathrm{𝑠OLD}}\left(U\right)=2^{nd}\left(1^{st}\left(U\right)\right)$$
10		fvprc	$$⊢\neg U\in \mathrm{V}\to {\cdot }_{\mathrm{𝑠OLD}}\left(U\right)=\varnothing$$
11		fvprc	$$⊢\neg U\in \mathrm{V}\to 1^{st}\left(U\right)=\varnothing$$
12	11	fveq2d	$$⊢\neg U\in \mathrm{V}\to 2^{nd}\left(1^{st}\left(U\right)\right)=2^{nd}\left(\varnothing \right)$$
13		2nd0	$$⊢2^{nd}\left(\varnothing \right)=\varnothing$$
14	12 13	eqtr2di	$$⊢\neg U\in \mathrm{V}\to \varnothing =2^{nd}\left(1^{st}\left(U\right)\right)$$
15	10 14	eqtrd	$$⊢\neg U\in \mathrm{V}\to {\cdot }_{\mathrm{𝑠OLD}}\left(U\right)=2^{nd}\left(1^{st}\left(U\right)\right)$$
16	9 15	pm2.61i	$$⊢{\cdot }_{\mathrm{𝑠OLD}}\left(U\right)=2^{nd}\left(1^{st}\left(U\right)\right)$$
17	1 16	eqtri	$$⊢S=2^{nd}\left(1^{st}\left(U\right)\right)$$