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 ‘ 𝑊 )