# 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 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
nvscl.4 ${⊢}{S}={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
Assertion nvscl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\to {A}{S}{B}\in {X}$

### Proof

Step Hyp Ref Expression
1 nvscl.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 nvscl.4 ${⊢}{S}={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
3 eqid ${⊢}{1}^{st}\left({U}\right)={1}^{st}\left({U}\right)$
4 3 nvvc ${⊢}{U}\in \mathrm{NrmCVec}\to {1}^{st}\left({U}\right)\in {CVec}_{\mathrm{OLD}}$
5 eqid ${⊢}{+}_{v}\left({U}\right)={+}_{v}\left({U}\right)$
6 5 vafval ${⊢}{+}_{v}\left({U}\right)={1}^{st}\left({1}^{st}\left({U}\right)\right)$
7 2 smfval ${⊢}{S}={2}^{nd}\left({1}^{st}\left({U}\right)\right)$
8 1 5 bafval ${⊢}{X}=\mathrm{ran}{+}_{v}\left({U}\right)$
9 6 7 8 vccl ${⊢}\left({1}^{st}\left({U}\right)\in {CVec}_{\mathrm{OLD}}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\to {A}{S}{B}\in {X}$
10 4 9 syl3an1 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\to {A}{S}{B}\in {X}$