Theorem 0vfval 8163

Description: Value of the function for the zero vector on a normed complex vector space.

Hypotheses

Ref	Expression
0vfval.2	|- G = (+v` U)
0vfval.5	|- Z = (0v` U)

Assertion

Ref	Expression
0vfval	|- Z = (Id` G)

Proof of Theorem 0vfval

Step	Hyp	Ref	Expression
1		visset 1804	. . . . . . . . . 10 |- x e. V
2		rnexg 3345	. . . . . . . . . 10 |- (x e. V -> ran x e. V)
3	1, 2	ax-mp 7	. . . . . . . . 9 |- ran x e. V
4	3	rabex 2715	. . . . . . . 8 |- {z e. ran x | A.w e. ran x(zxw) = w} e. V
5	4	uniex 2861	. . . . . . 7 |- U.{z e. ran x | A.w e. ran x(zxw) = w} e. V
6		df-gid 7972	. . . . . . 7 |- Id = {<.x, y>. | (x e. Grp /\ y = U.{z e. ran x | A.w e. ran x(zxw) = w})}
7	5, 6	fnopab2 3604	. . . . . 6 |- Id Fn Grp
8		fnfun 3571	. . . . . 6 |- (Id Fn Grp -> Fun Id)
9	7, 8	ax-mp 7	. . . . 5 |- Fun Id
10		fo1st 4075	. . . . . . . . 9 |- 1st:V-onto->V
11		fof 3657	. . . . . . . . 9 |- (1st:V-onto->V -> 1st:V-->V)
12	10, 11	ax-mp 7	. . . . . . . 8 |- 1st:V-->V
13		ffn 3613	. . . . . . . 8 |- (1st:V-->V -> 1st Fn V)
14	12, 13	ax-mp 7	. . . . . . 7 |- 1st Fn V
15		ssv 2071	. . . . . . 7 |- ran 1st (_ V
16		fnco 3581	. . . . . . 7 |- ((1st Fn V /\ 1st Fn V /\ ran 1st (_ V) -> (1st o. 1st) Fn V)
17	14, 14, 15, 16	mp3an 913	. . . . . 6 |- (1st o. 1st) Fn V
18		df-va 8152	. . . . . . 7 |- +v = (1st o. 1st)
19		fneq1 3568	. . . . . . 7 |- (+v = (1st o. 1st) -> (+v Fn V <-> (1st o. 1st) Fn V))
20	18, 19	ax-mp 7	. . . . . 6 |- (+v Fn V <-> (1st o. 1st) Fn V)
21	17, 20	mpbir 190	. . . . 5 |- +v Fn V
22		fvco2 3760	. . . . 5 |- ((Fun Id /\ +v Fn V /\ U e. V) -> ((Id o. +v)` U) = (Id` (+v` U)))
23	9, 21, 22	mp3an12 903	. . . 4 |- (U e. V -> ((Id o. +v)` U) = (Id` (+v` U)))
24		df-0v 8155	. . . . 5 |- 0v = (Id o. +v)
25	24	fveq1i 3710	. . . 4 |- (0v` U) = ((Id o. +v)` U)
26	23, 25	syl5eq 1511	. . 3 |- (U e. V -> (0v` U) = (Id` (+v` U)))
27		fvprc 3706	. . . 4 |- (-. U e. V -> (0v` U) = (/))
28		fvprc 3706	. . . . . 6 |- (-. U e. V -> (+v` U) = (/))
29	28	fveq2d 3713	. . . . 5 |- (-. U e. V -> (Id` (+v` U)) = (Id` (/)))
30		0ngrp 7989	. . . . . . 7 |- -. (/) e. Grp
31	5, 6	dmopab2 3605	. . . . . . . 8 |- dom Id = Grp
32	31	eleq2i 1530	. . . . . . 7 |- ((/) e. dom Id <-> (/) e. Grp)
33	30, 32	mtbir 192	. . . . . 6 |- -. (/) e. dom Id
34		ndmfv 3730	. . . . . 6 |- (-. (/) e. dom Id -> (Id` (/)) = (/))
35	33, 34	ax-mp 7	. . . . 5 |- (Id` (/)) = (/)
36	29, 35	syl6req 1516	. . . 4 |- (-. U e. V -> (/) = (Id` (+v` U)))
37	27, 36	eqtrd 1499	. . 3 |- (-. U e. V -> (0v` U) = (Id` (+v` U)))
38	26, 37	pm2.61i 126	. 2 |- (0v` U) = (Id` (+v` U))
39		0vfval.5	. 2 |- Z = (0v` U)
40		0vfval.2	. . 3 |- G = (+v` U)
41	40	fveq2i 3712	. 2 |- (Id` G) = (Id` (+v` U))
42	38, 39, 41	3eqtr4 1497	1 |- Z = (Id` G)

Syntax hints:  -. wn 2   <-> wb 146   = wceq 953   e. wcel 955  A.wral 1637  {crab 1640  Vcvv 1802   (_ wss 2037  (/)c0 2270  U.cuni 2493  dom cdm 3160  ran crn 3161   o. ccom 3164  Fun wfun 3166   Fn wfn 3167  -->wf 3168  -onto->wfo 3170  ` cfv 3172  (class class class)co 3948  1stc1st 4061  Grpcgr 7967  Idcgi 7968  +vcpv 8142  0vcn0v 8145

This theorem is referenced by:  nvi 8173  nvvc 8174  nvzcl 8195  nv0rid 8196  nv0lid 8197  nv0 8198  nvsz 8199  nvrinv 8213  nvlinv 8214  nvtri 8237  hh0v 8956  hhssabl 9053

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769  ax-un 2857

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-rex 1642  df-rab 1644  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-uni 2494  df-br 2610  df-opab 2657  df-id 2824  df-xp 3174  df-rel 3175  df-cnv 3176  df-co 3177  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fun 3182  df-fn 3183  df-f 3184  df-fo 3186  df-fv 3188  df-opr 3950  df-1st 4063  df-grp 7971  df-gid 7972  df-va 8152  df-0v 8155

Copyright terms: Public domain