Metamath Proof Explorer


Theorem cdleme11e

Description: Part of proof of Lemma E in Crawley p. 113. Lemma leading to cdleme11 . (Contributed by NM, 13-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
Assertion cdleme11e K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W T A P Q S T ¬ S ˙ P ˙ Q U ˙ S ˙ T C D

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 simp11 K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W T A P Q S T ¬ S ˙ P ˙ Q U ˙ S ˙ T K HL W H
10 simp12 K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W T A P Q S T ¬ S ˙ P ˙ Q U ˙ S ˙ T P A ¬ P ˙ W
11 simp22 K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W T A P Q S T ¬ S ˙ P ˙ Q U ˙ S ˙ T T A
12 simp21 K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W T A P Q S T ¬ S ˙ P ˙ Q U ˙ S ˙ T S A ¬ S ˙ W
13 simp11l K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W T A P Q S T ¬ S ˙ P ˙ Q U ˙ S ˙ T K HL
14 13 hllatd K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W T A P Q S T ¬ S ˙ P ˙ Q U ˙ S ˙ T K Lat
15 simp12l K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W T A P Q S T ¬ S ˙ P ˙ Q U ˙ S ˙ T P A
16 eqid Base K = Base K
17 16 4 atbase P A P Base K
18 15 17 syl K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W T A P Q S T ¬ S ˙ P ˙ Q U ˙ S ˙ T P Base K
19 simp21l K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W T A P Q S T ¬ S ˙ P ˙ Q U ˙ S ˙ T S A
20 16 4 atbase S A S Base K
21 19 20 syl K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W T A P Q S T ¬ S ˙ P ˙ Q U ˙ S ˙ T S Base K
22 16 4 atbase T A T Base K
23 11 22 syl K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W T A P Q S T ¬ S ˙ P ˙ Q U ˙ S ˙ T T Base K
24 simp1 K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W T A P Q S T ¬ S ˙ P ˙ Q U ˙ S ˙ T K HL W H P A ¬ P ˙ W Q A
25 simp2 K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W T A P Q S T ¬ S ˙ P ˙ Q U ˙ S ˙ T S A ¬ S ˙ W T A P Q
26 simp32 K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W T A P Q S T ¬ S ˙ P ˙ Q U ˙ S ˙ T ¬ S ˙ P ˙ Q
27 simp33 K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W T A P Q S T ¬ S ˙ P ˙ Q U ˙ S ˙ T U ˙ S ˙ T
28 1 2 3 4 5 6 cdleme11c K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W T A P Q ¬ S ˙ P ˙ Q U ˙ S ˙ T ¬ P ˙ S ˙ T
29 24 25 26 27 28 syl112anc K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W T A P Q S T ¬ S ˙ P ˙ Q U ˙ S ˙ T ¬ P ˙ S ˙ T
30 16 1 2 latnlej1r K Lat P Base K S Base K T Base K ¬ P ˙ S ˙ T P T
31 14 18 21 23 29 30 syl131anc K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W T A P Q S T ¬ S ˙ P ˙ Q U ˙ S ˙ T P T
32 simp31 K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W T A P Q S T ¬ S ˙ P ˙ Q U ˙ S ˙ T S T
33 1 2 4 hlatcon2 K HL S A T A P A S T ¬ P ˙ S ˙ T ¬ S ˙ P ˙ T
34 13 19 11 15 32 29 33 syl132anc K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W T A P Q S T ¬ S ˙ P ˙ Q U ˙ S ˙ T ¬ S ˙ P ˙ T
35 1 2 3 4 5 8 7 cdleme0e K HL W H P A ¬ P ˙ W T A S A ¬ S ˙ W P T ¬ S ˙ P ˙ T D C
36 9 10 11 12 31 34 35 syl132anc K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W T A P Q S T ¬ S ˙ P ˙ Q U ˙ S ˙ T D C
37 36 necomd K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W T A P Q S T ¬ S ˙ P ˙ Q U ˙ S ˙ T C D