Metamath Proof Explorer

Theorem dihvalb

Description: Value of isomorphism H for a lattice K when X .<_ W . (Contributed by NM, 4-Mar-2014)

Ref Expression
Hypotheses dihvalb.b ⊢ B = Base K
dihvalb.l ⊢ ≤ ˙ = ≤ K
dihvalb.h ⊢ H = LHyp ⁡ K
dihvalb.i ⊢ I = DIsoH ⁡ K ⁡ W
dihvalb.d ⊢ D = DIsoB ⁡ K ⁡ W
Assertion dihvalb ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → I ⁡ X = D ⁡ X

Proof

Step Hyp Ref Expression
1 dihvalb.b ⊢ B = Base K
2 dihvalb.l ⊢ ≤ ˙ = ≤ K
3 dihvalb.h ⊢ H = LHyp ⁡ K
4 dihvalb.i ⊢ I = DIsoH ⁡ K ⁡ W
5 dihvalb.d ⊢ D = DIsoB ⁡ K ⁡ W
6 eqid ⊢ join ⁡ K = join ⁡ K
7 eqid ⊢ meet ⁡ K = meet ⁡ K
8 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
9 eqid ⊢ DIsoC ⁡ K ⁡ W = DIsoC ⁡ K ⁡ W
10 eqid ⊢ DVecH ⁡ K ⁡ W = DVecH ⁡ K ⁡ W
11 eqid ⊢ LSubSp ⁡ DVecH ⁡ K ⁡ W = LSubSp ⁡ DVecH ⁡ K ⁡ W
12 eqid ⊢ LSSum ⁡ DVecH ⁡ K ⁡ W = LSSum ⁡ DVecH ⁡ K ⁡ W
13 1 2 6 7 8 3 4 5 9 10 11 12 dihval ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B → I ⁡ X = if X ≤ ˙ W D ⁡ X ι u ∈ LSubSp ⁡ DVecH ⁡ K ⁡ W | ∀ q ∈ Atoms ⁡ K ¬ q ≤ ˙ W ∧ q join ⁡ K X meet ⁡ K W = X → u = DIsoC ⁡ K ⁡ W ⁡ q LSSum ⁡ DVecH ⁡ K ⁡ W D ⁡ X meet ⁡ K W
14 iftrue ⊢ X ≤ ˙ W → if X ≤ ˙ W D ⁡ X ι u ∈ LSubSp ⁡ DVecH ⁡ K ⁡ W | ∀ q ∈ Atoms ⁡ K ¬ q ≤ ˙ W ∧ q join ⁡ K X meet ⁡ K W = X → u = DIsoC ⁡ K ⁡ W ⁡ q LSSum ⁡ DVecH ⁡ K ⁡ W D ⁡ X meet ⁡ K W = D ⁡ X
15 13 14 sylan9eq ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → I ⁡ X = D ⁡ X
16 15 anasss ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → I ⁡ X = D ⁡ X