Metamath Proof Explorer

Theorem hhsssm

Description: The scalar multiplication operation on a subspace. (Contributed by NM, 8-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypothesis hhss.1 ⊢ W = + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H
Assertion hhsssm ⊢ ⋅ ℎ ↾ ℂ × H = ⋅ 𝑠OLD ⁡ W

Proof

Step Hyp Ref Expression
1 hhss.1 ⊢ W = + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H
2 eqid ⊢ ⋅ 𝑠OLD ⁡ W = ⋅ 𝑠OLD ⁡ W
3 2 smfval ⊢ ⋅ 𝑠OLD ⁡ W = 2 nd ⁡ 1 st ⁡ W
4 1 fveq2i ⊢ 1 st ⁡ W = 1 st ⁡ + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H
5 opex ⊢ + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H ∈ V
6 normf ⊢ norm ℎ : ℋ ⟶ ℝ
7 ax-hilex ⊢ ℋ ∈ V
8 fex ⊢ norm ℎ : ℋ ⟶ ℝ ∧ ℋ ∈ V → norm ℎ ∈ V
9 6 7 8 mp2an ⊢ norm ℎ ∈ V
10 9 resex ⊢ norm ℎ ↾ H ∈ V
11 5 10 op1st ⊢ 1 st ⁡ + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H = + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H
12 4 11 eqtri ⊢ 1 st ⁡ W = + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H
13 12 fveq2i ⊢ 2 nd ⁡ 1 st ⁡ W = 2 nd ⁡ + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H
14 hilablo ⊢ + ℎ ∈ AbelOp
15 resexg ⊢ + ℎ ∈ AbelOp → + ℎ ↾ H × H ∈ V
16 14 15 ax-mp ⊢ + ℎ ↾ H × H ∈ V
17 hvmulex ⊢ ⋅ ℎ ∈ V
18 17 resex ⊢ ⋅ ℎ ↾ ℂ × H ∈ V
19 16 18 op2nd ⊢ 2 nd ⁡ + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H = ⋅ ℎ ↾ ℂ × H
20 3 13 19 3eqtrri ⊢ ⋅ ℎ ↾ ℂ × H = ⋅ 𝑠OLD ⁡ W