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	⊢ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) : ( 𝐻 × 𝐻 ) ⟶ 𝐻