Metamath Proof Explorer


Theorem cdleme17b

Description: Lemma leading to cdleme17c . (Contributed by NM, 11-Oct-2012)

Ref Expression
Hypotheses cdleme17.l ˙ = K
cdleme17.j ˙ = join K
cdleme17.m ˙ = meet K
cdleme17.a A = Atoms K
cdleme17.h H = LHyp K
cdleme17.u U = P ˙ Q ˙ W
cdleme17.f F = S ˙ U ˙ Q ˙ P ˙ S ˙ W
cdleme17.g G = P ˙ Q ˙ F ˙ P ˙ S ˙ W
cdleme17.c C = P ˙ S ˙ W
Assertion cdleme17b K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q ¬ C ˙ P ˙ Q

Proof

Step Hyp Ref Expression
1 cdleme17.l ˙ = K
2 cdleme17.j ˙ = join K
3 cdleme17.m ˙ = meet K
4 cdleme17.a A = Atoms K
5 cdleme17.h H = LHyp K
6 cdleme17.u U = P ˙ Q ˙ W
7 cdleme17.f F = S ˙ U ˙ Q ˙ P ˙ S ˙ W
8 cdleme17.g G = P ˙ Q ˙ F ˙ P ˙ S ˙ W
9 cdleme17.c C = P ˙ S ˙ W
10 simp33 K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q ¬ S ˙ P ˙ Q
11 eqid Base K = Base K
12 simpl1l K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q C ˙ P ˙ Q K HL
13 12 hllatd K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q C ˙ P ˙ Q K Lat
14 simpl32 K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q C ˙ P ˙ Q S A
15 11 4 atbase S A S Base K
16 14 15 syl K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q C ˙ P ˙ Q S Base K
17 simpl2l K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q C ˙ P ˙ Q P A
18 11 2 4 hlatjcl K HL P A S A P ˙ S Base K
19 12 17 14 18 syl3anc K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q C ˙ P ˙ Q P ˙ S Base K
20 simpl31 K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q C ˙ P ˙ Q Q A
21 11 2 4 hlatjcl K HL P A Q A P ˙ Q Base K
22 12 17 20 21 syl3anc K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q C ˙ P ˙ Q P ˙ Q Base K
23 1 2 4 hlatlej2 K HL P A S A S ˙ P ˙ S
24 12 17 14 23 syl3anc K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q C ˙ P ˙ Q S ˙ P ˙ S
25 simpl1r K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q C ˙ P ˙ Q W H
26 simpl2r K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q C ˙ P ˙ Q ¬ P ˙ W
27 1 2 3 4 5 9 cdleme8 K HL W H P A ¬ P ˙ W S A P ˙ C = P ˙ S
28 12 25 17 26 14 27 syl221anc K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q C ˙ P ˙ Q P ˙ C = P ˙ S
29 1 2 4 hlatlej1 K HL P A Q A P ˙ P ˙ Q
30 12 17 20 29 syl3anc K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q C ˙ P ˙ Q P ˙ P ˙ Q
31 simpr K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q C ˙ P ˙ Q C ˙ P ˙ Q
32 11 4 atbase P A P Base K
33 17 32 syl K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q C ˙ P ˙ Q P Base K
34 11 2 3 4 5 9 cdleme9b K HL P A S A W H C Base K
35 12 17 14 25 34 syl13anc K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q C ˙ P ˙ Q C Base K
36 11 1 2 latjle12 K Lat P Base K C Base K P ˙ Q Base K P ˙ P ˙ Q C ˙ P ˙ Q P ˙ C ˙ P ˙ Q
37 13 33 35 22 36 syl13anc K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q C ˙ P ˙ Q P ˙ P ˙ Q C ˙ P ˙ Q P ˙ C ˙ P ˙ Q
38 30 31 37 mpbi2and K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q C ˙ P ˙ Q P ˙ C ˙ P ˙ Q
39 28 38 eqbrtrrd K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q C ˙ P ˙ Q P ˙ S ˙ P ˙ Q
40 11 1 13 16 19 22 24 39 lattrd K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q C ˙ P ˙ Q S ˙ P ˙ Q
41 10 40 mtand K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q ¬ C ˙ P ˙ Q