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 30555

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 2729	. . 3 ⊢ (1^st ‘𝑈) = (1^st ‘𝑈)
2	1	nvvc 30544	. 2 ⊢ (𝑈 ∈ NrmCVec → (1^st ‘𝑈) ∈ CVec_OLD)
3		eqid 2729	. . . 4 ⊢ ( +_𝑣 ‘𝑈) = ( +_𝑣 ‘𝑈)
4	3	vafval 30532	. . 3 ⊢ ( +_𝑣 ‘𝑈) = (1^st ‘(1^st ‘𝑈))
5		nvscl.4	. . . 4 ⊢ 𝑆 = ( ·_𝑠OLD ‘𝑈)
6	5	smfval 30534	. . 3 ⊢ 𝑆 = (2^nd ‘(1^st ‘𝑈))
7		nvscl.1	. . . 4 ⊢ 𝑋 = (BaseSet‘𝑈)
8	7, 3	bafval 30533	. . 3 ⊢ 𝑋 = ran ( +_𝑣 ‘𝑈)
9	4, 6, 8	vccl 30492	. 2 ⊢ (((1^st ‘𝑈) ∈ CVec_OLD ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → (𝐴𝑆𝐵) ∈ 𝑋)
10	2, 9	syl3an1 1163	1 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → (𝐴𝑆𝐵) ∈ 𝑋)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ‘cfv 6511 (class class class)co 7387 1^st c1st 7966 ℂcc 11066 CVec_OLDcvc 30487 NrmCVeccnv 30513 +_𝑣 cpv 30514 BaseSetcba 30515 ·_𝑠OLD cns 30516

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pr 5387 ax-un 7711

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4297 df-if 4489 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-iun 4957 df-br 5108 df-opab 5170 df-mpt 5189 df-id 5533 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-ov 7390 df-oprab 7391 df-1st 7968 df-2nd 7969 df-vc 30488 df-nv 30521 df-va 30524 df-ba 30525 df-sm 30526 df-0v 30527 df-nmcv 30529

This theorem is referenced by: nvmval2 30572 nvmf 30574 nvmdi 30577 nvnegneg 30578 nvpncan2 30582 nvaddsub4 30586 nvdif 30595 nvpi 30596 nvmtri 30600 nvabs 30601 nvge0 30602 imsmetlem 30619 smcnlem 30626 ipval2lem2 30633 4ipval2 30637 ipval3 30638 sspmval 30662 lnocoi 30686 lnomul 30689 0lno 30719 nmlno0lem 30722 nmblolbii 30728 blocnilem 30733 ip0i 30754 ip1ilem 30755 ipdirilem 30758 ipasslem1 30760 ipasslem2 30761 ipasslem4 30763 ipasslem5 30764 ipasslem8 30766 ipasslem9 30767 ipasslem10 30768 ipasslem11 30769 dipassr 30775 dipsubdir 30777 siilem1 30780 ipblnfi 30784 ubthlem2 30800 minvecolem2 30804 hhshsslem2 31197

W3C validator