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