Metamath Proof Explorer


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 eqtrid
 |-  ( 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 )