Metamath Proof Explorer


Theorem cdleme32le

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 20-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 cdleme32le K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B 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 simpl1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y P Q ¬ X ˙ W K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
16 simpl2l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y P Q ¬ X ˙ W X B
17 simpl2r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y P Q ¬ X ˙ W Y B
18 simpr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y P Q ¬ X ˙ W P Q ¬ X ˙ W
19 simpl3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y P Q ¬ X ˙ W X ˙ Y
20 1 2 3 4 5 6 7 8 9 10 11 12 13 14 cdleme32d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B P Q ¬ X ˙ W X ˙ Y F X ˙ F Y
21 15 16 17 18 19 20 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y P Q ¬ X ˙ W F X ˙ F Y
22 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y P Q ¬ Y ˙ W ¬ P Q ¬ X ˙ W K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
23 simp12 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y P Q ¬ Y ˙ W ¬ P Q ¬ X ˙ W X B Y B
24 simp3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y P Q ¬ Y ˙ W ¬ P Q ¬ X ˙ W ¬ P Q ¬ X ˙ W
25 simp2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y P Q ¬ Y ˙ W ¬ P Q ¬ X ˙ W P Q ¬ Y ˙ W
26 simp13 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y P Q ¬ Y ˙ W ¬ P Q ¬ X ˙ W X ˙ Y
27 1 2 3 4 5 6 7 8 9 10 11 12 13 14 cdleme32f K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B ¬ P Q ¬ X ˙ W P Q ¬ Y ˙ W X ˙ Y F X ˙ F Y
28 22 23 24 25 26 27 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y P Q ¬ Y ˙ W ¬ P Q ¬ X ˙ W F X ˙ F Y
29 28 3exp K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y P Q ¬ Y ˙ W ¬ P Q ¬ X ˙ W F X ˙ F Y
30 simp13 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y ¬ P Q ¬ Y ˙ W ¬ P Q ¬ X ˙ W X ˙ Y
31 simp12l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y ¬ P Q ¬ Y ˙ W ¬ P Q ¬ X ˙ W X B
32 simp3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y ¬ P Q ¬ Y ˙ W ¬ P Q ¬ X ˙ W ¬ P Q ¬ X ˙ W
33 14 cdleme31fv2 X B ¬ P Q ¬ X ˙ W F X = X
34 31 32 33 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y ¬ P Q ¬ Y ˙ W ¬ P Q ¬ X ˙ W F X = X
35 simp12r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y ¬ P Q ¬ Y ˙ W ¬ P Q ¬ X ˙ W Y B
36 simp2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y ¬ P Q ¬ Y ˙ W ¬ P Q ¬ X ˙ W ¬ P Q ¬ Y ˙ W
37 14 cdleme31fv2 Y B ¬ P Q ¬ Y ˙ W F Y = Y
38 35 36 37 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y ¬ P Q ¬ Y ˙ W ¬ P Q ¬ X ˙ W F Y = Y
39 30 34 38 3brtr4d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y ¬ P Q ¬ Y ˙ W ¬ P Q ¬ X ˙ W F X ˙ F Y
40 39 3exp K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y ¬ P Q ¬ Y ˙ W ¬ P Q ¬ X ˙ W F X ˙ F Y
41 29 40 pm2.61d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y ¬ P Q ¬ X ˙ W F X ˙ F Y
42 41 imp K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y ¬ P Q ¬ X ˙ W F X ˙ F Y
43 21 42 pm2.61dan K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Y B X ˙ Y F X ˙ F Y