Metamath Proof Explorer


Theorem cdleme11h

Description: Part of proof of Lemma E in Crawley p. 113. Lemma leading to cdleme11 . (Contributed by NM, 14-Jun-2012)

Ref Expression
Hypotheses cdleme11.l ˙ = K
cdleme11.j ˙ = join K
cdleme11.m ˙ = meet K
cdleme11.a A = Atoms K
cdleme11.h H = LHyp K
cdleme11.u U = P ˙ Q ˙ W
cdleme11.c C = P ˙ S ˙ W
cdleme11.d D = P ˙ T ˙ W
cdleme11.f F = S ˙ U ˙ Q ˙ P ˙ S ˙ W
Assertion cdleme11h K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q F Q

Proof

Step Hyp Ref Expression
1 cdleme11.l ˙ = K
2 cdleme11.j ˙ = join K
3 cdleme11.m ˙ = meet K
4 cdleme11.a A = Atoms K
5 cdleme11.h H = LHyp K
6 cdleme11.u U = P ˙ Q ˙ W
7 cdleme11.c C = P ˙ S ˙ W
8 cdleme11.d D = P ˙ T ˙ W
9 cdleme11.f F = S ˙ U ˙ Q ˙ P ˙ S ˙ W
10 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q K HL W H
11 simp21l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q P A
12 simp23 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q S A
13 simp22l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q Q A
14 simp22r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q ¬ Q ˙ W
15 1 2 3 4 5 7 cdleme0c K HL W H P A S A Q A ¬ Q ˙ W C Q
16 10 11 12 13 14 15 syl122anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q C Q
17 16 necomd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q Q C
18 simp1l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q K HL
19 simp21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q P A ¬ P ˙ W
20 simp3r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q ¬ S ˙ P ˙ Q
21 1 2 3 4 cdleme00a K HL P A Q A S A ¬ S ˙ P ˙ Q S P
22 18 11 13 12 20 21 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q S P
23 22 necomd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q P S
24 1 2 3 4 5 7 cdleme9a K HL W H P A ¬ P ˙ W S A P S C A
25 10 19 12 23 24 syl112anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q C A
26 2 4 lnnat K HL Q A C A Q C ¬ Q ˙ C A
27 18 13 25 26 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q Q C ¬ Q ˙ C A
28 17 27 mpbid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q ¬ Q ˙ C A
29 2 4 hlatjidm K HL Q A Q ˙ Q = Q
30 18 13 29 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q Q ˙ Q = Q
31 30 13 eqeltrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q Q ˙ Q A
32 oveq2 F = Q Q ˙ F = Q ˙ Q
33 32 eleq1d F = Q Q ˙ F A Q ˙ Q A
34 31 33 syl5ibrcom K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q F = Q Q ˙ F A
35 simp22 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q Q A ¬ Q ˙ W
36 simp3l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q P Q
37 1 2 3 4 5 6 7 6 9 cdleme11g K HL W H P A Q A ¬ Q ˙ W S A P Q Q ˙ F = Q ˙ C
38 10 11 35 12 36 37 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q Q ˙ F = Q ˙ C
39 38 eleq1d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q Q ˙ F A Q ˙ C A
40 34 39 sylibd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q F = Q Q ˙ C A
41 40 necon3bd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q ¬ Q ˙ C A F Q
42 28 41 mpd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q F Q