Metamath Proof Explorer


Theorem cdleme21i

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 cdleme21i 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 r A ¬ r ˙ W P ˙ r = Q ˙ r 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 simpl11 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 r A ¬ r ˙ W P ˙ r = Q ˙ r K HL W H
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 P A ¬ P ˙ W
15 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 Q A ¬ Q ˙ W
16 simp21l 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 S A
17 14 15 16 3jca 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 P A ¬ P ˙ W Q A ¬ Q ˙ W S A
18 17 adantr 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 r A ¬ r ˙ W P ˙ r = Q ˙ r P A ¬ P ˙ W Q A ¬ Q ˙ W S A
19 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 P Q
20 19 adantr 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 r A ¬ r ˙ W P ˙ r = Q ˙ r P Q
21 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 ¬ S ˙ P ˙ Q
22 21 adantr 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 r A ¬ r ˙ W P ˙ r = Q ˙ r ¬ S ˙ P ˙ Q
23 simpr 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 r A ¬ r ˙ W P ˙ r = Q ˙ r r A ¬ r ˙ W P ˙ r = Q ˙ r
24 1 2 4 5 4atexlem7 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q r A ¬ r ˙ W P ˙ r = Q ˙ r z A ¬ z ˙ W P ˙ z = S ˙ z
25 13 18 20 22 23 24 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 r A ¬ r ˙ W P ˙ r = Q ˙ r z A ¬ z ˙ W P ˙ z = S ˙ z
26 25 ex 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 r A ¬ r ˙ W P ˙ r = Q ˙ r z A ¬ z ˙ W P ˙ z = S ˙ z
27 1 2 3 4 5 6 7 8 9 10 11 12 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
28 26 27 syld 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 r A ¬ r ˙ W P ˙ r = Q ˙ r N = O