nvsid - Metamath Proof Explorer

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

Theorem nvsid 30589

Description: Identity element for the scalar product of a normed complex vector space. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.)

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

**Assertion**
Ref	Expression
nvsid	⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (1𝑆𝐴) = 𝐴)

**Proof of Theorem nvsid**
Step	Hyp	Ref	Expression
1		eqid 2729	. . 3 ⊢ (1^st ‘𝑈) = (1^st ‘𝑈)
2	1	nvvc 30577	. 2 ⊢ (𝑈 ∈ NrmCVec → (1^st ‘𝑈) ∈ CVec_OLD)
3		eqid 2729	. . . 4 ⊢ ( +_𝑣 ‘𝑈) = ( +_𝑣 ‘𝑈)
4	3	vafval 30565	. . 3 ⊢ ( +_𝑣 ‘𝑈) = (1^st ‘(1^st ‘𝑈))
5		nvscl.4	. . . 4 ⊢ 𝑆 = ( ·_𝑠OLD ‘𝑈)
6	5	smfval 30567	. . 3 ⊢ 𝑆 = (2^nd ‘(1^st ‘𝑈))
7		nvscl.1	. . . 4 ⊢ 𝑋 = (BaseSet‘𝑈)
8	7, 3	bafval 30566	. . 3 ⊢ 𝑋 = ran ( +_𝑣 ‘𝑈)
9	4, 6, 8	vcidOLD 30526	. 2 ⊢ (((1^st ‘𝑈) ∈ CVec_OLD ∧ 𝐴 ∈ 𝑋) → (1𝑆𝐴) = 𝐴)
10	2, 9	sylan 580	1 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (1𝑆𝐴) = 𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ‘cfv 6486 (class class class)co 7353 1^st c1st 7929 1c1 11029 CVec_OLDcvc 30520 NrmCVeccnv 30546 +_𝑣 cpv 30547 BaseSetcba 30548 ·_𝑠OLD cns 30549

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 5221 ax-sep 5238 ax-nul 5248 ax-pr 5374 ax-un 7675

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 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4479 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4862 df-iun 4946 df-br 5096 df-opab 5158 df-mpt 5177 df-id 5518 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-ov 7356 df-oprab 7357 df-1st 7931 df-2nd 7932 df-vc 30521 df-nv 30554 df-va 30557 df-ba 30558 df-sm 30559 df-0v 30560 df-nmcv 30562

This theorem is referenced by: nvmul0or 30612 nvpi 30629 nvge0 30635 ipval2lem3 30667 ipval2 30669 ipidsq 30672 lnoadd 30720 ip1ilem 30788 ip2i 30790 ipdirilem 30791 ipasslem1 30793 ipasslem4 30796 ipasslem10 30801 minvecolem2 30837 hlmulid 30867

W3C validator