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 30754

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 30746	. . . . 5 ⊢ ·_𝑠OLD = (2^nd ∘ 1^st )
3	2	fveq1i 6864	. . . 4 ⊢ ( ·_𝑠OLD ‘𝑈) = ((2^nd ∘ 1^st )‘𝑈)
4		fo1st 7986	. . . . . 6 ⊢ 1^st :V–onto→V
5		fof 6774	. . . . . 6 ⊢ (1^st :V–onto→V → 1^st :V⟶V)
6	4, 5	ax-mp 5	. . . . 5 ⊢ 1^st :V⟶V
7		fvco3 6963	. . . . 5 ⊢ ((1^st :V⟶V ∧ 𝑈 ∈ V) → ((2^nd ∘ 1^st )‘𝑈) = (2^nd ‘(1^st ‘𝑈)))
8	6, 7	mpan 700	. . . 4 ⊢ (𝑈 ∈ V → ((2^nd ∘ 1^st )‘𝑈) = (2^nd ‘(1^st ‘𝑈)))
9	3, 8	eqtrid 2808	. . 3 ⊢ (𝑈 ∈ V → ( ·_𝑠OLD ‘𝑈) = (2^nd ‘(1^st ‘𝑈)))
10		fvprc 6855	. . . 4 ⊢ (¬ 𝑈 ∈ V → ( ·_𝑠OLD ‘𝑈) = ∅)
11		fvprc 6855	. . . . . 6 ⊢ (¬ 𝑈 ∈ V → (1^st ‘𝑈) = ∅)
12	11	fveq2d 6867	. . . . 5 ⊢ (¬ 𝑈 ∈ V → (2^nd ‘(1^st ‘𝑈)) = (2^nd ‘∅))
13		2nd0 7973	. . . . 5 ⊢ (2^nd ‘∅) = ∅
14	12, 13	eqtr2di 2813	. . . 4 ⊢ (¬ 𝑈 ∈ V → ∅ = (2^nd ‘(1^st ‘𝑈)))
15	10, 14	eqtrd 2796	. . 3 ⊢ (¬ 𝑈 ∈ V → ( ·_𝑠OLD ‘𝑈) = (2^nd ‘(1^st ‘𝑈)))
16	9, 15	pm2.61i 183	. 2 ⊢ ( ·_𝑠OLD ‘𝑈) = (2^nd ‘(1^st ‘𝑈))
17	1, 16	eqtri 2784	1 ⊢ 𝑆 = (2^nd ‘(1^st ‘𝑈))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 = wceq 1559 ∈ wcel 2141 Vcvv 3453 ∅c0 4285 ∘ ccom 5649 ⟶wf 6513 –onto→wfo 6515 ‘cfv 6517 1^st c1st 7964 2^nd c2nd 7965 ·_𝑠OLD cns 30736

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-sep 5245 ax-nul 5255 ax-pr 5389 ax-un 7714

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3076 df-rex 3086 df-rab 3414 df-v 3455 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-nul 4286 df-if 4480 df-sn 4582 df-pr 4584 df-op 4588 df-uni 4865 df-br 5100 df-opab 5162 df-mpt 5181 df-id 5540 df-xp 5651 df-rel 5652 df-cnv 5653 df-co 5654 df-dm 5655 df-rn 5656 df-res 5657 df-ima 5658 df-iota 6473 df-fun 6519 df-fn 6520 df-f 6521 df-fo 6523 df-fv 6525 df-1st 7966 df-2nd 7967 df-sm 30746

This theorem is referenced by: nvvop 30758 nvsf 30768 nvscl 30775 nvsid 30776 nvsass 30777 nvdi 30779 nvdir 30780 nv2 30781 nv0 30786 nvsz 30787 nvinv 30788 nvtri 30819 cnnvs 30829 phop 30967 ipdirilem 30978 h2hsm 31124 hhsssm 31407

W3C validator