cdlemftr3

Description: Special case of cdlemf showing existence of non-identity translation with trace different from any 3 given lattice elements. (Contributed by NM, 24-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	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 Z))$

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		eqid	$⊢ \leq_{K} = \leq_{K}$
6		eqid	$⊢ Atoms (K) = Atoms (K)$
7	5 6 2	lhpexle3	$⊢ (K \in HL \land W \in H) \to \exists u \in Atoms (K) (u \leq_{K} W \land (u \neq X \land u \neq Y \land u \neq Z))$
8		df-rex	$⊢ \exists u \in Atoms (K) (u \leq_{K} W \land (u \neq X \land u \neq Y \land u \neq Z)) \leftrightarrow \exists u (u \in Atoms (K) \land (u \leq_{K} W \land (u \neq X \land u \neq Y \land u \neq Z)))$
9	7 8	sylib	$⊢ (K \in HL \land W \in H) \to \exists u (u \in Atoms (K) \land (u \leq_{K} W \land (u \neq X \land u \neq Y \land u \neq Z)))$
10	1 5 6 2 3 4	cdlemfnid	$⊢ ((K \in HL \land W \in H) \land (u \in Atoms (K) \land u \leq_{K} W)) \to \exists f \in T (R (f) = u \land f \neq {I ↾}_{B})$
11	10	adantrrr	$⊢ ((K \in HL \land W \in H) \land (u \in Atoms (K) \land (u \leq_{K} W \land (u \neq X \land u \neq Y \land u \neq Z)))) \to \exists f \in T (R (f) = u \land f \neq {I ↾}_{B})$
12		eqcom	$⊢ R (f) = u \leftrightarrow u = R (f)$
13	12	anbi1i	$⊢ (R (f) = u \land f \neq {I ↾}_{B}) \leftrightarrow (u = R (f) \land f \neq {I ↾}_{B})$
14	13	rexbii	$⊢ \exists f \in T (R (f) = u \land f \neq {I ↾}_{B}) \leftrightarrow \exists f \in T (u = R (f) \land f \neq {I ↾}_{B})$
15	11 14	sylib	$⊢ ((K \in HL \land W \in H) \land (u \in Atoms (K) \land (u \leq_{K} W \land (u \neq X \land u \neq Y \land u \neq Z)))) \to \exists f \in T (u = R (f) \land f \neq {I ↾}_{B})$
16		simprrr	$⊢ ((K \in HL \land W \in H) \land (u \in Atoms (K) \land (u \leq_{K} W \land (u \neq X \land u \neq Y \land u \neq Z)))) \to (u \neq X \land u \neq Y \land u \neq Z)$
17	15 16	jca	$⊢ ((K \in HL \land W \in H) \land (u \in Atoms (K) \land (u \leq_{K} W \land (u \neq X \land u \neq Y \land u \neq Z)))) \to (\exists f \in T (u = R (f) \land f \neq {I ↾}_{B}) \land (u \neq X \land u \neq Y \land u \neq Z))$
18	17	ex	$⊢ (K \in HL \land W \in H) \to ((u \in Atoms (K) \land (u \leq_{K} W \land (u \neq X \land u \neq Y \land u \neq Z))) \to (\exists f \in T (u = R (f) \land f \neq {I ↾}_{B}) \land (u \neq X \land u \neq Y \land u \neq Z)))$
19	18	eximdv	$⊢ (K \in HL \land W \in H) \to (\exists u (u \in Atoms (K) \land (u \leq_{K} W \land (u \neq X \land u \neq Y \land u \neq Z))) \to \exists u (\exists f \in T (u = R (f) \land f \neq {I ↾}_{B}) \land (u \neq X \land u \neq Y \land u \neq Z)))$
20	9 19	mpd	$⊢ (K \in HL \land W \in H) \to \exists u (\exists f \in T (u = R (f) \land f \neq {I ↾}_{B}) \land (u \neq X \land u \neq Y \land u \neq Z))$
21		rexcom4	$⊢ \exists f \in T \exists u ((u = R (f) \land f \neq {I ↾}_{B}) \land (u \neq X \land u \neq Y \land u \neq Z)) \leftrightarrow \exists u \exists f \in T ((u = R (f) \land f \neq {I ↾}_{B}) \land (u \neq X \land u \neq Y \land u \neq Z))$
22		anass	$⊢ ((u = R (f) \land f \neq {I ↾}_{B}) \land (u \neq X \land u \neq Y \land u \neq Z)) \leftrightarrow (u = R (f) \land (f \neq {I ↾}_{B} \land (u \neq X \land u \neq Y \land u \neq Z)))$
23	22	exbii	$⊢ \exists u ((u = R (f) \land f \neq {I ↾}_{B}) \land (u \neq X \land u \neq Y \land u \neq Z)) \leftrightarrow \exists u (u = R (f) \land (f \neq {I ↾}_{B} \land (u \neq X \land u \neq Y \land u \neq Z)))$
24		fvex	$⊢ R (f) \in V$
25		neeq1	$⊢ u = R (f) \to (u \neq X \leftrightarrow R (f) \neq X)$
26		neeq1	$⊢ u = R (f) \to (u \neq Y \leftrightarrow R (f) \neq Y)$
27		neeq1	$⊢ u = R (f) \to (u \neq Z \leftrightarrow R (f) \neq Z)$
28	25 26 27	3anbi123d	$⊢ u = R (f) \to ((u \neq X \land u \neq Y \land u \neq Z) \leftrightarrow (R (f) \neq X \land R (f) \neq Y \land R (f) \neq Z))$
29	28	anbi2d	$⊢ u = R (f) \to ((f \neq {I ↾}_{B} \land (u \neq X \land u \neq Y \land u \neq Z)) \leftrightarrow (f \neq {I ↾}_{B} \land (R (f) \neq X \land R (f) \neq Y \land R (f) \neq Z)))$
30	24 29	ceqsexv	$⊢ \exists u (u = R (f) \land (f \neq {I ↾}_{B} \land (u \neq X \land u \neq Y \land u \neq Z))) \leftrightarrow (f \neq {I ↾}_{B} \land (R (f) \neq X \land R (f) \neq Y \land R (f) \neq Z))$
31	23 30	bitri	$⊢ \exists u ((u = R (f) \land f \neq {I ↾}_{B}) \land (u \neq X \land u \neq Y \land u \neq Z)) \leftrightarrow (f \neq {I ↾}_{B} \land (R (f) \neq X \land R (f) \neq Y \land R (f) \neq Z))$
32	31	rexbii	$⊢ \exists f \in T \exists u ((u = R (f) \land f \neq {I ↾}_{B}) \land (u \neq X \land u \neq Y \land u \neq Z)) \leftrightarrow \exists f \in T (f \neq {I ↾}_{B} \land (R (f) \neq X \land R (f) \neq Y \land R (f) \neq Z))$
33		r19.41v	$⊢ \exists f \in T ((u = R (f) \land f \neq {I ↾}_{B}) \land (u \neq X \land u \neq Y \land u \neq Z)) \leftrightarrow (\exists f \in T (u = R (f) \land f \neq {I ↾}_{B}) \land (u \neq X \land u \neq Y \land u \neq Z))$
34	33	exbii	$⊢ \exists u \exists f \in T ((u = R (f) \land f \neq {I ↾}_{B}) \land (u \neq X \land u \neq Y \land u \neq Z)) \leftrightarrow \exists u (\exists f \in T (u = R (f) \land f \neq {I ↾}_{B}) \land (u \neq X \land u \neq Y \land u \neq Z))$
35	21 32 34	3bitr3ri	$⊢ \exists u (\exists f \in T (u = R (f) \land f \neq {I ↾}_{B}) \land (u \neq X \land u \neq Y \land u \neq Z)) \leftrightarrow \exists f \in T (f \neq {I ↾}_{B} \land (R (f) \neq X \land R (f) \neq Y \land R (f) \neq Z))$
36	20 35	sylib	$⊢ (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 Z))$

Metamath Proof Explorer

Theorem cdlemftr3

Proof