Metamath Proof Explorer


Theorem cdleme17c

Description: Part of proof of Lemma E in Crawley p. 114, first part of 4th paragraph. C represents s_1. We show, in their notation, (p \/ q) /\ (q \/ s_1)=q. (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 cdleme17c K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q P ˙ Q ˙ Q ˙ C = Q

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 simp1l K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q K HL
11 simp2l K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q P A
12 simp31 K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q Q A
13 2 4 hlatjcom K HL P A Q A P ˙ Q = Q ˙ P
14 10 11 12 13 syl3anc K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q P ˙ Q = Q ˙ P
15 14 oveq1d K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q P ˙ Q ˙ Q ˙ C = Q ˙ P ˙ Q ˙ C
16 simp1r K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q W H
17 simp2r K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q ¬ P ˙ W
18 simp32 K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q S A
19 10 hllatd K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q K Lat
20 eqid Base K = Base K
21 20 4 atbase S A S Base K
22 18 21 syl K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q S Base K
23 20 4 atbase P A P Base K
24 11 23 syl K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q P Base K
25 20 4 atbase Q A Q Base K
26 12 25 syl K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q Q Base K
27 simp33 K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q ¬ S ˙ P ˙ Q
28 20 1 2 latnlej1l K Lat S Base K P Base K Q Base K ¬ S ˙ P ˙ Q S P
29 28 necomd K Lat S Base K P Base K Q Base K ¬ S ˙ P ˙ Q P S
30 19 22 24 26 27 29 syl131anc K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q P S
31 1 2 3 4 5 9 cdleme9a K HL W H P A ¬ P ˙ W S A P S C A
32 10 16 11 17 18 30 31 syl222anc K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q C A
33 1 2 3 4 5 6 7 8 9 cdleme17b K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q ¬ C ˙ P ˙ Q
34 1 2 3 4 2llnma1 K HL P A Q A C A ¬ C ˙ P ˙ Q Q ˙ P ˙ Q ˙ C = Q
35 10 11 12 32 33 34 syl131anc K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q Q ˙ P ˙ Q ˙ C = Q
36 15 35 eqtrd K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ P ˙ Q P ˙ Q ˙ Q ˙ C = Q