Metamath Proof Explorer


Theorem cdleme17a

Description: Part of proof of Lemma E in Crawley p. 114, first part of 4th paragraph. F , G , and C represent f(s), f_s(p), and s_1 respectively. We show, in their notation, f_s(p)=(p \/ q) /\ (q \/ s_1). (Contributed by NM, 11-Oct-2012)

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

Proof

Step Hyp Ref Expression
1 cdleme17.l ˙ = K
2 cdleme17.j ˙ = join K
3 cdleme17.m ˙ = meet K
4 cdleme17.a A = Atoms K
5 cdleme17.h H = LHyp K
6 cdleme17.u U = P ˙ Q ˙ W
7 cdleme17.f F = S ˙ U ˙ Q ˙ P ˙ S ˙ W
8 cdleme17.g G = P ˙ Q ˙ F ˙ P ˙ S ˙ W
9 cdleme17.c C = P ˙ S ˙ W
10 1 2 3 4 5 6 7 8 9 cdleme7a G = P ˙ Q ˙ F ˙ C
11 1 2 3 4 5 6 7 9 cdleme9 K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W ¬ S ˙ P ˙ Q F ˙ C = Q ˙ C
12 11 oveq2d K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W ¬ S ˙ P ˙ Q P ˙ Q ˙ F ˙ C = P ˙ Q ˙ Q ˙ C
13 10 12 syl5eq K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W ¬ S ˙ P ˙ Q G = P ˙ Q ˙ Q ˙ C