Metamath Proof Explorer


Theorem cdleme21f

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
cdleme21.b B = z ˙ U ˙ Q ˙ P ˙ z ˙ W
cdleme21.d D = R ˙ S ˙ W
cdleme21.e E = R ˙ z ˙ W
cdleme21d.n N = P ˙ Q ˙ F ˙ D
cdleme21d.z Z = P ˙ Q ˙ B ˙ E
cdleme21.g G = T ˙ U ˙ Q ˙ P ˙ T ˙ W
cdleme21.y Y = R ˙ T ˙ W
cdleme21.o O = P ˙ Q ˙ G ˙ Y
Assertion 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

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 cdleme21.b B = z ˙ U ˙ Q ˙ P ˙ z ˙ W
9 cdleme21.d D = R ˙ S ˙ W
10 cdleme21.e E = R ˙ z ˙ W
11 cdleme21d.n N = P ˙ Q ˙ F ˙ D
12 cdleme21d.z Z = P ˙ Q ˙ B ˙ E
13 cdleme21.g G = T ˙ U ˙ Q ˙ P ˙ T ˙ W
14 cdleme21.y Y = R ˙ T ˙ W
15 cdleme21.o O = P ˙ Q ˙ G ˙ Y
16 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
17 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 P A ¬ P ˙ W
18 simp13 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 Q A ¬ Q ˙ W
19 simp31 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
20 simp21 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
21 simp231 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 Q
22 simp232 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 ˙ P ˙ Q
23 simp32l 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
24 22 23 jca 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 ˙ P ˙ Q R ˙ P ˙ Q
25 simp33 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
26 1 2 3 4 5 6 7 8 9 10 11 12 cdleme21d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q R ˙ P ˙ Q z A ¬ z ˙ W P ˙ z = S ˙ z N = Z
27 16 17 18 19 20 21 24 25 26 syl323anc 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 = Z
28 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 cdleme21e 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 O = Z
29 27 28 eqtr4d 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