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

Metamath Proof Explorer

Theorem sspm

Description: Vector subtraction on a subspace is a restriction of vector subtraction on the parent space. (Contributed by NM, 28-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses sspm.y ⊢ Y = BaseSet ⁡ W
sspm.m ⊢ M = - v ⁡ U
sspm.l ⊢ L = - v ⁡ W
sspm.h ⊢ H = SubSp ⁡ U
Assertion sspm ⊢ U ∈ NrmCVec ∧ W ∈ H → L = M ↾ Y × Y

Proof

Step Hyp Ref Expression
1 sspm.y ⊢ Y = BaseSet ⁡ W
2 sspm.m ⊢ M = - v ⁡ U
3 sspm.l ⊢ L = - v ⁡ W
4 sspm.h ⊢ H = SubSp ⁡ U
5 1 2 3 4 sspmval ⊢ U ∈ NrmCVec ∧ W ∈ H ∧ x ∈ Y ∧ y ∈ Y → x L y = x M y
6 1 3 nvmf ⊢ W ∈ NrmCVec → L : Y × Y ⟶ Y
7 eqid ⊢ BaseSet ⁡ U = BaseSet ⁡ U
8 7 2 nvmf ⊢ U ∈ NrmCVec → M : BaseSet ⁡ U × BaseSet ⁡ U ⟶ BaseSet ⁡ U
9 1 4 5 6 8 sspmlem ⊢ U ∈ NrmCVec ∧ W ∈ H → L = M ↾ Y × Y