nvscl - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > nvscl		Structured version Visualization version GIF version

Theorem nvscl 31107

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

**Hypotheses**
Ref	Expression
nvscl.1	⊢ 𝑋 = (BaseSet‘𝑈)
nvscl.4	⊢ 𝑆 = ( ·_𝑠OLD ‘𝑈)

**Assertion**
Ref	Expression
nvscl	⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → (𝐴𝑆𝐵) ∈ 𝑋)

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

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ‘cfv 6533 (class class class)co 7413 1^st c1st 7984 ℂcc 11122 CVec_OLDcvc 31039 NrmCVeccnv 31065 +_𝑣 cpv 31066 BaseSetcba 31067 ·_𝑠OLD cns 31068

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pr 5398 ax-un 7736

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-id 5550 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-ov 7416 df-oprab 7417 df-1st 7986 df-2nd 7987 df-vc 31040 df-nv 31073 df-va 31076 df-ba 31077 df-sm 31078 df-0v 31079 df-nmcv 31081

This theorem is used by: nvmval2 31124 nvmf 31126 nvmdi 31129 nvnegneg 31130 nvpncan2 31134 nvaddsub4 31138 nvdif 31147 nvpi 31148 nvmtri 31152 nvabs 31153 nvge0 31154 imsmetlem 31171 smcnlem 31178 ipval2lem2 31185 4ipval2 31189 ipval3 31190 sspmval 31214 lnocoi 31238 lnomul 31241 0lno 31271 nmlno0lem 31274 nmblolbii 31280 blocnilem 31285 ip0i 31306 ip1ilem 31307 ipdirilem 31310 ipasslem1 31312 ipasslem2 31313 ipasslem4 31315 ipasslem5 31316 ipasslem8 31318 ipasslem9 31319 ipasslem10 31320 ipasslem11 31321 dipassr 31327 dipsubdir 31329 siilem1 31332 ipblnfi 31336 ubthlem2 31352 minvecolem2 31356 hhshsslem2 31749

W3C validator