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 27740

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 27732	. . . . 5 ⊢ ·_𝑠OLD = (2^nd ∘ 1^st )
3	2	fveq1i 6341	. . . 4 ⊢ ( ·_𝑠OLD ‘𝑈) = ((2^nd ∘ 1^st )‘𝑈)
4		fo1st 7341	. . . . . 6 ⊢ 1^st :V–onto→V
5		fof 6264	. . . . . 6 ⊢ (1^st :V–onto→V → 1^st :V⟶V)
6	4, 5	ax-mp 5	. . . . 5 ⊢ 1^st :V⟶V
7		fvco3 6425	. . . . 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 2794	. . 3 ⊢ (𝑈 ∈ V → ( ·_𝑠OLD ‘𝑈) = (2^nd ‘(1^st ‘𝑈)))
10		fvprc 6334	. . . 4 ⊢ (¬ 𝑈 ∈ V → ( ·_𝑠OLD ‘𝑈) = ∅)
11		fvprc 6334	. . . . . 6 ⊢ (¬ 𝑈 ∈ V → (1^st ‘𝑈) = ∅)
12	11	fveq2d 6344	. . . . 5 ⊢ (¬ 𝑈 ∈ V → (2^nd ‘(1^st ‘𝑈)) = (2^nd ‘∅))
13		2nd0 7328	. . . . 5 ⊢ (2^nd ‘∅) = ∅
14	12, 13	syl6req 2799	. . . 4 ⊢ (¬ 𝑈 ∈ V → ∅ = (2^nd ‘(1^st ‘𝑈)))
15	10, 14	eqtrd 2782	. . 3 ⊢ (¬ 𝑈 ∈ V → ( ·_𝑠OLD ‘𝑈) = (2^nd ‘(1^st ‘𝑈)))
16	9, 15	pm2.61i 176	. 2 ⊢ ( ·_𝑠OLD ‘𝑈) = (2^nd ‘(1^st ‘𝑈))
17	1, 16	eqtri 2770	1 ⊢ 𝑆 = (2^nd ‘(1^st ‘𝑈))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 = wceq 1620 ∈ wcel 2127 Vcvv 3328 ∅c0 4046 ∘ ccom 5258 ⟶wf 6033 –onto→wfo 6035 ‘cfv 6037 1^st c1st 7319 2^nd c2nd 7320 ·_𝑠OLD cns 27722

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-8 2129 ax-9 2136 ax-10 2156 ax-11 2171 ax-12 2184 ax-13 2379 ax-ext 2728 ax-sep 4921 ax-nul 4929 ax-pow 4980 ax-pr 5043 ax-un 7102

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1623 df-ex 1842 df-nf 1847 df-sb 2035 df-eu 2599 df-mo 2600 df-clab 2735 df-cleq 2741 df-clel 2744 df-nfc 2879 df-ne 2921 df-ral 3043 df-rex 3044 df-rab 3047 df-v 3330 df-sbc 3565 df-dif 3706 df-un 3708 df-in 3710 df-ss 3717 df-nul 4047 df-if 4219 df-sn 4310 df-pr 4312 df-op 4316 df-uni 4577 df-br 4793 df-opab 4853 df-mpt 4870 df-id 5162 df-xp 5260 df-rel 5261 df-cnv 5262 df-co 5263 df-dm 5264 df-rn 5265 df-res 5266 df-ima 5267 df-iota 6000 df-fun 6039 df-fn 6040 df-f 6041 df-fo 6043 df-fv 6045 df-1st 7321 df-2nd 7322 df-sm 27732

This theorem is referenced by: nvvop 27744 nvsf 27754 nvscl 27761 nvsid 27762 nvsass 27763 nvdi 27765 nvdir 27766 nv2 27767 nv0 27772 nvsz 27773 nvinv 27774 nvtri 27805 cnnvs 27815 phop 27953 phpar 27959 ipdirilem 27964 h2hsm 28112 hhsssm 28395

W3C validator