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 28573

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 2739	. . 3 ⊢ (1^st ‘𝑈) = (1^st ‘𝑈)
2	1	nvvc 28562	. 2 ⊢ (𝑈 ∈ NrmCVec → (1^st ‘𝑈) ∈ CVec_OLD)
3		eqid 2739	. . . 4 ⊢ ( +_𝑣 ‘𝑈) = ( +_𝑣 ‘𝑈)
4	3	vafval 28550	. . 3 ⊢ ( +_𝑣 ‘𝑈) = (1^st ‘(1^st ‘𝑈))
5		nvscl.4	. . . 4 ⊢ 𝑆 = ( ·_𝑠OLD ‘𝑈)
6	5	smfval 28552	. . 3 ⊢ 𝑆 = (2^nd ‘(1^st ‘𝑈))
7		nvscl.1	. . . 4 ⊢ 𝑋 = (BaseSet‘𝑈)
8	7, 3	bafval 28551	. . 3 ⊢ 𝑋 = ran ( +_𝑣 ‘𝑈)
9	4, 6, 8	vccl 28510	. 2 ⊢ (((1^st ‘𝑈) ∈ CVec_OLD ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → (𝐴𝑆𝐵) ∈ 𝑋)
10	2, 9	syl3an1 1164	1 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → (𝐴𝑆𝐵) ∈ 𝑋)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ w3a 1088 = wceq 1542 ∈ wcel 2114 ‘cfv 6349 (class class class)co 7182 1^st c1st 7724 ℂcc 10625 CVec_OLDcvc 28505 NrmCVeccnv 28531 +_𝑣 cpv 28532 BaseSetcba 28533 ·_𝑠OLD cns 28534

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2711 ax-rep 5164 ax-sep 5177 ax-nul 5184 ax-pr 5306 ax-un 7491

This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2541 df-eu 2571 df-clab 2718 df-cleq 2731 df-clel 2812 df-nfc 2882 df-ne 2936 df-ral 3059 df-rex 3060 df-reu 3061 df-rab 3063 df-v 3402 df-sbc 3686 df-csb 3801 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-nul 4222 df-if 4425 df-sn 4527 df-pr 4529 df-op 4533 df-uni 4807 df-iun 4893 df-br 5041 df-opab 5103 df-mpt 5121 df-id 5439 df-xp 5541 df-rel 5542 df-cnv 5543 df-co 5544 df-dm 5545 df-rn 5546 df-res 5547 df-ima 5548 df-iota 6307 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-fv 6357 df-ov 7185 df-oprab 7186 df-1st 7726 df-2nd 7727 df-vc 28506 df-nv 28539 df-va 28542 df-ba 28543 df-sm 28544 df-0v 28545 df-nmcv 28547

This theorem is referenced by: nvmval2 28590 nvmf 28592 nvmdi 28595 nvnegneg 28596 nvpncan2 28600 nvaddsub4 28604 nvdif 28613 nvpi 28614 nvmtri 28618 nvabs 28619 nvge0 28620 imsmetlem 28637 smcnlem 28644 ipval2lem2 28651 4ipval2 28655 ipval3 28656 sspmval 28680 lnocoi 28704 lnomul 28707 0lno 28737 nmlno0lem 28740 nmblolbii 28746 blocnilem 28751 ip0i 28772 ip1ilem 28773 ipdirilem 28776 ipasslem1 28778 ipasslem2 28779 ipasslem4 28781 ipasslem5 28782 ipasslem8 28784 ipasslem9 28785 ipasslem10 28786 ipasslem11 28787 dipassr 28793 dipsubdir 28795 siilem1 28798 ipblnfi 28802 ubthlem2 28818 minvecolem2 28822 hhshsslem2 29215

W3C validator