Metamath Proof Explorer


Theorem cdleme20j

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

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 simp33 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T ¬ R ˙ S ˙ T
13 simp11l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T K HL
14 simp22l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T S A
15 simp21l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T R A
16 eqid Base K = Base K
17 16 2 4 hlatjcl K HL R A S A R ˙ S Base K
18 13 15 14 17 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T R ˙ S Base K
19 simp11r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T W H
20 16 5 lhpbase W H W Base K
21 19 20 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T W Base K
22 1 2 4 hlatlej2 K HL R A S A S ˙ R ˙ S
23 13 15 14 22 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T S ˙ R ˙ S
24 16 1 2 3 4 atmod2i1 K HL S A R ˙ S Base K W Base K S ˙ R ˙ S R ˙ S ˙ W ˙ S = R ˙ S ˙ W ˙ S
25 13 14 18 21 23 24 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T R ˙ S ˙ W ˙ S = R ˙ S ˙ W ˙ S
26 simp22 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T S A ¬ S ˙ W
27 eqid 1. K = 1. K
28 1 2 27 4 5 lhpjat1 K HL W H S A ¬ S ˙ W W ˙ S = 1. K
29 13 19 26 28 syl21anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T W ˙ S = 1. K
30 29 oveq2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T R ˙ S ˙ W ˙ S = R ˙ S ˙ 1. K
31 hlol K HL K OL
32 13 31 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T K OL
33 16 3 27 olm11 K OL R ˙ S Base K R ˙ S ˙ 1. K = R ˙ S
34 32 18 33 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T R ˙ S ˙ 1. K = R ˙ S
35 25 30 34 3eqtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T R ˙ S ˙ W ˙ S = R ˙ S
36 35 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T D = Y R ˙ S ˙ W ˙ S = R ˙ S
37 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
38 simp23 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T T A ¬ T ˙ W
39 simp21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T R A ¬ R ˙ W
40 simp31 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T P Q S T
41 simp321 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T ¬ S ˙ P ˙ Q
42 simp322 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T ¬ T ˙ P ˙ Q
43 41 42 jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q
44 simp323 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T R ˙ P ˙ Q
45 1 2 3 4 5 6 7 8 9 10 11 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
46 37 26 38 39 40 43 44 45 syl133anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T F ˙ G ˙ D ˙ Y = V
47 13 hllatd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T K Lat
48 simp12l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T P A
49 simp13l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T Q A
50 1 2 3 4 5 6 7 16 cdleme1b K HL W H P A Q A S A F Base K
51 13 19 48 49 14 50 syl23anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T F Base K
52 simp23l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T T A
53 1 2 3 4 5 6 8 16 cdleme1b K HL W H P A Q A T A G Base K
54 13 19 48 49 52 53 syl23anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T G Base K
55 16 2 latjcl K Lat F Base K G Base K F ˙ G Base K
56 47 51 54 55 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T F ˙ G Base K
57 simp22r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T ¬ S ˙ W
58 1 2 3 4 5 9 cdlemeda K HL W H S A ¬ S ˙ W R A R ˙ P ˙ Q ¬ S ˙ P ˙ Q D A
59 13 19 14 57 15 44 41 58 syl223anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T D A
60 simp23r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T ¬ T ˙ W
61 1 2 3 4 5 10 cdlemeda K HL W H T A ¬ T ˙ W R A R ˙ P ˙ Q ¬ T ˙ P ˙ Q Y A
62 13 19 52 60 15 44 42 61 syl223anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T Y A
63 16 2 4 hlatjcl K HL D A Y A D ˙ Y Base K
64 13 59 62 63 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T D ˙ Y Base K
65 16 1 3 latmle2 K Lat F ˙ G Base K D ˙ Y Base K F ˙ G ˙ D ˙ Y ˙ D ˙ Y
66 47 56 64 65 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T F ˙ G ˙ D ˙ Y ˙ D ˙ Y
67 46 66 eqbrtrrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T V ˙ D ˙ Y
68 67 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T D = Y V ˙ D ˙ Y
69 2 4 hlatjidm K HL D A D ˙ D = D
70 13 59 69 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T D ˙ D = D
71 oveq2 D = Y D ˙ D = D ˙ Y
72 70 71 sylan9req K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T D = Y D = D ˙ Y
73 68 72 breqtrrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T D = Y V ˙ D
74 hlatl K HL K AtLat
75 13 74 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T K AtLat
76 simp31r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T S T
77 1 2 3 4 5 11 lhpat2 K HL W H S A ¬ S ˙ W T A S T V A
78 13 19 14 57 52 76 77 syl222anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T V A
79 1 4 atcmp K AtLat V A D A V ˙ D V = D
80 75 78 59 79 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T V ˙ D V = D
81 80 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T D = Y V ˙ D V = D
82 73 81 mpbid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T D = Y V = D
83 82 11 eqtr3di K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T D = Y D = S ˙ T ˙ W
84 9 83 eqtr3id K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T D = Y R ˙ S ˙ W = S ˙ T ˙ W
85 16 2 4 hlatjcl K HL S A T A S ˙ T Base K
86 13 14 52 85 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T S ˙ T Base K
87 16 1 3 latmle1 K Lat S ˙ T Base K W Base K S ˙ T ˙ W ˙ S ˙ T
88 47 86 21 87 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T S ˙ T ˙ W ˙ S ˙ T
89 88 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T D = Y S ˙ T ˙ W ˙ S ˙ T
90 84 89 eqbrtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T D = Y R ˙ S ˙ W ˙ S ˙ T
91 1 2 4 hlatlej1 K HL S A T A S ˙ S ˙ T
92 13 14 52 91 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T S ˙ S ˙ T
93 92 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T D = Y S ˙ S ˙ T
94 16 3 latmcl K Lat R ˙ S Base K W Base K R ˙ S ˙ W Base K
95 47 18 21 94 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T R ˙ S ˙ W Base K
96 16 4 atbase S A S Base K
97 14 96 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T S Base K
98 16 1 2 latjle12 K Lat R ˙ S ˙ W Base K S Base K S ˙ T Base K R ˙ S ˙ W ˙ S ˙ T S ˙ S ˙ T R ˙ S ˙ W ˙ S ˙ S ˙ T
99 47 95 97 86 98 syl13anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T R ˙ S ˙ W ˙ S ˙ T S ˙ S ˙ T R ˙ S ˙ W ˙ S ˙ S ˙ T
100 99 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T D = Y R ˙ S ˙ W ˙ S ˙ T S ˙ S ˙ T R ˙ S ˙ W ˙ S ˙ S ˙ T
101 90 93 100 mpbi2and K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T D = Y R ˙ S ˙ W ˙ S ˙ S ˙ T
102 36 101 eqbrtrrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T D = Y R ˙ S ˙ S ˙ T
103 16 4 atbase R A R Base K
104 15 103 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T R Base K
105 16 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
106 47 104 97 86 105 syl13anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T R ˙ S ˙ T S ˙ S ˙ T R ˙ S ˙ S ˙ T
107 106 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T D = Y R ˙ S ˙ T S ˙ S ˙ T R ˙ S ˙ S ˙ T
108 102 107 mpbird K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T D = Y R ˙ S ˙ T S ˙ S ˙ T
109 108 simpld K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T D = Y R ˙ S ˙ T
110 109 ex K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T D = Y R ˙ S ˙ T
111 110 necon3bd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T ¬ R ˙ S ˙ T D Y
112 12 111 mpd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ R ˙ S ˙ T D Y