Metamath Proof Explorer

Theorem tendo0plr

Description: Property of the additive identity endormorphism. (Contributed by NM, 21-Feb-2014)

Ref Expression
Hypotheses tendo0.b 
|- B = ( Base ` K )
tendo0.h 
|- H = ( LHyp ` K )
tendo0.t 
|- T = ( ( LTrn ` K ) ` W )
tendo0.e 
|- E = ( ( TEndo ` K ) ` W )
tendo0.o 
|- O = ( f e. T |-> ( _I |` B ) )
tendo0pl.p 
|- P = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )
Assertion tendo0plr 
|- ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> ( S P O ) = S )

Proof

Step Hyp Ref Expression
1 tendo0.b 
 |-  B = ( Base ` K )
2 tendo0.h 
 |-  H = ( LHyp ` K )
3 tendo0.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 tendo0.e 
 |-  E = ( ( TEndo ` K ) ` W )
5 tendo0.o 
 |-  O = ( f e. T |-> ( _I |` B ) )
6 tendo0pl.p 
 |-  P = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )
7 1 2 3 4 5 tendo0cl 
 |-  ( ( K e. HL /\ W e. H ) -> O e. E )
8 7 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> O e. E )
9 2 3 4 6 tendoplcom 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ O e. E ) -> ( S P O ) = ( O P S ) )
10 8 9 mpd3an3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> ( S P O ) = ( O P S ) )
11 1 2 3 4 5 6 tendo0pl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> ( O P S ) = S )
12 10 11 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> ( S P O ) = S )