Metamath Proof Explorer


Theorem cdleme18c

Description: Part of proof of Lemma E in Crawley p. 114, 2nd sentence of 4th paragraph. F , G represent f(s), f_s(q) respectively. We show -. f_s(q) = p whenever p \/ q has three atoms under it (implied by the negated existential condition). (Contributed by NM, 10-Nov-2012)

Ref Expression
Hypotheses cdleme18.l ˙ = K
cdleme18.j ˙ = join K
cdleme18.m ˙ = meet K
cdleme18.a A = Atoms K
cdleme18.h H = LHyp K
cdleme18.u U = P ˙ Q ˙ W
cdleme18.f F = S ˙ U ˙ Q ˙ P ˙ S ˙ W
cdleme18.g G = P ˙ Q ˙ F ˙ Q ˙ S ˙ W
Assertion cdleme18c K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r G = P

Proof

Step Hyp Ref Expression
1 cdleme18.l ˙ = K
2 cdleme18.j ˙ = join K
3 cdleme18.m ˙ = meet K
4 cdleme18.a A = Atoms K
5 cdleme18.h H = LHyp K
6 cdleme18.u U = P ˙ Q ˙ W
7 cdleme18.f F = S ˙ U ˙ Q ˙ P ˙ S ˙ W
8 cdleme18.g G = P ˙ Q ˙ F ˙ Q ˙ S ˙ W
9 simp31 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P Q
10 simp32 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r ¬ S ˙ P ˙ Q
11 9 10 jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P Q ¬ S ˙ P ˙ Q
12 1 2 3 4 5 6 7 8 cdleme18b K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q G Q
13 11 12 syld3an3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r G Q
14 13 neneqd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r ¬ G = Q
15 simp1l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r K HL
16 simp1r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r W H
17 simp21l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P A
18 simp22l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r Q A
19 simp23l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r S A
20 1 2 3 4 5 6 7 8 cdleme4a K HL W H P A Q A Q A S A G ˙ P ˙ Q
21 15 16 17 18 18 19 20 syl231anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r G ˙ P ˙ Q
22 simp33 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r
23 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r K HL W H
24 simp21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P A ¬ P ˙ W
25 simp22 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r Q A ¬ Q ˙ W
26 simp23 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r S A ¬ S ˙ W
27 1 2 4 hlatlej2 K HL P A Q A Q ˙ P ˙ Q
28 15 17 18 27 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r Q ˙ P ˙ Q
29 1 2 3 4 5 6 7 8 cdleme7ga K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q Q ˙ P ˙ Q ¬ S ˙ P ˙ Q G A
30 23 24 25 25 26 9 28 10 29 syl323anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r G A
31 1 2 3 4 5 6 7 8 cdleme18a K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ G ˙ W
32 11 31 syld3an3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r ¬ G ˙ W
33 1 2 4 cdleme0nex K HL G ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P A Q A P Q G A ¬ G ˙ W G = P G = Q
34 15 21 22 17 18 9 30 32 33 syl332anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r G = P G = Q
35 34 ord K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r ¬ G = P G = Q
36 14 35 mt3d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r G = P