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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihglblem.l ⊢ ≤ = ( le ‘ 𝐾 )
dihglblem.m ⊢ ∧ = ( meet ‘ 𝐾 )
dihglblem.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
dihglblem.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihglblem.t ⊢ 𝑇 = { 𝑢 ∈ 𝐵 ∣ ∃ 𝑣 ∈ 𝑆 𝑢 = ( 𝑣 ∧ 𝑊 ) }
dihglblem.i ⊢ 𝐽 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
dihglblem.ih ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
Assertion dihglblem3N ( ( ( 𝐾 ∈ 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 dihglblem.i ⊢ 𝐽 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
8 dihglblem.ih ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
9 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10 simp11l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆 ) → 𝐾 ∈ HL )
11 10 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆 ) → 𝐾 ∈ Lat )
12 simp12l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆 ) → 𝑆 ⊆ 𝐵 )
13 simp3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆 ) → 𝑣 ∈ 𝑆 )
14 12 13 sseldd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆 ) → 𝑣 ∈ 𝐵 )
15 simp11r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆 ) → 𝑊 ∈ 𝐻 )
16 1 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
17 15 16 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆 ) → 𝑊 ∈ 𝐵 )
18 1 2 3 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑣 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑣 ∧ 𝑊 ) ≤ 𝑊 )
19 11 14 17 18 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆 ) → ( 𝑣 ∧ 𝑊 ) ≤ 𝑊 )
20 19 3expia ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑢 ∈ 𝐵 ) → ( 𝑣 ∈ 𝑆 → ( 𝑣 ∧ 𝑊 ) ≤ 𝑊 ) )
21 breq1 ⊢ ( 𝑢 = ( 𝑣 ∧ 𝑊 ) → ( 𝑢 ≤ 𝑊 ↔ ( 𝑣 ∧ 𝑊 ) ≤ 𝑊 ) )
22 21 biimprcd ⊢ ( ( 𝑣 ∧ 𝑊 ) ≤ 𝑊 → ( 𝑢 = ( 𝑣 ∧ 𝑊 ) → 𝑢 ≤ 𝑊 ) )
23 20 22 syl6 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑢 ∈ 𝐵 ) → ( 𝑣 ∈ 𝑆 → ( 𝑢 = ( 𝑣 ∧ 𝑊 ) → 𝑢 ≤ 𝑊 ) ) )
24 23 rexlimdv ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑢 ∈ 𝐵 ) → ( ∃ 𝑣 ∈ 𝑆 𝑢 = ( 𝑣 ∧ 𝑊 ) → 𝑢 ≤ 𝑊 ) )
25 24 ss2rabdv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → { 𝑢 ∈ 𝐵 ∣ ∃ 𝑣 ∈ 𝑆 𝑢 = ( 𝑣 ∧ 𝑊 ) } ⊆ { 𝑢 ∈ 𝐵 ∣ 𝑢 ≤ 𝑊 } )
26 6 25 eqsstrid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → 𝑇 ⊆ { 𝑢 ∈ 𝐵 ∣ 𝑢 ≤ 𝑊 } )
27 1 2 5 7 dibdmN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → dom 𝐽 = { 𝑢 ∈ 𝐵 ∣ 𝑢 ≤ 𝑊 } )
28 27 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → dom 𝐽 = { 𝑢 ∈ 𝐵 ∣ 𝑢 ≤ 𝑊 } )
29 26 28 sseqtrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → 𝑇 ⊆ dom 𝐽 )
30 1 2 3 4 5 6 dihglblem2aN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → 𝑇 ≠ ∅ )
31 30 3adant3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → 𝑇 ≠ ∅ )
32 4 5 7 dibglbN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑇 ⊆ dom 𝐽 ∧ 𝑇 ≠ ∅ ) ) → ( 𝐽 ‘ ( 𝐺 ‘ 𝑇 ) ) = ∩ 𝑥 ∈ 𝑇 ( 𝐽 ‘ 𝑥 ) )
33 9 29 31 32 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐽 ‘ ( 𝐺 ‘ 𝑇 ) ) = ∩ 𝑥 ∈ 𝑇 ( 𝐽 ‘ 𝑥 ) )
34 1 2 3 4 5 6 dihglblem2N ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ 𝐵 ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐺 ‘ 𝑆 ) = ( 𝐺 ‘ 𝑇 ) )
35 34 3adant2r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐺 ‘ 𝑆 ) = ( 𝐺 ‘ 𝑇 ) )
36 35 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐽 ‘ ( 𝐺 ‘ 𝑆 ) ) = ( 𝐽 ‘ ( 𝐺 ‘ 𝑇 ) ) )
37 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
38 26 sselda ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑥 ∈ 𝑇 ) → 𝑥 ∈ { 𝑢 ∈ 𝐵 ∣ 𝑢 ≤ 𝑊 } )
39 breq1 ⊢ ( 𝑢 = 𝑥 → ( 𝑢 ≤ 𝑊 ↔ 𝑥 ≤ 𝑊 ) )
40 39 elrab ⊢ ( 𝑥 ∈ { 𝑢 ∈ 𝐵 ∣ 𝑢 ≤ 𝑊 } ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊 ) )
41 38 40 sylib ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊 ) )
42 1 2 5 8 7 dihvalb ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑥 ) = ( 𝐽 ‘ 𝑥 ) )
43 37 41 42 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝐼 ‘ 𝑥 ) = ( 𝐽 ‘ 𝑥 ) )
44 43 iineq2dv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ∩ 𝑥 ∈ 𝑇 ( 𝐼 ‘ 𝑥 ) = ∩ 𝑥 ∈ 𝑇 ( 𝐽 ‘ 𝑥 ) )
45 33 36 44 3eqtr4rd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ∩ 𝑥 ∈ 𝑇 ( 𝐼 ‘ 𝑥 ) = ( 𝐽 ‘ ( 𝐺 ‘ 𝑆 ) ) )
46 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → 𝐾 ∈ HL )
47 hlclat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CLat )
48 46 47 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → 𝐾 ∈ CLat )
49 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → 𝑆 ⊆ 𝐵 )
50 1 4 clatglbcl ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 )
51 48 49 50 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 )
52 simp3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 )
53 1 2 5 8 7 dihvalb ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) = ( 𝐽 ‘ ( 𝐺 ‘ 𝑆 ) ) )
54 9 51 52 53 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) = ( 𝐽 ‘ ( 𝐺 ‘ 𝑆 ) ) )
55 35 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) = ( 𝐼 ‘ ( 𝐺 ‘ 𝑇 ) ) )
56 45 54 55 3eqtr2rd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑇 ) ) = ∩ 𝑥 ∈ 𝑇 ( 𝐼 ‘ 𝑥 ) )