Metamath Proof Explorer

Theorem tendoi2

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

Ref Expression
Hypotheses tendoi.i 
|- I = ( s e. E |-> ( f e. T |-> `' ( s ` f ) ) )
tendoi.t 
|- T = ( ( LTrn ` K ) ` W )
Assertion tendoi2 
|- ( ( S e. E /\ F e. T ) -> ( ( I ` S ) ` F ) = `' ( S ` F ) )

Proof

Step Hyp Ref Expression
1 tendoi.i 
 |-  I = ( s e. E |-> ( f e. T |-> `' ( s ` f ) ) )
2 tendoi.t 
 |-  T = ( ( LTrn ` K ) ` W )
3 1 2 tendoi 
 |-  ( S e. E -> ( I ` S ) = ( g e. T |-> `' ( S ` g ) ) )
4 3 adantr 
 |-  ( ( S e. E /\ F e. T ) -> ( I ` S ) = ( g e. T |-> `' ( S ` g ) ) )
5 fveq2 
 |-  ( g = F -> ( S ` g ) = ( S ` F ) )
6 5 cnveqd 
 |-  ( g = F -> `' ( S ` g ) = `' ( S ` F ) )
7 6 adantl 
 |-  ( ( ( S e. E /\ F e. T ) /\ g = F ) -> `' ( S ` g ) = `' ( S ` F ) )
8 simpr 
 |-  ( ( S e. E /\ F e. T ) -> F e. T )
9 fvex 
 |-  ( S ` F ) e. _V
10 9 cnvex 
 |-  `' ( S ` F ) e. _V
11 10 a1i 
 |-  ( ( S e. E /\ F e. T ) -> `' ( S ` F ) e. _V )
12 4 7 8 11 fvmptd 
 |-  ( ( S e. E /\ F e. T ) -> ( ( I ` S ) ` F ) = `' ( S ` F ) )