trlnidatb

Description: A lattice translation is not the identity iff its trace is an atom. TODO: Can proofs be reorganized so this goes with trlnidat ? Why do both this and ltrnideq need trlnidat ? (Contributed by NM, 4-Jun-2013)

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

Proof

Step	Hyp	Ref	Expression
1		trlnidatb.b	$⊢ B = {Base}_{K}$
2		trlnidatb.a	$⊢ A = Atoms (K)$
3		trlnidatb.h	$⊢ H = LHyp (K)$
4		trlnidatb.t	$⊢ T = LTrn (K) (W)$
5		trlnidatb.r	$⊢ R = trL (K) (W)$
6	1 2 3 4 5	trlnidat	$⊢ ((K \in HL \land W \in H) \land F \in T \land F \neq {I ↾}_{B}) \to R (F) \in A$
7	6	3expia	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (F \neq {I ↾}_{B} \to R (F) \in A)$
8		eqid	$⊢ \leq_{K} = \leq_{K}$
9	8 2 3	lhpexnle	$⊢ (K \in HL \land W \in H) \to \exists p \in A \neg p \leq_{K} W$
10	9	adantr	$⊢ ((K \in HL \land W \in H) \land F \in T) \to \exists p \in A \neg p \leq_{K} W$
11	1 8 2 3 4	ltrnideq	$⊢ ((K \in HL \land W \in H) \land F \in T \land (p \in A \land \neg p \leq_{K} W)) \to (F = {I ↾}_{B} \leftrightarrow F (p) = p)$
12	11	3expa	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in A \land \neg p \leq_{K} W)) \to (F = {I ↾}_{B} \leftrightarrow F (p) = p)$
13		simp1l	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in A \land \neg p \leq_{K} W) \land F (p) = p) \to (K \in HL \land W \in H)$
14		simp2	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in A \land \neg p \leq_{K} W) \land F (p) = p) \to (p \in A \land \neg p \leq_{K} W)$
15		simp1r	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in A \land \neg p \leq_{K} W) \land F (p) = p) \to F \in T$
16		simp3	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in A \land \neg p \leq_{K} W) \land F (p) = p) \to F (p) = p$
17		eqid	$⊢ 0. (K) = 0. (K)$
18	8 17 2 3 4 5	trl0	$⊢ ((K \in HL \land W \in H) \land (p \in A \land \neg p \leq_{K} W) \land (F \in T \land F (p) = p)) \to R (F) = 0. (K)$
19	13 14 15 16 18	syl112anc	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in A \land \neg p \leq_{K} W) \land F (p) = p) \to R (F) = 0. (K)$
20	19	3expia	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in A \land \neg p \leq_{K} W)) \to (F (p) = p \to R (F) = 0. (K))$
21		simplll	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in A \land \neg p \leq_{K} W)) \to K \in HL$
22		hlatl	$⊢ K \in HL \to K \in AtLat$
23	17 2	atn0	$⊢ (K \in AtLat \land R (F) \in A) \to R (F) \neq 0. (K)$
24	23	ex	$⊢ K \in AtLat \to (R (F) \in A \to R (F) \neq 0. (K))$
25	21 22 24	3syl	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in A \land \neg p \leq_{K} W)) \to (R (F) \in A \to R (F) \neq 0. (K))$
26	25	necon2bd	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in A \land \neg p \leq_{K} W)) \to (R (F) = 0. (K) \to \neg R (F) \in A)$
27	20 26	syld	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in A \land \neg p \leq_{K} W)) \to (F (p) = p \to \neg R (F) \in A)$
28	12 27	sylbid	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in A \land \neg p \leq_{K} W)) \to (F = {I ↾}_{B} \to \neg R (F) \in A)$
29	10 28	rexlimddv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (F = {I ↾}_{B} \to \neg R (F) \in A)$
30	29	necon2ad	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (R (F) \in A \to F \neq {I ↾}_{B})$
31	7 30	impbid	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (F \neq {I ↾}_{B} \leftrightarrow R (F) \in A)$

Metamath Proof Explorer

Theorem trlnidatb

Proof