Metamath Proof Explorer


Theorem cdlemf2

Description: Part of Lemma F in Crawley p. 116. (Contributed by NM, 12-Apr-2013)

Ref Expression
Hypotheses cdlemf1.l ˙ = K
cdlemf1.j ˙ = join K
cdlemf1.a A = Atoms K
cdlemf1.h H = LHyp K
cdlemf2.m ˙ = meet K
Assertion cdlemf2 K HL W H U A U ˙ W p A q A ¬ p ˙ W ¬ q ˙ W U = p ˙ q ˙ W

Proof

Step Hyp Ref Expression
1 cdlemf1.l ˙ = K
2 cdlemf1.j ˙ = join K
3 cdlemf1.a A = Atoms K
4 cdlemf1.h H = LHyp K
5 cdlemf2.m ˙ = meet K
6 1 3 4 lhpexnle K HL W H p A ¬ p ˙ W
7 6 adantr K HL W H U A U ˙ W p A ¬ p ˙ W
8 1 2 3 4 cdlemf1 K HL W H U A U ˙ W p A ¬ p ˙ W q A p q ¬ q ˙ W U ˙ p ˙ q
9 simpr1r K HL W H U A U ˙ W p A ¬ p ˙ W q A p q ¬ q ˙ W U ˙ p ˙ q ¬ p ˙ W
10 simpr32 K HL W H U A U ˙ W p A ¬ p ˙ W q A p q ¬ q ˙ W U ˙ p ˙ q ¬ q ˙ W
11 simpr33 K HL W H U A U ˙ W p A ¬ p ˙ W q A p q ¬ q ˙ W U ˙ p ˙ q U ˙ p ˙ q
12 simplrr K HL W H U A U ˙ W p A ¬ p ˙ W q A p q ¬ q ˙ W U ˙ p ˙ q U ˙ W
13 hllat K HL K Lat
14 13 ad3antrrr K HL W H U A U ˙ W p A ¬ p ˙ W q A p q ¬ q ˙ W U ˙ p ˙ q K Lat
15 simplrl K HL W H U A U ˙ W p A ¬ p ˙ W q A p q ¬ q ˙ W U ˙ p ˙ q U A
16 eqid Base K = Base K
17 16 3 atbase U A U Base K
18 15 17 syl K HL W H U A U ˙ W p A ¬ p ˙ W q A p q ¬ q ˙ W U ˙ p ˙ q U Base K
19 simplll K HL W H U A U ˙ W p A ¬ p ˙ W q A p q ¬ q ˙ W U ˙ p ˙ q K HL
20 simpr1l K HL W H U A U ˙ W p A ¬ p ˙ W q A p q ¬ q ˙ W U ˙ p ˙ q p A
21 simpr2 K HL W H U A U ˙ W p A ¬ p ˙ W q A p q ¬ q ˙ W U ˙ p ˙ q q A
22 16 2 3 hlatjcl K HL p A q A p ˙ q Base K
23 19 20 21 22 syl3anc K HL W H U A U ˙ W p A ¬ p ˙ W q A p q ¬ q ˙ W U ˙ p ˙ q p ˙ q Base K
24 16 4 lhpbase W H W Base K
25 24 ad3antlr K HL W H U A U ˙ W p A ¬ p ˙ W q A p q ¬ q ˙ W U ˙ p ˙ q W Base K
26 16 1 5 latlem12 K Lat U Base K p ˙ q Base K W Base K U ˙ p ˙ q U ˙ W U ˙ p ˙ q ˙ W
27 14 18 23 25 26 syl13anc K HL W H U A U ˙ W p A ¬ p ˙ W q A p q ¬ q ˙ W U ˙ p ˙ q U ˙ p ˙ q U ˙ W U ˙ p ˙ q ˙ W
28 11 12 27 mpbi2and K HL W H U A U ˙ W p A ¬ p ˙ W q A p q ¬ q ˙ W U ˙ p ˙ q U ˙ p ˙ q ˙ W
29 hlatl K HL K AtLat
30 29 ad3antrrr K HL W H U A U ˙ W p A ¬ p ˙ W q A p q ¬ q ˙ W U ˙ p ˙ q K AtLat
31 simpll K HL W H U A U ˙ W p A ¬ p ˙ W q A p q ¬ q ˙ W U ˙ p ˙ q K HL W H
32 simpr31 K HL W H U A U ˙ W p A ¬ p ˙ W q A p q ¬ q ˙ W U ˙ p ˙ q p q
33 1 2 5 3 4 lhpat K HL W H p A ¬ p ˙ W q A p q p ˙ q ˙ W A
34 31 20 9 21 32 33 syl122anc K HL W H U A U ˙ W p A ¬ p ˙ W q A p q ¬ q ˙ W U ˙ p ˙ q p ˙ q ˙ W A
35 1 3 atcmp K AtLat U A p ˙ q ˙ W A U ˙ p ˙ q ˙ W U = p ˙ q ˙ W
36 30 15 34 35 syl3anc K HL W H U A U ˙ W p A ¬ p ˙ W q A p q ¬ q ˙ W U ˙ p ˙ q U ˙ p ˙ q ˙ W U = p ˙ q ˙ W
37 28 36 mpbid K HL W H U A U ˙ W p A ¬ p ˙ W q A p q ¬ q ˙ W U ˙ p ˙ q U = p ˙ q ˙ W
38 9 10 37 jca31 K HL W H U A U ˙ W p A ¬ p ˙ W q A p q ¬ q ˙ W U ˙ p ˙ q ¬ p ˙ W ¬ q ˙ W U = p ˙ q ˙ W
39 38 3exp2 K HL W H U A U ˙ W p A ¬ p ˙ W q A p q ¬ q ˙ W U ˙ p ˙ q ¬ p ˙ W ¬ q ˙ W U = p ˙ q ˙ W
40 39 3impia K HL W H U A U ˙ W p A ¬ p ˙ W q A p q ¬ q ˙ W U ˙ p ˙ q ¬ p ˙ W ¬ q ˙ W U = p ˙ q ˙ W
41 40 reximdvai K HL W H U A U ˙ W p A ¬ p ˙ W q A p q ¬ q ˙ W U ˙ p ˙ q q A ¬ p ˙ W ¬ q ˙ W U = p ˙ q ˙ W
42 8 41 mpd K HL W H U A U ˙ W p A ¬ p ˙ W q A ¬ p ˙ W ¬ q ˙ W U = p ˙ q ˙ W
43 42 3expia K HL W H U A U ˙ W p A ¬ p ˙ W q A ¬ p ˙ W ¬ q ˙ W U = p ˙ q ˙ W
44 43 expd K HL W H U A U ˙ W p A ¬ p ˙ W q A ¬ p ˙ W ¬ q ˙ W U = p ˙ q ˙ W
45 44 reximdvai K HL W H U A U ˙ W p A ¬ p ˙ W p A q A ¬ p ˙ W ¬ q ˙ W U = p ˙ q ˙ W
46 7 45 mpd K HL W H U A U ˙ W p A q A ¬ p ˙ W ¬ q ˙ W U = p ˙ q ˙ W