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

Metamath Proof Explorer

Theorem dihglbcN

Description: Isomorphism H of a lattice glb when the glb is not under the fiducial hyperplane W . (Contributed by NM, 26-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihglbc.b ⊢ B = Base K
dihglbc.g ⊢ G = glb ⁡ K
dihglbc.h ⊢ H = LHyp ⁡ K
dihglbc.i ⊢ I = DIsoH ⁡ K ⁡ W
dihglbc.l ⊢ ≤ ˙ = ≤ K
Assertion dihglbcN ⊢ K ∈ HL ∧ W ∈ H ∧ S ⊆ B ∧ S ≠ ∅ ∧ ¬ G ⁡ S ≤ ˙ W → I ⁡ G ⁡ S = ⋂ x ∈ S I ⁡ x

Proof

Step Hyp Ref Expression
1 dihglbc.b ⊢ B = Base K
2 dihglbc.g ⊢ G = glb ⁡ K
3 dihglbc.h ⊢ H = LHyp ⁡ K
4 dihglbc.i ⊢ I = DIsoH ⁡ K ⁡ W
5 dihglbc.l ⊢ ≤ ˙ = ≤ K
6 eqid ⊢ join ⁡ K = join ⁡ K
7 eqid ⊢ meet ⁡ K = meet ⁡ K
8 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
9 eqid ⊢ oc ⁡ K ⁡ W = oc ⁡ K ⁡ W
10 eqid ⊢ LTrn ⁡ K ⁡ W = LTrn ⁡ K ⁡ W
11 eqid ⊢ trL ⁡ K ⁡ W = trL ⁡ K ⁡ W
12 eqid ⊢ TEndo ⁡ K ⁡ W = TEndo ⁡ K ⁡ W
13 eqid ⊢ ι g ∈ LTrn ⁡ K ⁡ W | g ⁡ oc ⁡ K ⁡ W = q = ι g ∈ LTrn ⁡ K ⁡ W | g ⁡ oc ⁡ K ⁡ W = q
14 1 2 3 4 5 6 7 8 9 10 11 12 13 dihglbcpreN ⊢ K ∈ HL ∧ W ∈ H ∧ S ⊆ B ∧ S ≠ ∅ ∧ ¬ G ⁡ S ≤ ˙ W → I ⁡ G ⁡ S = ⋂ x ∈ S I ⁡ x