Metamath Proof Explorer


Theorem tendoipl2

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

Ref Expression
Hypotheses tendoicl.h H=LHypK
tendoicl.t T=LTrnKW
tendoicl.e E=TEndoKW
tendoicl.i I=sEfTsf-1
tendoi.b B=BaseK
tendoi.p P=sE,tEfTsftf
tendoi.o O=fTIB
Assertion tendoipl2 KHLWHSESPIS=O

Proof

Step Hyp Ref Expression
1 tendoicl.h H=LHypK
2 tendoicl.t T=LTrnKW
3 tendoicl.e E=TEndoKW
4 tendoicl.i I=sEfTsf-1
5 tendoi.b B=BaseK
6 tendoi.p P=sE,tEfTsftf
7 tendoi.o O=fTIB
8 1 2 3 4 tendoicl KHLWHSEISE
9 1 2 3 6 tendoplcom KHLWHSEISESPIS=ISPS
10 8 9 mpd3an3 KHLWHSESPIS=ISPS
11 1 2 3 4 5 6 7 tendoipl KHLWHSEISPS=O
12 10 11 eqtrd KHLWHSESPIS=O