Metamath Proof Explorer

Theorem trlnidat

Description: The trace of a lattice translation other than the identity is an atom. Remark above Lemma C in Crawley p. 112. (Contributed by NM, 23-May-2012)

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

Proof

Step	Hyp	Ref	Expression
1		trlnidat.b	$⊢ B = {Base}_{K}$
2		trlnidat.a	$⊢ A = Atoms (K)$
3		trlnidat.h	$⊢ H = LHyp (K)$
4		trlnidat.t	$⊢ T = LTrn (K) (W)$
5		trlnidat.r	$⊢ R = trL (K) (W)$
6		eqid	$⊢ \leq_{K} = \leq_{K}$
7	1 6 2 3 4	ltrnnid	$⊢ ((K \in HL \land W \in H) \land F \in T \land F \neq {I ↾}_{B}) \to \exists p \in A (\neg p \leq_{K} W \land F (p) \neq p)$
8		simp11	$⊢ (((K \in HL \land W \in H) \land F \in T \land F \neq {I ↾}_{B}) \land p \in A \land (\neg p \leq_{K} W \land F (p) \neq p)) \to (K \in HL \land W \in H)$
9		simp2	$⊢ (((K \in HL \land W \in H) \land F \in T \land F \neq {I ↾}_{B}) \land p \in A \land (\neg p \leq_{K} W \land F (p) \neq p)) \to p \in A$
10		simp3l	$⊢ (((K \in HL \land W \in H) \land F \in T \land F \neq {I ↾}_{B}) \land p \in A \land (\neg p \leq_{K} W \land F (p) \neq p)) \to \neg p \leq_{K} W$
11		simp12	$⊢ (((K \in HL \land W \in H) \land F \in T \land F \neq {I ↾}_{B}) \land p \in A \land (\neg p \leq_{K} W \land F (p) \neq p)) \to F \in T$
12		simp3r	$⊢ (((K \in HL \land W \in H) \land F \in T \land F \neq {I ↾}_{B}) \land p \in A \land (\neg p \leq_{K} W \land F (p) \neq p)) \to F (p) \neq p$
13	6 2 3 4 5	trlat	$⊢ ((K \in HL \land W \in H) \land (p \in A \land \neg p \leq_{K} W) \land (F \in T \land F (p) \neq p)) \to R (F) \in A$
14	8 9 10 11 12 13	syl122anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land F \neq {I ↾}_{B}) \land p \in A \land (\neg p \leq_{K} W \land F (p) \neq p)) \to R (F) \in A$
15	14	rexlimdv3a	$⊢ ((K \in HL \land W \in H) \land F \in T \land F \neq {I ↾}_{B}) \to (\exists p \in A (\neg p \leq_{K} W \land F (p) \neq p) \to R (F) \in A)$
16	7 15	mpd	$⊢ ((K \in HL \land W \in H) \land F \in T \land F \neq {I ↾}_{B}) \to R (F) \in A$