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

Metamath Proof Explorer

Theorem sspnval

Description: The norm on a subspace in terms of the norm on the parent space. (Contributed by NM, 28-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses sspn.y ⊢ Y = BaseSet ⁡ W
sspn.n ⊢ N = norm CV ⁡ U
sspn.m ⊢ M = norm CV ⁡ W
sspn.h ⊢ H = SubSp ⁡ U
Assertion sspnval ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A ∈ Y → M ⁡ A = N ⁡ A

Proof

Step Hyp Ref Expression
1 sspn.y ⊢ Y = BaseSet ⁡ W
2 sspn.n ⊢ N = norm CV ⁡ U
3 sspn.m ⊢ M = norm CV ⁡ W
4 sspn.h ⊢ H = SubSp ⁡ U
5 1 2 3 4 sspn ⊢ U ∈ NrmCVec ∧ W ∈ H → M = N ↾ Y
6 5 fveq1d ⊢ U ∈ NrmCVec ∧ W ∈ H → M ⁡ A = N ↾ Y ⁡ A
7 fvres ⊢ A ∈ Y → N ↾ Y ⁡ A = N ⁡ A
8 6 7 sylan9eq ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A ∈ Y → M ⁡ A = N ⁡ A
9 8 3impa ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ A ∈ Y → M ⁡ A = N ⁡ A