Metamath Proof Explorer

Theorem cdlemftr2

Description: Special case of cdlemf showing existence of non-identity translation with trace different from any 2 given lattice elements. (Contributed by NM, 25-Jul-2013)

		Ref	Expression
	Hypotheses	cdlemftr.b	$⊢ B = {Base}_{K}$
		cdlemftr.h	$⊢ H = LHyp (K)$
		cdlemftr.t	$⊢ T = LTrn (K) (W)$
		cdlemftr.r	$⊢ R = trL (K) (W)$
	Assertion	cdlemftr2	$⊢ (K \in HL \land W \in H) \to \exists f \in T (f \neq {I ↾}_{B} \land R (f) \neq X \land R (f) \neq Y)$

Proof

Step	Hyp	Ref	Expression
1		cdlemftr.b	$⊢ B = {Base}_{K}$
2		cdlemftr.h	$⊢ H = LHyp (K)$
3		cdlemftr.t	$⊢ T = LTrn (K) (W)$
4		cdlemftr.r	$⊢ R = trL (K) (W)$
5	1 2 3 4	cdlemftr3	$⊢ (K \in HL \land W \in H) \to \exists f \in T (f \neq {I ↾}_{B} \land (R (f) \neq X \land R (f) \neq Y \land R (f) \neq Y))$
6		simpl	$⊢ (f \neq {I ↾}_{B} \land (R (f) \neq X \land R (f) \neq Y \land R (f) \neq Y)) \to f \neq {I ↾}_{B}$
7		simpr1	$⊢ (f \neq {I ↾}_{B} \land (R (f) \neq X \land R (f) \neq Y \land R (f) \neq Y)) \to R (f) \neq X$
8		simpr2	$⊢ (f \neq {I ↾}_{B} \land (R (f) \neq X \land R (f) \neq Y \land R (f) \neq Y)) \to R (f) \neq Y$
9	6 7 8	3jca	$⊢ (f \neq {I ↾}_{B} \land (R (f) \neq X \land R (f) \neq Y \land R (f) \neq Y)) \to (f \neq {I ↾}_{B} \land R (f) \neq X \land R (f) \neq Y)$
10	9	reximi	$⊢ \exists f \in T (f \neq {I ↾}_{B} \land (R (f) \neq X \land R (f) \neq Y \land R (f) \neq Y)) \to \exists f \in T (f \neq {I ↾}_{B} \land R (f) \neq X \land R (f) \neq Y)$
11	5 10	syl	$⊢ (K \in HL \land W \in H) \to \exists f \in T (f \neq {I ↾}_{B} \land R (f) \neq X \land R (f) \neq Y)$