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