cdleme1b

Description: Part of proof of Lemma E in Crawley p. 113. Utility lemma showing F is a lattice element. F represents their f(r). (Contributed by NM, 6-Jun-2012)

	Ref	Expression
Hypotheses	cdleme1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme1.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme1.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme1.a	$⊢ A = Atoms (K)$
	cdleme1.h	$⊢ H = LHyp (K)$
	cdleme1.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme1.f	$⊢ F = (R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W))$
	cdleme1.b	$⊢ B = {Base}_{K}$
Assertion	cdleme1b	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land R \in A)) \to F \in B$

Proof

Step	Hyp	Ref	Expression
1		cdleme1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme1.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme1.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme1.a	$⊢ A = Atoms (K)$
5		cdleme1.h	$⊢ H = LHyp (K)$
6		cdleme1.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme1.f	$⊢ F = (R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W))$
8		cdleme1.b	$⊢ B = {Base}_{K}$
9		hllat	$⊢ K \in HL \to K \in Lat$
10	9	ad2antrr	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land R \in A)) \to K \in Lat$
11		simpr3	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land R \in A)) \to R \in A$
12	8 4	atbase	$⊢ R \in A \to R \in B$
13	11 12	syl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land R \in A)) \to R \in B$
14	1 2 3 4 5 6 8	cdleme0aa	$⊢ ((K \in HL \land W \in H) \land P \in A \land Q \in A) \to U \in B$
15	14	3adant3r3	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land R \in A)) \to U \in B$
16	8 2	latjcl	$⊢ (K \in Lat \land R \in B \land U \in B) \to R \underset{˙}{\lor} U \in B$
17	10 13 15 16	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land R \in A)) \to R \underset{˙}{\lor} U \in B$
18		simpr2	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land R \in A)) \to Q \in A$
19	8 4	atbase	$⊢ Q \in A \to Q \in B$
20	18 19	syl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land R \in A)) \to Q \in B$
21		simpr1	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land R \in A)) \to P \in A$
22	8 4	atbase	$⊢ P \in A \to P \in B$
23	21 22	syl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land R \in A)) \to P \in B$
24	8 2	latjcl	$⊢ (K \in Lat \land P \in B \land R \in B) \to P \underset{˙}{\lor} R \in B$
25	10 23 13 24	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land R \in A)) \to P \underset{˙}{\lor} R \in B$
26	8 5	lhpbase	$⊢ W \in H \to W \in B$
27	26	ad2antlr	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land R \in A)) \to W \in B$
28	8 3	latmcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} R \in B \land W \in B) \to (P \underset{˙}{\lor} R) \underset{˙}{\land} W \in B$
29	10 25 27 28	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land R \in A)) \to (P \underset{˙}{\lor} R) \underset{˙}{\land} W \in B$
30	8 2	latjcl	$⊢ (K \in Lat \land Q \in B \land (P \underset{˙}{\lor} R) \underset{˙}{\land} W \in B) \to Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W) \in B$
31	10 20 29 30	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land R \in A)) \to Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W) \in B$
32	8 3	latmcl	$⊢ (K \in Lat \land R \underset{˙}{\lor} U \in B \land Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W) \in B) \to (R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W)) \in B$
33	10 17 31 32	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land R \in A)) \to (R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W)) \in B$
34	7 33	eqeltrid	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land R \in A)) \to F \in B$

Metamath Proof Explorer

Theorem cdleme1b

Proof