trlconid

Description: The composition of two different translations is not the identity translation. (Contributed by NM, 22-Jul-2013)

	Ref	Expression
Hypotheses	trlconid.b	$⊢ B = {Base}_{K}$
	trlconid.h	$⊢ H = LHyp (K)$
	trlconid.t	$⊢ T = LTrn (K) (W)$
	trlconid.r	$⊢ R = trL (K) (W)$
Assertion	trlconid	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \to F \circ G \neq {I ↾}_{B}$

Step	Hyp	Ref	Expression
1		trlconid.b	$⊢ B = {Base}_{K}$
2		trlconid.h	$⊢ H = LHyp (K)$
3		trlconid.t	$⊢ T = LTrn (K) (W)$
4		trlconid.r	$⊢ R = trL (K) (W)$
5		eqid	$⊢ Atoms (K) = Atoms (K)$
6	5 2 3 4	trlcoat	$⊢ ((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) \in Atoms (K)$
7		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)$
8		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$
9		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$
10	2 3	ltrnco	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to F \circ G \in T$
11	7 8 9 10	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \to F \circ G \in T$
12	1 5 2 3 4	trlnidatb	$⊢ ((K \in HL \land W \in H) \land F \circ G \in T) \to (F \circ G \neq {I ↾}_{B} \leftrightarrow R (F \circ G) \in Atoms (K))$
13	7 11 12	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \to (F \circ G \neq {I ↾}_{B} \leftrightarrow R (F \circ G) \in Atoms (K))$
14	6 13	mpbird	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \to F \circ G \neq {I ↾}_{B}$

Metamath Proof Explorer