# Metamath Proof Explorer

## Theorem omlspjN

Description: Contraction of a Sasaki projection. (Contributed by NM, 6-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses omlspj.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
omlspj.l
omlspj.j
omlspj.m
omlspj.o
Assertion omlspjN

### Proof

Step Hyp Ref Expression
1 omlspj.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 omlspj.l
3 omlspj.j
4 omlspj.m
5 omlspj.o
6 omllat ${⊢}{K}\in \mathrm{OML}\to {K}\in \mathrm{Lat}$
8 omlop ${⊢}{K}\in \mathrm{OML}\to {K}\in \mathrm{OP}$
10 simp2r
11 1 5 opoccl
12 9 10 11 syl2anc
13 1 4 latmcom
14 7 12 10 13 syl3anc
15 eqid ${⊢}\mathrm{0.}\left({K}\right)=\mathrm{0.}\left({K}\right)$
16 1 5 4 15 opnoncon
17 9 10 16 syl2anc
18 14 17 eqtrd
19 18 oveq2d
20 simp1
21 simp2l
22 simp3
23 eqid ${⊢}\mathrm{cm}\left({K}\right)=\mathrm{cm}\left({K}\right)$
24 1 23 cmtidN ${⊢}\left({K}\in \mathrm{OML}\wedge {Y}\in {B}\right)\to {Y}\mathrm{cm}\left({K}\right){Y}$
25 20 10 24 syl2anc
26 1 5 23 cmt3N
27 20 10 10 26 syl3anc
28 25 27 mpbid
29 1 2 3 4 23 omlmod1i2N
30 20 21 12 10 22 28 29 syl132anc
31 omlol ${⊢}{K}\in \mathrm{OML}\to {K}\in \mathrm{OL}$