Metamath Proof Explorer


Theorem cdleme32snaw

Description: Show that [_ R / s ]_ N is an atom not under W . (Contributed by NM, 6-Mar-2013)

Ref Expression
Hypotheses cdleme32.b B = Base K
cdleme32.l ˙ = K
cdleme32.j ˙ = join K
cdleme32.m ˙ = meet K
cdleme32.a A = Atoms K
cdleme32.h H = LHyp K
cdleme32.u U = P ˙ Q ˙ W
cdleme32.c C = s ˙ U ˙ Q ˙ P ˙ s ˙ W
cdleme32.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdleme32.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
cdleme32.i I = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E
cdleme32.n N = if s ˙ P ˙ Q I C
Assertion cdleme32snaw K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R / s N A ¬ R / s N ˙ W

Proof

Step Hyp Ref Expression
1 cdleme32.b B = Base K
2 cdleme32.l ˙ = K
3 cdleme32.j ˙ = join K
4 cdleme32.m ˙ = meet K
5 cdleme32.a A = Atoms K
6 cdleme32.h H = LHyp K
7 cdleme32.u U = P ˙ Q ˙ W
8 cdleme32.c C = s ˙ U ˙ Q ˙ P ˙ s ˙ W
9 cdleme32.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
10 cdleme32.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
11 cdleme32.i I = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E
12 cdleme32.n N = if s ˙ P ˙ Q I C
13 eqid P ˙ Q ˙ D ˙ R ˙ t ˙ W = P ˙ Q ˙ D ˙ R ˙ t ˙ W
14 eqid ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = P ˙ Q ˙ D ˙ R ˙ t ˙ W = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = P ˙ Q ˙ D ˙ R ˙ t ˙ W
15 1 2 3 4 5 6 7 9 10 11 12 13 14 cdlemefs32sn1aw K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q R / s N A ¬ R / s N ˙ W
16 15 3expa K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q R / s N A ¬ R / s N ˙ W
17 1 2 3 4 5 6 7 8 12 cdlemefr32sn2aw K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q R / s N A ¬ R / s N ˙ W
18 17 3expa K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q R / s N A ¬ R / s N ˙ W
19 16 18 pm2.61dan K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R / s N A ¬ R / s N ˙ W