Metamath Proof Explorer

Theorem ltrnmw

Description: Property of lattice translation value. Remark below Lemma B in Crawley p. 112. TODO: Can this be used in more places? (Contributed by NM, 20-May-2012) (Proof shortened by OpenAI, 25-Mar-2020)

		Ref	Expression
	Hypotheses	ltrnmw.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		ltrnmw.m	$⊢ \underset{˙}{\land} = meet (K)$
		ltrnmw.z	$⊢ \underset{˙}{0} = 0. (K)$
		ltrnmw.a	$⊢ A = Atoms (K)$
		ltrnmw.h	$⊢ H = LHyp (K)$
		ltrnmw.t	$⊢ T = LTrn (K) (W)$
	Assertion	ltrnmw	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F (P) \underset{˙}{\land} W = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		ltrnmw.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		ltrnmw.m	$⊢ \underset{˙}{\land} = meet (K)$
3		ltrnmw.z	$⊢ \underset{˙}{0} = 0. (K)$
4		ltrnmw.a	$⊢ A = Atoms (K)$
5		ltrnmw.h	$⊢ H = LHyp (K)$
6		ltrnmw.t	$⊢ T = LTrn (K) (W)$
7		simp1	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
8	1 4 5 6	ltrnel	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)$
9	1 2 3 4 5	lhpmat	$⊢ ((K \in HL \land W \in H) \land (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)) \to F (P) \underset{˙}{\land} W = \underset{˙}{0}$
10	7 8 9	syl2anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F (P) \underset{˙}{\land} W = \underset{˙}{0}$