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 \in HL \land W \in H) \land F \in T \land G \in T) \to R (F \circ G^{-1}) = R (G \circ F^{-1})$

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		simp1	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to (K \in HL \land W \in H)$
5	1 2	ltrncnv	$⊢ ((K \in HL \land W \in H) \land G \in T) \to G^{-1} \in T$
6	5	3adant2	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to G^{-1} \in T$
7	1 2	ltrnco	$⊢ ((K \in HL \land W \in H) \land F \in T \land G^{-1} \in T) \to F \circ G^{-1} \in T$
8	6 7	syld3an3	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to F \circ G^{-1} \in T$
9	1 2 3	trlcnv	$⊢ ((K \in HL \land W \in H) \land F \circ G^{-1} \in T) \to R ({(F \circ G^{-1})}^{-1}) = R (F \circ G^{-1})$
10	4 8 9	syl2anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to R ({(F \circ G^{-1})}^{-1}) = R (F \circ G^{-1})$
11		cnvco	$⊢ {(F \circ G^{-1})}^{-1} = {G^{-1}}^{-1} \circ F^{-1}$
12		cocnvcnv1	$⊢ {G^{-1}}^{-1} \circ F^{-1} = G \circ F^{-1}$
13	11 12	eqtri	$⊢ {(F \circ G^{-1})}^{-1} = G \circ F^{-1}$
14	13	fveq2i	$⊢ R ({(F \circ G^{-1})}^{-1}) = R (G \circ F^{-1})$
15	10 14	eqtr3di	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to R (F \circ G^{-1}) = R (G \circ F^{-1})$

Metamath Proof Explorer