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 = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.
	hhssba.2	|- H e. SH
Assertion	hhssba	|- H = ( BaseSet ` W )

Proof

Step	Hyp	Ref	Expression
1		hhsssh2.1	|- W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.
2		hhssba.2	|- H e. SH
3		eqid	|- <. <. +h , .h >. , normh >. = <. <. +h , .h >. , normh >.
4	3 1	hhsst	|- ( H e. SH -> W e. ( SubSp ` <. <. +h , .h >. , normh >. ) )
5	2 4	ax-mp	|- W e. ( SubSp ` <. <. +h , .h >. , normh >. )
6	2	shssii	|- H C_ ~H
7	3 1 5 6	hhshsslem1	|- H = ( BaseSet ` W )