lhple

Description: Property of a lattice element under a co-atom. (Contributed by NM, 28-Feb-2014)

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

Proof

Step	Hyp	Ref	Expression
1		lhple.b	$⊢ B = {Base}_{K}$
2		lhple.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		lhple.j	$⊢ \underset{˙}{\lor} = join (K)$
4		lhple.m	$⊢ \underset{˙}{\land} = meet (K)$
5		lhple.a	$⊢ A = Atoms (K)$
6		lhple.h	$⊢ H = LHyp (K)$
7		simp1l	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \to K \in HL$
8	7	hllatd	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \to K \in Lat$
9		simp2l	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \to P \in A$
10	1 5	atbase	$⊢ P \in A \to P \in B$
11	9 10	syl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \to P \in B$
12		simp3l	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \to X \in B$
13	1 3	latjcom	$⊢ (K \in Lat \land P \in B \land X \in B) \to P \underset{˙}{\lor} X = X \underset{˙}{\lor} P$
14	8 11 12 13	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \to P \underset{˙}{\lor} X = X \underset{˙}{\lor} P$
15	14	oveq1d	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \to (P \underset{˙}{\lor} X) \underset{˙}{\land} W = (X \underset{˙}{\lor} P) \underset{˙}{\land} W$
16		simp1	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
17		simp3r	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \to X \underset{˙}{\leq} W$
18	1 2 3 4 6	lhpmod6i1	$⊢ ((K \in HL \land W \in H) \land (X \in B \land P \in B) \land X \underset{˙}{\leq} W) \to X \underset{˙}{\lor} (P \underset{˙}{\land} W) = (X \underset{˙}{\lor} P) \underset{˙}{\land} W$
19	16 12 11 17 18	syl121anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \to X \underset{˙}{\lor} (P \underset{˙}{\land} W) = (X \underset{˙}{\lor} P) \underset{˙}{\land} W$
20		eqid	$⊢ 0. (K) = 0. (K)$
21	2 4 20 5 6	lhpmat	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \underset{˙}{\land} W = 0. (K)$
22	21	3adant3	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \to P \underset{˙}{\land} W = 0. (K)$
23	22	oveq2d	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \to X \underset{˙}{\lor} (P \underset{˙}{\land} W) = X \underset{˙}{\lor} 0. (K)$
24		hlol	$⊢ K \in HL \to K \in OL$
25	7 24	syl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \to K \in OL$
26	1 3 20	olj01	$⊢ (K \in OL \land X \in B) \to X \underset{˙}{\lor} 0. (K) = X$
27	25 12 26	syl2anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \to X \underset{˙}{\lor} 0. (K) = X$
28	23 27	eqtrd	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \to X \underset{˙}{\lor} (P \underset{˙}{\land} W) = X$
29	15 19 28	3eqtr2d	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \to (P \underset{˙}{\lor} X) \underset{˙}{\land} W = X$

Metamath Proof Explorer

Theorem lhple

Proof