Metamath Proof Explorer


Theorem dihvalc

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

Ref Expression
Hypotheses dihval.b B = Base K
dihval.l ˙ = K
dihval.j ˙ = join K
dihval.m ˙ = meet K
dihval.a A = Atoms K
dihval.h H = LHyp K
dihval.i I = DIsoH K W
dihval.d D = DIsoB K W
dihval.c C = DIsoC K W
dihval.u U = DVecH K W
dihval.s S = LSubSp U
dihval.p ˙ = LSSum U
Assertion dihvalc K V W H X B ¬ X ˙ W I X = ι u S | q A ¬ q ˙ W q ˙ X ˙ W = X u = C q ˙ D X ˙ W

Proof

Step Hyp Ref Expression
1 dihval.b B = Base K
2 dihval.l ˙ = K
3 dihval.j ˙ = join K
4 dihval.m ˙ = meet K
5 dihval.a A = Atoms K
6 dihval.h H = LHyp K
7 dihval.i I = DIsoH K W
8 dihval.d D = DIsoB K W
9 dihval.c C = DIsoC K W
10 dihval.u U = DVecH K W
11 dihval.s S = LSubSp U
12 dihval.p ˙ = LSSum U
13 1 2 3 4 5 6 7 8 9 10 11 12 dihval K V W H X B I X = if X ˙ W D X ι u S | q A ¬ q ˙ W q ˙ X ˙ W = X u = C q ˙ D X ˙ W
14 iffalse ¬ X ˙ W if X ˙ W D X ι u S | q A ¬ q ˙ W q ˙ X ˙ W = X u = C q ˙ D X ˙ W = ι u S | q A ¬ q ˙ W q ˙ X ˙ W = X u = C q ˙ D X ˙ W
15 13 14 sylan9eq K V W H X B ¬ X ˙ W I X = ι u S | q A ¬ q ˙ W q ˙ X ˙ W = X u = C q ˙ D X ˙ W
16 15 anasss K V W H X B ¬ X ˙ W I X = ι u S | q A ¬ q ˙ W q ˙ X ˙ W = X u = C q ˙ D X ˙ W