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 = ( Base ` K )
dihglblem.l 
|- .<_ = ( le ` K )
dihglblem.m 
|- ./\ = ( meet ` K )
dihglblem.g 
|- G = ( glb ` K )
dihglblem.h 
|- H = ( LHyp ` K )
dihglblem.t 
|- T = { u e. B | E. v e. S u = ( v ./\ W ) }
Assertion dihglblem2N 
|- ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) -> ( G ` S ) = ( G ` T ) )

Proof

Step Hyp Ref Expression
1 dihglblem.b 
 |-  B = ( Base ` K )
2 dihglblem.l 
 |-  .<_ = ( le ` K )
3 dihglblem.m 
 |-  ./\ = ( meet ` K )
4 dihglblem.g 
 |-  G = ( glb ` K )
5 dihglblem.h 
 |-  H = ( LHyp ` K )
6 dihglblem.t 
 |-  T = { u e. B | E. v e. S u = ( v ./\ W ) }
7 simpl1l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ x e. S ) -> K e. HL )
8 7 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ x e. S ) -> K e. Lat )
9 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) -> K e. HL )
10 hlclat 
 |-  ( K e. HL -> K e. CLat )
11 9 10 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) -> K e. CLat )
12 ssrab2 
 |-  { u e. B | E. v e. S u = ( v ./\ W ) } C_ B
13 6 12 eqsstri 
 |-  T C_ B
14 1 4 clatglbcl 
 |-  ( ( K e. CLat /\ T C_ B ) -> ( G ` T ) e. B )
15 11 13 14 sylancl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) -> ( G ` T ) e. B )
16 15 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ x e. S ) -> ( G ` T ) e. B )
17 simpl2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ x e. S ) -> S C_ B )
18 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ x e. S ) -> x e. S )
19 17 18 sseldd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ x e. S ) -> x e. B )
20 simpl1r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ x e. S ) -> W e. H )
21 1 5 lhpbase 
 |-  ( W e. H -> W e. B )
22 20 21 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ x e. S ) -> W e. B )
23 1 3 latmcl 
 |-  ( ( K e. Lat /\ x e. B /\ W e. B ) -> ( x ./\ W ) e. B )
24 8 19 22 23 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ x e. S ) -> ( x ./\ W ) e. B )
25 7 10 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ x e. S ) -> K e. CLat )
26 eqidd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ x e. S ) -> ( x ./\ W ) = ( x ./\ W ) )
27 oveq1 
 |-  ( v = x -> ( v ./\ W ) = ( x ./\ W ) )
28 27 rspceeqv 
 |-  ( ( x e. S /\ ( x ./\ W ) = ( x ./\ W ) ) -> E. v e. S ( x ./\ W ) = ( v ./\ W ) )
29 18 26 28 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ x e. S ) -> E. v e. S ( x ./\ W ) = ( v ./\ W ) )
30 eqeq1 
 |-  ( u = ( x ./\ W ) -> ( u = ( v ./\ W ) <-> ( x ./\ W ) = ( v ./\ W ) ) )
31 30 rexbidv 
 |-  ( u = ( x ./\ W ) -> ( E. v e. S u = ( v ./\ W ) <-> E. v e. S ( x ./\ W ) = ( v ./\ W ) ) )
32 31 elrab 
 |-  ( ( x ./\ W ) e. { u e. B | E. v e. S u = ( v ./\ W ) } <-> ( ( x ./\ W ) e. B /\ E. v e. S ( x ./\ W ) = ( v ./\ W ) ) )
33 24 29 32 sylanbrc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ x e. S ) -> ( x ./\ W ) e. { u e. B | E. v e. S u = ( v ./\ W ) } )
34 33 6 eleqtrrdi 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ x e. S ) -> ( x ./\ W ) e. T )
35 1 2 4 clatglble 
 |-  ( ( K e. CLat /\ T C_ B /\ ( x ./\ W ) e. T ) -> ( G ` T ) .<_ ( x ./\ W ) )
36 13 35 mp3an2 
 |-  ( ( K e. CLat /\ ( x ./\ W ) e. T ) -> ( G ` T ) .<_ ( x ./\ W ) )
37 25 34 36 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ x e. S ) -> ( G ` T ) .<_ ( x ./\ W ) )
38 1 2 3 latmle1 
 |-  ( ( K e. Lat /\ x e. B /\ W e. B ) -> ( x ./\ W ) .<_ x )
