Metamath Proof Explorer


Theorem cdleme32b

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 19-Feb-2013)

Ref Expression
Hypotheses cdleme32.b B = Base K
cdleme32.l ˙ = K
cdleme32.j ˙ = join K
cdleme32.m ˙ = meet K
cdleme32.a A = Atoms K
cdleme32.h H = LHyp K
cdleme32.u U = P ˙ Q ˙ W
cdleme32.c C = s ˙ U ˙ Q ˙ P ˙ s ˙ W
cdleme32.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdleme32.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
cdleme32.i I = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E
cdleme32.n N = if s ˙ P ˙ Q I C
cdleme32.o O = ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = N ˙ x ˙ W
cdleme32.f F = x B if P Q ¬ x ˙ W O x
Assertion cdleme32b K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B P Q ¬ X ˙ W s A ¬ s ˙ W s ˙ X ˙ W = X X ˙ Y F Y = N ˙ Y ˙ W

Proof

Step Hyp Ref Expression
1 cdleme32.b B = Base K
2 cdleme32.l ˙ = K
3 cdleme32.j ˙ = join K
4 cdleme32.m ˙ = meet K
5 cdleme32.a A = Atoms K
6 cdleme32.h H = LHyp K
7 cdleme32.u U = P ˙ Q ˙ W
8 cdleme32.c C = s ˙ U ˙ Q ˙ P ˙ s ˙ W
9 cdleme32.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
10 cdleme32.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
11 cdleme32.i I = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E
12 cdleme32.n N = if s ˙ P ˙ Q I C
13 cdleme32.o O = ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = N ˙ x ˙ W
14 cdleme32.f F = x B if P Q ¬ x ˙ W O x
15 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B P Q ¬ X ˙ W s A ¬ s ˙ W s ˙ X ˙ W = X X ˙ Y K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
16 simp22 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B P Q ¬ X ˙ W s A ¬ s ˙ W s ˙ X ˙ W = X X ˙ Y Y B
17 simp23l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B P Q ¬ X ˙ W s A ¬ s ˙ W s ˙ X ˙ W = X X ˙ Y P Q
18 simp23r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B P Q ¬ X ˙ W s A ¬ s ˙ W s ˙ X ˙ W = X X ˙ Y ¬ X ˙ W
19 simp33 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B P Q ¬ X ˙ W s A ¬ s ˙ W s ˙ X ˙ W = X X ˙ Y X ˙ Y
20 simp11l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B P Q ¬ X ˙ W s A ¬ s ˙ W s ˙ X ˙ W = X X ˙ Y K HL
21 20 hllatd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B P Q ¬ X ˙ W s A ¬ s ˙ W s ˙ X ˙ W = X X ˙ Y K Lat
22 simp21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B P Q ¬ X ˙ W s A ¬ s ˙ W s ˙ X ˙ W = X X ˙ Y X B
23 simp11r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B P Q ¬ X ˙ W s A ¬ s ˙ W s ˙ X ˙ W = X X ˙ Y W H
24 1 6 lhpbase W H W B
25 23 24 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B P Q ¬ X ˙ W s A ¬ s ˙ W s ˙ X ˙ W = X X ˙ Y W B
26 1 2 lattr K Lat X B Y B W B X ˙ Y Y ˙ W X ˙ W
27 21 22 16 25 26 syl13anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B P Q ¬ X ˙ W s A ¬ s ˙ W s ˙ X ˙ W = X X ˙ Y X ˙ Y Y ˙ W X ˙ W
28 19 27 mpand K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B P Q ¬ X ˙ W s A ¬ s ˙ W s ˙ X ˙ W = X X ˙ Y Y ˙ W X ˙ W
29 18 28 mtod K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B P Q ¬ X ˙ W s A ¬ s ˙ W s ˙ X ˙ W = X X ˙ Y ¬ Y ˙ W
30 17 29 jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B P Q ¬ X ˙ W s A ¬ s ˙ W s ˙ X ˙ W = X X ˙ Y P Q ¬ Y ˙ W
31 simp31 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B P Q ¬ X ˙ W s A ¬ s ˙ W s ˙ X ˙ W = X X ˙ Y s A ¬ s ˙ W
32 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B P Q ¬ X ˙ W s A ¬ s ˙ W s ˙ X ˙ W = X X ˙ Y K HL W H
33 simp31l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B P Q ¬ X ˙ W s A ¬ s ˙ W s ˙ X ˙ W = X X ˙ Y s A
34 22 18 jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B P Q ¬ X ˙ W s A ¬ s ˙ W s ˙ X ˙ W = X X ˙ Y X B ¬ X ˙ W
35 simp32 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B P Q ¬ X ˙ W s A ¬ s ˙ W s ˙ X ˙ W = X X ˙ Y s ˙ X ˙ W = X
36 1 2 3 4 5 6 cdleme30a K HL W H s A X B ¬ X ˙ W Y B s ˙ X ˙ W = X X ˙ Y s ˙ Y ˙ W = Y
37 32 33 34 16 35 19 36 syl132anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B P Q ¬ X ˙ W s A ¬ s ˙ W s ˙ X ˙ W = X X ˙ Y s ˙ Y ˙ W = Y
38 1 2 3 4 5 6 7 8 9 10 11 12 13 14 cdleme32a K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W Y B P Q ¬ Y ˙ W s A ¬ s ˙ W s ˙ Y ˙ W = Y F Y = N ˙ Y ˙ W
39 15 16 30 31 37 38 syl122anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B P Q ¬ X ˙ W s A ¬ s ˙ W s ˙ X ˙ W = X X ˙ Y F Y = N ˙ Y ˙ W