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 𝑊 = ⟨ ⟨ ( + ↾ ( 𝐻 × 𝐻 ) ) , ( · ↾ ( ℂ × 𝐻 ) ) ⟩ , ( norm𝐻 ) ⟩
hhssba.2 𝐻S
Assertion hhssvsf ( − ↾ ( 𝐻 × 𝐻 ) ) : ( 𝐻 × 𝐻 ) ⟶ 𝐻

Proof

Step Hyp Ref Expression
1 hhsssh2.1 𝑊 = ⟨ ⟨ ( + ↾ ( 𝐻 × 𝐻 ) ) , ( · ↾ ( ℂ × 𝐻 ) ) ⟩ , ( norm𝐻 ) ⟩
2 hhssba.2 𝐻S
3 1 2 hhssnv 𝑊 ∈ NrmCVec
4 1 2 hhssba 𝐻 = ( BaseSet ‘ 𝑊 )
5 1 2 hhssvs ( − ↾ ( 𝐻 × 𝐻 ) ) = ( −𝑣𝑊 )
6 4 5 nvmf ( 𝑊 ∈ NrmCVec → ( − ↾ ( 𝐻 × 𝐻 ) ) : ( 𝐻 × 𝐻 ) ⟶ 𝐻 )
7 3 6 ax-mp ( − ↾ ( 𝐻 × 𝐻 ) ) : ( 𝐻 × 𝐻 ) ⟶ 𝐻