Metamath Proof Explorer


Theorem cdleme10

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

Ref Expression
Hypotheses cdleme10.l ˙ = K
cdleme10.j ˙ = join K
cdleme10.m ˙ = meet K
cdleme10.a A = Atoms K
cdleme10.h H = LHyp K
cdleme10.d D = R ˙ S ˙ W
Assertion cdleme10 K HL W H R A S A ¬ S ˙ W S ˙ D = S ˙ R

Proof

Step Hyp Ref Expression
1 cdleme10.l ˙ = K
2 cdleme10.j ˙ = join K
3 cdleme10.m ˙ = meet K
4 cdleme10.a A = Atoms K
5 cdleme10.h H = LHyp K
6 cdleme10.d D = R ˙ S ˙ W
7 6 oveq2i S ˙ D = S ˙ R ˙ S ˙ W
8 simp1l K HL W H R A S A ¬ S ˙ W K HL
9 simp3l K HL W H R A S A ¬ S ˙ W S A
10 simp2 K HL W H R A S A ¬ S ˙ W R A
11 eqid Base K = Base K
12 11 2 4 hlatjcl K HL R A S A R ˙ S Base K
13 8 10 9 12 syl3anc K HL W H R A S A ¬ S ˙ W R ˙ S Base K
14 simp1r K HL W H R A S A ¬ S ˙ W W H
15 11 5 lhpbase W H W Base K
16 14 15 syl K HL W H R A S A ¬ S ˙ W W Base K
17 8 hllatd K HL W H R A S A ¬ S ˙ W K Lat
18 11 4 atbase R A R Base K
19 18 3ad2ant2 K HL W H R A S A ¬ S ˙ W R Base K
20 11 4 atbase S A S Base K
21 9 20 syl K HL W H R A S A ¬ S ˙ W S Base K
22 11 1 2 latlej2 K Lat R Base K S Base K S ˙ R ˙ S
23 17 19 21 22 syl3anc K HL W H R A S A ¬ S ˙ W S ˙ R ˙ S
24 11 1 2 3 4 atmod3i1 K HL S A R ˙ S Base K W Base K S ˙ R ˙ S S ˙ R ˙ S ˙ W = R ˙ S ˙ S ˙ W
25 8 9 13 16 23 24 syl131anc K HL W H R A S A ¬ S ˙ W S ˙ R ˙ S ˙ W = R ˙ S ˙ S ˙ W
26 11 2 latjcom K Lat R Base K S Base K R ˙ S = S ˙ R
27 17 19 21 26 syl3anc K HL W H R A S A ¬ S ˙ W R ˙ S = S ˙ R
28 eqid 1. K = 1. K
29 1 2 28 4 5 lhpjat2 K HL W H S A ¬ S ˙ W S ˙ W = 1. K
30 29 3adant2 K HL W H R A S A ¬ S ˙ W S ˙ W = 1. K
31 27 30 oveq12d K HL W H R A S A ¬ S ˙ W R ˙ S ˙ S ˙ W = S ˙ R ˙ 1. K
32 hlol K HL K OL
33 8 32 syl K HL W H R A S A ¬ S ˙ W K OL
34 11 2 latjcl K Lat S Base K R Base K S ˙ R Base K
35 17 21 19 34 syl3anc K HL W H R A S A ¬ S ˙ W S ˙ R Base K
36 11 3 28 olm11 K OL S ˙ R Base K S ˙ R ˙ 1. K = S ˙ R
37 33 35 36 syl2anc K HL W H R A S A ¬ S ˙ W S ˙ R ˙ 1. K = S ˙ R
38 25 31 37 3eqtrd K HL W H R A S A ¬ S ˙ W S ˙ R ˙ S ˙ W = S ˙ R
39 7 38 syl5eq K HL W H R A S A ¬ S ˙ W S ˙ D = S ˙ R