Theorem hhssba

Description: The base set of 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	hhssba	$$⊢H=\mathrm{BaseSet}\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 1	hhsst	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}\to W\in \mathrm{SubSp}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
5	2 4	ax-mp	$$⊢W\in \mathrm{SubSp}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
6	2	shssii	$$⊢H\subseteq \mathscr{H}$$
7	3 1 5 6	hhshsslem1	$$⊢H=\mathrm{BaseSet}\left(W\right)$$