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

Metamath Proof Explorer

Theorem hhsst

Description: A member of SH is a subspace. (Contributed by NM, 6-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypotheses hhsst.1 ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
hhsst.2 ⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
Assertion hhsst ( 𝐻 ∈ Sℋ → 𝑊 ∈ ( SubSp ‘ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 hhsst.1 ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2 hhsst.2 ⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
3 2 hhssnvt ⊢ ( 𝐻 ∈ Sℋ → 𝑊 ∈ NrmCVec )
4 resss ⊢ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ +ℎ
5 resss ⊢ ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⊆ ·ℎ
6 resss ⊢ ( normℎ ↾ 𝐻 ) ⊆ normℎ
7 4 5 6 3pm3.2i ⊢ ( ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ +ℎ ∧ ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⊆ ·ℎ ∧ ( normℎ ↾ 𝐻 ) ⊆ normℎ )
8 3 7 jctir ⊢ ( 𝐻 ∈ Sℋ → ( 𝑊 ∈ NrmCVec ∧ ( ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ +ℎ ∧ ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⊆ ·ℎ ∧ ( normℎ ↾ 𝐻 ) ⊆ normℎ ) ) )
9 1 hhnv ⊢ 𝑈 ∈ NrmCVec
10 1 hhva ⊢ +ℎ = ( +𝑣 ‘ 𝑈 )
11 2 hhssva ⊢ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) = ( +𝑣 ‘ 𝑊 )
12 1 hhsm ⊢ ·ℎ = ( ·𝑠OLD ‘ 𝑈 )
13 2 hhsssm ⊢ ( ·ℎ ↾ ( ℂ × 𝐻 ) ) = ( ·𝑠OLD ‘ 𝑊 )
14 1 hhnm ⊢ normℎ = ( normCV ‘ 𝑈 )
15 2 hhssnm ⊢ ( normℎ ↾ 𝐻 ) = ( normCV ‘ 𝑊 )
16 eqid ⊢ ( SubSp ‘ 𝑈 ) = ( SubSp ‘ 𝑈 )
17 10 11 12 13 14 15 16 isssp ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ↔ ( 𝑊 ∈ NrmCVec ∧ ( ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ +ℎ ∧ ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⊆ ·ℎ ∧ ( normℎ ↾ 𝐻 ) ⊆ normℎ ) ) ) )
18 9 17 ax-mp ⊢ ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ↔ ( 𝑊 ∈ NrmCVec ∧ ( ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ +ℎ ∧ ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⊆ ·ℎ ∧ ( normℎ ↾ 𝐻 ) ⊆ normℎ ) ) )
19 8 18 sylibr ⊢ ( 𝐻 ∈ Sℋ → 𝑊 ∈ ( SubSp ‘ 𝑈 ) )