cdleme9b

Description: Utility lemma for Lemma E in Crawley p. 113. (Contributed by NM, 9-Oct-2012)

	Ref	Expression
Hypotheses	cdleme9b.b	$⊢ B = {Base}_{K}$
	cdleme9b.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme9b.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme9b.a	$⊢ A = Atoms (K)$
	cdleme9b.h	$⊢ H = LHyp (K)$
	cdleme9b.c	$⊢ C = (P \underset{˙}{\lor} S) \underset{˙}{\land} W$
Assertion	cdleme9b	$⊢ (K \in HL \land (P \in A \land S \in A \land W \in H)) \to C \in B$

Step	Hyp	Ref	Expression
1		cdleme9b.b	$⊢ B = {Base}_{K}$
2		cdleme9b.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme9b.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme9b.a	$⊢ A = Atoms (K)$
5		cdleme9b.h	$⊢ H = LHyp (K)$
6		cdleme9b.c	$⊢ C = (P \underset{˙}{\lor} S) \underset{˙}{\land} W$
7		hllat	$⊢ K \in HL \to K \in Lat$
8	7	adantr	$⊢ (K \in HL \land (P \in A \land S \in A \land W \in H)) \to K \in Lat$
9	1 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land S \in A) \to P \underset{˙}{\lor} S \in B$
10	9	3adant3r3	$⊢ (K \in HL \land (P \in A \land S \in A \land W \in H)) \to P \underset{˙}{\lor} S \in B$
11		simpr3	$⊢ (K \in HL \land (P \in A \land S \in A \land W \in H)) \to W \in H$
12	1 5	lhpbase	$⊢ W \in H \to W \in B$
13	11 12	syl	$⊢ (K \in HL \land (P \in A \land S \in A \land W \in H)) \to W \in B$
14	1 3	latmcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} S \in B \land W \in B) \to (P \underset{˙}{\lor} S) \underset{˙}{\land} W \in B$
15	8 10 13 14	syl3anc	$⊢ (K \in HL \land (P \in A \land S \in A \land W \in H)) \to (P \underset{˙}{\lor} S) \underset{˙}{\land} W \in B$
16	6 15	eqeltrid	$⊢ (K \in HL \land (P \in A \land S \in A \land W \in H)) \to C \in B$

Metamath Proof Explorer