lhpmcvr3

Description: Specialization of lhpmcvr2 . TODO: Use this to simplify many uses of ( P .\/ ( X ./\ W ) ) = X to become P .<_ X . (Contributed by NM, 6-Apr-2014)

	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	lhpmcvr3	$⊢ ((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)) \to (P \underset{˙}{\leq} X \leftrightarrow P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)$

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		simpl1l	$⊢ (((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 P \underset{˙}{\leq} X) \to K \in HL$
8		simpl3l	$⊢ (((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 P \underset{˙}{\leq} X) \to P \in A$
9		simpl2l	$⊢ (((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 P \underset{˙}{\leq} X) \to X \in B$
10		simpl1r	$⊢ (((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 P \underset{˙}{\leq} X) \to W \in H$
11	1 6	lhpbase	$⊢ W \in H \to W \in B$
12	10 11	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 P \underset{˙}{\leq} X) \to W \in B$
13		simpr	$⊢ (((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 P \underset{˙}{\leq} X) \to P \underset{˙}{\leq} X$
14	1 2 3 4 5	atmod3i1	$⊢ (K \in HL \land (P \in A \land X \in B \land W \in B) \land P \underset{˙}{\leq} X) \to P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \underset{˙}{\land} (P \underset{˙}{\lor} W)$
15	7 8 9 12 13 14	syl131anc	$⊢ (((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 P \underset{˙}{\leq} X) \to P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \underset{˙}{\land} (P \underset{˙}{\lor} W)$
16		simpl1	$⊢ (((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 P \underset{˙}{\leq} X) \to (K \in HL \land W \in H)$
17		simpl3	$⊢ (((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 P \underset{˙}{\leq} X) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
18		eqid	$⊢ 1. (K) = 1. (K)$
19	2 3 18 5 6	lhpjat2	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \underset{˙}{\lor} W = 1. (K)$
20	16 17 19	syl2anc	$⊢ (((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 P \underset{˙}{\leq} X) \to P \underset{˙}{\lor} W = 1. (K)$
21	20	oveq2d	$⊢ (((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 P \underset{˙}{\leq} X) \to X \underset{˙}{\land} (P \underset{˙}{\lor} W) = X \underset{˙}{\land} 1. (K)$
22		hlol	$⊢ K \in HL \to K \in OL$
23	7 22	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 P \underset{˙}{\leq} X) \to K \in OL$
24	1 4 18	olm11	$⊢ (K \in OL \land X \in B) \to X \underset{˙}{\land} 1. (K) = X$
25	23 9 24	syl2anc	$⊢ (((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 P \underset{˙}{\leq} X) \to X \underset{˙}{\land} 1. (K) = X$
26	15 21 25	3eqtrd	$⊢ (((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 P \underset{˙}{\leq} X) \to P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X$
27		simpl1l	$⊢ (((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 P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to K \in HL$
28	27	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 P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to K \in Lat$
29		simpl3l	$⊢ (((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 P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to P \in A$
30	1 5	atbase	$⊢ P \in A \to P \in B$
31	29 30	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 P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to P \in B$
32		simpl2l	$⊢ (((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 P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to X \in B$
33		simpl1r	$⊢ (((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 P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to W \in H$
34	33 11	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 P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to W \in B$
35	1 4	latmcl	$⊢ (K \in Lat \land X \in B \land W \in B) \to X \underset{˙}{\land} W \in B$
36	28 32 34 35	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 P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to X \underset{˙}{\land} W \in B$
37	1 2 3	latlej1	$⊢ (K \in Lat \land P \in B \land X \underset{˙}{\land} W \in B) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} (X \underset{˙}{\land} W))$
38	28 31 36 37	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 P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} (X \underset{˙}{\land} W))$
39		simpr	$⊢ (((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 P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X$
40	38 39	breqtrd	$⊢ (((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 P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to P \underset{˙}{\leq} X$
41	26 40	impbida	$⊢ ((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)) \to (P \underset{˙}{\leq} X \leftrightarrow P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)$

Metamath Proof Explorer

Theorem lhpmcvr3

Proof