Theorem hhsssm

Description: The scalar multiplication operation on a subspace. (Contributed by NM, 8-Apr-2008) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hhss.1	$$⊢W=⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩,{{norm}_{ℎ}\upharpoonright }_H⟩$$
Assertion	hhsssm	$$⊢{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}={\cdot }_{\mathrm{𝑠OLD}}\left(W\right)$$

Proof

Step	Hyp	Ref	Expression
1		hhss.1	$$⊢W=⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩,{{norm}_{ℎ}\upharpoonright }_H⟩$$
2		eqid	$$⊢{\cdot }_{\mathrm{𝑠OLD}}\left(W\right)={\cdot }_{\mathrm{𝑠OLD}}\left(W\right)$$
3	2	smfval	$$⊢{\cdot }_{\mathrm{𝑠OLD}}\left(W\right)=2^{nd}\left(1^{st}\left(W\right)\right)$$
4	1	fveq2i	$$⊢1^{st}\left(W\right)=1^{st}\left(⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩,{{norm}_{ℎ}\upharpoonright }_H⟩\right)$$
5		opex	$$⊢⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩\in \mathrm{V}$$
6		normf	$$⊢{norm}_{ℎ}:\mathscr{H}⟶ℝ$$
7		ax-hilex	$$⊢\mathscr{H}\in \mathrm{V}$$
8		fex	$$⊢\left({norm}_{ℎ}:\mathscr{H}⟶ℝ\wedge \mathscr{H}\in \mathrm{V}\right)\to {norm}_{ℎ}\in \mathrm{V}$$
9	6 7 8	mp2an	$$⊢{norm}_{ℎ}\in \mathrm{V}$$
10	9	resex	$$⊢{{norm}_{ℎ}\upharpoonright }_H\in \mathrm{V}$$
11	5 10	op1st	$$⊢1^{st}\left(⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩,{{norm}_{ℎ}\upharpoonright }_H⟩\right)=⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩$$
12	4 11	eqtri	$$⊢1^{st}\left(W\right)=⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩$$
13	12	fveq2i	$$⊢2^{nd}\left(1^{st}\left(W\right)\right)=2^{nd}\left(⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩\right)$$
14		hilablo	$$⊢{+}_{ℎ}\in \mathrm{AbelOp}$$
15		resexg	$$⊢{+}_{ℎ}\in \mathrm{AbelOp}\to {{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)}\in \mathrm{V}$$
16	14 15	ax-mp	$$⊢{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)}\in \mathrm{V}$$
17		hvmulex	$$⊢{\cdot }_{ℎ}\in \mathrm{V}$$
18	17	resex	$$⊢{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}\in \mathrm{V}$$
19	16 18	op2nd	$$⊢2^{nd}\left(⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩\right)={{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}$$
20	3 13 19	3eqtrri	$$⊢{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}={\cdot }_{\mathrm{𝑠OLD}}\left(W\right)$$