39 8 19 22 38 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ x e. S ) -> ( x ./\ W ) .<_ x )
40 1 2 8 16 24 19 37 39 lattrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ x e. S ) -> ( G ` T ) .<_ x )
41 eqeq1 
 |-  ( u = w -> ( u = ( v ./\ W ) <-> w = ( v ./\ W ) ) )
42 41 rexbidv 
 |-  ( u = w -> ( E. v e. S u = ( v ./\ W ) <-> E. v e. S w = ( v ./\ W ) ) )
43 oveq1 
 |-  ( v = y -> ( v ./\ W ) = ( y ./\ W ) )
44 43 eqeq2d 
 |-  ( v = y -> ( w = ( v ./\ W ) <-> w = ( y ./\ W ) ) )
45 44 cbvrexvw 
 |-  ( E. v e. S w = ( v ./\ W ) <-> E. y e. S w = ( y ./\ W ) )
46 42 45 bitrdi 
 |-  ( u = w -> ( E. v e. S u = ( v ./\ W ) <-> E. y e. S w = ( y ./\ W ) ) )
47 46 6 elrab2 
 |-  ( w e. T <-> ( w e. B /\ E. y e. S w = ( y ./\ W ) ) )
48 simp3 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) /\ w e. B /\ y e. S ) -> y e. S )
49 simp13 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) /\ w e. B /\ y e. S ) -> A. x e. S z .<_ x )
50 breq2 
 |-  ( x = y -> ( z .<_ x <-> z .<_ y ) )
51 50 rspcva 
 |-  ( ( y e. S /\ A. x e. S z .<_ x ) -> z .<_ y )
52 48 49 51 syl2anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) /\ w e. B /\ y e. S ) -> z .<_ y )
53 simp11l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) -> K e. HL )
54 53 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) /\ w e. B /\ y e. S ) -> K e. HL )
55 54 hllatd 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) /\ w e. B /\ y e. S ) -> K e. Lat )
56 simp12 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) /\ w e. B /\ y e. S ) -> z e. B )
57 54 10 syl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) /\ w e. B /\ y e. S ) -> K e. CLat )
58 simp112 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) /\ w e. B /\ y e. S ) -> S C_ B )
59 1 4 clatglbcl 
 |-  ( ( K e. CLat /\ S C_ B ) -> ( G ` S ) e. B )
60 57 58 59 syl2anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) /\ w e. B /\ y e. S ) -> ( G ` S ) e. B )
61 simp11r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) -> W e. H )
62 61 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) /\ w e. B /\ y e. S ) -> W e. H )
63 62 21 syl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) /\ w e. B /\ y e. S ) -> W e. B )
64 1 2 4 clatleglb 
 |-  ( ( K e. CLat /\ z e. B /\ S C_ B ) -> ( z .<_ ( G ` S ) <-> A. x e. S z .<_ x ) )
65 57 56 58 64 syl3anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) /\ w e. B /\ y e. S ) -> ( z .<_ ( G ` S ) <-> A. x e. S z .<_ x ) )
66 49 65 mpbird 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) /\ w e. B /\ y e. S ) -> z .<_ ( G ` S ) )
67 simp113 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) /\ w e. B /\ y e. S ) -> ( G ` S ) .<_ W )
68 1 2 55 56 60 63 66 67 lattrd 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) /\ w e. B /\ y e. S ) -> z .<_ W )
69 58 48 sseldd 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) /\ w e. B /\ y e. S ) -> y e. B )
70 1 2 3 latlem12 
 |-  ( ( K e. Lat /\ ( z e. B /\ y e. B /\ W e. B ) ) -> ( ( z .<_ y /\ z .<_ W ) <-> z .<_ ( y ./\ W ) ) )
71 55 56 69 63 70 syl13anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) /\ w e. B /\ y e. S ) -> ( ( z .<_ y /\ z .<_ W ) <-> z .<_ ( y ./\ W ) ) )
72 52 68 71 mpbi2and 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) /\ w e. B /\ y e. S ) -> z .<_ ( y ./\ W ) )
73 72 3expia 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) /\ w e. B ) -> ( y e. S -> z .<_ ( y ./\ W ) ) )
74 breq2 
 |-  ( w = ( y ./\ W ) -> ( z .<_ w <-> z .<_ ( y ./\ W ) ) )
75 74 biimprcd 
 |-  ( z .<_ ( y ./\ W ) -> ( w = ( y ./\ W ) -> z .<_ w ) )
76 73 75 syl6 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) /\ w e. B ) -> ( y e. S -> ( w = ( y ./\ W ) -> z .<_ w ) ) )
77 76 rexlimdv 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) /\ w e. B ) -> ( E. y e. S w = ( y ./\ W ) -> z .<_ w ) )
78 77 expimpd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) -> ( ( w e. B /\ E. y e. S w = ( y ./\ W ) ) -> z .<_ w ) )
79 47 78 biimtrid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) -> ( w e. T -> z .<_ w ) )
80 79 ralrimiv 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) -> A. w e. T z .<_ w )
81 53 10 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) -> K e. CLat )
82 simp2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) -> z e. B )
83 1 2 4 clatleglb 
 |-  ( ( K e. CLat /\ z e. B /\ T C_ B ) -> ( z .<_ ( G ` T ) <-> A. w e. T z .<_ w ) )
84 13 83 mp3an3 
 |-  ( ( K e. CLat /\ z e. B ) -> ( z .<_ ( G ` T ) <-> A. w e. T z .<_ w ) )
85 81 82 84 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) -> ( z .<_ ( G ` T ) <-> A. w e. T z .<_ w ) )
86 80 85 mpbird 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) /\ z e. B /\ A. x e. S z .<_ x ) -> z .<_ ( G ` T ) )
87 simp2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) -> S C_ B )
88 1 2 4 40 86 11 87 15 isglbd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S C_ B /\ ( G ` S ) .<_ W ) -> ( G ` S ) = ( G ` T ) )