lhpmcvr4N

Description: Specialization of lhpmcvr2 . (Contributed by NM, 6-Apr-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lhpmcvr2.b	$⊢ B = {Base}_{K}$
	lhpmcvr2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lhpmcvr2.j	$⊢ \underset{˙}{\lor} = join (K)$
	lhpmcvr2.m	$⊢ \underset{˙}{\land} = meet (K)$
	lhpmcvr2.a	$⊢ A = Atoms (K)$
	lhpmcvr2.h	$⊢ H = LHyp (K)$
Assertion	lhpmcvr4N	$⊢ ((K \in HL \land W \in H) \land ((X \in B \land \neg X \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land P \underset{˙}{\leq} X)) \to \neg P \underset{˙}{\leq} Y$

Proof

Step	Hyp	Ref	Expression
1		lhpmcvr2.b	$⊢ B = {Base}_{K}$
2		lhpmcvr2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		lhpmcvr2.j	$⊢ \underset{˙}{\lor} = join (K)$
4		lhpmcvr2.m	$⊢ \underset{˙}{\land} = meet (K)$
5		lhpmcvr2.a	$⊢ A = Atoms (K)$
6		lhpmcvr2.h	$⊢ H = LHyp (K)$
7		simp2rr	$⊢ ((K \in HL \land W \in H) \land ((X \in B \land \neg X \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land P \underset{˙}{\leq} X)) \to \neg P \underset{˙}{\leq} W$
8		simp33	$⊢ ((K \in HL \land W \in H) \land ((X \in B \land \neg X \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land P \underset{˙}{\leq} X)) \to P \underset{˙}{\leq} X$
9		simp1l	$⊢ ((K \in HL \land W \in H) \land ((X \in B \land \neg X \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land P \underset{˙}{\leq} X)) \to K \in HL$
10	9	hllatd	$⊢ ((K \in HL \land W \in H) \land ((X \in B \land \neg X \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land P \underset{˙}{\leq} X)) \to K \in Lat$
11		simp2rl	$⊢ ((K \in HL \land W \in H) \land ((X \in B \land \neg X \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land P \underset{˙}{\leq} X)) \to P \in A$
12	1 5	atbase	$⊢ P \in A \to P \in B$
13	11 12	syl	$⊢ ((K \in HL \land W \in H) \land ((X \in B \land \neg X \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land P \underset{˙}{\leq} X)) \to P \in B$
14		simp2ll	$⊢ ((K \in HL \land W \in H) \land ((X \in B \land \neg X \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land P \underset{˙}{\leq} X)) \to X \in B$
15		simp31	$⊢ ((K \in HL \land W \in H) \land ((X \in B \land \neg X \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land P \underset{˙}{\leq} X)) \to Y \in B$
16	1 2 4	latlem12	$⊢ (K \in Lat \land (P \in B \land X \in B \land Y \in B)) \to ((P \underset{˙}{\leq} X \land P \underset{˙}{\leq} Y) \leftrightarrow P \underset{˙}{\leq} (X \underset{˙}{\land} Y))$
17	10 13 14 15 16	syl13anc	$⊢ ((K \in HL \land W \in H) \land ((X \in B \land \neg X \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land P \underset{˙}{\leq} X)) \to ((P \underset{˙}{\leq} X \land P \underset{˙}{\leq} Y) \leftrightarrow P \underset{˙}{\leq} (X \underset{˙}{\land} Y))$
18	17	biimpd	$⊢ ((K \in HL \land W \in H) \land ((X \in B \land \neg X \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land P \underset{˙}{\leq} X)) \to ((P \underset{˙}{\leq} X \land P \underset{˙}{\leq} Y) \to P \underset{˙}{\leq} (X \underset{˙}{\land} Y))$
19	8 18	mpand	$⊢ ((K \in HL \land W \in H) \land ((X \in B \land \neg X \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land P \underset{˙}{\leq} X)) \to (P \underset{˙}{\leq} Y \to P \underset{˙}{\leq} (X \underset{˙}{\land} Y))$
20		simp32	$⊢ ((K \in HL \land W \in H) \land ((X \in B \land \neg X \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land P \underset{˙}{\leq} X)) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} W$
21	1 4	latmcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y \in B$
22	10 14 15 21	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((X \in B \land \neg X \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land P \underset{˙}{\leq} X)) \to X \underset{˙}{\land} Y \in B$
23		simp1r	$⊢ ((K \in HL \land W \in H) \land ((X \in B \land \neg X \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land P \underset{˙}{\leq} X)) \to W \in H$
24	1 6	lhpbase	$⊢ W \in H \to W \in B$
25	23 24	syl	$⊢ ((K \in HL \land W \in H) \land ((X \in B \land \neg X \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land P \underset{˙}{\leq} X)) \to W \in B$
26	1 2	lattr	$⊢ (K \in Lat \land (P \in B \land X \underset{˙}{\land} Y \in B \land W \in B)) \to ((P \underset{˙}{\leq} (X \underset{˙}{\land} Y) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to P \underset{˙}{\leq} W)$
27	10 13 22 25 26	syl13anc	$⊢ ((K \in HL \land W \in H) \land ((X \in B \land \neg X \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land P \underset{˙}{\leq} X)) \to ((P \underset{˙}{\leq} (X \underset{˙}{\land} Y) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to P \underset{˙}{\leq} W)$
28	20 27	mpan2d	$⊢ ((K \in HL \land W \in H) \land ((X \in B \land \neg X \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land P \underset{˙}{\leq} X)) \to (P \underset{˙}{\leq} (X \underset{˙}{\land} Y) \to P \underset{˙}{\leq} W)$
29	19 28	syld	$⊢ ((K \in HL \land W \in H) \land ((X \in B \land \neg X \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land P \underset{˙}{\leq} X)) \to (P \underset{˙}{\leq} Y \to P \underset{˙}{\leq} W)$
30	7 29	mtod	$⊢ ((K \in HL \land W \in H) \land ((X \in B \land \neg X \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W \land P \underset{˙}{\leq} X)) \to \neg P \underset{˙}{\leq} Y$

Metamath Proof Explorer

Theorem lhpmcvr4N

Proof