Metamath Proof Explorer


Theorem cdleme11j

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 cdleme11j K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q C ˙ Q ˙ F

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 simp1l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q K HL
11 simp22l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q Q A
12 1 2 3 4 5 6 9 cdleme3fa K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q F A
13 1 2 4 hlatlej2 K HL Q A F A F ˙ Q ˙ F
14 10 11 12 13 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q F ˙ Q ˙ F
15 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q K HL W H
16 simp21l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q P A
17 simp22 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q Q A ¬ Q ˙ W
18 simp23l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q S A
19 simp3l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q P Q
20 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
21 15 16 17 18 19 20 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q Q ˙ F = Q ˙ C
22 14 21 breqtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q F ˙ Q ˙ C
23 simp21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q P A ¬ P ˙ W
24 simp3r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ S ˙ P ˙ Q
25 1 2 3 4 cdleme00a K HL P A Q A S A ¬ S ˙ P ˙ Q S P
26 10 16 11 18 24 25 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q S P
27 26 necomd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q P S
28 1 2 3 4 5 7 cdleme9a K HL W H P A ¬ P ˙ W S A P S C A
29 15 23 18 27 28 syl112anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q C A
30 simp3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q P Q ¬ S ˙ P ˙ Q
31 1 2 3 4 5 6 7 6 9 cdleme11h K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q F Q
32 15 23 17 18 30 31 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q F Q
33 1 2 4 hlatexch1 K HL F A C A Q A F Q F ˙ Q ˙ C C ˙ Q ˙ F
34 10 12 29 11 32 33 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q F ˙ Q ˙ C C ˙ Q ˙ F
35 22 34 mpd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q C ˙ Q ˙ F