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 30826

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 2762	. . 3 ⊢ (1^st ‘𝑈) = (1^st ‘𝑈)
2	1	nvvc 30815	. 2 ⊢ (𝑈 ∈ NrmCVec → (1^st ‘𝑈) ∈ CVec_OLD)
3		eqid 2762	. . . 4 ⊢ ( +_𝑣 ‘𝑈) = ( +_𝑣 ‘𝑈)
4	3	vafval 30803	. . 3 ⊢ ( +_𝑣 ‘𝑈) = (1^st ‘(1^st ‘𝑈))
5		nvscl.4	. . . 4 ⊢ 𝑆 = ( ·_𝑠OLD ‘𝑈)
6	5	smfval 30805	. . 3 ⊢ 𝑆 = (2^nd ‘(1^st ‘𝑈))
7		nvscl.1	. . . 4 ⊢ 𝑋 = (BaseSet‘𝑈)
8	7, 3	bafval 30804	. . 3 ⊢ 𝑋 = ran ( +_𝑣 ‘𝑈)
9	4, 6, 8	vccl 30763	. 2 ⊢ (((1^st ‘𝑈) ∈ CVec_OLD ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → (𝐴𝑆𝐵) ∈ 𝑋)
10	2, 9	syl3an1 1176	1 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → (𝐴𝑆𝐵) ∈ 𝑋)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ w3a 1098 = wceq 1560 ∈ wcel 2142 ‘cfv 6521 (class class class)co 7396 1^st c1st 7968 ℂcc 11071 CVec_OLDcvc 30758 NrmCVeccnv 30784 +_𝑣 cpv 30785 BaseSetcba 30786 ·_𝑠OLD cns 30787

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5227 ax-sep 5246 ax-nul 5256 ax-pr 5390 ax-un 7718

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-ral 3077 df-rex 3087 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-nul 4286 df-if 4481 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-id 5542 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-ov 7399 df-oprab 7400 df-1st 7970 df-2nd 7971 df-vc 30759 df-nv 30792 df-va 30795 df-ba 30796 df-sm 30797 df-0v 30798 df-nmcv 30800

This theorem is referenced by: nvmval2 30843 nvmf 30845 nvmdi 30848 nvnegneg 30849 nvpncan2 30853 nvaddsub4 30857 nvdif 30866 nvpi 30867 nvmtri 30871 nvabs 30872 nvge0 30873 imsmetlem 30890 smcnlem 30897 ipval2lem2 30904 4ipval2 30908 ipval3 30909 sspmval 30933 lnocoi 30957 lnomul 30960 0lno 30990 nmlno0lem 30993 nmblolbii 30999 blocnilem 31004 ip0i 31025 ip1ilem 31026 ipdirilem 31029 ipasslem1 31031 ipasslem2 31032 ipasslem4 31034 ipasslem5 31035 ipasslem8 31037 ipasslem9 31038 ipasslem10 31039 ipasslem11 31040 dipassr 31046 dipsubdir 31048 siilem1 31051 ipblnfi 31055 ubthlem2 31071 minvecolem2 31075 hhshsslem2 31468

W3C validator