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 ` U )
	vsfval.3	|- M = ( -v ` U )
Assertion	vsfval	|- M = ( /g ` G )

Proof

Step	Hyp	Ref	Expression
1		vsfval.2	|- G = ( +v ` U )
2		vsfval.3	|- M = ( -v ` U )
3		df-vs	|- -v = ( /g o. +v )
4	3	fveq1i	|- ( -v ` U ) = ( ( /g o. +v ) ` U )
5		fo1st	|- 1st : _V -onto-> _V
6		fof	|- ( 1st : _V -onto-> _V -> 1st : _V --> _V )
7	5 6	ax-mp	|- 1st : _V --> _V
8		fco	|- ( ( 1st : _V --> _V /\ 1st : _V --> _V ) -> ( 1st o. 1st ) : _V --> _V )
9	7 7 8	mp2an	|- ( 1st o. 1st ) : _V --> _V
10		df-va	|- +v = ( 1st o. 1st )
11	10	feq1i	|- ( +v : _V --> _V <-> ( 1st o. 1st ) : _V --> _V )
12	9 11	mpbir	|- +v : _V --> _V
13		fvco3	|- ( ( +v : _V --> _V /\ U e. _V ) -> ( ( /g o. +v ) ` U ) = ( /g ` ( +v ` U ) ) )
14	12 13	mpan	|- ( U e. _V -> ( ( /g o. +v ) ` U ) = ( /g ` ( +v ` U ) ) )
15	4 14	syl5eq	|- ( U e. _V -> ( -v ` U ) = ( /g ` ( +v ` U ) ) )
16		0ngrp	|- -. (/) e. GrpOp
17		vex	|- g e. _V
18	17	rnex	|- ran g e. _V
19	18 18	mpoex	|- ( x e. ran g , y e. ran g |-> ( x g ( ( inv ` g ) ` y ) ) ) e. _V
20		df-gdiv	|- /g = ( g e. GrpOp |-> ( x e. ran g , y e. ran g |-> ( x g ( ( inv ` g ) ` y ) ) ) )
21	19 20	dmmpti	|- dom /g = GrpOp
22	21	eleq2i	|- ( (/) e. dom /g <-> (/) e. GrpOp )
23	16 22	mtbir	|- -. (/) e. dom /g
24		ndmfv	|- ( -. (/) e. dom /g -> ( /g ` (/) ) = (/) )
25	23 24	mp1i	|- ( -. U e. _V -> ( /g ` (/) ) = (/) )
26		fvprc	|- ( -. U e. _V -> ( +v ` U ) = (/) )
27	26	fveq2d	|- ( -. U e. _V -> ( /g ` ( +v ` U ) ) = ( /g ` (/) ) )
28		fvprc	|- ( -. U e. _V -> ( -v ` U ) = (/) )
29	25 27 28	3eqtr4rd	|- ( -. U e. _V -> ( -v ` U ) = ( /g ` ( +v ` U ) ) )
30	15 29	pm2.61i	|- ( -v ` U ) = ( /g ` ( +v ` U ) )
31	1	fveq2i	|- ( /g ` G ) = ( /g ` ( +v ` U ) )
32	30 2 31	3eqtr4i	|- M = ( /g ` G )