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 = LHyp ⁡ K
trlcocnv.t ⊢ T = LTrn ⁡ K ⁡ W
trlcocnv.r ⊢ R = trL ⁡ K ⁡ W
Assertion trlcocnv ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T → R ⁡ F ∘ G -1 = R ⁡ G ∘ F -1

Proof

Step Hyp Ref Expression
1 trlcocnv.h ⊢ H = LHyp ⁡ K
2 trlcocnv.t ⊢ T = LTrn ⁡ K ⁡ W
3 trlcocnv.r ⊢ R = trL ⁡ K ⁡ W
4 cnvco ⊢ F ∘ G -1 -1 = G -1 -1 ∘ F -1
5 cocnvcnv1 ⊢ G -1 -1 ∘ F -1 = G ∘ F -1
6 4 5 eqtri ⊢ F ∘ G -1 -1 = G ∘ F -1
7 6 fveq2i ⊢ R ⁡ F ∘ G -1 -1 = R ⁡ G ∘ F -1
8 simp1 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T → K ∈ HL ∧ W ∈ H
9 1 2 ltrncnv ⊢ K ∈ HL ∧ W ∈ H ∧ G ∈ T → G -1 ∈ T
10 9 3adant2 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T → G -1 ∈ T
11 1 2 ltrnco ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G -1 ∈ T → F ∘ G -1 ∈ T
12 10 11 syld3an3 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T → F ∘ G -1 ∈ T
13 1 2 3 trlcnv ⊢ K ∈ HL ∧ W ∈ H ∧ F ∘ G -1 ∈ T → R ⁡ F ∘ G -1 -1 = R ⁡ F ∘ G -1
14 8 12 13 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T → R ⁡ F ∘ G -1 -1 = R ⁡ F ∘ G -1
15 7 14 syl5reqr ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T → R ⁡ F ∘ G -1 = R ⁡ G ∘ F -1