cdlemedb

Description: Part of proof of Lemma E in Crawley p. 113. Utility lemma. D represents s_2. (Contributed by NM, 20-Nov-2012)

	Ref	Expression
Hypotheses	cdlemeda.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemeda.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemeda.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemeda.a	$⊢ A = Atoms (K)$
	cdlemeda.h	$⊢ H = LHyp (K)$
	cdlemeda.d	$⊢ D = (R \underset{˙}{\lor} S) \underset{˙}{\land} W$
	cdlemedb.b	$⊢ B = {Base}_{K}$
Assertion	cdlemedb	$⊢ ((K \in HL \land W \in H) \land (R \in A \land S \in A)) \to D \in B$

Step	Hyp	Ref	Expression
1		cdlemeda.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemeda.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemeda.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdlemeda.a	$⊢ A = Atoms (K)$
5		cdlemeda.h	$⊢ H = LHyp (K)$
6		cdlemeda.d	$⊢ D = (R \underset{˙}{\lor} S) \underset{˙}{\land} W$
7		cdlemedb.b	$⊢ B = {Base}_{K}$
8		hllat	$⊢ K \in HL \to K \in Lat$
9	8	ad2antrr	$⊢ ((K \in HL \land W \in H) \land (R \in A \land S \in A)) \to K \in Lat$
10		simpll	$⊢ ((K \in HL \land W \in H) \land (R \in A \land S \in A)) \to K \in HL$
11		simprl	$⊢ ((K \in HL \land W \in H) \land (R \in A \land S \in A)) \to R \in A$
12		simprr	$⊢ ((K \in HL \land W \in H) \land (R \in A \land S \in A)) \to S \in A$
13	7 2 4	hlatjcl	$⊢ (K \in HL \land R \in A \land S \in A) \to R \underset{˙}{\lor} S \in B$
14	10 11 12 13	syl3anc	$⊢ ((K \in HL \land W \in H) \land (R \in A \land S \in A)) \to R \underset{˙}{\lor} S \in B$
15	7 5	lhpbase	$⊢ W \in H \to W \in B$
16	15	ad2antlr	$⊢ ((K \in HL \land W \in H) \land (R \in A \land S \in A)) \to W \in B$
17	7 3	latmcl	$⊢ (K \in Lat \land R \underset{˙}{\lor} S \in B \land W \in B) \to (R \underset{˙}{\lor} S) \underset{˙}{\land} W \in B$
18	9 14 16 17	syl3anc	$⊢ ((K \in HL \land W \in H) \land (R \in A \land S \in A)) \to (R \underset{˙}{\lor} S) \underset{˙}{\land} W \in B$
19	6 18	eqeltrid	$⊢ ((K \in HL \land W \in H) \land (R \in A \land S \in A)) \to D \in B$

Metamath Proof Explorer