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 ⊢ W = + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H
Assertion hhssnm ⊢ norm ℎ ↾ H = norm CV ⁡ W

Proof

Step Hyp Ref Expression
1 hhss.1 ⊢ W = + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H
2 eqid ⊢ norm CV ⁡ W = norm CV ⁡ W
3 2 nmcvfval ⊢ norm CV ⁡ W = 2 nd ⁡ W
4 1 fveq2i ⊢ 2 nd ⁡ W = 2 nd ⁡ + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H
5 opex ⊢ + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H ∈ 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 ℎ ↾ H ∈ V
11 5 10 op2nd ⊢ 2 nd ⁡ + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H = norm ℎ ↾ H
12 3 4 11 3eqtrri ⊢ norm ℎ ↾ H = norm CV ⁡ W