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

Metamath Proof Explorer

Theorem tendoipl2

Description: Property of the additive inverse endomorphism. (Contributed by NM, 29-Sep-2014)

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

Proof

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