Metamath Proof Explorer

Theorem trlcolem

Description: Lemma for trlco . (Contributed by NM, 1-Jun-2013)

Ref Expression
Hypotheses trlco.l ⊢ ≤ ˙ = ≤ K
trlco.j ⊢ ∨ ˙ = join ⁡ K
trlco.h ⊢ H = LHyp ⁡ K
trlco.t ⊢ T = LTrn ⁡ K ⁡ W
trlco.r ⊢ R = trL ⁡ K ⁡ W
trlcolem.m ⊢ ∧ ˙ = meet ⁡ K
trlcolem.a ⊢ A = Atoms ⁡ K
Assertion trlcolem ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → R ⁡ F ∘ G ≤ ˙ R ⁡ F ∨ ˙ R ⁡ G

Proof

Step Hyp Ref Expression
1 trlco.l ⊢ ≤ ˙ = ≤ K
2 trlco.j ⊢ ∨ ˙ = join ⁡ K
3 trlco.h ⊢ H = LHyp ⁡ K
4 trlco.t ⊢ T = LTrn ⁡ K ⁡ W
5 trlco.r ⊢ R = trL ⁡ K ⁡ W
6 trlcolem.m ⊢ ∧ ˙ = meet ⁡ K
7 trlcolem.a ⊢ A = Atoms ⁡ K
8 simp1l ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → K ∈ HL
9 8 hllatd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → K ∈ Lat
10 simp3l ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∈ A
11 eqid ⊢ Base K = Base K
12 11 7 atbase ⊢ P ∈ A → P ∈ Base K
13 10 12 syl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∈ Base K
14 simp1 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → K ∈ HL ∧ W ∈ H
15 simp2r ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → G ∈ T
16 1 7 3 4 ltrnat ⊢ K ∈ HL ∧ W ∈ H ∧ G ∈ T ∧ P ∈ A → G ⁡ P ∈ A
17 14 15 10 16 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → G ⁡ P ∈ A
18 11 7 atbase ⊢ G ⁡ P ∈ A → G ⁡ P ∈ Base K
19 17 18 syl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → G ⁡ P ∈ Base K
20 11 1 2 latlej1 ⊢ K ∈ Lat ∧ P ∈ Base K ∧ G ⁡ P ∈ Base K → P ≤ ˙ P ∨ ˙ G ⁡ P
21 9 13 19 20 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ≤ ˙ P ∨ ˙ G ⁡ P
22 11 2 7 hlatjcl ⊢ K ∈ HL ∧ P ∈ A ∧ G ⁡ P ∈ A → P ∨ ˙ G ⁡ P ∈ Base K
23 8 10 17 22 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ G ⁡ P ∈ Base K
24 simp2l ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → F ∈ T
25 11 3 4 ltrncl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ⁡ P ∈ Base K → F ⁡ G ⁡ P ∈ Base K
26 14 24 19 25 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → F ⁡ G ⁡ P ∈ Base K
27 11 1 2 latjlej1 ⊢ K ∈ Lat ∧ P ∈ Base K ∧ P ∨ ˙ G ⁡ P ∈ Base K ∧ F ⁡ G ⁡ P ∈ Base K → P ≤ ˙ P ∨ ˙ G ⁡ P → P ∨ ˙ F ⁡ G ⁡ P ≤ ˙ P ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P
28 9 13 23 26 27 syl13anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ≤ ˙ P ∨ ˙ G ⁡ P → P ∨ ˙ F ⁡ G ⁡ P ≤ ˙ P ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P
29 21 28 mpd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ F ⁡ G ⁡ P ≤ ˙ P ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P
30 11 2 latjcl ⊢ K ∈ Lat ∧ P ∈ Base K ∧ F ⁡ G ⁡ P ∈ Base K → P ∨ ˙ F ⁡ G ⁡ P ∈ Base K
31 9 13 26 30 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ F ⁡ G ⁡ P ∈ Base K
32 11 2 latjcl ⊢ K ∈ Lat ∧ P ∨ ˙ G ⁡ P ∈ Base K ∧ F ⁡ G ⁡ P ∈ Base K → P ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∈ Base K
33 9 23 26 32 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∈ Base K
34 simp1r ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → W ∈ H
35 11 3 lhpbase ⊢ W ∈ H → W ∈ Base K
36 34 35 syl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → W ∈ Base K
37 11 1 6 latmlem1 ⊢ K ∈ Lat ∧ P ∨ ˙ F ⁡ G ⁡ P ∈ Base K ∧ P ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∈ Base K ∧ W ∈ Base K → P ∨ ˙ F ⁡ G ⁡ P ≤ ˙ P ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P → P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W ≤ ˙ P ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W
38 9 31 33 36 37 syl13anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ F ⁡ G ⁡ P ≤ ˙ P ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P → P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W ≤ ˙ P ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W
39 29 38 mpd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W ≤ ˙ P ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W
40 3 4 ltrnco ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T → F ∘ G ∈ T
41 14 24 15 40 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → F ∘ G ∈ T
42 1 2 6 7 3 4 5 trlval2 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∘ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → R ⁡ F ∘ G = P ∨ ˙ F ∘ G ⁡ P ∧ ˙ W
43 41 42 syld3an2 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → R ⁡ F ∘ G = P ∨ ˙ F ∘ G ⁡ P ∧ ˙ W
44 1 7 3 4 ltrncoval ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A → F ∘ G ⁡ P = F ⁡ G ⁡ P
45 44 3adant3r ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → F ∘ G ⁡ P = F ⁡ G ⁡ P
46 45 oveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ F ∘ G ⁡ P = P ∨ ˙ F ⁡ G ⁡ P
47 46 oveq1d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ F ∘ G ⁡ P ∧ ˙ W = P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W
48 43 47 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → R ⁡ F ∘ G = P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W
49 1 7 3 4 ltrnel ⊢ K ∈ HL ∧ W ∈ H ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → G ⁡ P ∈ A ∧ ¬ G ⁡ P ≤ ˙ W
50 15 49 syld3an2 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → G ⁡ P ∈ A ∧ ¬ G ⁡ P ≤ ˙ W
51 1 2 6 7 3 4 5 trlval2 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ⁡ P ∈ A ∧ ¬ G ⁡ P ≤ ˙ W → R ⁡ F = G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W
52 14 24 50 51 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → R ⁡ F = G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W
53 1 2 6 7 3 4 5 trlval2 ⊢ K ∈ HL ∧ W ∈ H ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → R ⁡ G = P ∨ ˙ G ⁡ P ∧ ˙ W
54 15 53 syld3an2 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → R ⁡ G = P ∨ ˙ G ⁡ P ∧ ˙ W
55 52 54 oveq12d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → R ⁡ F ∨ ˙ R ⁡ G = G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W ∨ ˙ P ∨ ˙ G ⁡ P ∧ ˙ W
56 1 7 3 4 ltrnat ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ⁡ P ∈ A → F ⁡ G ⁡ P ∈ A
57 14 24 17 56 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → F ⁡ G ⁡ P ∈ A
58 11 2 7 hlatjcl ⊢ K ∈ HL ∧ G ⁡ P ∈ A ∧ F ⁡ G ⁡ P ∈ A → G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∈ Base K
59 8 17 57 58 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∈ Base K
60 11 6 latmcl ⊢ K ∈ Lat ∧ G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∈ Base K ∧ W ∈ Base K → G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W ∈ Base K
61 9 59 36 60 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W ∈ Base K
62 11 6 latmcl ⊢ K ∈ Lat ∧ P ∨ ˙ G ⁡ P ∈ Base K ∧ W ∈ Base K → P ∨ ˙ G ⁡ P ∧ ˙ W ∈ Base K
63 9 23 36 62 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ G ⁡ P ∧ ˙ W ∈ Base K
64 11 2 latjcom ⊢ K ∈ Lat ∧ G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W ∈ Base K ∧ P ∨ ˙ G ⁡ P ∧ ˙ W ∈ Base K → G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W ∨ ˙ P ∨ ˙ G ⁡ P ∧ ˙ W = P ∨ ˙ G ⁡ P ∧ ˙ W ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W
65 9 61 63 64 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W ∨ ˙ P ∨ ˙ G ⁡ P ∧ ˙ W = P ∨ ˙ G ⁡ P ∧ ˙ W ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W
66 11 2 latjcl ⊢ K ∈ Lat ∧ G ⁡ P ∈ Base K ∧ F ⁡ G ⁡ P ∈ Base K → G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∈ Base K
67 9 19 26 66 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∈ Base K
68 11 1 6 latmle2 ⊢ K ∈ Lat ∧ P ∨ ˙ G ⁡ P ∈ Base K ∧ W ∈ Base K → P ∨ ˙ G ⁡ P ∧ ˙ W ≤ ˙ W
69 9 23 36 68 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ G ⁡ P ∧ ˙ W ≤ ˙ W
70 11 1 2 6 3 lhpmod6i1 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∨ ˙ G ⁡ P ∧ ˙ W ∈ Base K ∧ G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∈ Base K ∧ P ∨ ˙ G ⁡ P ∧ ˙ W ≤ ˙ W → P ∨ ˙ G ⁡ P ∧ ˙ W ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W = P ∨ ˙ G ⁡ P ∧ ˙ W ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W
71 14 63 67 69 70 syl121anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ G ⁡ P ∧ ˙ W ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W = P ∨ ˙ G ⁡ P ∧ ˙ W ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W
72 11 2 latjass ⊢ K ∈ Lat ∧ P ∨ ˙ G ⁡ P ∧ ˙ W ∈ Base K ∧ G ⁡ P ∈ Base K ∧ F ⁡ G ⁡ P ∈ Base K → P ∨ ˙ G ⁡ P ∧ ˙ W ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P = P ∨ ˙ G ⁡ P ∧ ˙ W ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P
73 9 63 19 26 72 syl13anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ G ⁡ P ∧ ˙ W ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P = P ∨ ˙ G ⁡ P ∧ ˙ W ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P
74 11 1 2 latlej2 ⊢ K ∈ Lat ∧ P ∈ Base K ∧ G ⁡ P ∈ Base K → G ⁡ P ≤ ˙ P ∨ ˙ G ⁡ P
75 9 13 19 74 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → G ⁡ P ≤ ˙ P ∨ ˙ G ⁡ P
76 11 1 2 6 3 lhpmod2i2 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∨ ˙ G ⁡ P ∈ Base K ∧ G ⁡ P ∈ Base K ∧ G ⁡ P ≤ ˙ P ∨ ˙ G ⁡ P → P ∨ ˙ G ⁡ P ∧ ˙ W ∨ ˙ G ⁡ P = P ∨ ˙ G ⁡ P ∧ ˙ W ∨ ˙ G ⁡ P
77 14 23 19 75 76 syl121anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ G ⁡ P ∧ ˙ W ∨ ˙ G ⁡ P = P ∨ ˙ G ⁡ P ∧ ˙ W ∨ ˙ G ⁡ P
78 eqid ⊢ 1. ⁡ K = 1. ⁡ K
79 1 2 78 7 3 lhpjat1 ⊢ K ∈ HL ∧ W ∈ H ∧ G ⁡ P ∈ A ∧ ¬ G ⁡ P ≤ ˙ W → W ∨ ˙ G ⁡ P = 1. ⁡ K
80 14 50 79 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → W ∨ ˙ G ⁡ P = 1. ⁡ K
81 80 oveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ G ⁡ P ∧ ˙ W ∨ ˙ G ⁡ P = P ∨ ˙ G ⁡ P ∧ ˙ 1. ⁡ K
82 hlol ⊢ K ∈ HL → K ∈ OL
83 8 82 syl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → K ∈ OL
84 11 6 78 olm11 ⊢ K ∈ OL ∧ P ∨ ˙ G ⁡ P ∈ Base K → P ∨ ˙ G ⁡ P ∧ ˙ 1. ⁡ K = P ∨ ˙ G ⁡ P
85 83 23 84 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ G ⁡ P ∧ ˙ 1. ⁡ K = P ∨ ˙ G ⁡ P
86 77 81 85 3eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ G ⁡ P ∧ ˙ W ∨ ˙ G ⁡ P = P ∨ ˙ G ⁡ P
87 86 oveq1d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ G ⁡ P ∧ ˙ W ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P = P ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P
88 73 87 eqtr3d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ G ⁡ P ∧ ˙ W ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P = P ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P
89 88 oveq1d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ G ⁡ P ∧ ˙ W ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W = P ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W
90 71 89 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ G ⁡ P ∧ ˙ W ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W = P ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W
91 55 65 90 3eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → R ⁡ F ∨ ˙ R ⁡ G = P ∨ ˙ G ⁡ P ∨ ˙ F ⁡ G ⁡ P ∧ ˙ W
92 39 48 91 3brtr4d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → R ⁡ F ∘ G ≤ ˙ R ⁡ F ∨ ˙ R ⁡ G