Theorem vsfval

Description: Value of the function for the vector subtraction operation on a normed complex vector space. (Contributed by NM, 15-Feb-2008) (Revised by Mario Carneiro, 27-Dec-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	vsfval.2	$$⊢G={+}_v\left(U\right)$$
	vsfval.3	$$⊢M={-}_v\left(U\right)$$
Assertion	vsfval	$$⊢M={/}_g\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		vsfval.2	$$⊢G={+}_v\left(U\right)$$
2		vsfval.3	$$⊢M={-}_v\left(U\right)$$
3		df-vs	$$⊢{-}_v={/}_g\circ {+}_v$$
4	3	fveq1i	$$⊢{-}_v\left(U\right)=\left({/}_g\circ {+}_v\right)\left(U\right)$$
5		fo1st	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$
6		fof	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to 1^{st}:\mathrm{V}⟶\mathrm{V}$$
7	5 6	ax-mp	$$⊢1^{st}:\mathrm{V}⟶\mathrm{V}$$
8		fco	$$⊢\left(1^{st}:\mathrm{V}⟶\mathrm{V}\wedge 1^{st}:\mathrm{V}⟶\mathrm{V}\right)\to \left(1^{st}\circ 1^{st}\right):\mathrm{V}⟶\mathrm{V}$$
9	7 7 8	mp2an	$$⊢\left(1^{st}\circ 1^{st}\right):\mathrm{V}⟶\mathrm{V}$$
10		df-va	$$⊢{+}_v=1^{st}\circ 1^{st}$$
11	10	feq1i	$$⊢{+}_v:\mathrm{V}⟶\mathrm{V}\leftrightarrow \left(1^{st}\circ 1^{st}\right):\mathrm{V}⟶\mathrm{V}$$
12	9 11	mpbir	$$⊢{+}_v:\mathrm{V}⟶\mathrm{V}$$
13		fvco3	$$⊢\left({+}_v:\mathrm{V}⟶\mathrm{V}\wedge U\in \mathrm{V}\right)\to \left({/}_g\circ {+}_v\right)\left(U\right)={/}_g\left({+}_v\left(U\right)\right)$$
14	12 13	mpan	$$⊢U\in \mathrm{V}\to \left({/}_g\circ {+}_v\right)\left(U\right)={/}_g\left({+}_v\left(U\right)\right)$$
15	4 14	syl5eq	$$⊢U\in \mathrm{V}\to {-}_v\left(U\right)={/}_g\left({+}_v\left(U\right)\right)$$
16		0ngrp	$$⊢\neg \varnothing \in \mathrm{GrpOp}$$
17		vex	$$⊢g\in \mathrm{V}$$
18	17	rnex	$$⊢\mathrm{ran}g\in \mathrm{V}$$
19	18 18	mpoex	$$⊢\left(x\in \mathrm{ran}g,y\in \mathrm{ran}g⟼xg\mathrm{inv}\left(g\right)\left(y\right)\right)\in \mathrm{V}$$
20		df-gdiv	$$⊢{/}_g=\left(g\in \mathrm{GrpOp}⟼\left(x\in \mathrm{ran}g,y\in \mathrm{ran}g⟼xg\mathrm{inv}\left(g\right)\left(y\right)\right)\right)$$
21	19 20	dmmpti	$$⊢\mathrm{dom}{/}_g=\mathrm{GrpOp}$$
22	21	eleq2i	$$⊢\varnothing \in \mathrm{dom}{/}_g\leftrightarrow \varnothing \in \mathrm{GrpOp}$$
23	16 22	mtbir	$$⊢\neg \varnothing \in \mathrm{dom}{/}_g$$
24		ndmfv	$$⊢\neg \varnothing \in \mathrm{dom}{/}_g\to {/}_g\left(\varnothing \right)=\varnothing$$
25	23 24	mp1i	$$⊢\neg U\in \mathrm{V}\to {/}_g\left(\varnothing \right)=\varnothing$$
26		fvprc	$$⊢\neg U\in \mathrm{V}\to {+}_v\left(U\right)=\varnothing$$
27	26	fveq2d	$$⊢\neg U\in \mathrm{V}\to {/}_g\left({+}_v\left(U\right)\right)={/}_g\left(\varnothing \right)$$
28		fvprc	$$⊢\neg U\in \mathrm{V}\to {-}_v\left(U\right)=\varnothing$$
29	25 27 28	3eqtr4rd	$$⊢\neg U\in \mathrm{V}\to {-}_v\left(U\right)={/}_g\left({+}_v\left(U\right)\right)$$
30	15 29	pm2.61i	$$⊢{-}_v\left(U\right)={/}_g\left({+}_v\left(U\right)\right)$$
31	1	fveq2i	$$⊢{/}_g\left(G\right)={/}_g\left({+}_v\left(U\right)\right)$$
32	30 2 31	3eqtr4i	$$⊢M={/}_g\left(G\right)$$