Metamath Proof Explorer


Theorem cdleme20d

Description: Part of proof of Lemma E in Crawley p. 113, last paragraph on p. 114, second line. D , F , Y , G represent s_2, f(s), t_2, f(t). (Contributed by NM, 17-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
cdleme20.v V = S ˙ T ˙ W
Assertion cdleme20d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q F ˙ G ˙ D ˙ Y = V

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 cdleme20.v V = S ˙ T ˙ W
12 simp11l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q K HL
13 hlol K HL K OL
14 12 13 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q K OL
15 12 hllatd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q K Lat
16 simp11r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q W H
17 simp12l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q P A
18 simp13l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q Q A
19 simp21l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q S A
20 eqid Base K = Base K
21 1 2 3 4 5 6 7 20 cdleme1b K HL W H P A Q A S A F Base K
22 12 16 17 18 19 21 syl23anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q F Base K
23 simp22l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q T A
24 1 2 3 4 5 6 8 20 cdleme1b K HL W H P A Q A T A G Base K
25 12 16 17 18 23 24 syl23anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q G Base K
26 20 2 latjcl K Lat F Base K G Base K F ˙ G Base K
27 15 22 25 26 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q F ˙ G Base K
28 20 5 lhpbase W H W Base K
29 16 28 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q W Base K
30 simp23l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q R A
31 20 2 4 hlatjcl K HL R A S A R ˙ S Base K
32 12 30 19 31 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q R ˙ S Base K
33 20 4 atbase T A T Base K
34 23 33 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q T Base K
35 20 2 latjcl K Lat R ˙ S Base K T Base K R ˙ S ˙ T Base K
36 15 32 34 35 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q R ˙ S ˙ T Base K
37 20 3 latmassOLD K OL F ˙ G Base K W Base K R ˙ S ˙ T Base K F ˙ G ˙ W ˙ R ˙ S ˙ T = F ˙ G ˙ W ˙ R ˙ S ˙ T
38 14 27 29 36 37 syl13anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q F ˙ G ˙ W ˙ R ˙ S ˙ T = F ˙ G ˙ W ˙ R ˙ S ˙ T
39 1 2 4 hlatlej2 K HL R A S A S ˙ R ˙ S
40 12 30 19 39 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q S ˙ R ˙ S
41 20 4 atbase S A S Base K
42 19 41 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q S Base K
43 20 1 2 latjlej1 K Lat S Base K R ˙ S Base K T Base K S ˙ R ˙ S S ˙ T ˙ R ˙ S ˙ T
44 15 42 32 34 43 syl13anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q S ˙ R ˙ S S ˙ T ˙ R ˙ S ˙ T
45 40 44 mpd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q S ˙ T ˙ R ˙ S ˙ T
46 20 2 4 hlatjcl K HL S A T A S ˙ T Base K
47 12 19 23 46 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q S ˙ T Base K
48 20 1 3 latleeqm1 K Lat S ˙ T Base K R ˙ S ˙ T Base K S ˙ T ˙ R ˙ S ˙ T S ˙ T ˙ R ˙ S ˙ T = S ˙ T
49 15 47 36 48 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q S ˙ T ˙ R ˙ S ˙ T S ˙ T ˙ R ˙ S ˙ T = S ˙ T
50 45 49 mpbid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q S ˙ T ˙ R ˙ S ˙ T = S ˙ T
51 50 oveq1d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q S ˙ T ˙ R ˙ S ˙ T ˙ W = S ˙ T ˙ W
52 11 51 eqtr4id K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q V = S ˙ T ˙ R ˙ S ˙ T ˙ W
53 20 3 latm32 K OL S ˙ T Base K R ˙ S ˙ T Base K W Base K S ˙ T ˙ R ˙ S ˙ T ˙ W = S ˙ T ˙ W ˙ R ˙ S ˙ T
54 14 47 36 29 53 syl13anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q S ˙ T ˙ R ˙ S ˙ T ˙ W = S ˙ T ˙ W ˙ R ˙ S ˙ T
55 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
56 simp21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q S A ¬ S ˙ W
57 simp22 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q T A ¬ T ˙ W
58 simp31 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q P Q S T
59 simp32l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q
60 simp32r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ T ˙ P ˙ Q
61 1 2 3 4 5 6 7 8 cdleme16 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q S ˙ T ˙ W = F ˙ G ˙ W
62 55 56 57 58 59 60 61 syl132anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q S ˙ T ˙ W = F ˙ G ˙ W
63 62 oveq1d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q S ˙ T ˙ W ˙ R ˙ S ˙ T = F ˙ G ˙ W ˙ R ˙ S ˙ T
64 54 63 eqtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q S ˙ T ˙ R ˙ S ˙ T ˙ W = F ˙ G ˙ W ˙ R ˙ S ˙ T
65 52 64 eqtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q V = F ˙ G ˙ W ˙ R ˙ S ˙ T
66 simp23 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q R A ¬ R ˙ W
67 simp33 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q R ˙ P ˙ Q
68 1 2 3 4 5 6 7 8 9 10 11 cdleme20c K HL W H R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ S ˙ P ˙ Q R ˙ P ˙ Q D ˙ Y = R ˙ S ˙ T ˙ W
69 12 16 66 56 23 59 67 68 syl232anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q D ˙ Y = R ˙ S ˙ T ˙ W
70 20 3 latmcom K Lat R ˙ S ˙ T Base K W Base K R ˙ S ˙ T ˙ W = W ˙ R ˙ S ˙ T
71 15 36 29 70 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q R ˙ S ˙ T ˙ W = W ˙ R ˙ S ˙ T
72 69 71 eqtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q D ˙ Y = W ˙ R ˙ S ˙ T
73 72 oveq2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q F ˙ G ˙ D ˙ Y = F ˙ G ˙ W ˙ R ˙ S ˙ T
74 38 65 73 3eqtr4rd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W R A ¬ R ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q F ˙ G ˙ D ˙ Y = V