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 𝐵 = ( Base ‘ 𝐾 )
dihglblem.l = ( le ‘ 𝐾 )
dihglblem.m = ( meet ‘ 𝐾 )
dihglblem.g 𝐺 = ( glb ‘ 𝐾 )
dihglblem.h 𝐻 = ( LHyp ‘ 𝐾 )
dihglblem.t 𝑇 = { 𝑢𝐵 ∣ ∃ 𝑣𝑆 𝑢 = ( 𝑣 𝑊 ) }
Assertion dihglblem2N ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) → ( 𝐺𝑆 ) = ( 𝐺𝑇 ) )

Proof

Step Hyp Ref Expression
1 dihglblem.b 𝐵 = ( Base ‘ 𝐾 )
2 dihglblem.l = ( le ‘ 𝐾 )
3 dihglblem.m = ( meet ‘ 𝐾 )
4 dihglblem.g 𝐺 = ( glb ‘ 𝐾 )
5 dihglblem.h 𝐻 = ( LHyp ‘ 𝐾 )
6 dihglblem.t 𝑇 = { 𝑢𝐵 ∣ ∃ 𝑣𝑆 𝑢 = ( 𝑣 𝑊 ) }
7 simpl1l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑥𝑆 ) → 𝐾 ∈ HL )
8 7 hllatd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑥𝑆 ) → 𝐾 ∈ Lat )
9 simp1l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) → 𝐾 ∈ HL )
10 hlclat ( 𝐾 ∈ HL → 𝐾 ∈ CLat )
11 9 10 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) → 𝐾 ∈ CLat )
12 ssrab2 { 𝑢𝐵 ∣ ∃ 𝑣𝑆 𝑢 = ( 𝑣 𝑊 ) } ⊆ 𝐵
13 6 12 eqsstri 𝑇𝐵
14 1 4 clatglbcl ( ( 𝐾 ∈ CLat ∧ 𝑇𝐵 ) → ( 𝐺𝑇 ) ∈ 𝐵 )
15 11 13 14 sylancl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) → ( 𝐺𝑇 ) ∈ 𝐵 )
16 15 adantr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑥𝑆 ) → ( 𝐺𝑇 ) ∈ 𝐵 )
17 simpl2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑥𝑆 ) → 𝑆𝐵 )
18 simpr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑥𝑆 ) → 𝑥𝑆 )
19 17 18 sseldd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑥𝑆 ) → 𝑥𝐵 )
20 simpl1r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑥𝑆 ) → 𝑊𝐻 )
21 1 5 lhpbase ( 𝑊𝐻𝑊𝐵 )
22 20 21 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑥𝑆 ) → 𝑊𝐵 )
23 1 3 latmcl ( ( 𝐾 ∈ Lat ∧ 𝑥𝐵𝑊𝐵 ) → ( 𝑥 𝑊 ) ∈ 𝐵 )
24 8 19 22 23 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑥𝑆 ) → ( 𝑥 𝑊 ) ∈ 𝐵 )
25 7 10 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑥𝑆 ) → 𝐾 ∈ CLat )
26 eqidd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑥𝑆 ) → ( 𝑥 𝑊 ) = ( 𝑥 𝑊 ) )
27 oveq1 ( 𝑣 = 𝑥 → ( 𝑣 𝑊 ) = ( 𝑥 𝑊 ) )
28 27 rspceeqv ( ( 𝑥𝑆 ∧ ( 𝑥 𝑊 ) = ( 𝑥 𝑊 ) ) → ∃ 𝑣𝑆 ( 𝑥 𝑊 ) = ( 𝑣 𝑊 ) )
29 18 26 28 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑥𝑆 ) → ∃ 𝑣𝑆 ( 𝑥 𝑊 ) = ( 𝑣 𝑊 ) )
30 eqeq1 ( 𝑢 = ( 𝑥 𝑊 ) → ( 𝑢 = ( 𝑣 𝑊 ) ↔ ( 𝑥 𝑊 ) = ( 𝑣 𝑊 ) ) )
31 30 rexbidv ( 𝑢 = ( 𝑥 𝑊 ) → ( ∃ 𝑣𝑆 𝑢 = ( 𝑣 𝑊 ) ↔ ∃ 𝑣𝑆 ( 𝑥 𝑊 ) = ( 𝑣 𝑊 ) ) )
32 31 elrab ( ( 𝑥 𝑊 ) ∈ { 𝑢𝐵 ∣ ∃ 𝑣𝑆 𝑢 = ( 𝑣 𝑊 ) } ↔ ( ( 𝑥 𝑊 ) ∈ 𝐵 ∧ ∃ 𝑣𝑆 ( 𝑥 𝑊 ) = ( 𝑣 𝑊 ) ) )
33 24 29 32 sylanbrc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑥𝑆 ) → ( 𝑥 𝑊 ) ∈ { 𝑢𝐵 ∣ ∃ 𝑣𝑆 𝑢 = ( 𝑣 𝑊 ) } )
34 33 6 eleqtrrdi ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑥𝑆 ) → ( 𝑥 𝑊 ) ∈ 𝑇 )
35 1 2 4 clatglble ( ( 𝐾 ∈ CLat ∧ 𝑇𝐵 ∧ ( 𝑥 𝑊 ) ∈ 𝑇 ) → ( 𝐺𝑇 ) ( 𝑥 𝑊 ) )
36 13 35 mp3an2 ( ( 𝐾 ∈ CLat ∧ ( 𝑥 𝑊 ) ∈ 𝑇 ) → ( 𝐺𝑇 ) ( 𝑥 𝑊 ) )
37 25 34 36 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑥𝑆 ) → ( 𝐺𝑇 ) ( 𝑥 𝑊 ) )
38 1 2 3 latmle1 ( ( 𝐾 ∈ Lat ∧ 𝑥𝐵𝑊𝐵 ) → ( 𝑥 𝑊 ) 𝑥 )
39 8 19 22 38 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑥𝑆 ) → ( 𝑥 𝑊 ) 𝑥 )
40 1 2 8 16 24 19 37 39 lattrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑥𝑆 ) → ( 𝐺𝑇 ) 𝑥 )
41 eqeq1 ( 𝑢 = 𝑤 → ( 𝑢 = ( 𝑣 𝑊 ) ↔ 𝑤 = ( 𝑣 𝑊 ) ) )
42 41 rexbidv ( 𝑢 = 𝑤 → ( ∃ 𝑣𝑆 𝑢 = ( 𝑣 𝑊 ) ↔ ∃ 𝑣𝑆 𝑤 = ( 𝑣 𝑊 ) ) )
43 oveq1 ( 𝑣 = 𝑦 → ( 𝑣 𝑊 ) = ( 𝑦 𝑊 ) )
44 43 eqeq2d ( 𝑣 = 𝑦 → ( 𝑤 = ( 𝑣 𝑊 ) ↔ 𝑤 = ( 𝑦 𝑊 ) ) )
45 44 cbvrexvw ( ∃ 𝑣𝑆 𝑤 = ( 𝑣 𝑊 ) ↔ ∃ 𝑦𝑆 𝑤 = ( 𝑦 𝑊 ) )
46 42 45 bitrdi ( 𝑢 = 𝑤 → ( ∃ 𝑣𝑆 𝑢 = ( 𝑣 𝑊 ) ↔ ∃ 𝑦𝑆 𝑤 = ( 𝑦 𝑊 ) ) )
47 46 6 elrab2 ( 𝑤𝑇 ↔ ( 𝑤𝐵 ∧ ∃ 𝑦𝑆 𝑤 = ( 𝑦 𝑊 ) ) )
48 simp3 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) ∧ 𝑤𝐵𝑦𝑆 ) → 𝑦𝑆 )
49 simp13 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) ∧ 𝑤𝐵𝑦𝑆 ) → ∀ 𝑥𝑆 𝑧 𝑥 )
50 breq2 ( 𝑥 = 𝑦 → ( 𝑧 𝑥𝑧 𝑦 ) )
51 50 rspcva ( ( 𝑦𝑆 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) → 𝑧 𝑦 )
52 48 49 51 syl2anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) ∧ 𝑤𝐵𝑦𝑆 ) → 𝑧 𝑦 )
53 simp11l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) → 𝐾 ∈ HL )
54 53 3ad2ant1 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) ∧ 𝑤𝐵𝑦𝑆 ) → 𝐾 ∈ HL )
55 54 hllatd ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) ∧ 𝑤𝐵𝑦𝑆 ) → 𝐾 ∈ Lat )
56 simp12 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) ∧ 𝑤𝐵𝑦𝑆 ) → 𝑧𝐵 )
57 54 10 syl ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) ∧ 𝑤𝐵𝑦𝑆 ) → 𝐾 ∈ CLat )
58 simp112 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) ∧ 𝑤𝐵𝑦𝑆 ) → 𝑆𝐵 )
59 1 4 clatglbcl ( ( 𝐾 ∈ CLat ∧ 𝑆𝐵 ) → ( 𝐺𝑆 ) ∈ 𝐵 )
60 57 58 59 syl2anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) ∧ 𝑤𝐵𝑦𝑆 ) → ( 𝐺𝑆 ) ∈ 𝐵 )
61 simp11r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) → 𝑊𝐻 )
62 61 3ad2ant1 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) ∧ 𝑤𝐵𝑦𝑆 ) → 𝑊𝐻 )
63 62 21 syl ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) ∧ 𝑤𝐵𝑦𝑆 ) → 𝑊𝐵 )
64 1 2 4 clatleglb ( ( 𝐾 ∈ CLat ∧ 𝑧𝐵𝑆𝐵 ) → ( 𝑧 ( 𝐺𝑆 ) ↔ ∀ 𝑥𝑆 𝑧 𝑥 ) )
65 57 56 58 64 syl3anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) ∧ 𝑤𝐵𝑦𝑆 ) → ( 𝑧 ( 𝐺𝑆 ) ↔ ∀ 𝑥𝑆 𝑧 𝑥 ) )
66 49 65 mpbird ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) ∧ 𝑤𝐵𝑦𝑆 ) → 𝑧 ( 𝐺𝑆 ) )
67 simp113 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) ∧ 𝑤𝐵𝑦𝑆 ) → ( 𝐺𝑆 ) 𝑊 )
68 1 2 55 56 60 63 66 67 lattrd ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) ∧ 𝑤𝐵𝑦𝑆 ) → 𝑧 𝑊 )
69 58 48 sseldd ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) ∧ 𝑤𝐵𝑦𝑆 ) → 𝑦𝐵 )
70 1 2 3 latlem12 ( ( 𝐾 ∈ Lat ∧ ( 𝑧𝐵𝑦𝐵𝑊𝐵 ) ) → ( ( 𝑧 𝑦𝑧 𝑊 ) ↔ 𝑧 ( 𝑦 𝑊 ) ) )
71 55 56 69 63 70 syl13anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) ∧ 𝑤𝐵𝑦𝑆 ) → ( ( 𝑧 𝑦𝑧 𝑊 ) ↔ 𝑧 ( 𝑦 𝑊 ) ) )
72 52 68 71 mpbi2and ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) ∧ 𝑤𝐵𝑦𝑆 ) → 𝑧 ( 𝑦 𝑊 ) )
73 72 3expia ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) ∧ 𝑤𝐵 ) → ( 𝑦𝑆𝑧 ( 𝑦 𝑊 ) ) )
74 breq2 ( 𝑤 = ( 𝑦 𝑊 ) → ( 𝑧 𝑤𝑧 ( 𝑦 𝑊 ) ) )
75 74 biimprcd ( 𝑧 ( 𝑦 𝑊 ) → ( 𝑤 = ( 𝑦 𝑊 ) → 𝑧 𝑤 ) )
76 73 75 syl6 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) ∧ 𝑤𝐵 ) → ( 𝑦𝑆 → ( 𝑤 = ( 𝑦 𝑊 ) → 𝑧 𝑤 ) ) )
77 76 rexlimdv ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) ∧ 𝑤𝐵 ) → ( ∃ 𝑦𝑆 𝑤 = ( 𝑦 𝑊 ) → 𝑧 𝑤 ) )
78 77 expimpd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) → ( ( 𝑤𝐵 ∧ ∃ 𝑦𝑆 𝑤 = ( 𝑦 𝑊 ) ) → 𝑧 𝑤 ) )
79 47 78 syl5bi ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) → ( 𝑤𝑇𝑧 𝑤 ) )
80 79 ralrimiv ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) → ∀ 𝑤𝑇 𝑧 𝑤 )
81 53 10 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) → 𝐾 ∈ CLat )
82 simp2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) → 𝑧𝐵 )
83 1 2 4 clatleglb ( ( 𝐾 ∈ CLat ∧ 𝑧𝐵𝑇𝐵 ) → ( 𝑧 ( 𝐺𝑇 ) ↔ ∀ 𝑤𝑇 𝑧 𝑤 ) )
84 13 83 mp3an3 ( ( 𝐾 ∈ CLat ∧ 𝑧𝐵 ) → ( 𝑧 ( 𝐺𝑇 ) ↔ ∀ 𝑤𝑇 𝑧 𝑤 ) )
85 81 82 84 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) → ( 𝑧 ( 𝐺𝑇 ) ↔ ∀ 𝑤𝑇 𝑧 𝑤 ) )
86 80 85 mpbird ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) ∧ 𝑧𝐵 ∧ ∀ 𝑥𝑆 𝑧 𝑥 ) → 𝑧 ( 𝐺𝑇 ) )
87 simp2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) → 𝑆𝐵 )
88 1 2 4 40 86 11 87 15 isglbd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐵 ∧ ( 𝐺𝑆 ) 𝑊 ) → ( 𝐺𝑆 ) = ( 𝐺𝑇 ) )