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 )