trlnle

Description: The atom not under the fiducial co-atom W is not less than the trace of a lattice translation. Part of proof of Lemma C in Crawley p. 112. (Contributed by NM, 26-May-2012)

	Ref	Expression
Hypotheses	trlne.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	trlne.a	$⊢ A = Atoms (K)$
	trlne.h	$⊢ H = LHyp (K)$
	trlne.t	$⊢ T = LTrn (K) (W)$
	trlne.r	$⊢ R = trL (K) (W)$
Assertion	trlnle	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to \neg P \underset{˙}{\leq} R (F)$

Proof

Step	Hyp	Ref	Expression
1		trlne.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		trlne.a	$⊢ A = Atoms (K)$
3		trlne.h	$⊢ H = LHyp (K)$
4		trlne.t	$⊢ T = LTrn (K) (W)$
5		trlne.r	$⊢ R = trL (K) (W)$
6		simpl1l	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) = P) \to K \in HL$
7		hlatl	$⊢ K \in HL \to K \in AtLat$
8	6 7	syl	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) = P) \to K \in AtLat$
9		simpl3l	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) = P) \to P \in A$
10		eqid	$⊢ 0. (K) = 0. (K)$
11	1 10 2	atnle0	$⊢ (K \in AtLat \land P \in A) \to \neg P \underset{˙}{\leq} 0. (K)$
12	8 9 11	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) = P) \to \neg P \underset{˙}{\leq} 0. (K)$
13		simpl1	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) = P) \to (K \in HL \land W \in H)$
14		simpl3	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) = P) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
15		simpl2	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) = P) \to F \in T$
16		simpr	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) = P) \to F (P) = P$
17	1 10 2 3 4 5	trl0	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (F \in T \land F (P) = P)) \to R (F) = 0. (K)$
18	13 14 15 16 17	syl112anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) = P) \to R (F) = 0. (K)$
19	18	breq2d	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) = P) \to (P \underset{˙}{\leq} R (F) \leftrightarrow P \underset{˙}{\leq} 0. (K))$
20	12 19	mtbird	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) = P) \to \neg P \underset{˙}{\leq} R (F)$
21	1 2 3 4 5	trlne	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \neq R (F)$
22	21	adantr	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) \neq P) \to P \neq R (F)$
23		simpl1l	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) \neq P) \to K \in HL$
24	23 7	syl	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) \neq P) \to K \in AtLat$
25		simpl3l	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) \neq P) \to P \in A$
26		simpl1	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) \neq P) \to (K \in HL \land W \in H)$
27		simpl3	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) \neq P) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
28		simpl2	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) \neq P) \to F \in T$
29		simpr	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) \neq P) \to F (P) \neq P$
30	1 2 3 4 5	trlat	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (F \in T \land F (P) \neq P)) \to R (F) \in A$
31	26 27 28 29 30	syl112anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) \neq P) \to R (F) \in A$
32	1 2	atncmp	$⊢ (K \in AtLat \land P \in A \land R (F) \in A) \to (\neg P \underset{˙}{\leq} R (F) \leftrightarrow P \neq R (F))$
33	24 25 31 32	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) \neq P) \to (\neg P \underset{˙}{\leq} R (F) \leftrightarrow P \neq R (F))$
34	22 33	mpbird	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F (P) \neq P) \to \neg P \underset{˙}{\leq} R (F)$
35	20 34	pm2.61dane	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to \neg P \underset{˙}{\leq} R (F)$

Metamath Proof Explorer

Theorem trlnle

Proof