Metamath Proof Explorer


Theorem tendoicl

Description: Closure 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
Assertion tendoicl K HL W H S E I S E

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 eqid K = K
6 eqid trL K W = trL K W
7 simpl K HL W H S E K HL W H
8 simpll K HL W H S E g T K HL W H
9 1 2 3 tendocl K HL W H S E g T S g T
10 9 3expa K HL W H S E g T S g T
11 1 2 ltrncnv K HL W H S g T S g -1 T
12 8 10 11 syl2anc K HL W H S E g T S g -1 T
13 12 fmpttd K HL W H S E g T S g -1 : T T
14 4 2 tendoi S E I S = g T S g -1
15 14 adantl K HL W H S E I S = g T S g -1
16 15 feq1d K HL W H S E I S : T T g T S g -1 : T T
17 13 16 mpbird K HL W H S E I S : T T
18 simp1r K HL W H S E g T h T S E
19 1 2 ltrnco K HL W H g T h T g h T
20 19 3adant1r K HL W H S E g T h T g h T
21 4 2 tendoi2 S E g h T I S g h = S g h -1
22 18 20 21 syl2anc K HL W H S E g T h T I S g h = S g h -1
23 cnvco S h S g -1 = S g -1 S h -1
24 1 2 ltrncom K HL W H g T h T g h = h g
25 24 3adant1r K HL W H S E g T h T g h = h g
26 25 fveq2d K HL W H S E g T h T S g h = S h g
27 simp1ll K HL W H S E g T h T K HL
28 simp1lr K HL W H S E g T h T W H
29 simp3 K HL W H S E g T h T h T
30 simp2 K HL W H S E g T h T g T
31 1 2 3 tendovalco K HL W H S E h T g T S h g = S h S g
32 27 28 18 29 30 31 syl32anc K HL W H S E g T h T S h g = S h S g
33 26 32 eqtrd K HL W H S E g T h T S g h = S h S g
34 33 cnveqd K HL W H S E g T h T S g h -1 = S h S g -1
35 4 2 tendoi2 S E g T I S g = S g -1
36 18 30 35 syl2anc K HL W H S E g T h T I S g = S g -1
37 4 2 tendoi2 S E h T I S h = S h -1
38 18 29 37 syl2anc K HL W H S E g T h T I S h = S h -1
39 36 38 coeq12d K HL W H S E g T h T I S g I S h = S g -1 S h -1
40 23 34 39 3eqtr4a K HL W H S E g T h T S g h -1 = I S g I S h
41 22 40 eqtrd K HL W H S E g T h T I S g h = I S g I S h
42 35 adantll K HL W H S E g T I S g = S g -1
43 42 fveq2d K HL W H S E g T trL K W I S g = trL K W S g -1
44 1 2 6 trlcnv K HL W H S g T trL K W S g -1 = trL K W S g
45 8 10 44 syl2anc K HL W H S E g T trL K W S g -1 = trL K W S g
46 43 45 eqtrd K HL W H S E g T trL K W I S g = trL K W S g
47 5 1 2 6 3 tendotp K HL W H S E g T trL K W S g K trL K W g
48 47 3expa K HL W H S E g T trL K W S g K trL K W g
49 46 48 eqbrtrd K HL W H S E g T trL K W I S g K trL K W g
50 5 1 2 6 3 7 17 41 49 istendod K HL W H S E I S E