Metamath Proof Explorer


Theorem trlcocnv

Description: Swap the arguments of the trace of a composition with converse. (Contributed by NM, 1-Jul-2013)

Ref Expression
Hypotheses trlcocnv.h H=LHypK
trlcocnv.t T=LTrnKW
trlcocnv.r R=trLKW
Assertion trlcocnv KHLWHFTGTRFG-1=RGF-1

Proof

Step Hyp Ref Expression
1 trlcocnv.h H=LHypK
2 trlcocnv.t T=LTrnKW
3 trlcocnv.r R=trLKW
4 simp1 KHLWHFTGTKHLWH
5 1 2 ltrncnv KHLWHGTG-1T
6 5 3adant2 KHLWHFTGTG-1T
7 1 2 ltrnco KHLWHFTG-1TFG-1T
8 6 7 syld3an3 KHLWHFTGTFG-1T
9 1 2 3 trlcnv KHLWHFG-1TRFG-1-1=RFG-1
10 4 8 9 syl2anc KHLWHFTGTRFG-1-1=RFG-1
11 cnvco FG-1-1=G-1-1F-1
12 cocnvcnv1 G-1-1F-1=GF-1
13 11 12 eqtri FG-1-1=GF-1
14 13 fveq2i RFG-1-1=RGF-1
15 10 14 eqtr3di KHLWHFTGTRFG-1=RGF-1