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 ⊢BaseK=BaseK
12 11 7 atbase ⊢P∈A→P∈BaseK
13 10 12 syl ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W→P∈BaseK
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∈BaseK
19 17 18 syl ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W→G⁡P∈BaseK
20 11 1 2 latlej1 ⊢K∈Lat∧P∈BaseK∧G⁡P∈BaseK→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∈BaseK
23 8 10 17 22 syl3anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W→P∨˙G⁡P∈BaseK
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∈BaseK→F⁡G⁡P∈BaseK
26 14 24 19 25 syl3anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W→F⁡G⁡P∈BaseK
27 11 1 2 latjlej1 ⊢K∈Lat∧P∈BaseK∧P∨˙G⁡P∈BaseK∧F⁡G⁡P∈BaseK→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∈BaseK∧F⁡G⁡P∈BaseK→P∨˙F⁡G⁡P∈BaseK
31 9 13 26 30 syl3anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W→P∨˙F⁡G⁡P∈BaseK
32 11 2 latjcl ⊢K∈Lat∧P∨˙G⁡P∈BaseK∧F⁡G⁡P∈BaseK→P∨˙G⁡P∨˙F⁡G⁡P∈BaseK
33 9 23 26 32 syl3anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W→P∨˙G⁡P∨˙F⁡G⁡P∈BaseK
34 simp1r ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W→W∈H
35 11 3 lhpbase ⊢W∈H→W∈BaseK
36 34 35 syl ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W→W∈BaseK
37 11 1 6 latmlem1 ⊢K∈Lat∧P∨˙F⁡G⁡P∈BaseK∧P∨˙G⁡P∨˙F⁡G⁡P∈BaseK∧W∈BaseK→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∈BaseK
59 8 17 57 58 syl3anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W→G⁡P∨˙F⁡G⁡P∈BaseK
60 11 6 latmcl ⊢K∈Lat∧G⁡P∨˙F⁡G⁡P∈BaseK∧W∈BaseK→G⁡P∨˙F⁡G⁡P∧˙W∈BaseK
61 9 59 36 60 syl3anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W→G⁡P∨˙F⁡G⁡P∧˙W∈BaseK
62 11 6 latmcl ⊢K∈Lat∧P∨˙G⁡P∈BaseK∧W∈BaseK→P∨˙G⁡P∧˙W∈BaseK
63 9 23 36 62 syl3anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W→P∨˙G⁡P∧˙W∈BaseK
64 11 2 latjcom ⊢K∈Lat∧G⁡P∨˙F⁡G⁡P∧˙W∈BaseK∧P∨˙G⁡P∧˙W∈BaseK→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∈BaseK∧F⁡G⁡P∈BaseK→G⁡P∨˙F⁡G⁡P∈BaseK
67 9 19 26 66 syl3anc ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A∧¬P≤˙W→G⁡P∨˙F⁡G⁡P∈BaseK
68 11 1 6 latmle2 ⊢K∈Lat∧P∨˙G⁡P∈BaseK∧W∈BaseK→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∈BaseK∧G⁡P∨˙F⁡G⁡P∈BaseK∧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∈BaseK∧G⁡P∈BaseK∧F⁡G⁡P∈BaseK→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∈BaseK∧G⁡P∈BaseK→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∈BaseK∧G⁡P∈BaseK∧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∈BaseK→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