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

Metamath Proof Explorer

Theorem hhssvs

Description: 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 hhssvs ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) = ( −𝑣 ‘ 𝑊 )

Proof

Step Hyp Ref Expression
1 hhsssh2.1 ⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
2 hhssba.2 ⊢ 𝐻 ∈ Sℋ
3 eqid ⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
4 3 hhnv ⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ NrmCVec
5 3 1 hhsst ⊢ ( 𝐻 ∈ Sℋ → 𝑊 ∈ ( SubSp ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) )
6 2 5 ax-mp ⊢ 𝑊 ∈ ( SubSp ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
7 1 2 hhssba ⊢ 𝐻 = ( BaseSet ‘ 𝑊 )
8 3 hhvs ⊢ −ℎ = ( −𝑣 ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
9 eqid ⊢ ( −𝑣 ‘ 𝑊 ) = ( −𝑣 ‘ 𝑊 )
10 eqid ⊢ ( SubSp ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) = ( SubSp ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
11 7 8 9 10 sspm ⊢ ( ( ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ NrmCVec ∧ 𝑊 ∈ ( SubSp ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ) → ( −𝑣 ‘ 𝑊 ) = ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) )
12 4 6 11 mp2an ⊢ ( −𝑣 ‘ 𝑊 ) = ( −ℎ ↾ ( 𝐻 × 𝐻 ) )
13 12 eqcomi ⊢ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) = ( −𝑣 ‘ 𝑊 )