Theorem 0vfval

Description: Value of the function for the zero vector on a normed complex vector space. (Contributed by NM, 24-Apr-2007) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	0vfval.2	$$⊢G={+}_v\left(U\right)$$
	0vfval.5	$$⊢Z=0_{\mathrm{vec}}\left(U\right)$$
Assertion	0vfval	$$⊢U\in V\to Z=\mathrm{GId}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		0vfval.2	$$⊢G={+}_v\left(U\right)$$
2		0vfval.5	$$⊢Z=0_{\mathrm{vec}}\left(U\right)$$
3		elex	$$⊢U\in V\to U\in \mathrm{V}$$
4		fo1st	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$
5		fofn	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to 1^{st}Fn\mathrm{V}$$
6	4 5	ax-mp	$$⊢1^{st}Fn\mathrm{V}$$
7		ssv	$$⊢\mathrm{ran}{1}^{st}\subseteq \mathrm{V}$$
8		fnco	$$⊢\left(1^{st}Fn\mathrm{V}\wedge 1^{st}Fn\mathrm{V}\wedge \mathrm{ran}{1}^{st}\subseteq \mathrm{V}\right)\to \left(1^{st}\circ 1^{st}\right)Fn\mathrm{V}$$
9	6 6 7 8	mp3an	$$⊢\left(1^{st}\circ 1^{st}\right)Fn\mathrm{V}$$
10		df-va	$$⊢{+}_v=1^{st}\circ 1^{st}$$
11	10	fneq1i	$$⊢{+}_{v}Fn\mathrm{V}\leftrightarrow \left(1^{st}\circ 1^{st}\right)Fn\mathrm{V}$$
12	9 11	mpbir	$$⊢{+}_{v}Fn\mathrm{V}$$
13		fvco2	$$⊢\left({+}_{v}Fn\mathrm{V}\wedge U\in \mathrm{V}\right)\to \left(\mathrm{GId}\circ {+}_v\right)\left(U\right)=\mathrm{GId}\left({+}_v\left(U\right)\right)$$
14	12 13	mpan	$$⊢U\in \mathrm{V}\to \left(\mathrm{GId}\circ {+}_v\right)\left(U\right)=\mathrm{GId}\left({+}_v\left(U\right)\right)$$
15		df-0v	$$⊢0_{\mathrm{vec}}=\mathrm{GId}\circ {+}_v$$
16	15	fveq1i	$$⊢0_{\mathrm{vec}}\left(U\right)=\left(\mathrm{GId}\circ {+}_v\right)\left(U\right)$$
17	2 16	eqtri	$$⊢Z=\left(\mathrm{GId}\circ {+}_v\right)\left(U\right)$$
18	1	fveq2i	$$⊢\mathrm{GId}\left(G\right)=\mathrm{GId}\left({+}_v\left(U\right)\right)$$
19	14 17 18	3eqtr4g	$$⊢U\in \mathrm{V}\to Z=\mathrm{GId}\left(G\right)$$
20	3 19	syl	$$⊢U\in V\to Z=\mathrm{GId}\left(G\right)$$