Metamath Proof Explorer


Theorem cdleme21h

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 cdleme21h 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 simp11 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 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
14 simp12 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 S A ¬ S ˙ W T A ¬ T ˙ W P Q ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q
15 simp13l 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 R A ¬ R ˙ W
16 simp13r 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 R ˙ P ˙ Q U ˙ S ˙ T
17 simp2 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 z A
18 simp3l 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 ¬ z ˙ W
19 simp3r 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 P ˙ z = S ˙ z
20 17 18 19 jca31 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 z A ¬ z ˙ W P ˙ z = S ˙ z
21 1 2 3 4 5 6 7 8 9 10 11 12 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
22 13 14 15 16 20 21 syl113anc 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
23 22 rexlimdv3a 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