This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H
hhssba.2 ⊢ H ∈ S ℋ
Assertion hhssba ⊢ H = BaseSet ⁡ W

Proof

Step Hyp Ref Expression
1 hhsssh2.1 ⊢ W = + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H
2 hhssba.2 ⊢ H ∈ S ℋ
3 eqid ⊢ + ℎ ⋅ ℎ norm ℎ = + ℎ ⋅ ℎ norm ℎ
4 3 1 hhsst ⊢ H ∈ S ℋ → W ∈ SubSp ⁡ + ℎ ⋅ ℎ norm ℎ
5 2 4 ax-mp ⊢ W ∈ SubSp ⁡ + ℎ ⋅ ℎ norm ℎ
6 2 shssii ⊢ H ⊆ ℋ
7 3 1 5 6 hhshsslem1 ⊢ H = BaseSet ⁡ W