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 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ 𝐵 ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐺 ‘ 𝑆 ) = ( 𝐺 ‘ 𝑇 ) )