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

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 ⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
Assertion hhsssm ( ·ℎ ↾ ( ℂ × 𝐻 ) ) = ( ·𝑠OLD ‘ 𝑊 )

Proof

Step Hyp Ref Expression
1 hhss.1 ⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
2 eqid ⊢ ( ·𝑠OLD ‘ 𝑊 ) = ( ·𝑠OLD ‘ 𝑊 )
3 2 smfval ⊢ ( ·𝑠OLD ‘ 𝑊 ) = ( 2nd ‘ ( 1st ‘ 𝑊 ) )
4 1 fveq2i ⊢ ( 1st ‘ 𝑊 ) = ( 1st ‘ ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ )
5 opex ⊢ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ ∈ 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ℎ ↾ 𝐻 ) ∈ V
11 5 10 op1st ⊢ ( 1st ‘ ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ ) = ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩
12 4 11 eqtri ⊢ ( 1st ‘ 𝑊 ) = ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩
13 12 fveq2i ⊢ ( 2nd ‘ ( 1st ‘ 𝑊 ) ) = ( 2nd ‘ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ )
14 hilablo ⊢ +ℎ ∈ AbelOp
15 resexg ⊢ ( +ℎ ∈ AbelOp → ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ∈ V )
16 14 15 ax-mp ⊢ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ∈ V
17 hvmulex ⊢ ·ℎ ∈ V
18 17 resex ⊢ ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ∈ V
19 16 18 op2nd ⊢ ( 2nd ‘ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ ) = ( ·ℎ ↾ ( ℂ × 𝐻 ) )
20 3 13 19 3eqtrri ⊢ ( ·ℎ ↾ ( ℂ × 𝐻 ) ) = ( ·𝑠OLD ‘ 𝑊 )