Metamath Proof Explorer


Theorem cdleme8

Description: Part of proof of Lemma E in Crawley p. 113, 2nd paragraph on p. 114. C represents s_1. In their notation, we prove p \/ s_1 = p \/ s. (Contributed by NM, 9-Jun-2012)

Ref Expression
Hypotheses cdleme8.l ˙ = K
cdleme8.j ˙ = join K
cdleme8.m ˙ = meet K
cdleme8.a A = Atoms K
cdleme8.h H = LHyp K
cdleme8.4 C = P ˙ S ˙ W
Assertion cdleme8 K HL W H P A ¬ P ˙ W S A P ˙ C = P ˙ S

Proof

Step Hyp Ref Expression
1 cdleme8.l ˙ = K
2 cdleme8.j ˙ = join K
3 cdleme8.m ˙ = meet K
4 cdleme8.a A = Atoms K
5 cdleme8.h H = LHyp K
6 cdleme8.4 C = P ˙ S ˙ W
7 6 oveq2i P ˙ C = P ˙ P ˙ S ˙ W
8 simp1l K HL W H P A ¬ P ˙ W S A K HL
9 simp2l K HL W H P A ¬ P ˙ W S A P A
10 8 hllatd K HL W H P A ¬ P ˙ W S A K Lat
11 eqid Base K = Base K
12 11 4 atbase P A P Base K
13 9 12 syl K HL W H P A ¬ P ˙ W S A P Base K
14 11 4 atbase S A S Base K
15 14 3ad2ant3 K HL W H P A ¬ P ˙ W S A S Base K
16 11 2 latjcl K Lat P Base K S Base K P ˙ S Base K
17 10 13 15 16 syl3anc K HL W H P A ¬ P ˙ W S A P ˙ S Base K
18 simp1r K HL W H P A ¬ P ˙ W S A W H
19 11 5 lhpbase W H W Base K
20 18 19 syl K HL W H P A ¬ P ˙ W S A W Base K
21 11 1 2 latlej1 K Lat P Base K S Base K P ˙ P ˙ S
22 10 13 15 21 syl3anc K HL W H P A ¬ P ˙ W S A P ˙ P ˙ S
23 11 1 2 3 4 atmod3i1 K HL P A P ˙ S Base K W Base K P ˙ P ˙ S P ˙ P ˙ S ˙ W = P ˙ S ˙ P ˙ W
24 8 9 17 20 22 23 syl131anc K HL W H P A ¬ P ˙ W S A P ˙ P ˙ S ˙ W = P ˙ S ˙ P ˙ W
25 eqid 1. K = 1. K
26 1 2 25 4 5 lhpjat2 K HL W H P A ¬ P ˙ W P ˙ W = 1. K
27 26 3adant3 K HL W H P A ¬ P ˙ W S A P ˙ W = 1. K
28 27 oveq2d K HL W H P A ¬ P ˙ W S A P ˙ S ˙ P ˙ W = P ˙ S ˙ 1. K
29 hlol K HL K OL
30 8 29 syl K HL W H P A ¬ P ˙ W S A K OL
31 11 3 25 olm11 K OL P ˙ S Base K P ˙ S ˙ 1. K = P ˙ S
32 30 17 31 syl2anc K HL W H P A ¬ P ˙ W S A P ˙ S ˙ 1. K = P ˙ S
33 24 28 32 3eqtrd K HL W H P A ¬ P ˙ W S A P ˙ P ˙ S ˙ W = P ˙ S
34 7 33 syl5eq K HL W H P A ¬ P ˙ W S A P ˙ C = P ˙ S