trlcocnvat

Description: Commonly used special case of trlcoat . (Contributed by NM, 1-Jul-2013)

	Ref	Expression
Hypotheses	trlcoat.a	$⊢ A = Atoms (K)$
	trlcoat.h	$⊢ H = LHyp (K)$
	trlcoat.t	$⊢ T = LTrn (K) (W)$
	trlcoat.r	$⊢ R = trL (K) (W)$
Assertion	trlcocnvat	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \to R (F \circ G^{-1}) \in A$

Step	Hyp	Ref	Expression
1		trlcoat.a	$⊢ A = Atoms (K)$
2		trlcoat.h	$⊢ H = LHyp (K)$
3		trlcoat.t	$⊢ T = LTrn (K) (W)$
4		trlcoat.r	$⊢ R = trL (K) (W)$
5		simp1	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \to (K \in HL \land W \in H)$
6		simp2l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \to F \in T$
7		simp2r	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \to G \in T$
8	2 3	ltrncnv	$⊢ ((K \in HL \land W \in H) \land G \in T) \to G^{-1} \in T$
9	5 7 8	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \to G^{-1} \in T$
10		simp3	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \to R (F) \neq R (G)$
11	2 3 4	trlcnv	$⊢ ((K \in HL \land W \in H) \land G \in T) \to R (G^{-1}) = R (G)$
12	5 7 11	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \to R (G^{-1}) = R (G)$
13	10 12	neeqtrrd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \to R (F) \neq R (G^{-1})$
14	1 2 3 4	trlcoat	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G^{-1} \in T) \land R (F) \neq R (G^{-1})) \to R (F \circ G^{-1}) \in A$
15	5 6 9 13 14	syl121anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \to R (F \circ G^{-1}) \in A$

Metamath Proof Explorer