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 30860

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 30852	. . . . 5 ⊢ +_𝑣 = (1^st ∘ 1^st )
3	2	fveq1i 6872	. . . 4 ⊢ ( +_𝑣 ‘𝑈) = ((1^st ∘ 1^st )‘𝑈)
4		fo1st 7994	. . . . . 6 ⊢ 1^st :V–onto→V
5		fof 6782	. . . . . 6 ⊢ (1^st :V–onto→V → 1^st :V⟶V)
6	4, 5	ax-mp 5	. . . . 5 ⊢ 1^st :V⟶V
7		fvco3 6971	. . . . 5 ⊢ ((1^st :V⟶V ∧ 𝑈 ∈ V) → ((1^st ∘ 1^st )‘𝑈) = (1^st ‘(1^st ‘𝑈)))
8	6, 7	mpan 702	. . . 4 ⊢ (𝑈 ∈ V → ((1^st ∘ 1^st )‘𝑈) = (1^st ‘(1^st ‘𝑈)))
9	3, 8	eqtrid 2812	. . 3 ⊢ (𝑈 ∈ V → ( +_𝑣 ‘𝑈) = (1^st ‘(1^st ‘𝑈)))
10		fvprc 6863	. . . 4 ⊢ (¬ 𝑈 ∈ V → ( +_𝑣 ‘𝑈) = ∅)
11		fvprc 6863	. . . . . 6 ⊢ (¬ 𝑈 ∈ V → (1^st ‘𝑈) = ∅)
12	11	fveq2d 6875	. . . . 5 ⊢ (¬ 𝑈 ∈ V → (1^st ‘(1^st ‘𝑈)) = (1^st ‘∅))
13		1st0 7980	. . . . 5 ⊢ (1^st ‘∅) = ∅
14	12, 13	eqtr2di 2817	. . . 4 ⊢ (¬ 𝑈 ∈ V → ∅ = (1^st ‘(1^st ‘𝑈)))
15	10, 14	eqtrd 2800	. . 3 ⊢ (¬ 𝑈 ∈ V → ( +_𝑣 ‘𝑈) = (1^st ‘(1^st ‘𝑈)))
16	9, 15	pm2.61i 184	. 2 ⊢ ( +_𝑣 ‘𝑈) = (1^st ‘(1^st ‘𝑈))
17	1, 16	eqtri 2788	1 ⊢ 𝐺 = (1^st ‘(1^st ‘𝑈))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 = wceq 1563 ∈ wcel 2145 Vcvv 3457 ∅c0 4288 ∘ ccom 5655 ⟶wf 6521 –onto→wfo 6523 ‘cfv 6525 1^st c1st 7972 +_𝑣 cpv 30842

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5250 ax-nul 5260 ax-pr 5394 ax-un 7722

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3080 df-rex 3090 df-rab 3418 df-v 3459 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-br 5105 df-opab 5167 df-mpt 5186 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-fo 6531 df-fv 6533 df-1st 7974 df-va 30852

This theorem is referenced by: nvvop 30866 nvablo 30873 nvsf 30876 nvscl 30883 nvsid 30884 nvsass 30885 nvdi 30887 nvdir 30888 nv2 30889 nv0 30894 nvsz 30895 nvinv 30896 cnnvg 30935 phop 31075 ip0i 31082 ipdirilem 31086 h2hva 31231 hhssva 31514 hhshsslem1 31524

W3C validator