Metamath Proof Explorer


Theorem cdleme25a

Description: Lemma for cdleme25b . (Contributed by NM, 1-Jan-2013)

Ref Expression
Hypotheses cdleme24.b B = Base K
cdleme24.l ˙ = K
cdleme24.j ˙ = join K
cdleme24.m ˙ = meet K
cdleme24.a A = Atoms K
cdleme24.h H = LHyp K
cdleme24.u U = P ˙ Q ˙ W
cdleme24.f F = s ˙ U ˙ Q ˙ P ˙ s ˙ W
cdleme24.n N = P ˙ Q ˙ F ˙ R ˙ s ˙ W
Assertion cdleme25a K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R ˙ P ˙ Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q N B

Proof

Step Hyp Ref Expression
1 cdleme24.b B = Base K
2 cdleme24.l ˙ = K
3 cdleme24.j ˙ = join K
4 cdleme24.m ˙ = meet K
5 cdleme24.a A = Atoms K
6 cdleme24.h H = LHyp K
7 cdleme24.u U = P ˙ Q ˙ W
8 cdleme24.f F = s ˙ U ˙ Q ˙ P ˙ s ˙ W
9 cdleme24.n N = P ˙ Q ˙ F ˙ R ˙ s ˙ W
10 simp11l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R ˙ P ˙ Q K HL
11 simp11r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R ˙ P ˙ Q W H
12 simp12 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R ˙ P ˙ Q P A ¬ P ˙ W
13 simp13 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R ˙ P ˙ Q Q A ¬ Q ˙ W
14 simp3l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R ˙ P ˙ Q P Q
15 2 3 5 6 cdlemb2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q
16 10 11 12 13 14 15 syl221anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R ˙ P ˙ Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q
17 10 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R ˙ P ˙ Q s A K HL
18 11 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R ˙ P ˙ Q s A W H
19 simp12l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R ˙ P ˙ Q P A
20 19 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R ˙ P ˙ Q s A P A
21 simp13l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R ˙ P ˙ Q Q A
22 21 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R ˙ P ˙ Q s A Q A
23 simpl2l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R ˙ P ˙ Q s A R A
24 simpr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R ˙ P ˙ Q s A s A
25 2 3 4 5 6 7 8 9 1 cdleme22gb K HL W H P A Q A R A s A N B
26 17 18 20 22 23 24 25 syl222anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R ˙ P ˙ Q s A N B
27 26 a1d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R ˙ P ˙ Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q N B
28 27 ancld K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R ˙ P ˙ Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q ¬ s ˙ W ¬ s ˙ P ˙ Q N B
29 28 reximdva K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R ˙ P ˙ Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q N B
30 16 29 mpd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R ˙ P ˙ Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q N B