Metamath Proof Explorer

Theorem nvscl

Description: Closure law for the scalar product operation of a normed complex vector space. (Contributed by NM, 1-Feb-2007) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	nvscl.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
		nvscl.4	⊢ 𝑆 = ( ·_𝑠OLD ‘ 𝑈 )
	Assertion	nvscl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑆 𝐵 ) ∈ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		nvscl.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		nvscl.4	⊢ 𝑆 = ( ·_𝑠OLD ‘ 𝑈 )
3		eqid	⊢ ( 1^st ‘ 𝑈 ) = ( 1^st ‘ 𝑈 )
4	3	nvvc	⊢ ( 𝑈 ∈ NrmCVec → ( 1^st ‘ 𝑈 ) ∈ CVec_OLD )
5		eqid	⊢ ( +_𝑣 ‘ 𝑈 ) = ( +_𝑣 ‘ 𝑈 )
6	5	vafval	⊢ ( +_𝑣 ‘ 𝑈 ) = ( 1^st ‘ ( 1^st ‘ 𝑈 ) )
7	2	smfval	⊢ 𝑆 = ( 2^nd ‘ ( 1^st ‘ 𝑈 ) )
8	1 5	bafval	⊢ 𝑋 = ran ( +_𝑣 ‘ 𝑈 )
9	6 7 8	vccl	⊢ ( ( ( 1^st ‘ 𝑈 ) ∈ CVec_OLD ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑆 𝐵 ) ∈ 𝑋 )
10	4 9	syl3an1	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑆 𝐵 ) ∈ 𝑋 )