Metamath Proof Explorer


Theorem cdlema2N

Description: A condition for required for proof of Lemma A in Crawley p. 112. (Contributed by NM, 9-May-2012) (New usage is discouraged.)

Ref Expression
Hypotheses cdlema2.b B = Base K
cdlema2.l ˙ = K
cdlema2.j ˙ = join K
cdlema2.m ˙ = meet K
cdlema2.z 0 ˙ = 0. K
cdlema2.a A = Atoms K
Assertion cdlema2N K HL X B P A Q A R A R P R ˙ P ˙ Q P ˙ X ¬ Q ˙ X R ˙ X = 0 ˙

Proof

Step Hyp Ref Expression
1 cdlema2.b B = Base K
2 cdlema2.l ˙ = K
3 cdlema2.j ˙ = join K
4 cdlema2.m ˙ = meet K
5 cdlema2.z 0 ˙ = 0. K
6 cdlema2.a A = Atoms K
7 simp3ll K HL X B P A Q A R A R P R ˙ P ˙ Q P ˙ X ¬ Q ˙ X R P
8 simp3rl K HL X B P A Q A R A R P R ˙ P ˙ Q P ˙ X ¬ Q ˙ X P ˙ X
9 simp3rr K HL X B P A Q A R A R P R ˙ P ˙ Q P ˙ X ¬ Q ˙ X ¬ Q ˙ X
10 simp3lr K HL X B P A Q A R A R P R ˙ P ˙ Q P ˙ X ¬ Q ˙ X R ˙ P ˙ Q
11 8 9 10 3jca K HL X B P A Q A R A R P R ˙ P ˙ Q P ˙ X ¬ Q ˙ X P ˙ X ¬ Q ˙ X R ˙ P ˙ Q
12 1 2 3 6 exatleN K HL X B P A Q A R A P ˙ X ¬ Q ˙ X R ˙ P ˙ Q R ˙ X R = P
13 11 12 syld3an3 K HL X B P A Q A R A R P R ˙ P ˙ Q P ˙ X ¬ Q ˙ X R ˙ X R = P
14 13 necon3bbid K HL X B P A Q A R A R P R ˙ P ˙ Q P ˙ X ¬ Q ˙ X ¬ R ˙ X R P
15 7 14 mpbird K HL X B P A Q A R A R P R ˙ P ˙ Q P ˙ X ¬ Q ˙ X ¬ R ˙ X
16 simp1l K HL X B P A Q A R A R P R ˙ P ˙ Q P ˙ X ¬ Q ˙ X K HL
17 hlatl K HL K AtLat
18 16 17 syl K HL X B P A Q A R A R P R ˙ P ˙ Q P ˙ X ¬ Q ˙ X K AtLat
19 simp23 K HL X B P A Q A R A R P R ˙ P ˙ Q P ˙ X ¬ Q ˙ X R A
20 simp1r K HL X B P A Q A R A R P R ˙ P ˙ Q P ˙ X ¬ Q ˙ X X B
21 1 2 4 5 6 atnle K AtLat R A X B ¬ R ˙ X R ˙ X = 0 ˙
22 18 19 20 21 syl3anc K HL X B P A Q A R A R P R ˙ P ˙ Q P ˙ X ¬ Q ˙ X ¬ R ˙ X R ˙ X = 0 ˙
23 15 22 mpbid K HL X B P A Q A R A R P R ˙ P ˙ Q P ˙ X ¬ Q ˙ X R ˙ X = 0 ˙