Metamath Proof Explorer


Theorem tendocnv

Description: Converse of a trace-preserving endomorphism value. (Contributed by NM, 7-Apr-2014)

Ref Expression
Hypotheses tendosp.h H = LHyp K
tendosp.t T = LTrn K W
tendosp.e E = TEndo K W
Assertion tendocnv K HL W H S E F T S F -1 = S F -1

Proof

Step Hyp Ref Expression
1 tendosp.h H = LHyp K
2 tendosp.t T = LTrn K W
3 tendosp.e E = TEndo K W
4 simp1 K HL W H S E F T K HL W H
5 1 2 3 tendocl K HL W H S E F T S F T
6 eqid Base K = Base K
7 6 1 2 ltrn1o K HL W H S F T S F : Base K 1-1 onto Base K
8 4 5 7 syl2anc K HL W H S E F T S F : Base K 1-1 onto Base K
9 f1ococnv1 S F : Base K 1-1 onto Base K S F -1 S F = I Base K
10 8 9 syl K HL W H S E F T S F -1 S F = I Base K
11 10 coeq1d K HL W H S E F T S F -1 S F S F -1 = I Base K S F -1
12 simp2 K HL W H S E F T S E
13 6 1 3 tendoid K HL W H S E S I Base K = I Base K
14 4 12 13 syl2anc K HL W H S E F T S I Base K = I Base K
15 6 1 2 ltrn1o K HL W H F T F : Base K 1-1 onto Base K
16 15 3adant2 K HL W H S E F T F : Base K 1-1 onto Base K
17 f1ococnv2 F : Base K 1-1 onto Base K F F -1 = I Base K
18 16 17 syl K HL W H S E F T F F -1 = I Base K
19 18 fveq2d K HL W H S E F T S F F -1 = S I Base K
20 f1ococnv2 S F : Base K 1-1 onto Base K S F S F -1 = I Base K
21 8 20 syl K HL W H S E F T S F S F -1 = I Base K
22 14 19 21 3eqtr4rd K HL W H S E F T S F S F -1 = S F F -1
23 simp3 K HL W H S E F T F T
24 1 2 ltrncnv K HL W H F T F -1 T
25 24 3adant2 K HL W H S E F T F -1 T
26 1 2 3 tendospdi1 K HL W H S E F T F -1 T S F F -1 = S F S F -1
27 4 12 23 25 26 syl13anc K HL W H S E F T S F F -1 = S F S F -1
28 22 27 eqtrd K HL W H S E F T S F S F -1 = S F S F -1
29 28 coeq2d K HL W H S E F T S F -1 S F S F -1 = S F -1 S F S F -1
30 coass S F -1 S F S F -1 = S F -1 S F S F -1
31 coass S F -1 S F S F -1 = S F -1 S F S F -1
32 29 30 31 3eqtr4g K HL W H S E F T S F -1 S F S F -1 = S F -1 S F S F -1
33 10 coeq1d K HL W H S E F T S F -1 S F S F -1 = I Base K S F -1
34 1 2 3 tendocl K HL W H S E F -1 T S F -1 T
35 25 34 syld3an3 K HL W H S E F T S F -1 T
36 6 1 2 ltrn1o K HL W H S F -1 T S F -1 : Base K 1-1 onto Base K
37 4 35 36 syl2anc K HL W H S E F T S F -1 : Base K 1-1 onto Base K
38 f1of S F -1 : Base K 1-1 onto Base K S F -1 : Base K Base K
39 fcoi2 S F -1 : Base K Base K I Base K S F -1 = S F -1
40 37 38 39 3syl K HL W H S E F T I Base K S F -1 = S F -1
41 32 33 40 3eqtrd K HL W H S E F T S F -1 S F S F -1 = S F -1
42 1 2 ltrncnv K HL W H S F T S F -1 T
43 4 5 42 syl2anc K HL W H S E F T S F -1 T
44 6 1 2 ltrn1o K HL W H S F -1 T S F -1 : Base K 1-1 onto Base K
45 4 43 44 syl2anc K HL W H S E F T S F -1 : Base K 1-1 onto Base K
46 f1of S F -1 : Base K 1-1 onto Base K S F -1 : Base K Base K
47 fcoi2 S F -1 : Base K Base K I Base K S F -1 = S F -1
48 45 46 47 3syl K HL W H S E F T I Base K S F -1 = S F -1
49 11 41 48 3eqtr3rd K HL W H S E F T S F -1 = S F -1