This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )