Theorem hhssvsf

Description: Mapping of the vector subtraction operation on a subspace. (Contributed by NM, 10-Apr-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hhsssh2.1	$$⊢W=⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩,{{norm}_{ℎ}\upharpoonright }_H⟩$$
	hhssba.2	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}$$
Assertion	hhssvsf	$$⊢\left({{-}_{ℎ}\upharpoonright }_{\left(H\times H\right)}\right):H\times H⟶H$$

Proof

Step	Hyp	Ref	Expression
1		hhsssh2.1	$$⊢W=⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩,{{norm}_{ℎ}\upharpoonright }_H⟩$$
2		hhssba.2	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}$$
3	1 2	hhssnv	$$⊢W\in \mathrm{NrmCVec}$$
4	1 2	hhssba	$$⊢H=\mathrm{BaseSet}\left(W\right)$$
5	1 2	hhssvs	$$⊢{{-}_{ℎ}\upharpoonright }_{\left(H\times H\right)}={-}_v\left(W\right)$$
6	4 5	nvmf	$$⊢W\in \mathrm{NrmCVec}\to \left({{-}_{ℎ}\upharpoonright }_{\left(H\times H\right)}\right):H\times H⟶H$$
7	3 6	ax-mp	$$⊢\left({{-}_{ℎ}\upharpoonright }_{\left(H\times H\right)}\right):H\times H⟶H$$