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 ⊢ W = + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H
hhssba.2 ⊢ H ∈ S ℋ
Assertion hhssvs ⊢ - ℎ ↾ H × H = - v ⁡ W

Proof

Step Hyp Ref Expression
1 hhsssh2.1 ⊢ W = + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H
2 hhssba.2 ⊢ H ∈ S ℋ
3 eqid ⊢ + ℎ ⋅ ℎ norm ℎ = + ℎ ⋅ ℎ norm ℎ
4 3 hhnv ⊢ + ℎ ⋅ ℎ norm ℎ ∈ NrmCVec
5 3 1 hhsst ⊢ H ∈ S ℋ → W ∈ SubSp ⁡ + ℎ ⋅ ℎ norm ℎ
6 2 5 ax-mp ⊢ W ∈ SubSp ⁡ + ℎ ⋅ ℎ norm ℎ
7 1 2 hhssba ⊢ H = BaseSet ⁡ W
8 3 hhvs ⊢ - ℎ = - v ⁡ + ℎ ⋅ ℎ norm ℎ
9 eqid ⊢ - v ⁡ W = - v ⁡ W
10 eqid ⊢ SubSp ⁡ + ℎ ⋅ ℎ norm ℎ = SubSp ⁡ + ℎ ⋅ ℎ norm ℎ
11 7 8 9 10 sspm ⊢ + ℎ ⋅ ℎ norm ℎ ∈ NrmCVec ∧ W ∈ SubSp ⁡ + ℎ ⋅ ℎ norm ℎ → - v ⁡ W = - ℎ ↾ H × H
12 4 6 11 mp2an ⊢ - v ⁡ W = - ℎ ↾ H × H
13 12 eqcomi ⊢ - ℎ ↾ H × H = - v ⁡ W