vafval - Metamath Proof Explorer

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

Theorem vafval 27304

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

**Hypothesis**
Ref	Expression
vafval.2	⊢ 𝐺 = ( +_𝑣 ‘𝑈)

**Assertion**
Ref	Expression
vafval	⊢ 𝐺 = (1^st ‘(1^st ‘𝑈))

**Proof of Theorem vafval**
Step	Hyp	Ref	Expression
1		vafval.2	. 2 ⊢ 𝐺 = ( +_𝑣 ‘𝑈)
2		df-va 27296	. . . . 5 ⊢ +_𝑣 = (1^st ∘ 1^st )
3	2	fveq1i 6149	. . . 4 ⊢ ( +_𝑣 ‘𝑈) = ((1^st ∘ 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) → ((1^st ∘ 1^st )‘𝑈) = (1^st ‘(1^st ‘𝑈)))
8	6, 7	mpan 705	. . . 4 ⊢ (𝑈 ∈ V → ((1^st ∘ 1^st )‘𝑈) = (1^st ‘(1^st ‘𝑈)))
9	3, 8	syl5eq 2667	. . 3 ⊢ (𝑈 ∈ V → ( +_𝑣 ‘𝑈) = (1^st ‘(1^st ‘𝑈)))
10		fvprc 6142	. . . 4 ⊢ (¬ 𝑈 ∈ V → ( +_𝑣 ‘𝑈) = ∅)
11		fvprc 6142	. . . . . 6 ⊢ (¬ 𝑈 ∈ V → (1^st ‘𝑈) = ∅)
12	11	fveq2d 6152	. . . . 5 ⊢ (¬ 𝑈 ∈ V → (1^st ‘(1^st ‘𝑈)) = (1^st ‘∅))
13		1st0 7119	. . . . 5 ⊢ (1^st ‘∅) = ∅
14	12, 13	syl6req 2672	. . . 4 ⊢ (¬ 𝑈 ∈ V → ∅ = (1^st ‘(1^st ‘𝑈)))
15	10, 14	eqtrd 2655	. . 3 ⊢ (¬ 𝑈 ∈ V → ( +_𝑣 ‘𝑈) = (1^st ‘(1^st ‘𝑈)))
16	9, 15	pm2.61i 176	. 2 ⊢ ( +_𝑣 ‘𝑈) = (1^st ‘(1^st ‘𝑈))
17	1, 16	eqtri 2643	1 ⊢ 𝐺 = (1^st ‘(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 +_𝑣 cpv 27286

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-va 27296

This theorem is referenced by: nvvop 27310 nvablo 27317 nvsf 27320 nvscl 27327 nvsid 27328 nvsass 27329 nvdi 27331 nvdir 27332 nv2 27333 nv0 27338 nvsz 27339 nvinv 27340 cnnvg 27379 phop 27519 phpar 27525 ip0i 27526 ipdirilem 27530 h2hva 27677 hhssva 27960 hhshsslem1 27970

W3C validator