# Metamath Proof Explorer

## Theorem dihlsscpre

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

Ref Expression
Hypotheses dihval.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
dihval.l
dihval.j
dihval.m
dihval.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
dihval.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dihval.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
dihval.d ${⊢}{D}=\mathrm{DIsoB}\left({K}\right)\left({W}\right)$
dihval.c ${⊢}{C}=\mathrm{DIsoC}\left({K}\right)\left({W}\right)$
dihval.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dihval.s ${⊢}{S}=\mathrm{LSubSp}\left({U}\right)$
dihval.p
Assertion dihlsscpre

### Proof

Step Hyp Ref Expression
1 dihval.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 dihval.l
3 dihval.j
4 dihval.m
5 dihval.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
6 dihval.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
7 dihval.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
8 dihval.d ${⊢}{D}=\mathrm{DIsoB}\left({K}\right)\left({W}\right)$
9 dihval.c ${⊢}{C}=\mathrm{DIsoC}\left({K}\right)\left({W}\right)$
10 dihval.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
11 dihval.s ${⊢}{S}=\mathrm{LSubSp}\left({U}\right)$
12 dihval.p
13 1 2 3 4 5 6 7 8 9 10 11 12 dihvalc
14 simp1l
15 simp2l
16 simp3ll
17 15 16 jca
18 simp2r
19 simp3rl
20 18 19 jca
21 simp1rl
22 simp3lr
23 simp3rr
24 22 23 eqtr4d
25 1 2 3 4 5 6 8 9 10 12 dihjust
26 14 17 20 21 24 25 syl131anc
27 26 3exp
28 27 ralrimivv
29 1 2 3 4 5 6 lhpmcvr2
30 simpll
31 6 10 30 dvhlmod
32 2 5 6 10 9 11 diclss
34 hllat ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{Lat}$
36 simplrl
37 1 6 lhpbase ${⊢}{W}\in {H}\to {W}\in {B}$
39 1 4 latmcl
40 35 36 38 39 syl3anc
41 1 2 4 latmle2
42 35 36 38 41 syl3anc
43 1 2 6 10 8 11 diblss
44 30 40 42 43 syl12anc
45 11 12 lsmcl
46 31 33 44 45 syl3anc
47 46 a1d
48 47 expr
49 48 impd
50 49 ancld
51 50 reximdva
52 29 51 mpd
53 breq1
54 53 notbid
55 oveq1
56 55 eqeq1d
57 54 56 anbi12d
58 fveq2 ${⊢}{q}={r}\to {C}\left({q}\right)={C}\left({r}\right)$
59 58 oveq1d
60 57 59 reusv3
61 52 60 syl
62 28 61 mpbid
63 reusv1
64 29 63 syl
65 62 64 mpbird
66 riotacl
67 65 66 syl
68 13 67 eqeltrd