Theorem vccl

Description: Closure of the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	vciOLD.1	⊢ 𝐺 = ( 1st ‘ 𝑊 )
	vciOLD.2	⊢ 𝑆 = ( 2nd ‘ 𝑊 )
	vciOLD.3	⊢ 𝑋 = ran 𝐺
Assertion	vccl	⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑆 𝐵 ) ∈ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		vciOLD.1	⊢ 𝐺 = ( 1st ‘ 𝑊 )
2		vciOLD.2	⊢ 𝑆 = ( 2nd ‘ 𝑊 )
3		vciOLD.3	⊢ 𝑋 = ran 𝐺
4	1 2 3	vcsm	⊢ ( 𝑊 ∈ CVecOLD → 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 )
5		fovrn	⊢ ( ( 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑆 𝐵 ) ∈ 𝑋 )
6	4 5	syl3an1	⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑆 𝐵 ) ∈ 𝑋 )