Metamath Proof Explorer


Theorem tendoipl

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

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 f T s f -1
tendoi.b B = Base K
tendoi.p P = s E , t E f T s f t f
tendoi.o O = f T I B
Assertion tendoipl K HL W H S E I S P 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 f T s f -1
5 tendoi.b B = Base K
6 tendoi.p P = s E , t E f T s f t f
7 tendoi.o O = f T I B
8 simpl K HL W H S E K HL W H
9 1 2 3 4 tendoicl K HL W H S E I S E
10 simpr K HL W H S E S E
11 1 2 3 6 tendoplcl K HL W H I S E S E I S P S E
12 8 9 10 11 syl3anc K HL W H S E I S P S E
13 5 1 2 3 7 tendo0cl K HL W H O E
14 13 adantr K HL W H S E O E
15 4 2 tendoi2 S E g T I S g = S g -1
16 15 adantll K HL W H S E g T I S g = S g -1
17 16 coeq1d K HL W H S E g T I S g S g = S g -1 S g
18 simpll K HL W H S E g T K HL W H
19 1 2 3 tendocl K HL W H S E g T S g T
20 19 3expa K HL W H S E g T S g T
21 5 1 2 ltrn1o K HL W H S g T S g : B 1-1 onto B
22 18 20 21 syl2anc K HL W H S E g T S g : B 1-1 onto B
23 f1ococnv1 S g : B 1-1 onto B S g -1 S g = I B
24 22 23 syl K HL W H S E g T S g -1 S g = I B
25 17 24 eqtrd K HL W H S E g T I S g S g = I B
26 9 adantr K HL W H S E g T I S E
27 simplr K HL W H S E g T S E
28 simpr K HL W H S E g T g T
29 6 2 tendopl2 I S E S E g T I S P S g = I S g S g
30 26 27 28 29 syl3anc K HL W H S E g T I S P S g = I S g S g
31 7 5 tendo02 g T O g = I B
32 31 adantl K HL W H S E g T O g = I B
33 25 30 32 3eqtr4d K HL W H S E g T I S P S g = O g
34 33 ralrimiva K HL W H S E g T I S P S g = O g
35 1 2 3 tendoeq1 K HL W H I S P S E O E g T I S P S g = O g I S P S = O
36 8 12 14 34 35 syl121anc K HL W H S E I S P S = O