Metamath Proof Explorer

Theorem dihglblem3aN

Description: Isomorphism H of a lattice glb. (Contributed by NM, 7-Apr-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihglblem.b ⊢ B = Base K
dihglblem.l ⊢ ≤ ˙ = ≤ K
dihglblem.m ⊢ ∧ ˙ = meet ⁡ K
dihglblem.g ⊢ G = glb ⁡ K
dihglblem.h ⊢ H = LHyp ⁡ K
dihglblem.t ⊢ T = u ∈ B | ∃ v ∈ S u = v ∧ ˙ W
dihglblem.i ⊢ J = DIsoB ⁡ K ⁡ W
dihglblem.ih ⊢ I = DIsoH ⁡ K ⁡ W
Assertion dihglblem3aN ⊢ K ∈ HL ∧ W ∈ H ∧ S ⊆ B ∧ S ≠ ∅ ∧ G ⁡ S ≤ ˙ W → I ⁡ G ⁡ S = ⋂ x ∈ T I ⁡ x

Proof

Step Hyp Ref Expression
1 dihglblem.b ⊢ B = Base K
2 dihglblem.l ⊢ ≤ ˙ = ≤ K
3 dihglblem.m ⊢ ∧ ˙ = meet ⁡ K
4 dihglblem.g ⊢ G = glb ⁡ K
5 dihglblem.h ⊢ H = LHyp ⁡ K
6 dihglblem.t ⊢ T = u ∈ B | ∃ v ∈ S u = v ∧ ˙ W
7 dihglblem.i ⊢ J = DIsoB ⁡ K ⁡ W
8 dihglblem.ih ⊢ I = DIsoH ⁡ K ⁡ W
9 1 2 3 4 5 6 dihglblem2N ⊢ K ∈ HL ∧ W ∈ H ∧ S ⊆ B ∧ G ⁡ S ≤ ˙ W → G ⁡ S = G ⁡ T
10 9 3adant2r ⊢ K ∈ HL ∧ W ∈ H ∧ S ⊆ B ∧ S ≠ ∅ ∧ G ⁡ S ≤ ˙ W → G ⁡ S = G ⁡ T
11 10 fveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ S ⊆ B ∧ S ≠ ∅ ∧ G ⁡ S ≤ ˙ W → I ⁡ G ⁡ S = I ⁡ G ⁡ T
12 1 2 3 4 5 6 7 8 dihglblem3N ⊢ K ∈ HL ∧ W ∈ H ∧ S ⊆ B ∧ S ≠ ∅ ∧ G ⁡ S ≤ ˙ W → I ⁡ G ⁡ T = ⋂ x ∈ T I ⁡ x
13 11 12 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ S ⊆ B ∧ S ≠ ∅ ∧ G ⁡ S ≤ ˙ W → I ⁡ G ⁡ S = ⋂ x ∈ T I ⁡ x