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 31198

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 31190	. . . . 5 ⊢ +_𝑣 = (1^st ∘ 1^st )
3	2	fveq1i 6884	. . . 4 ⊢ ( +_𝑣 ‘𝑈) = ((1^st ∘ 1^st )‘𝑈)
4		fo1st 8019	. . . . . 6 ⊢ 1^st :V–onto→V
5		fof 6794	. . . . . 6 ⊢ (1^st :V–onto→V → 1^st :V⟶V)
6	4, 5	ax-mp 5	. . . . 5 ⊢ 1^st :V⟶V
7		fvco3 6983	. . . . 5 ⊢ ((1^st :V⟶V ∧ 𝑈 ∈ V) → ((1^st ∘ 1^st )‘𝑈) = (1^st ‘(1^st ‘𝑈)))
8	6, 7	mpan 703	. . . 4 ⊢ (𝑈 ∈ V → ((1^st ∘ 1^st )‘𝑈) = (1^st ‘(1^st ‘𝑈)))
9	3, 8	eqtrid 2808	. . 3 ⊢ (𝑈 ∈ V → ( +_𝑣 ‘𝑈) = (1^st ‘(1^st ‘𝑈)))
10		fvprc 6875	. . . 4 ⊢ (¬ 𝑈 ∈ V → ( +_𝑣 ‘𝑈) = ∅)
11		fvprc 6875	. . . . . 6 ⊢ (¬ 𝑈 ∈ V → (1^st ‘𝑈) = ∅)
12	11	fveq2d 6887	. . . . 5 ⊢ (¬ 𝑈 ∈ V → (1^st ‘(1^st ‘𝑈)) = (1^st ‘∅))
13		1st0 8005	. . . . 5 ⊢ (1^st ‘∅) = ∅
14	12, 13	eqtr2di 2813	. . . 4 ⊢ (¬ 𝑈 ∈ V → ∅ = (1^st ‘(1^st ‘𝑈)))
15	10, 14	eqtrd 2796	. . 3 ⊢ (¬ 𝑈 ∈ V → ( +_𝑣 ‘𝑈) = (1^st ‘(1^st ‘𝑈)))
16	9, 15	pm2.61i 184	. 2 ⊢ ( +_𝑣 ‘𝑈) = (1^st ‘(1^st ‘𝑈))
17	1, 16	eqtri 2784	1 ⊢ 𝐺 = (1^st ‘(1^st ‘𝑈))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 = wceq 1570 ∈ wcel 2145 Vcvv 3451 ∅c0 4279 ∘ ccom 5655 ⟶wf 6533 –onto→wfo 6535 ‘cfv 6537 1^st c1st 7997 +_𝑣 cpv 31180

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-sep 5249 ax-nul 5260 ax-pr 5391 ax-un 7749

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3078 df-rex 3088 df-rab 3414 df-v 3453 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-br 5104 df-opab 5168 df-mpt 5187 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 6493 df-fun 6539 df-fn 6540 df-f 6541 df-fo 6543 df-fv 6545 df-1st 7999 df-va 31190

This theorem is used by: nvvop 31204 nvablo 31211 nvsf 31214 nvscl 31221 nvsid 31222 nvsass 31223 nvdi 31225 nvdir 31226 nv2 31227 nv0 31232 nvsz 31233 nvinv 31234 cnnvg 31273 phop 31413 ip0i 31420 ipdirilem 31424 h2hva 31569 hhssva 31852 hhshsslem1 31862

W3C validator