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

Metamath Proof Explorer

Theorem hhssvsf

Description: Mapping of the vector subtraction operation on a subspace. (Contributed by NM, 10-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypotheses hhsssh2.1 ⊢ W = + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H
hhssba.2 ⊢ H ∈ S ℋ
Assertion hhssvsf ⊢ - ℎ ↾ H × H : H × H ⟶ H

Proof

Step Hyp Ref Expression
1 hhsssh2.1 ⊢ W = + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H
2 hhssba.2 ⊢ H ∈ S ℋ
3 1 2 hhssnv ⊢ W ∈ NrmCVec
4 1 2 hhssba ⊢ H = BaseSet ⁡ W
5 1 2 hhssvs ⊢ - ℎ ↾ H × H = - v ⁡ W
6 4 5 nvmf ⊢ W ∈ NrmCVec → - ℎ ↾ H × H : H × H ⟶ H
7 3 6 ax-mp ⊢ - ℎ ↾ H × H : H × H ⟶ H