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