Metamath Proof Explorer


Theorem cdleme32c

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 cdleme32c 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 X ˙ F Y

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 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
16 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
17 16 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
18 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
19 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
20 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
21 1 6 lhpbase W H W B
22 20 21 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
23 1 2 4 latmlem1 K Lat X B Y B W B X ˙ Y X ˙ W ˙ Y ˙ W
24 17 18 19 22 23 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 X ˙ W ˙ Y ˙ W
25 15 24 mpd 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 ˙ Y ˙ W
26 1 4 latmcl K Lat X B W B X ˙ W B
27 17 18 22 26 syl3anc 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 B
28 1 4 latmcl K Lat Y B W B Y ˙ W B
29 17 19 22 28 syl3anc 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 B
30 simp12 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 A ¬ P ˙ W
31 simp13 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 Q A ¬ Q ˙ W
32 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
33 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
34 1 2 3 4 5 6 7 8 9 10 11 12 cdleme27cl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W s A ¬ s ˙ W P Q N B
35 16 20 30 31 32 33 34 syl222anc 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 N B
36 1 2 3 latjlej2 K Lat X ˙ W B Y ˙ W B N B X ˙ W ˙ Y ˙ W N ˙ X ˙ W ˙ N ˙ Y ˙ W
37 17 27 29 35 36 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 ˙ W ˙ Y ˙ W N ˙ X ˙ W ˙ N ˙ Y ˙ W
38 25 37 mpd 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 N ˙ X ˙ W ˙ N ˙ Y ˙ W
39 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
40 simp23 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 ¬ X ˙ W
41 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
42 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 X B P Q ¬ X ˙ W s A ¬ s ˙ W s ˙ X ˙ W = X F X = N ˙ X ˙ W
43 39 18 40 32 41 42 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 X = N ˙ X ˙ W
44 1 2 3 4 5 6 7 8 9 10 11 12 13 14 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
45 38 43 44 3brtr4d 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 X ˙ F Y