cdleme0cp

Description: Part of proof of Lemma E in Crawley p. 113. TODO: Reformat as in cdlemg3a - swap consequent equality; make antecedent use df-3an . (Contributed by NM, 13-Jun-2012)

	Ref	Expression
Hypotheses	cdleme0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme0.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme0.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme0.a	$⊢ A = Atoms (K)$
	cdleme0.h	$⊢ H = LHyp (K)$
	cdleme0.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
Assertion	cdleme0cp	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A)) \to P \underset{˙}{\lor} U = P \underset{˙}{\lor} Q$

Proof

Step	Hyp	Ref	Expression
1		cdleme0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme0.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme0.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme0.a	$⊢ A = Atoms (K)$
5		cdleme0.h	$⊢ H = LHyp (K)$
6		cdleme0.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7	6	oveq2i	$⊢ P \underset{˙}{\lor} U = P \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)$
8		simpll	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A)) \to K \in HL$
9		simprll	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A)) \to P \in A$
10		hllat	$⊢ K \in HL \to K \in Lat$
11	10	ad2antrr	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A)) \to K \in Lat$
12		eqid	$⊢ {Base}_{K} = {Base}_{K}$
13	12 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
14	9 13	syl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A)) \to P \in {Base}_{K}$
15		simprr	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A)) \to Q \in A$
16	12 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
17	15 16	syl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A)) \to Q \in {Base}_{K}$
18	12 2	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land Q \in {Base}_{K}) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
19	11 14 17 18	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A)) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
20	12 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
21	20	ad2antlr	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A)) \to W \in {Base}_{K}$
22	1 2 4	hlatlej1	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
23	8 9 15 22	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A)) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
24	12 1 2 3 4	atmod3i1	$⊢ (K \in HL \land (P \in A \land P \underset{˙}{\lor} Q \in {Base}_{K} \land W \in {Base}_{K}) \land P \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (P \underset{˙}{\lor} W)$
25	8 9 19 21 23 24	syl131anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A)) \to P \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (P \underset{˙}{\lor} W)$
26		eqid	$⊢ 1. (K) = 1. (K)$
27	1 2 26 4 5	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)$
28	27	adantrr	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A)) \to P \underset{˙}{\lor} W = 1. (K)$
29	28	oveq2d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (P \underset{˙}{\lor} W) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} 1. (K)$
30		hlol	$⊢ K \in HL \to K \in OL$
31	30	ad2antrr	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A)) \to K \in OL$
32	12 3 26	olm11	$⊢ (K \in OL \land P \underset{˙}{\lor} Q \in {Base}_{K}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} 1. (K) = P \underset{˙}{\lor} Q$
33	31 19 32	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} 1. (K) = P \underset{˙}{\lor} Q$
34	25 29 33	3eqtrd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A)) \to P \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = P \underset{˙}{\lor} Q$
35	7 34	eqtrid	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A)) \to P \underset{˙}{\lor} U = P \underset{˙}{\lor} Q$

Metamath Proof Explorer

Theorem cdleme0cp

Proof