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𝑊 )