smfval - Metamath Proof Explorer

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

Theorem smfval 27306

Description: Value of the function for the scalar multiplication operation on a normed complex vector space. (Contributed by NM, 24-Apr-2007.) (New usage is discouraged.)

**Hypothesis**
Ref	Expression
smfval.4	⊢ 𝑆 = ( ·_𝑠OLD ‘𝑈)

**Assertion**
Ref	Expression
smfval	⊢ 𝑆 = (2^nd ‘(1^st ‘𝑈))

**Proof of Theorem smfval**
Step	Hyp	Ref	Expression
1		smfval.4	. 2 ⊢ 𝑆 = ( ·_𝑠OLD ‘𝑈)
2		df-sm 27298	. . . . 5 ⊢ ·_𝑠OLD = (2^nd ∘ 1^st )
3	2	fveq1i 6149	. . . 4 ⊢ ( ·_𝑠OLD ‘𝑈) = ((2^nd ∘ 1^st )‘𝑈)
4		fo1st 7133	. . . . . 6 ⊢ 1^st :V–onto→V
5		fof 6072	. . . . . 6 ⊢ (1^st :V–onto→V → 1^st :V⟶V)
6	4, 5	ax-mp 5	. . . . 5 ⊢ 1^st :V⟶V
7		fvco3 6232	. . . . 5 ⊢ ((1^st :V⟶V ∧ 𝑈 ∈ V) → ((2^nd ∘ 1^st )‘𝑈) = (2^nd ‘(1^st ‘𝑈)))
8	6, 7	mpan 705	. . . 4 ⊢ (𝑈 ∈ V → ((2^nd ∘ 1^st )‘𝑈) = (2^nd ‘(1^st ‘𝑈)))
9	3, 8	syl5eq 2667	. . 3 ⊢ (𝑈 ∈ V → ( ·_𝑠OLD ‘𝑈) = (2^nd ‘(1^st ‘𝑈)))
10		fvprc 6142	. . . 4 ⊢ (¬ 𝑈 ∈ V → ( ·_𝑠OLD ‘𝑈) = ∅)
11		fvprc 6142	. . . . . 6 ⊢ (¬ 𝑈 ∈ V → (1^st ‘𝑈) = ∅)
12	11	fveq2d 6152	. . . . 5 ⊢ (¬ 𝑈 ∈ V → (2^nd ‘(1^st ‘𝑈)) = (2^nd ‘∅))
13		2nd0 7120	. . . . 5 ⊢ (2^nd ‘∅) = ∅
14	12, 13	syl6req 2672	. . . 4 ⊢ (¬ 𝑈 ∈ V → ∅ = (2^nd ‘(1^st ‘𝑈)))
15	10, 14	eqtrd 2655	. . 3 ⊢ (¬ 𝑈 ∈ V → ( ·_𝑠OLD ‘𝑈) = (2^nd ‘(1^st ‘𝑈)))
16	9, 15	pm2.61i 176	. 2 ⊢ ( ·_𝑠OLD ‘𝑈) = (2^nd ‘(1^st ‘𝑈))
17	1, 16	eqtri 2643	1 ⊢ 𝑆 = (2^nd ‘(1^st ‘𝑈))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 = wceq 1480 ∈ wcel 1987 Vcvv 3186 ∅c0 3891 ∘ ccom 5078 ⟶wf 5843 –onto→wfo 5845 ‘cfv 5847 1^st c1st 7111 2^nd c2nd 7112 ·_𝑠OLD cns 27288

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1719 ax-4 1734 ax-5 1836 ax-6 1885 ax-7 1932 ax-8 1989 ax-9 1996 ax-10 2016 ax-11 2031 ax-12 2044 ax-13 2245 ax-ext 2601 ax-sep 4741 ax-nul 4749 ax-pow 4803 ax-pr 4867 ax-un 6902

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1038 df-tru 1483 df-ex 1702 df-nf 1707 df-sb 1878 df-eu 2473 df-mo 2474 df-clab 2608 df-cleq 2614 df-clel 2617 df-nfc 2750 df-ne 2791 df-ral 2912 df-rex 2913 df-rab 2916 df-v 3188 df-sbc 3418 df-dif 3558 df-un 3560 df-in 3562 df-ss 3569 df-nul 3892 df-if 4059 df-sn 4149 df-pr 4151 df-op 4155 df-uni 4403 df-br 4614 df-opab 4674 df-mpt 4675 df-id 4989 df-xp 5080 df-rel 5081 df-cnv 5082 df-co 5083 df-dm 5084 df-rn 5085 df-res 5086 df-ima 5087 df-iota 5810 df-fun 5849 df-fn 5850 df-f 5851 df-fo 5853 df-fv 5855 df-1st 7113 df-2nd 7114 df-sm 27298

This theorem is referenced by: nvvop 27310 nvsf 27320 nvscl 27327 nvsid 27328 nvsass 27329 nvdi 27331 nvdir 27332 nv2 27333 nv0 27338 nvsz 27339 nvinv 27340 nvtri 27371 cnnvs 27381 phop 27519 phpar 27525 ipdirilem 27530 h2hsm 27678 hhsssm 27961

W3C validator