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 30674

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 30666	. . . . 5 ⊢ +_𝑣 = (1^st ∘ 1^st )
3	2	fveq1i 6841	. . . 4 ⊢ ( +_𝑣 ‘𝑈) = ((1^st ∘ 1^st )‘𝑈)
4		fo1st 7962	. . . . . 6 ⊢ 1^st :V–onto→V
5		fof 6752	. . . . . 6 ⊢ (1^st :V–onto→V → 1^st :V⟶V)
6	4, 5	ax-mp 5	. . . . 5 ⊢ 1^st :V⟶V
7		fvco3 6939	. . . . 5 ⊢ ((1^st :V⟶V ∧ 𝑈 ∈ V) → ((1^st ∘ 1^st )‘𝑈) = (1^st ‘(1^st ‘𝑈)))
8	6, 7	mpan 691	. . . 4 ⊢ (𝑈 ∈ V → ((1^st ∘ 1^st )‘𝑈) = (1^st ‘(1^st ‘𝑈)))
9	3, 8	eqtrid 2783	. . 3 ⊢ (𝑈 ∈ V → ( +_𝑣 ‘𝑈) = (1^st ‘(1^st ‘𝑈)))
10		fvprc 6832	. . . 4 ⊢ (¬ 𝑈 ∈ V → ( +_𝑣 ‘𝑈) = ∅)
11		fvprc 6832	. . . . . 6 ⊢ (¬ 𝑈 ∈ V → (1^st ‘𝑈) = ∅)
12	11	fveq2d 6844	. . . . 5 ⊢ (¬ 𝑈 ∈ V → (1^st ‘(1^st ‘𝑈)) = (1^st ‘∅))
13		1st0 7948	. . . . 5 ⊢ (1^st ‘∅) = ∅
14	12, 13	eqtr2di 2788	. . . 4 ⊢ (¬ 𝑈 ∈ V → ∅ = (1^st ‘(1^st ‘𝑈)))
15	10, 14	eqtrd 2771	. . 3 ⊢ (¬ 𝑈 ∈ V → ( +_𝑣 ‘𝑈) = (1^st ‘(1^st ‘𝑈)))
16	9, 15	pm2.61i 182	. 2 ⊢ ( +_𝑣 ‘𝑈) = (1^st ‘(1^st ‘𝑈))
17	1, 16	eqtri 2759	1 ⊢ 𝐺 = (1^st ‘(1^st ‘𝑈))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 = wceq 1542 ∈ wcel 2114 Vcvv 3429 ∅c0 4273 ∘ ccom 5635 ⟶wf 6494 –onto→wfo 6496 ‘cfv 6498 1^st c1st 7940 +_𝑣 cpv 30656

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-sep 5231 ax-nul 5241 ax-pr 5375 ax-un 7689

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3062 df-rab 3390 df-v 3431 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-nul 4274 df-if 4467 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4851 df-br 5086 df-opab 5148 df-mpt 5167 df-id 5526 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-fo 6504 df-fv 6506 df-1st 7942 df-va 30666

This theorem is referenced by: nvvop 30680 nvablo 30687 nvsf 30690 nvscl 30697 nvsid 30698 nvsass 30699 nvdi 30701 nvdir 30702 nv2 30703 nv0 30708 nvsz 30709 nvinv 30710 cnnvg 30749 phop 30889 ip0i 30896 ipdirilem 30900 h2hva 31045 hhssva 31328 hhshsslem1 31338

W3C validator