# 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 = ( Base ` K )`
omlspj.l
`|- .<_ = ( le ` K )`
omlspj.j
`|- .\/ = ( join ` K )`
omlspj.m
`|- ./\ = ( meet ` K )`
omlspj.o
`|- ._|_ = ( oc ` K )`
Assertion omlspjN
`|- ( ( K e. OML /\ ( X e. B /\ Y e. B ) /\ X .<_ Y ) -> ( ( X .\/ ( ._|_ ` Y ) ) ./\ Y ) = X )`

### Proof

Step Hyp Ref Expression
1 omlspj.b
` |-  B = ( Base ` K )`
2 omlspj.l
` |-  .<_ = ( le ` K )`
3 omlspj.j
` |-  .\/ = ( join ` K )`
4 omlspj.m
` |-  ./\ = ( meet ` K )`
5 omlspj.o
` |-  ._|_ = ( oc ` K )`
6 omllat
` |-  ( K e. OML -> K e. Lat )`
` |-  ( ( K e. OML /\ ( X e. B /\ Y e. B ) /\ X .<_ Y ) -> K e. Lat )`
8 omlop
` |-  ( K e. OML -> K e. OP )`
` |-  ( ( K e. OML /\ ( X e. B /\ Y e. B ) /\ X .<_ Y ) -> K e. OP )`
10 simp2r
` |-  ( ( K e. OML /\ ( X e. B /\ Y e. B ) /\ X .<_ Y ) -> Y e. B )`
11 1 5 opoccl
` |-  ( ( K e. OP /\ Y e. B ) -> ( ._|_ ` Y ) e. B )`
12 9 10 11 syl2anc
` |-  ( ( K e. OML /\ ( X e. B /\ Y e. B ) /\ X .<_ Y ) -> ( ._|_ ` Y ) e. B )`
13 1 4 latmcom
` |-  ( ( K e. Lat /\ ( ._|_ ` Y ) e. B /\ Y e. B ) -> ( ( ._|_ ` Y ) ./\ Y ) = ( Y ./\ ( ._|_ ` Y ) ) )`
14 7 12 10 13 syl3anc
` |-  ( ( K e. OML /\ ( X e. B /\ Y e. B ) /\ X .<_ Y ) -> ( ( ._|_ ` Y ) ./\ Y ) = ( Y ./\ ( ._|_ ` Y ) ) )`
15 eqid
` |-  ( 0. ` K ) = ( 0. ` K )`
16 1 5 4 15 opnoncon
` |-  ( ( K e. OP /\ Y e. B ) -> ( Y ./\ ( ._|_ ` Y ) ) = ( 0. ` K ) )`
17 9 10 16 syl2anc
` |-  ( ( K e. OML /\ ( X e. B /\ Y e. B ) /\ X .<_ Y ) -> ( Y ./\ ( ._|_ ` Y ) ) = ( 0. ` K ) )`
18 14 17 eqtrd
` |-  ( ( K e. OML /\ ( X e. B /\ Y e. B ) /\ X .<_ Y ) -> ( ( ._|_ ` Y ) ./\ Y ) = ( 0. ` K ) )`
19 18 oveq2d
` |-  ( ( K e. OML /\ ( X e. B /\ Y e. B ) /\ X .<_ Y ) -> ( X .\/ ( ( ._|_ ` Y ) ./\ Y ) ) = ( X .\/ ( 0. ` K ) ) )`
20 simp1
` |-  ( ( K e. OML /\ ( X e. B /\ Y e. B ) /\ X .<_ Y ) -> K e. OML )`
21 simp2l
` |-  ( ( K e. OML /\ ( X e. B /\ Y e. B ) /\ X .<_ Y ) -> X e. B )`
22 simp3
` |-  ( ( K e. OML /\ ( X e. B /\ Y e. B ) /\ X .<_ Y ) -> X .<_ Y )`
23 eqid
` |-  ( cm ` K ) = ( cm ` K )`
24 1 23 cmtidN
` |-  ( ( K e. OML /\ Y e. B ) -> Y ( cm ` K ) Y )`
25 20 10 24 syl2anc
` |-  ( ( K e. OML /\ ( X e. B /\ Y e. B ) /\ X .<_ Y ) -> Y ( cm ` K ) Y )`
26 1 5 23 cmt3N
` |-  ( ( K e. OML /\ Y e. B /\ Y e. B ) -> ( Y ( cm ` K ) Y <-> ( ._|_ ` Y ) ( cm ` K ) Y ) )`
27 20 10 10 26 syl3anc
` |-  ( ( K e. OML /\ ( X e. B /\ Y e. B ) /\ X .<_ Y ) -> ( Y ( cm ` K ) Y <-> ( ._|_ ` Y ) ( cm ` K ) Y ) )`
28 25 27 mpbid
` |-  ( ( K e. OML /\ ( X e. B /\ Y e. B ) /\ X .<_ Y ) -> ( ._|_ ` Y ) ( cm ` K ) Y )`
29 1 2 3 4 23 omlmod1i2N
` |-  ( ( K e. OML /\ ( X e. B /\ ( ._|_ ` Y ) e. B /\ Y e. B ) /\ ( X .<_ Y /\ ( ._|_ ` Y ) ( cm ` K ) Y ) ) -> ( X .\/ ( ( ._|_ ` Y ) ./\ Y ) ) = ( ( X .\/ ( ._|_ ` Y ) ) ./\ Y ) )`
30 20 21 12 10 22 28 29 syl132anc
` |-  ( ( K e. OML /\ ( X e. B /\ Y e. B ) /\ X .<_ Y ) -> ( X .\/ ( ( ._|_ ` Y ) ./\ Y ) ) = ( ( X .\/ ( ._|_ ` Y ) ) ./\ Y ) )`
31 omlol
` |-  ( K e. OML -> K e. OL )`
` |-  ( ( K e. OML /\ ( X e. B /\ Y e. B ) /\ X .<_ Y ) -> K e. OL )`
` |-  ( ( K e. OL /\ X e. B ) -> ( X .\/ ( 0. ` K ) ) = X )`
` |-  ( ( K e. OML /\ ( X e. B /\ Y e. B ) /\ X .<_ Y ) -> ( X .\/ ( 0. ` K ) ) = X )`
` |-  ( ( K e. OML /\ ( X e. B /\ Y e. B ) /\ X .<_ Y ) -> ( ( X .\/ ( ._|_ ` Y ) ) ./\ Y ) = X )`