Metamath Proof Explorer


Theorem cdlemefr29exN

Description: Lemma for cdlemefs29bpre1N . (Compare cdleme25a .) TODO: FIX COMMENT. TODO: IS THIS NEEDED? (Contributed by NM, 28-Mar-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemefr29.b B = Base K
cdlemefr29.l ˙ = K
cdlemefr29.j ˙ = join K
cdlemefr29.m ˙ = meet K
cdlemefr29.a A = Atoms K
cdlemefr29.h H = LHyp K
Assertion cdlemefr29exN K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A C B s A ¬ s ˙ W s ˙ X ˙ W = X C ˙ X ˙ W B

Proof

Step Hyp Ref Expression
1 cdlemefr29.b B = Base K
2 cdlemefr29.l ˙ = K
3 cdlemefr29.j ˙ = join K
4 cdlemefr29.m ˙ = meet K
5 cdlemefr29.a A = Atoms K
6 cdlemefr29.h H = LHyp K
7 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A C B K HL W H
8 simp2r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A C B X B ¬ X ˙ W
9 1 2 3 4 5 6 lhpmcvr2 K HL W H X B ¬ X ˙ W s A ¬ s ˙ W s ˙ X ˙ W = X
10 7 8 9 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A C B s A ¬ s ˙ W s ˙ X ˙ W = X
11 nfv s K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
12 nfv s P Q X B ¬ X ˙ W
13 nfra1 s s A C B
14 11 12 13 nf3an s K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A C B
15 simp11l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A C B K HL
16 15 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A C B s A ¬ s ˙ W K HL
17 16 hllatd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A C B s A ¬ s ˙ W K Lat
18 simpl3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A C B s A ¬ s ˙ W s A C B
19 simprl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A C B s A ¬ s ˙ W s A
20 rsp s A C B s A C B
21 18 19 20 sylc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A C B s A ¬ s ˙ W C B
22 15 hllatd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A C B K Lat
23 simp2rl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A C B X B
24 simp11r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A C B W H
25 1 6 lhpbase W H W B
26 24 25 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A C B W B
27 1 4 latmcl K Lat X B W B X ˙ W B
28 22 23 26 27 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A C B X ˙ W B
29 28 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A C B s A ¬ s ˙ W X ˙ W B
30 1 3 latjcl K Lat C B X ˙ W B C ˙ X ˙ W B
31 17 21 29 30 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A C B s A ¬ s ˙ W C ˙ X ˙ W B
32 31 expr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A C B s A ¬ s ˙ W C ˙ X ˙ W B
33 32 adantrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A C B s A ¬ s ˙ W s ˙ X ˙ W = X C ˙ X ˙ W B
34 33 ancld K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A C B s A ¬ s ˙ W s ˙ X ˙ W = X ¬ s ˙ W s ˙ X ˙ W = X C ˙ X ˙ W B
35 34 ex K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A C B s A ¬ s ˙ W s ˙ X ˙ W = X ¬ s ˙ W s ˙ X ˙ W = X C ˙ X ˙ W B
36 14 35 reximdai K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A C B s A ¬ s ˙ W s ˙ X ˙ W = X s A ¬ s ˙ W s ˙ X ˙ W = X C ˙ X ˙ W B
37 10 36 mpd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q X B ¬ X ˙ W s A C B s A ¬ s ˙ W s ˙ X ˙ W = X C ˙ X ˙ W B