Metamath Proof Explorer


Theorem dihglbcpreN

Description: Isomorphism H of a lattice glb when the glb is not under the fiducial hyperplane W . (Contributed by NM, 20-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihglbc.b B = Base K
dihglbc.g G = glb K
dihglbc.h H = LHyp K
dihglbc.i I = DIsoH K W
dihglbc.l ˙ = K
dihglbcpre.j ˙ = join K
dihglbcpre.m ˙ = meet K
dihglbcpre.a A = Atoms K
dihglbcpre.p P = oc K W
dihglbcpre.t T = LTrn K W
dihglbcpre.r R = trL K W
dihglbcpre.e E = TEndo K W
dihglbcpre.f F = ι g T | g P = q
Assertion dihglbcpreN K HL W H S B S ¬ G S ˙ W I G S = x S I x

Proof

Step Hyp Ref Expression
1 dihglbc.b B = Base K
2 dihglbc.g G = glb K
3 dihglbc.h H = LHyp K
4 dihglbc.i I = DIsoH K W
5 dihglbc.l ˙ = K
6 dihglbcpre.j ˙ = join K
7 dihglbcpre.m ˙ = meet K
8 dihglbcpre.a A = Atoms K
9 dihglbcpre.p P = oc K W
10 dihglbcpre.t T = LTrn K W
11 dihglbcpre.r R = trL K W
12 dihglbcpre.e E = TEndo K W
13 dihglbcpre.f F = ι g T | g P = q
14 3 4 dihvalrel K HL W H Rel I G S
15 14 3ad2ant1 K HL W H S B S ¬ G S ˙ W Rel I G S
16 simp2r K HL W H S B S ¬ G S ˙ W S
17 n0 S x x S
18 16 17 sylib K HL W H S B S ¬ G S ˙ W x x S
19 simpr K HL W H S B S ¬ G S ˙ W x S x S
20 simpl1 K HL W H S B S ¬ G S ˙ W x S K HL W H
21 3 4 dihvalrel K HL W H Rel I x
22 20 21 syl K HL W H S B S ¬ G S ˙ W x S Rel I x
23 19 22 jca K HL W H S B S ¬ G S ˙ W x S x S Rel I x
24 23 ex K HL W H S B S ¬ G S ˙ W x S x S Rel I x
25 24 eximdv K HL W H S B S ¬ G S ˙ W x x S x x S Rel I x
26 18 25 mpd K HL W H S B S ¬ G S ˙ W x x S Rel I x
27 df-rex x S Rel I x x x S Rel I x
28 26 27 sylibr K HL W H S B S ¬ G S ˙ W x S Rel I x
29 reliin x S Rel I x Rel x S I x
30 28 29 syl K HL W H S B S ¬ G S ˙ W Rel x S I x
31 id K HL W H S B S ¬ G S ˙ W K HL W H S B S ¬ G S ˙ W
32 simp1 K HL W H S B S ¬ G S ˙ W K HL W H
33 simp1l K HL W H S B S ¬ G S ˙ W K HL
34 hlclat K HL K CLat
35 33 34 syl K HL W H S B S ¬ G S ˙ W K CLat
36 simp2l K HL W H S B S ¬ G S ˙ W S B
37 1 2 clatglbcl K CLat S B G S B
38 35 36 37 syl2anc K HL W H S B S ¬ G S ˙ W G S B
39 simp3 K HL W H S B S ¬ G S ˙ W ¬ G S ˙ W
40 1 5 6 7 8 3 lhpmcvr2 K HL W H G S B ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S
41 32 38 39 40 syl12anc K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S
42 simpl1 K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S K HL W H
43 38 adantr K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S G S B
44 simpl3 K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S ¬ G S ˙ W
45 simpr K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S q A ¬ q ˙ W q ˙ G S ˙ W = G S
46 vex f V
47 vex s V
48 1 5 6 7 8 3 9 10 11 12 4 13 46 47 dihopelvalc K HL W H G S B ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S f s I G S f T s E R f s F -1 ˙ G S
49 42 43 44 45 48 syl121anc K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S f s I G S f T s E R f s F -1 ˙ G S
50 simpl2r K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S S
51 r19.28zv S x S f T s E R f s F -1 ˙ x f T s E x S R f s F -1 ˙ x
52 50 51 syl K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S f T s E R f s F -1 ˙ x f T s E x S R f s F -1 ˙ x
53 simp11 K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S K HL W H
54 simp12l K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S S B
55 simp3 K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S x S
56 54 55 sseldd K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S x B
57 simp13 K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S ¬ G S ˙ W
58 simp11l K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S K HL
59 58 34 syl K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S K CLat
60 1 5 2 clatglble K CLat S B x S G S ˙ x
61 59 54 55 60 syl3anc K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S G S ˙ x
62 58 hllatd K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S K Lat
63 38 3ad2ant1 K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S G S B
64 simp11r K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S W H
65 1 3 lhpbase W H W B
66 64 65 syl K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S W B
67 1 5 lattr K Lat G S B x B W B G S ˙ x x ˙ W G S ˙ W
68 62 63 56 66 67 syl13anc K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S G S ˙ x x ˙ W G S ˙ W
69 61 68 mpand K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S x ˙ W G S ˙ W
70 57 69 mtod K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S ¬ x ˙ W
71 simp2l K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S q A ¬ q ˙ W
72 simp2ll K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S q A
73 1 8 atbase q A q B
74 72 73 syl K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S q B
75 1 7 latmcl K Lat G S B W B G S ˙ W B
76 62 63 66 75 syl3anc K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S G S ˙ W B
77 1 5 6 latlej1 K Lat q B G S ˙ W B q ˙ q ˙ G S ˙ W
78 62 74 76 77 syl3anc K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S q ˙ q ˙ G S ˙ W
79 simp2r K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S q ˙ G S ˙ W = G S
80 78 79 breqtrd K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S q ˙ G S
81 1 5 62 74 63 56 80 61 lattrd K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S q ˙ x
82 1 5 6 7 8 atmod3i1 K HL q A x B W B q ˙ x q ˙ x ˙ W = x ˙ q ˙ W
83 58 72 56 66 81 82 syl131anc K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S q ˙ x ˙ W = x ˙ q ˙ W
84 eqid 1. K = 1. K
85 5 6 84 8 3 lhpjat2 K HL W H q A ¬ q ˙ W q ˙ W = 1. K
86 53 71 85 syl2anc K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S q ˙ W = 1. K
87 86 oveq2d K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S x ˙ q ˙ W = x ˙ 1. K
88 hlol K HL K OL
89 58 88 syl K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S K OL
90 1 7 84 olm11 K OL x B x ˙ 1. K = x
91 89 56 90 syl2anc K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S x ˙ 1. K = x
92 83 87 91 3eqtrd K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S q ˙ x ˙ W = x
93 1 5 6 7 8 3 9 10 11 12 4 13 46 47 dihopelvalc K HL W H x B ¬ x ˙ W q A ¬ q ˙ W q ˙ x ˙ W = x f s I x f T s E R f s F -1 ˙ x
94 53 56 70 71 92 93 syl122anc K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S f s I x f T s E R f s F -1 ˙ x
95 94 3expa K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S f s I x f T s E R f s F -1 ˙ x
96 95 ralbidva K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S x S f s I x x S f T s E R f s F -1 ˙ x
97 simp11l K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S f T s E K HL
98 97 34 syl K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S f T s E K CLat
99 simp11 K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S f T s E K HL W H
100 simp3l K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S f T s E f T
101 simp3r K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S f T s E s E
102 5 8 3 9 lhpocnel2 K HL W H P A ¬ P ˙ W
103 99 102 syl K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S f T s E P A ¬ P ˙ W
104 simp2l K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S f T s E q A ¬ q ˙ W
105 5 8 3 10 13 ltrniotacl K HL W H P A ¬ P ˙ W q A ¬ q ˙ W F T
106 99 103 104 105 syl3anc K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S f T s E F T
107 3 10 12 tendocl K HL W H s E F T s F T
108 99 101 106 107 syl3anc K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S f T s E s F T
109 3 10 ltrncnv K HL W H s F T s F -1 T
110 99 108 109 syl2anc K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S f T s E s F -1 T
111 3 10 ltrnco K HL W H f T s F -1 T f s F -1 T
112 99 100 110 111 syl3anc K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S f T s E f s F -1 T
113 1 3 10 11 trlcl K HL W H f s F -1 T R f s F -1 B
114 99 112 113 syl2anc K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S f T s E R f s F -1 B
115 simp12l K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S f T s E S B
116 1 5 2 clatleglb K CLat R f s F -1 B S B R f s F -1 ˙ G S x S R f s F -1 ˙ x
117 98 114 115 116 syl3anc K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S f T s E R f s F -1 ˙ G S x S R f s F -1 ˙ x
118 117 3expa K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S f T s E R f s F -1 ˙ G S x S R f s F -1 ˙ x
119 118 pm5.32da K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S f T s E R f s F -1 ˙ G S f T s E x S R f s F -1 ˙ x
120 52 96 119 3bitr4rd K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S f T s E R f s F -1 ˙ G S x S f s I x
121 opex f s V
122 eliin f s V f s x S I x x S f s I x
123 121 122 ax-mp f s x S I x x S f s I x
124 120 123 bitr4di K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S f T s E R f s F -1 ˙ G S f s x S I x
125 49 124 bitrd K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S f s I G S f s x S I x
126 125 exp44 K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S f s I G S f s x S I x
127 126 imp4a K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S f s I G S f s x S I x
128 127 rexlimdv K HL W H S B S ¬ G S ˙ W q A ¬ q ˙ W q ˙ G S ˙ W = G S f s I G S f s x S I x
129 41 128 mpd K HL W H S B S ¬ G S ˙ W f s I G S f s x S I x
130 129 eqrelrdv2 Rel I G S Rel x S I x K HL W H S B S ¬ G S ˙ W I G S = x S I x
131 15 30 31 130 syl21anc K HL W H S B S ¬ G S ˙ W I G S = x S I x