Metamath Proof Explorer


Theorem cdleme21g

Description: Part of proof of Lemma E in Crawley p. 115. (Contributed by NM, 29-Nov-2012)

Ref Expression
Hypotheses cdleme21.l ˙ = K
cdleme21.j ˙ = join K
cdleme21.m ˙ = meet K
cdleme21.a A = Atoms K
cdleme21.h H = LHyp K
cdleme21.u U = P ˙ Q ˙ W
cdleme21.f F = S ˙ U ˙ Q ˙ P ˙ S ˙ W
cdleme21g.g G = T ˙ U ˙ Q ˙ P ˙ T ˙ W
cdleme21g.d D = R ˙ S ˙ W
cdleme21g.y Y = R ˙ T ˙ W
cdleme21g.n N = P ˙ Q ˙ F ˙ D
cdleme21g.o O = P ˙ Q ˙ G ˙ Y
Assertion cdleme21g K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R A ¬ R ˙ W R ˙ P ˙ Q U ˙ S ˙ T z A ¬ z ˙ W P ˙ z = S ˙ z N = O

Proof

Step Hyp Ref Expression
1 cdleme21.l ˙ = K
2 cdleme21.j ˙ = join K
3 cdleme21.m ˙ = meet K
4 cdleme21.a A = Atoms K
5 cdleme21.h H = LHyp K
6 cdleme21.u U = P ˙ Q ˙ W
7 cdleme21.f F = S ˙ U ˙ Q ˙ P ˙ S ˙ W
8 cdleme21g.g G = T ˙ U ˙ Q ˙ P ˙ T ˙ W
9 cdleme21g.d D = R ˙ S ˙ W
10 cdleme21g.y Y = R ˙ T ˙ W
11 cdleme21g.n N = P ˙ Q ˙ F ˙ D
12 cdleme21g.o O = P ˙ Q ˙ G ˙ Y
13 eqid z ˙ U ˙ Q ˙ P ˙ z ˙ W = z ˙ U ˙ Q ˙ P ˙ z ˙ W
14 eqid R ˙ z ˙ W = R ˙ z ˙ W
15 eqid P ˙ Q ˙ z ˙ U ˙ Q ˙ P ˙ z ˙ W ˙ R ˙ z ˙ W = P ˙ Q ˙ z ˙ U ˙ Q ˙ P ˙ z ˙ W ˙ R ˙ z ˙ W
16 1 2 3 4 5 6 7 13 9 14 11 15 8 10 12 cdleme21f K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R A ¬ R ˙ W R ˙ P ˙ Q U ˙ S ˙ T z A ¬ z ˙ W P ˙ z = S ˙ z N = O