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 30567

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 30559	. . . . 5 ⊢ ·_𝑠OLD = (2^nd ∘ 1^st )
3	2	fveq1i 6827	. . . 4 ⊢ ( ·_𝑠OLD ‘𝑈) = ((2^nd ∘ 1^st )‘𝑈)
4		fo1st 7951	. . . . . 6 ⊢ 1^st :V–onto→V
5		fof 6740	. . . . . 6 ⊢ (1^st :V–onto→V → 1^st :V⟶V)
6	4, 5	ax-mp 5	. . . . 5 ⊢ 1^st :V⟶V
7		fvco3 6926	. . . . 5 ⊢ ((1^st :V⟶V ∧ 𝑈 ∈ V) → ((2^nd ∘ 1^st )‘𝑈) = (2^nd ‘(1^st ‘𝑈)))
8	6, 7	mpan 690	. . . 4 ⊢ (𝑈 ∈ V → ((2^nd ∘ 1^st )‘𝑈) = (2^nd ‘(1^st ‘𝑈)))
9	3, 8	eqtrid 2776	. . 3 ⊢ (𝑈 ∈ V → ( ·_𝑠OLD ‘𝑈) = (2^nd ‘(1^st ‘𝑈)))
10		fvprc 6818	. . . 4 ⊢ (¬ 𝑈 ∈ V → ( ·_𝑠OLD ‘𝑈) = ∅)
11		fvprc 6818	. . . . . 6 ⊢ (¬ 𝑈 ∈ V → (1^st ‘𝑈) = ∅)
12	11	fveq2d 6830	. . . . 5 ⊢ (¬ 𝑈 ∈ V → (2^nd ‘(1^st ‘𝑈)) = (2^nd ‘∅))
13		2nd0 7938	. . . . 5 ⊢ (2^nd ‘∅) = ∅
14	12, 13	eqtr2di 2781	. . . 4 ⊢ (¬ 𝑈 ∈ V → ∅ = (2^nd ‘(1^st ‘𝑈)))
15	10, 14	eqtrd 2764	. . 3 ⊢ (¬ 𝑈 ∈ V → ( ·_𝑠OLD ‘𝑈) = (2^nd ‘(1^st ‘𝑈)))
16	9, 15	pm2.61i 182	. 2 ⊢ ( ·_𝑠OLD ‘𝑈) = (2^nd ‘(1^st ‘𝑈))
17	1, 16	eqtri 2752	1 ⊢ 𝑆 = (2^nd ‘(1^st ‘𝑈))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 = wceq 1540 ∈ wcel 2109 Vcvv 3438 ∅c0 4286 ∘ ccom 5627 ⟶wf 6482 –onto→wfo 6484 ‘cfv 6486 1^st c1st 7929 2^nd c2nd 7930 ·_𝑠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-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-rab 3397 df-v 3440 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-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-fo 6492 df-fv 6494 df-1st 7931 df-2nd 7932 df-sm 30559

This theorem is referenced by: nvvop 30571 nvsf 30581 nvscl 30588 nvsid 30589 nvsass 30590 nvdi 30592 nvdir 30593 nv2 30594 nv0 30599 nvsz 30600 nvinv 30601 nvtri 30632 cnnvs 30642 phop 30780 ipdirilem 30791 h2hsm 30937 hhsssm 31220

W3C validator