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 27914

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 27906	. . . . 5 ⊢ +_𝑣 = (1^st ∘ 1^st )
3	2	fveq1i 6376	. . . 4 ⊢ ( +_𝑣 ‘𝑈) = ((1^st ∘ 1^st )‘𝑈)
4		fo1st 7386	. . . . . 6 ⊢ 1^st :V–onto→V
5		fof 6298	. . . . . 6 ⊢ (1^st :V–onto→V → 1^st :V⟶V)
6	4, 5	ax-mp 5	. . . . 5 ⊢ 1^st :V⟶V
7		fvco3 6464	. . . . 5 ⊢ ((1^st :V⟶V ∧ 𝑈 ∈ V) → ((1^st ∘ 1^st )‘𝑈) = (1^st ‘(1^st ‘𝑈)))
8	6, 7	mpan 681	. . . 4 ⊢ (𝑈 ∈ V → ((1^st ∘ 1^st )‘𝑈) = (1^st ‘(1^st ‘𝑈)))
9	3, 8	syl5eq 2811	. . 3 ⊢ (𝑈 ∈ V → ( +_𝑣 ‘𝑈) = (1^st ‘(1^st ‘𝑈)))
10		fvprc 6368	. . . 4 ⊢ (¬ 𝑈 ∈ V → ( +_𝑣 ‘𝑈) = ∅)
11		fvprc 6368	. . . . . 6 ⊢ (¬ 𝑈 ∈ V → (1^st ‘𝑈) = ∅)
12	11	fveq2d 6379	. . . . 5 ⊢ (¬ 𝑈 ∈ V → (1^st ‘(1^st ‘𝑈)) = (1^st ‘∅))
13		1st0 7372	. . . . 5 ⊢ (1^st ‘∅) = ∅
14	12, 13	syl6req 2816	. . . 4 ⊢ (¬ 𝑈 ∈ V → ∅ = (1^st ‘(1^st ‘𝑈)))
15	10, 14	eqtrd 2799	. . 3 ⊢ (¬ 𝑈 ∈ V → ( +_𝑣 ‘𝑈) = (1^st ‘(1^st ‘𝑈)))
16	9, 15	pm2.61i 176	. 2 ⊢ ( +_𝑣 ‘𝑈) = (1^st ‘(1^st ‘𝑈))
17	1, 16	eqtri 2787	1 ⊢ 𝐺 = (1^st ‘(1^st ‘𝑈))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 = wceq 1652 ∈ wcel 2155 Vcvv 3350 ∅c0 4079 ∘ ccom 5281 ⟶wf 6064 –onto→wfo 6066 ‘cfv 6068 1^st c1st 7364 +_𝑣 cpv 27896

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1890 ax-4 1904 ax-5 2005 ax-6 2070 ax-7 2105 ax-8 2157 ax-9 2164 ax-10 2183 ax-11 2198 ax-12 2211 ax-13 2352 ax-ext 2743 ax-sep 4941 ax-nul 4949 ax-pow 5001 ax-pr 5062 ax-un 7147

This theorem depends on definitions: df-bi 198 df-an 385 df-or 874 df-3an 1109 df-tru 1656 df-ex 1875 df-nf 1879 df-sb 2063 df-mo 2565 df-eu 2582 df-clab 2752 df-cleq 2758 df-clel 2761 df-nfc 2896 df-ne 2938 df-ral 3060 df-rex 3061 df-rab 3064 df-v 3352 df-sbc 3597 df-dif 3735 df-un 3737 df-in 3739 df-ss 3746 df-nul 4080 df-if 4244 df-sn 4335 df-pr 4337 df-op 4341 df-uni 4595 df-br 4810 df-opab 4872 df-mpt 4889 df-id 5185 df-xp 5283 df-rel 5284 df-cnv 5285 df-co 5286 df-dm 5287 df-rn 5288 df-res 5289 df-ima 5290 df-iota 6031 df-fun 6070 df-fn 6071 df-f 6072 df-fo 6074 df-fv 6076 df-1st 7366 df-va 27906

This theorem is referenced by: nvvop 27920 nvablo 27927 nvsf 27930 nvscl 27937 nvsid 27938 nvsass 27939 nvdi 27941 nvdir 27942 nv2 27943 nv0 27948 nvsz 27949 nvinv 27950 cnnvg 27989 phop 28129 ip0i 28136 ipdirilem 28140 h2hva 28287 hhssva 28570 hhshsslem1 28580

W3C validator