Metamath Proof Explorer

Theorem dihvalcq2

Description: Value of isomorphism H for a lattice K when -. X .<_ W , given auxiliary atom Q . (Contributed by NM, 26-Sep-2014)

Ref Expression
Hypotheses dihvalcq2.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
dihvalcq2.l
dihvalcq2.j
dihvalcq2.m
dihvalcq2.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
dihvalcq2.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dihvalcq2.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
dihvalcq2.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dihvalcq2.p
Assertion dihvalcq2

Proof

Step Hyp Ref Expression
1 dihvalcq2.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 dihvalcq2.l
3 dihvalcq2.j
4 dihvalcq2.m
5 dihvalcq2.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
6 dihvalcq2.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
7 dihvalcq2.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
8 dihvalcq2.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
9 dihvalcq2.p
10 simp1
11 simp2
12 simp3l
13 simp3r
14 1 2 3 4 5 6 lhpmcvr3
15 10 11 12 14 syl3anc
16 13 15 mpbid
17 eqid ${⊢}\mathrm{DIsoB}\left({K}\right)\left({W}\right)=\mathrm{DIsoB}\left({K}\right)\left({W}\right)$
18 eqid ${⊢}\mathrm{DIsoC}\left({K}\right)\left({W}\right)=\mathrm{DIsoC}\left({K}\right)\left({W}\right)$
19 1 2 3 4 5 6 7 17 18 8 9 dihvalcq
20 10 11 12 16 19 syl112anc
21 2 5 6 18 7 dihvalcqat
22 10 12 21 syl2anc
23 simp1l
24 23 hllatd
25 simp2l
26 simp1r
27 1 6 lhpbase ${⊢}{W}\in {H}\to {W}\in {B}$
28 26 27 syl
29 1 4 latmcl
30 24 25 28 29 syl3anc
31 1 2 4 latmle2
32 24 25 28 31 syl3anc
33 1 2 6 7 17 dihvalb
34 10 30 32 33 syl12anc
35 22 34 oveq12d
36 20 35 eqtr4d