Theorem hhssba

Description: The base set of a subspace. (Contributed by NM, 10-Apr-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hhsssh2.1	⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
	hhssba.2	⊢ 𝐻 ∈ Sℋ
Assertion	hhssba	⊢ 𝐻 = ( BaseSet ‘ 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		hhsssh2.1	⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
2		hhssba.2	⊢ 𝐻 ∈ Sℋ
3		eqid	⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
4	3 1	hhsst	⊢ ( 𝐻 ∈ Sℋ → 𝑊 ∈ ( SubSp ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) )
5	2 4	ax-mp	⊢ 𝑊 ∈ ( SubSp ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
6	2	shssii	⊢ 𝐻 ⊆ ℋ
7	3 1 5 6	hhshsslem1	⊢ 𝐻 = ( BaseSet ‘ 𝑊 )