Metamath Proof Explorer


Theorem dihglblem2N

Description: The GLB of a set of lattice elements S is the same as that of the set T with elements of S cut down to be under W . (Contributed by NM, 19-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihglblem.b B=BaseK
dihglblem.l ˙=K
dihglblem.m ˙=meetK
dihglblem.g G=glbK
dihglblem.h H=LHypK
dihglblem.t T=uB|vSu=v˙W
Assertion dihglblem2N KHLWHSBGS˙WGS=GT

Proof

Step Hyp Ref Expression
1 dihglblem.b B=BaseK
2 dihglblem.l ˙=K
3 dihglblem.m ˙=meetK
4 dihglblem.g G=glbK
5 dihglblem.h H=LHypK
6 dihglblem.t T=uB|vSu=v˙W
7 simpl1l KHLWHSBGS˙WxSKHL
8 7 hllatd KHLWHSBGS˙WxSKLat
9 simp1l KHLWHSBGS˙WKHL
10 hlclat KHLKCLat
11 9 10 syl KHLWHSBGS˙WKCLat
12 ssrab2 uB|vSu=v˙WB
13 6 12 eqsstri TB
14 1 4 clatglbcl KCLatTBGTB
15 11 13 14 sylancl KHLWHSBGS˙WGTB
16 15 adantr KHLWHSBGS˙WxSGTB
17 simpl2 KHLWHSBGS˙WxSSB
18 simpr KHLWHSBGS˙WxSxS
19 17 18 sseldd KHLWHSBGS˙WxSxB
20 simpl1r KHLWHSBGS˙WxSWH
21 1 5 lhpbase WHWB
22 20 21 syl KHLWHSBGS˙WxSWB
23 1 3 latmcl KLatxBWBx˙WB
24 8 19 22 23 syl3anc KHLWHSBGS˙WxSx˙WB
25 7 10 syl KHLWHSBGS˙WxSKCLat
26 eqidd KHLWHSBGS˙WxSx˙W=x˙W
27 oveq1 v=xv˙W=x˙W
28 27 rspceeqv xSx˙W=x˙WvSx˙W=v˙W
29 18 26 28 syl2anc KHLWHSBGS˙WxSvSx˙W=v˙W
30 eqeq1 u=x˙Wu=v˙Wx˙W=v˙W
31 30 rexbidv u=x˙WvSu=v˙WvSx˙W=v˙W
32 31 elrab x˙WuB|vSu=v˙Wx˙WBvSx˙W=v˙W
33 24 29 32 sylanbrc KHLWHSBGS˙WxSx˙WuB|vSu=v˙W
34 33 6 eleqtrrdi KHLWHSBGS˙WxSx˙WT
35 1 2 4 clatglble KCLatTBx˙WTGT˙x˙W
36 13 35 mp3an2 KCLatx˙WTGT˙x˙W
37 25 34 36 syl2anc KHLWHSBGS˙WxSGT˙x˙W
38 1 2 3 latmle1 KLatxBWBx˙W˙x
39 8 19 22 38 syl3anc KHLWHSBGS˙WxSx˙W˙x
40 1 2 8 16 24 19 37 39 lattrd KHLWHSBGS˙WxSGT˙x
41 eqeq1 u=wu=v˙Ww=v˙W
42 41 rexbidv u=wvSu=v˙WvSw=v˙W
43 oveq1 v=yv˙W=y˙W
44 43 eqeq2d v=yw=v˙Ww=y˙W
45 44 cbvrexvw vSw=v˙WySw=y˙W
46 42 45 bitrdi u=wvSu=v˙WySw=y˙W
47 46 6 elrab2 wTwBySw=y˙W
48 simp3 KHLWHSBGS˙WzBxSz˙xwBySyS
49 simp13 KHLWHSBGS˙WzBxSz˙xwBySxSz˙x
50 breq2 x=yz˙xz˙y
51 50 rspcva ySxSz˙xz˙y
52 48 49 51 syl2anc KHLWHSBGS˙WzBxSz˙xwBySz˙y
53 simp11l KHLWHSBGS˙WzBxSz˙xKHL
54 53 3ad2ant1 KHLWHSBGS˙WzBxSz˙xwBySKHL
55 54 hllatd KHLWHSBGS˙WzBxSz˙xwBySKLat
56 simp12 KHLWHSBGS˙WzBxSz˙xwBySzB
57 54 10 syl KHLWHSBGS˙WzBxSz˙xwBySKCLat
58 simp112 KHLWHSBGS˙WzBxSz˙xwBySSB
59 1 4 clatglbcl KCLatSBGSB
60 57 58 59 syl2anc KHLWHSBGS˙WzBxSz˙xwBySGSB
61 simp11r KHLWHSBGS˙WzBxSz˙xWH
62 61 3ad2ant1 KHLWHSBGS˙WzBxSz˙xwBySWH
63 62 21 syl KHLWHSBGS˙WzBxSz˙xwBySWB
64 1 2 4 clatleglb KCLatzBSBz˙GSxSz˙x
65 57 56 58 64 syl3anc KHLWHSBGS˙WzBxSz˙xwBySz˙GSxSz˙x
66 49 65 mpbird KHLWHSBGS˙WzBxSz˙xwBySz˙GS
67 simp113 KHLWHSBGS˙WzBxSz˙xwBySGS˙W
68 1 2 55 56 60 63 66 67 lattrd KHLWHSBGS˙WzBxSz˙xwBySz˙W
69 58 48 sseldd KHLWHSBGS˙WzBxSz˙xwBySyB
70 1 2 3 latlem12 KLatzByBWBz˙yz˙Wz˙y˙W
71 55 56 69 63 70 syl13anc KHLWHSBGS˙WzBxSz˙xwBySz˙yz˙Wz˙y˙W
72 52 68 71 mpbi2and KHLWHSBGS˙WzBxSz˙xwBySz˙y˙W
73 72 3expia KHLWHSBGS˙WzBxSz˙xwBySz˙y˙W
74 breq2 w=y˙Wz˙wz˙y˙W
75 74 biimprcd z˙y˙Ww=y˙Wz˙w
76 73 75 syl6 KHLWHSBGS˙WzBxSz˙xwBySw=y˙Wz˙w
77 76 rexlimdv KHLWHSBGS˙WzBxSz˙xwBySw=y˙Wz˙w
78 77 expimpd KHLWHSBGS˙WzBxSz˙xwBySw=y˙Wz˙w
79 47 78 syl5bi KHLWHSBGS˙WzBxSz˙xwTz˙w
80 79 ralrimiv KHLWHSBGS˙WzBxSz˙xwTz˙w
81 53 10 syl KHLWHSBGS˙WzBxSz˙xKCLat
82 simp2 KHLWHSBGS˙WzBxSz˙xzB
83 1 2 4 clatleglb KCLatzBTBz˙GTwTz˙w
84 13 83 mp3an3 KCLatzBz˙GTwTz˙w
85 81 82 84 syl2anc KHLWHSBGS˙WzBxSz˙xz˙GTwTz˙w
86 80 85 mpbird KHLWHSBGS˙WzBxSz˙xz˙GT
87 simp2 KHLWHSBGS˙WSB
88 1 2 4 40 86 11 87 15 isglbd KHLWHSBGS˙WGS=GT