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 30715

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 ‘cfv 6485 (class class class)co 7356 1^st c1st 7929 ℂcc 11027 CVec_OLDcvc 30647 NrmCVeccnv 30673 +_𝑣 cpv 30674 BaseSetcba 30675 ·_𝑠OLD cns 30676

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 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5199 ax-sep 5218 ax-nul 5228 ax-pr 5362 ax-un 7678

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-ral 3054 df-rex 3064 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4262 df-if 4455 df-sn 4556 df-pr 4558 df-op 4562 df-uni 4839 df-iun 4923 df-br 5073 df-opab 5135 df-mpt 5154 df-id 5513 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-ov 7359 df-oprab 7360 df-1st 7931 df-2nd 7932 df-vc 30648 df-nv 30681 df-va 30684 df-ba 30685 df-sm 30686 df-0v 30687 df-nmcv 30689

This theorem is referenced by: nvmval2 30732 nvmf 30734 nvmdi 30737 nvnegneg 30738 nvpncan2 30742 nvaddsub4 30746 nvdif 30755 nvpi 30756 nvmtri 30760 nvabs 30761 nvge0 30762 imsmetlem 30779 smcnlem 30786 ipval2lem2 30793 4ipval2 30797 ipval3 30798 sspmval 30822 lnocoi 30846 lnomul 30849 0lno 30879 nmlno0lem 30882 nmblolbii 30888 blocnilem 30893 ip0i 30914 ip1ilem 30915 ipdirilem 30918 ipasslem1 30920 ipasslem2 30921 ipasslem4 30923 ipasslem5 30924 ipasslem8 30926 ipasslem9 30927 ipasslem10 30928 ipasslem11 30929 dipassr 30935 dipsubdir 30937 siilem1 30940 ipblnfi 30944 ubthlem2 30960 minvecolem2 30964 hhshsslem2 31357

W3C validator