Metamath Proof Explorer

Theorem tendo02

Description: Value of additive identity endomorphism. (Contributed by NM, 11-Jun-2013)

Ref Expression
Hypotheses tendo0cbv.o 
|- O = ( f e. T |-> ( _I |` B ) )
tendo02.b 
|- B = ( Base ` K )
Assertion tendo02 
|- ( F e. T -> ( O ` F ) = ( _I |` B ) )

Proof

Step Hyp Ref Expression
1 tendo0cbv.o 
 |-  O = ( f e. T |-> ( _I |` B ) )
2 tendo02.b 
 |-  B = ( Base ` K )
3 eqidd 
 |-  ( g = F -> ( _I |` B ) = ( _I |` B ) )
4 1 tendo0cbv 
 |-  O = ( g e. T |-> ( _I |` B ) )
5 funi 
 |-  Fun _I
6 2 fvexi 
 |-  B e. _V
7 resfunexg 
 |-  ( ( Fun _I /\ B e. _V ) -> ( _I |` B ) e. _V )
8 5 6 7 mp2an 
 |-  ( _I |` B ) e. _V
9 3 4 8 fvmpt 
 |-  ( F e. T -> ( O ` F ) = ( _I |` B ) )