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

Metamath Proof Explorer

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 ` U )
0vfval.5 
|- Z = ( 0vec ` U )
Assertion 0vfval 
|- ( U e. V -> Z = ( GId ` G ) )

Proof

Step Hyp Ref Expression
1 0vfval.2 
 |-  G = ( +v ` U )
2 0vfval.5 
 |-  Z = ( 0vec ` U )
3 elex 
 |-  ( U e. V -> U e. _V )
4 fo1st 
 |-  1st : _V -onto-> _V
5 fofn 
 |-  ( 1st : _V -onto-> _V -> 1st Fn _V )
6 4 5 ax-mp 
 |-  1st Fn _V
7 ssv 
 |-  ran 1st C_ _V
8 fnco 
 |-  ( ( 1st Fn _V /\ 1st Fn _V /\ ran 1st C_ _V ) -> ( 1st o. 1st ) Fn _V )
9 6 6 7 8 mp3an 
 |-  ( 1st o. 1st ) Fn _V
10 df-va 
 |-  +v = ( 1st o. 1st )
11 10 fneq1i 
 |-  ( +v Fn _V <-> ( 1st o. 1st ) Fn _V )
12 9 11 mpbir 
 |-  +v Fn _V
13 fvco2 
 |-  ( ( +v Fn _V /\ U e. _V ) -> ( ( GId o. +v ) ` U ) = ( GId ` ( +v ` U ) ) )
14 12 13 mpan 
 |-  ( U e. _V -> ( ( GId o. +v ) ` U ) = ( GId ` ( +v ` U ) ) )
15 df-0v 
 |-  0vec = ( GId o. +v )
16 15 fveq1i 
 |-  ( 0vec ` U ) = ( ( GId o. +v ) ` U )
17 2 16 eqtri 
 |-  Z = ( ( GId o. +v ) ` U )
18 1 fveq2i 
 |-  ( GId ` G ) = ( GId ` ( +v ` U ) )
19 14 17 18 3eqtr4g 
 |-  ( U e. _V -> Z = ( GId ` G ) )
20 3 19 syl 
 |-  ( U e. V -> Z = ( GId ` G ) )