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