Metamath Proof Explorer

Theorem cdlemd2

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 29-May-2012)

Ref Expression
Hypotheses cdlemd2.l ⊢≤˙=≤K
cdlemd2.j ⊢∨˙=join⁡K
cdlemd2.a ⊢A=Atoms⁡K
cdlemd2.h ⊢H=LHyp⁡K
cdlemd2.t ⊢T=LTrn⁡K⁡W
Assertion cdlemd2 ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→F⁡R=G⁡R

Proof

Step Hyp Ref Expression
1 cdlemd2.l ⊢≤˙=≤K
2 cdlemd2.j ⊢∨˙=join⁡K
3 cdlemd2.a ⊢A=Atoms⁡K
4 cdlemd2.h ⊢H=LHyp⁡K
5 cdlemd2.t ⊢T=LTrn⁡K⁡W
6 simp3l ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→F⁡P=G⁡P
7 simp11 ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→K∈HL∧W∈H
8 simp12l ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→F∈T
9 simp11l ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→K∈HL
10 9 hllatd ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→K∈Lat
11 simp21l ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→P∈A
12 simp13 ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→R∈A
13 eqid ⊢BaseK=BaseK
14 13 2 3 hlatjcl ⊢K∈HL∧P∈A∧R∈A→P∨˙R∈BaseK
15 9 11 12 14 syl3anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→P∨˙R∈BaseK
16 simp11r ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→W∈H
17 13 4 lhpbase ⊢W∈H→W∈BaseK
18 16 17 syl ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→W∈BaseK
19 eqid ⊢meet⁡K=meet⁡K
20 13 19 latmcl ⊢K∈Lat∧P∨˙R∈BaseK∧W∈BaseK→P∨˙Rmeet⁡KW∈BaseK
21 10 15 18 20 syl3anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→P∨˙Rmeet⁡KW∈BaseK
22 13 1 19 latmle2 ⊢K∈Lat∧P∨˙R∈BaseK∧W∈BaseK→P∨˙Rmeet⁡KW≤˙W
23 10 15 18 22 syl3anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→P∨˙Rmeet⁡KW≤˙W
24 13 1 4 5 ltrnval1 ⊢K∈HL∧W∈H∧F∈T∧P∨˙Rmeet⁡KW∈BaseK∧P∨˙Rmeet⁡KW≤˙W→F⁡P∨˙Rmeet⁡KW=P∨˙Rmeet⁡KW
25 7 8 21 23 24 syl112anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→F⁡P∨˙Rmeet⁡KW=P∨˙Rmeet⁡KW
26 simp12r ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→G∈T
27 13 1 4 5 ltrnval1 ⊢K∈HL∧W∈H∧G∈T∧P∨˙Rmeet⁡KW∈BaseK∧P∨˙Rmeet⁡KW≤˙W→G⁡P∨˙Rmeet⁡KW=P∨˙Rmeet⁡KW
28 7 26 21 23 27 syl112anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→G⁡P∨˙Rmeet⁡KW=P∨˙Rmeet⁡KW
29 25 28 eqtr4d ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→F⁡P∨˙Rmeet⁡KW=G⁡P∨˙Rmeet⁡KW
30 6 29 oveq12d ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→F⁡P∨˙F⁡P∨˙Rmeet⁡KW=G⁡P∨˙G⁡P∨˙Rmeet⁡KW
31 13 3 atbase ⊢P∈A→P∈BaseK
32 11 31 syl ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→P∈BaseK
33 13 2 4 5 ltrnj ⊢K∈HL∧W∈H∧F∈T∧P∈BaseK∧P∨˙Rmeet⁡KW∈BaseK→F⁡P∨˙P∨˙Rmeet⁡KW=F⁡P∨˙F⁡P∨˙Rmeet⁡KW
34 7 8 32 21 33 syl112anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→F⁡P∨˙P∨˙Rmeet⁡KW=F⁡P∨˙F⁡P∨˙Rmeet⁡KW
35 13 2 4 5 ltrnj ⊢K∈HL∧W∈H∧G∈T∧P∈BaseK∧P∨˙Rmeet⁡KW∈BaseK→G⁡P∨˙P∨˙Rmeet⁡KW=G⁡P∨˙G⁡P∨˙Rmeet⁡KW
36 7 26 32 21 35 syl112anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→G⁡P∨˙P∨˙Rmeet⁡KW=G⁡P∨˙G⁡P∨˙Rmeet⁡KW
37 30 34 36 3eqtr4d ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→F⁡P∨˙P∨˙Rmeet⁡KW=G⁡P∨˙P∨˙Rmeet⁡KW
38 simp3r ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→F⁡Q=G⁡Q
39 simp22l ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→Q∈A
40 13 2 3 hlatjcl ⊢K∈HL∧Q∈A∧R∈A→Q∨˙R∈BaseK
41 9 39 12 40 syl3anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→Q∨˙R∈BaseK
42 13 19 latmcl ⊢K∈Lat∧Q∨˙R∈BaseK∧W∈BaseK→Q∨˙Rmeet⁡KW∈BaseK
43 10 41 18 42 syl3anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→Q∨˙Rmeet⁡KW∈BaseK
44 13 1 19 latmle2 ⊢K∈Lat∧Q∨˙R∈BaseK∧W∈BaseK→Q∨˙Rmeet⁡KW≤˙W
45 10 41 18 44 syl3anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→Q∨˙Rmeet⁡KW≤˙W
46 13 1 4 5 ltrnval1 ⊢K∈HL∧W∈H∧F∈T∧Q∨˙Rmeet⁡KW∈BaseK∧Q∨˙Rmeet⁡KW≤˙W→F⁡Q∨˙Rmeet⁡KW=Q∨˙Rmeet⁡KW
47 7 8 43 45 46 syl112anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→F⁡Q∨˙Rmeet⁡KW=Q∨˙Rmeet⁡KW
48 13 1 4 5 ltrnval1 ⊢K∈HL∧W∈H∧G∈T∧Q∨˙Rmeet⁡KW∈BaseK∧Q∨˙Rmeet⁡KW≤˙W→G⁡Q∨˙Rmeet⁡KW=Q∨˙Rmeet⁡KW
49 7 26 43 45 48 syl112anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→G⁡Q∨˙Rmeet⁡KW=Q∨˙Rmeet⁡KW
50 47 49 eqtr4d ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→F⁡Q∨˙Rmeet⁡KW=G⁡Q∨˙Rmeet⁡KW
51 38 50 oveq12d ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→F⁡Q∨˙F⁡Q∨˙Rmeet⁡KW=G⁡Q∨˙G⁡Q∨˙Rmeet⁡KW
52 13 3 atbase ⊢Q∈A→Q∈BaseK
53 39 52 syl ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→Q∈BaseK
54 13 2 4 5 ltrnj ⊢K∈HL∧W∈H∧F∈T∧Q∈BaseK∧Q∨˙Rmeet⁡KW∈BaseK→F⁡Q∨˙Q∨˙Rmeet⁡KW=F⁡Q∨˙F⁡Q∨˙Rmeet⁡KW
55 7 8 53 43 54 syl112anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→F⁡Q∨˙Q∨˙Rmeet⁡KW=F⁡Q∨˙F⁡Q∨˙Rmeet⁡KW
56 13 2 4 5 ltrnj ⊢K∈HL∧W∈H∧G∈T∧Q∈BaseK∧Q∨˙Rmeet⁡KW∈BaseK→G⁡Q∨˙Q∨˙Rmeet⁡KW=G⁡Q∨˙G⁡Q∨˙Rmeet⁡KW
57 7 26 53 43 56 syl112anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→G⁡Q∨˙Q∨˙Rmeet⁡KW=G⁡Q∨˙G⁡Q∨˙Rmeet⁡KW
58 51 55 57 3eqtr4d ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→F⁡Q∨˙Q∨˙Rmeet⁡KW=G⁡Q∨˙Q∨˙Rmeet⁡KW
59 37 58 oveq12d ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→F⁡P∨˙P∨˙Rmeet⁡KWmeet⁡KF⁡Q∨˙Q∨˙Rmeet⁡KW=G⁡P∨˙P∨˙Rmeet⁡KWmeet⁡KG⁡Q∨˙Q∨˙Rmeet⁡KW
60 13 2 latjcl ⊢K∈Lat∧P∈BaseK∧P∨˙Rmeet⁡KW∈BaseK→P∨˙P∨˙Rmeet⁡KW∈BaseK
61 10 32 21 60 syl3anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→P∨˙P∨˙Rmeet⁡KW∈BaseK
62 13 2 latjcl ⊢K∈Lat∧Q∈BaseK∧Q∨˙Rmeet⁡KW∈BaseK→Q∨˙Q∨˙Rmeet⁡KW∈BaseK
63 10 53 43 62 syl3anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→Q∨˙Q∨˙Rmeet⁡KW∈BaseK
64 13 19 4 5 ltrnm ⊢K∈HL∧W∈H∧F∈T∧P∨˙P∨˙Rmeet⁡KW∈BaseK∧Q∨˙Q∨˙Rmeet⁡KW∈BaseK→F⁡P∨˙P∨˙Rmeet⁡KWmeet⁡KQ∨˙Q∨˙Rmeet⁡KW=F⁡P∨˙P∨˙Rmeet⁡KWmeet⁡KF⁡Q∨˙Q∨˙Rmeet⁡KW
65 7 8 61 63 64 syl112anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→F⁡P∨˙P∨˙Rmeet⁡KWmeet⁡KQ∨˙Q∨˙Rmeet⁡KW=F⁡P∨˙P∨˙Rmeet⁡KWmeet⁡KF⁡Q∨˙Q∨˙Rmeet⁡KW
66 13 19 4 5 ltrnm ⊢K∈HL∧W∈H∧G∈T∧P∨˙P∨˙Rmeet⁡KW∈BaseK∧Q∨˙Q∨˙Rmeet⁡KW∈BaseK→G⁡P∨˙P∨˙Rmeet⁡KWmeet⁡KQ∨˙Q∨˙Rmeet⁡KW=G⁡P∨˙P∨˙Rmeet⁡KWmeet⁡KG⁡Q∨˙Q∨˙Rmeet⁡KW
67 7 26 61 63 66 syl112anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→G⁡P∨˙P∨˙Rmeet⁡KWmeet⁡KQ∨˙Q∨˙Rmeet⁡KW=G⁡P∨˙P∨˙Rmeet⁡KWmeet⁡KG⁡Q∨˙Q∨˙Rmeet⁡KW
68 59 65 67 3eqtr4d ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→F⁡P∨˙P∨˙Rmeet⁡KWmeet⁡KQ∨˙Q∨˙Rmeet⁡KW=G⁡P∨˙P∨˙Rmeet⁡KWmeet⁡KQ∨˙Q∨˙Rmeet⁡KW
69 simp21 ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→P∈A∧¬P≤˙W
70 simp22 ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→Q∈A∧¬Q≤˙W
71 simp23l ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→P≠Q
72 simp23r ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→¬R≤˙P∨˙Q
73 12 71 72 3jca ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→R∈A∧P≠Q∧¬R≤˙P∨˙Q
74 1 2 19 3 4 cdlemd1 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧R∈A∧P≠Q∧¬R≤˙P∨˙Q→R=P∨˙P∨˙Rmeet⁡KWmeet⁡KQ∨˙Q∨˙Rmeet⁡KW
75 7 69 70 73 74 syl13anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→R=P∨˙P∨˙Rmeet⁡KWmeet⁡KQ∨˙Q∨˙Rmeet⁡KW
76 75 fveq2d ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→F⁡R=F⁡P∨˙P∨˙Rmeet⁡KWmeet⁡KQ∨˙Q∨˙Rmeet⁡KW
77 75 fveq2d ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→G⁡R=G⁡P∨˙P∨˙Rmeet⁡KWmeet⁡KQ∨˙Q∨˙Rmeet⁡KW
78 68 76 77 3eqtr4d ⊢K∈HL∧W∈H∧F∈T∧G∈T∧R∈A∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R≤˙P∨˙Q∧F⁡P=G⁡P∧F⁡Q=G⁡Q→F⁡R=G⁡R