trlator0

Description: The trace of a lattice translation is an atom or zero. (Contributed by NM, 5-May-2013)

	Ref	Expression
Hypotheses	trl0a.z	$⊢ \underset{˙}{0} = 0. (K)$
	trl0a.a	$⊢ A = Atoms (K)$
	trl0a.h	$⊢ H = LHyp (K)$
	trl0a.t	$⊢ T = LTrn (K) (W)$
	trl0a.r	$⊢ R = trL (K) (W)$
Assertion	trlator0	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (R (F) \in A \lor R (F) = \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		trl0a.z	$⊢ \underset{˙}{0} = 0. (K)$
2		trl0a.a	$⊢ A = Atoms (K)$
3		trl0a.h	$⊢ H = LHyp (K)$
4		trl0a.t	$⊢ T = LTrn (K) (W)$
5		trl0a.r	$⊢ R = trL (K) (W)$
6		df-ne	$⊢ R (F) \neq \underset{˙}{0} \leftrightarrow \neg R (F) = \underset{˙}{0}$
7		eqid	$⊢ \leq_{K} = \leq_{K}$
8	7 2 3	lhpexnle	$⊢ (K \in HL \land W \in H) \to \exists p \in A \neg p \leq_{K} W$
9	8	ad2antrr	$⊢ (((K \in HL \land W \in H) \land F \in T) \land R (F) \neq \underset{˙}{0}) \to \exists p \in A \neg p \leq_{K} W$
10		simplll	$⊢ ((((K \in HL \land W \in H) \land F \in T) \land R (F) \neq \underset{˙}{0}) \land (p \in A \land \neg p \leq_{K} W)) \to (K \in HL \land W \in H)$
11		simpr	$⊢ ((((K \in HL \land W \in H) \land F \in T) \land R (F) \neq \underset{˙}{0}) \land (p \in A \land \neg p \leq_{K} W)) \to (p \in A \land \neg p \leq_{K} W)$
12		simpllr	$⊢ ((((K \in HL \land W \in H) \land F \in T) \land R (F) \neq \underset{˙}{0}) \land (p \in A \land \neg p \leq_{K} W)) \to F \in T$
13		simplr	$⊢ ((((K \in HL \land W \in H) \land F \in T) \land R (F) \neq \underset{˙}{0}) \land (p \in A \land \neg p \leq_{K} W)) \to R (F) \neq \underset{˙}{0}$
14	10	adantr	$⊢ (((((K \in HL \land W \in H) \land F \in T) \land R (F) \neq \underset{˙}{0}) \land (p \in A \land \neg p \leq_{K} W)) \land F (p) = p) \to (K \in HL \land W \in H)$
15		simplr	$⊢ (((((K \in HL \land W \in H) \land F \in T) \land R (F) \neq \underset{˙}{0}) \land (p \in A \land \neg p \leq_{K} W)) \land F (p) = p) \to (p \in A \land \neg p \leq_{K} W)$
16	12	adantr	$⊢ (((((K \in HL \land W \in H) \land F \in T) \land R (F) \neq \underset{˙}{0}) \land (p \in A \land \neg p \leq_{K} W)) \land F (p) = p) \to F \in T$
17		simpr	$⊢ (((((K \in HL \land W \in H) \land F \in T) \land R (F) \neq \underset{˙}{0}) \land (p \in A \land \neg p \leq_{K} W)) \land F (p) = p) \to F (p) = p$
18	7 1 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) = \underset{˙}{0}$
19	14 15 16 17 18	syl112anc	$⊢ (((((K \in HL \land W \in H) \land F \in T) \land R (F) \neq \underset{˙}{0}) \land (p \in A \land \neg p \leq_{K} W)) \land F (p) = p) \to R (F) = \underset{˙}{0}$
20	19	ex	$⊢ ((((K \in HL \land W \in H) \land F \in T) \land R (F) \neq \underset{˙}{0}) \land (p \in A \land \neg p \leq_{K} W)) \to (F (p) = p \to R (F) = \underset{˙}{0})$
21	20	necon3d	$⊢ ((((K \in HL \land W \in H) \land F \in T) \land R (F) \neq \underset{˙}{0}) \land (p \in A \land \neg p \leq_{K} W)) \to (R (F) \neq \underset{˙}{0} \to F (p) \neq p)$
22	13 21	mpd	$⊢ ((((K \in HL \land W \in H) \land F \in T) \land R (F) \neq \underset{˙}{0}) \land (p \in A \land \neg p \leq_{K} W)) \to F (p) \neq p$
23	7 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$
24	10 11 12 22 23	syl112anc	$⊢ ((((K \in HL \land W \in H) \land F \in T) \land R (F) \neq \underset{˙}{0}) \land (p \in A \land \neg p \leq_{K} W)) \to R (F) \in A$
25	9 24	rexlimddv	$⊢ (((K \in HL \land W \in H) \land F \in T) \land R (F) \neq \underset{˙}{0}) \to R (F) \in A$
26	25	ex	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (R (F) \neq \underset{˙}{0} \to R (F) \in A)$
27	6 26	syl5bir	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (\neg R (F) = \underset{˙}{0} \to R (F) \in A)$
28	27	orrd	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (R (F) = \underset{˙}{0} \lor R (F) \in A)$
29	28	orcomd	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (R (F) \in A \lor R (F) = \underset{˙}{0})$

Metamath Proof Explorer

Theorem trlator0

Proof