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