Metamath Proof Explorer


Theorem dihglblem3N

Description: Isomorphism H of a lattice glb. (Contributed by NM, 20-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
dihglblem.i J=DIsoBKW
dihglblem.ih I=DIsoHKW
Assertion dihglblem3N KHLWHSBSGS˙WIGT=xTIx

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 dihglblem.i J=DIsoBKW
8 dihglblem.ih I=DIsoHKW
9 simp1 KHLWHSBSGS˙WKHLWH
10 simp11l KHLWHSBSGS˙WuBvSKHL
11 10 hllatd KHLWHSBSGS˙WuBvSKLat
12 simp12l KHLWHSBSGS˙WuBvSSB
13 simp3 KHLWHSBSGS˙WuBvSvS
14 12 13 sseldd KHLWHSBSGS˙WuBvSvB
15 simp11r KHLWHSBSGS˙WuBvSWH
16 1 5 lhpbase WHWB
17 15 16 syl KHLWHSBSGS˙WuBvSWB
18 1 2 3 latmle2 KLatvBWBv˙W˙W
19 11 14 17 18 syl3anc KHLWHSBSGS˙WuBvSv˙W˙W
20 19 3expia KHLWHSBSGS˙WuBvSv˙W˙W
21 breq1 u=v˙Wu˙Wv˙W˙W
22 21 biimprcd v˙W˙Wu=v˙Wu˙W
23 20 22 syl6 KHLWHSBSGS˙WuBvSu=v˙Wu˙W
24 23 rexlimdv KHLWHSBSGS˙WuBvSu=v˙Wu˙W
25 24 ss2rabdv KHLWHSBSGS˙WuB|vSu=v˙WuB|u˙W
26 6 25 eqsstrid KHLWHSBSGS˙WTuB|u˙W
27 1 2 5 7 dibdmN KHLWHdomJ=uB|u˙W
28 27 3ad2ant1 KHLWHSBSGS˙WdomJ=uB|u˙W
29 26 28 sseqtrrd KHLWHSBSGS˙WTdomJ
30 1 2 3 4 5 6 dihglblem2aN KHLWHSBST
31 30 3adant3 KHLWHSBSGS˙WT
32 4 5 7 dibglbN KHLWHTdomJTJGT=xTJx
33 9 29 31 32 syl12anc KHLWHSBSGS˙WJGT=xTJx
34 1 2 3 4 5 6 dihglblem2N KHLWHSBGS˙WGS=GT
35 34 3adant2r KHLWHSBSGS˙WGS=GT
36 35 fveq2d KHLWHSBSGS˙WJGS=JGT
37 simpl1 KHLWHSBSGS˙WxTKHLWH
38 26 sselda KHLWHSBSGS˙WxTxuB|u˙W
39 breq1 u=xu˙Wx˙W
40 39 elrab xuB|u˙WxBx˙W
41 38 40 sylib KHLWHSBSGS˙WxTxBx˙W
42 1 2 5 8 7 dihvalb KHLWHxBx˙WIx=Jx
43 37 41 42 syl2anc KHLWHSBSGS˙WxTIx=Jx
44 43 iineq2dv KHLWHSBSGS˙WxTIx=xTJx
45 33 36 44 3eqtr4rd KHLWHSBSGS˙WxTIx=JGS
46 simp1l KHLWHSBSGS˙WKHL
47 hlclat KHLKCLat
48 46 47 syl KHLWHSBSGS˙WKCLat
49 simp2l KHLWHSBSGS˙WSB
50 1 4 clatglbcl KCLatSBGSB
51 48 49 50 syl2anc KHLWHSBSGS˙WGSB
52 simp3 KHLWHSBSGS˙WGS˙W
53 1 2 5 8 7 dihvalb KHLWHGSBGS˙WIGS=JGS
54 9 51 52 53 syl12anc KHLWHSBSGS˙WIGS=JGS
55 35 fveq2d KHLWHSBSGS˙WIGS=IGT
56 45 54 55 3eqtr2rd KHLWHSBSGS˙WIGT=xTIx