This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dihglblem4

Description: Isomorphism H of a lattice glb. (Contributed by NM, 21-Mar-2014)

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 dihglblem4 ( ( ( 𝐾 ∈ 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 hlclat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CLat )
10 9 ad3antrrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐾 ∈ CLat )
11 simplrl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑆 ⊆ 𝐵 )
12 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
13 1 2 4 clatglble ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑥 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑆 ) ≤ 𝑥 )
14 10 11 12 13 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑆 ) ≤ 𝑥 )
15 simpll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
16 1 4 clatglbcl ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 )
17 10 11 16 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 )
18 11 12 sseldd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝐵 )
19 1 2 5 8 dihord ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ( 𝐼 ‘ 𝑥 ) ↔ ( 𝐺 ‘ 𝑆 ) ≤ 𝑥 ) )
20 15 17 18 19 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ( 𝐼 ‘ 𝑥 ) ↔ ( 𝐺 ‘ 𝑆 ) ≤ 𝑥 ) )
21 14 20 mpbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ( 𝐼 ‘ 𝑥 ) )
22 21 ralrimiva ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ( 𝐼 ‘ 𝑥 ) )
23 ssiin ⊢ ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ( 𝐼 ‘ 𝑥 ) )
24 22 23 sylibr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ⊆ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) )