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

Metamath Proof Explorer

Theorem hhssnm

Description: The norm operation on a subspace. (Contributed by NM, 8-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypothesis hhss.1 ⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
Assertion hhssnm ( normℎ ↾ 𝐻 ) = ( normCV ‘ 𝑊 )

Proof

Step Hyp Ref Expression
1 hhss.1 ⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
2 eqid ⊢ ( normCV ‘ 𝑊 ) = ( normCV ‘ 𝑊 )
3 2 nmcvfval ⊢ ( normCV ‘ 𝑊 ) = ( 2nd ‘ 𝑊 )
4 1 fveq2i ⊢ ( 2nd ‘ 𝑊 ) = ( 2nd ‘ ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ )
5 opex ⊢ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ ∈ V
6 normf ⊢ normℎ : ℋ ⟶ ℝ
7 ax-hilex ⊢ ℋ ∈ V
8 fex ⊢ ( ( normℎ : ℋ ⟶ ℝ ∧ ℋ ∈ V ) → normℎ ∈ V )
9 6 7 8 mp2an ⊢ normℎ ∈ V
10 9 resex ⊢ ( normℎ ↾ 𝐻 ) ∈ V
11 5 10 op2nd ⊢ ( 2nd ‘ ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ ) = ( normℎ ↾ 𝐻 )
12 3 4 11 3eqtrri ⊢ ( normℎ ↾ 𝐻 ) = ( normCV ‘ 𝑊 )