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 27765

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 27757	. . . . 5 ⊢ ·_𝑠OLD = (2^nd ∘ 1^st )
3	2	fveq1i 6349	. . . 4 ⊢ ( ·_𝑠OLD ‘𝑈) = ((2^nd ∘ 1^st )‘𝑈)
4		fo1st 7349	. . . . . 6 ⊢ 1^st :V–onto→V
5		fof 6272	. . . . . 6 ⊢ (1^st :V–onto→V → 1^st :V⟶V)
6	4, 5	ax-mp 5	. . . . 5 ⊢ 1^st :V⟶V
7		fvco3 6433	. . . . 5 ⊢ ((1^st :V⟶V ∧ 𝑈 ∈ V) → ((2^nd ∘ 1^st )‘𝑈) = (2^nd ‘(1^st ‘𝑈)))
8	6, 7	mpan 708	. . . 4 ⊢ (𝑈 ∈ V → ((2^nd ∘ 1^st )‘𝑈) = (2^nd ‘(1^st ‘𝑈)))
9	3, 8	syl5eq 2802	. . 3 ⊢ (𝑈 ∈ V → ( ·_𝑠OLD ‘𝑈) = (2^nd ‘(1^st ‘𝑈)))
10		fvprc 6342	. . . 4 ⊢ (¬ 𝑈 ∈ V → ( ·_𝑠OLD ‘𝑈) = ∅)
11		fvprc 6342	. . . . . 6 ⊢ (¬ 𝑈 ∈ V → (1^st ‘𝑈) = ∅)
12	11	fveq2d 6352	. . . . 5 ⊢ (¬ 𝑈 ∈ V → (2^nd ‘(1^st ‘𝑈)) = (2^nd ‘∅))
13		2nd0 7336	. . . . 5 ⊢ (2^nd ‘∅) = ∅
14	12, 13	syl6req 2807	. . . 4 ⊢ (¬ 𝑈 ∈ V → ∅ = (2^nd ‘(1^st ‘𝑈)))
15	10, 14	eqtrd 2790	. . 3 ⊢ (¬ 𝑈 ∈ V → ( ·_𝑠OLD ‘𝑈) = (2^nd ‘(1^st ‘𝑈)))
16	9, 15	pm2.61i 176	. 2 ⊢ ( ·_𝑠OLD ‘𝑈) = (2^nd ‘(1^st ‘𝑈))
17	1, 16	eqtri 2778	1 ⊢ 𝑆 = (2^nd ‘(1^st ‘𝑈))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 = wceq 1628 ∈ wcel 2135 Vcvv 3336 ∅c0 4054 ∘ ccom 5266 ⟶wf 6041 –onto→wfo 6043 ‘cfv 6045 1^st c1st 7327 2^nd c2nd 7328 ·_𝑠OLD cns 27747

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1867 ax-4 1882 ax-5 1984 ax-6 2050 ax-7 2086 ax-8 2137 ax-9 2144 ax-10 2164 ax-11 2179 ax-12 2192 ax-13 2387 ax-ext 2736 ax-sep 4929 ax-nul 4937 ax-pow 4988 ax-pr 5051 ax-un 7110

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1631 df-ex 1850 df-nf 1855 df-sb 2043 df-eu 2607 df-mo 2608 df-clab 2743 df-cleq 2749 df-clel 2752 df-nfc 2887 df-ne 2929 df-ral 3051 df-rex 3052 df-rab 3055 df-v 3338 df-sbc 3573 df-dif 3714 df-un 3716 df-in 3718 df-ss 3725 df-nul 4055 df-if 4227 df-sn 4318 df-pr 4320 df-op 4324 df-uni 4585 df-br 4801 df-opab 4861 df-mpt 4878 df-id 5170 df-xp 5268 df-rel 5269 df-cnv 5270 df-co 5271 df-dm 5272 df-rn 5273 df-res 5274 df-ima 5275 df-iota 6008 df-fun 6047 df-fn 6048 df-f 6049 df-fo 6051 df-fv 6053 df-1st 7329 df-2nd 7330 df-sm 27757

This theorem is referenced by: nvvop 27769 nvsf 27779 nvscl 27786 nvsid 27787 nvsass 27788 nvdi 27790 nvdir 27791 nv2 27792 nv0 27797 nvsz 27798 nvinv 27799 nvtri 27830 cnnvs 27840 phop 27978 phpar 27984 ipdirilem 27989 h2hsm 28137 hhsssm 28420

W3C validator