Metamath Proof Explorer


Theorem cdleme19a

Description: Part of proof of Lemma E in Crawley p. 113, 5th paragraph on p. 114, 1st line. D represents s_2. In their notation, we prove that if r <_ s \/ t, then s_2=(s \/ t) /\ w. (Contributed by NM, 13-Nov-2012)

Ref Expression
Hypotheses cdleme19.l ˙ = K
cdleme19.j ˙ = join K
cdleme19.m ˙ = meet K
cdleme19.a A = Atoms K
cdleme19.h H = LHyp K
cdleme19.u U = P ˙ Q ˙ W
cdleme19.f F = S ˙ U ˙ Q ˙ P ˙ S ˙ W
cdleme19.g G = T ˙ U ˙ Q ˙ P ˙ T ˙ W
cdleme19.d D = R ˙ S ˙ W
cdleme19.y Y = R ˙ T ˙ W
Assertion cdleme19a K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T D = S ˙ T ˙ W

Proof

Step Hyp Ref Expression
1 cdleme19.l ˙ = K
2 cdleme19.j ˙ = join K
3 cdleme19.m ˙ = meet K
4 cdleme19.a A = Atoms K
5 cdleme19.h H = LHyp K
6 cdleme19.u U = P ˙ Q ˙ W
7 cdleme19.f F = S ˙ U ˙ Q ˙ P ˙ S ˙ W
8 cdleme19.g G = T ˙ U ˙ Q ˙ P ˙ T ˙ W
9 cdleme19.d D = R ˙ S ˙ W
10 cdleme19.y Y = R ˙ T ˙ W
11 eqid Base K = Base K
12 hllat K HL K Lat
13 12 3ad2ant1 K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T K Lat
14 simp1 K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T K HL
15 simp21 K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T R A
16 simp22 K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T S A
17 11 2 4 hlatjcl K HL R A S A R ˙ S Base K
18 14 15 16 17 syl3anc K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T R ˙ S Base K
19 simp23 K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T T A
20 11 2 4 hlatjcl K HL S A T A S ˙ T Base K
21 14 16 19 20 syl3anc K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T S ˙ T Base K
22 simp33 K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T R ˙ S ˙ T
23 1 2 4 hlatlej1 K HL S A T A S ˙ S ˙ T
24 14 16 19 23 syl3anc K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T S ˙ S ˙ T
25 11 4 atbase R A R Base K
26 15 25 syl K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T R Base K
27 11 4 atbase S A S Base K
28 16 27 syl K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T S Base K
29 11 1 2 latjle12 K Lat R Base K S Base K S ˙ T Base K R ˙ S ˙ T S ˙ S ˙ T R ˙ S ˙ S ˙ T
30 13 26 28 21 29 syl13anc K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T R ˙ S ˙ T S ˙ S ˙ T R ˙ S ˙ S ˙ T
31 22 24 30 mpbi2and K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T R ˙ S ˙ S ˙ T
32 1 2 4 hlatlej2 K HL R A S A S ˙ R ˙ S
33 14 15 16 32 syl3anc K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T S ˙ R ˙ S
34 hlcvl K HL K CvLat
35 34 3ad2ant1 K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T K CvLat
36 simp31 K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T R ˙ P ˙ Q
37 simp32 K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T ¬ S ˙ P ˙ Q
38 nbrne2 R ˙ P ˙ Q ¬ S ˙ P ˙ Q R S
39 36 37 38 syl2anc K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T R S
40 1 2 4 cvlatexch1 K CvLat R A T A S A R S R ˙ S ˙ T T ˙ S ˙ R
41 35 15 19 16 39 40 syl131anc K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T R ˙ S ˙ T T ˙ S ˙ R
42 22 41 mpd K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T T ˙ S ˙ R
43 2 4 hlatjcom K HL R A S A R ˙ S = S ˙ R
44 14 15 16 43 syl3anc K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T R ˙ S = S ˙ R
45 42 44 breqtrrd K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T T ˙ R ˙ S
46 11 4 atbase T A T Base K
47 19 46 syl K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T T Base K
48 11 1 2 latjle12 K Lat S Base K T Base K R ˙ S Base K S ˙ R ˙ S T ˙ R ˙ S S ˙ T ˙ R ˙ S
49 13 28 47 18 48 syl13anc K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T S ˙ R ˙ S T ˙ R ˙ S S ˙ T ˙ R ˙ S
50 33 45 49 mpbi2and K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T S ˙ T ˙ R ˙ S
51 11 1 13 18 21 31 50 latasymd K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T R ˙ S = S ˙ T
52 51 oveq1d K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T R ˙ S ˙ W = S ˙ T ˙ W
53 9 52 syl5eq K HL R A S A T A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ T D = S ˙ T ˙ W