Theorem hhssvs

Description: 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	hhssvs	$$⊢{{-}_{ℎ}\upharpoonright }_{\left(H\times H\right)}={-}_v\left(W\right)$$

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		eqid	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
4	3	hhnv	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\in \mathrm{NrmCVec}$$
5	3 1	hhsst	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}\to W\in \mathrm{SubSp}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
6	2 5	ax-mp	$$⊢W\in \mathrm{SubSp}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
7	1 2	hhssba	$$⊢H=\mathrm{BaseSet}\left(W\right)$$
8	3	hhvs	$$⊢{-}_{ℎ}={-}_v\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
9		eqid	$$⊢{-}_v\left(W\right)={-}_v\left(W\right)$$
10		eqid	$$⊢\mathrm{SubSp}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)=\mathrm{SubSp}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
11	7 8 9 10	sspm	$$⊢\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\in \mathrm{NrmCVec}\wedge W\in \mathrm{SubSp}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\to {-}_v\left(W\right)={{-}_{ℎ}\upharpoonright }_{\left(H\times H\right)}$$
12	4 6 11	mp2an	$$⊢{-}_v\left(W\right)={{-}_{ℎ}\upharpoonright }_{\left(H\times H\right)}$$
13	12	eqcomi	$$⊢{{-}_{ℎ}\upharpoonright }_{\left(H\times H\right)}={-}_v\left(W\right)$$