# Metamath Proof Explorer

## Theorem omllaw5N

Description: The orthomodular law. Remark in Kalmbach p. 22. ( pjoml5 analog.) (Contributed by NM, 14-Nov-2011) (New usage is discouraged.)

Ref Expression
Hypotheses omllaw5.b
`|- B = ( Base ` K )`
omllaw5.j
`|- .\/ = ( join ` K )`
omllaw5.m
`|- ./\ = ( meet ` K )`
omllaw5.o
`|- ._|_ = ( oc ` K )`
Assertion omllaw5N
`|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X .\/ ( ( ._|_ ` X ) ./\ ( X .\/ Y ) ) ) = ( X .\/ Y ) )`

### Proof

Step Hyp Ref Expression
1 omllaw5.b
` |-  B = ( Base ` K )`
2 omllaw5.j
` |-  .\/ = ( join ` K )`
3 omllaw5.m
` |-  ./\ = ( meet ` K )`
4 omllaw5.o
` |-  ._|_ = ( oc ` K )`
5 simp1
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. OML )`
6 simp2
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> X e. B )`
7 omllat
` |-  ( K e. OML -> K e. Lat )`
8 1 2 latjcl
` |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) e. B )`
9 7 8 syl3an1
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) e. B )`
10 5 6 9 3jca
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( K e. OML /\ X e. B /\ ( X .\/ Y ) e. B ) )`
11 eqid
` |-  ( le ` K ) = ( le ` K )`
12 1 11 2 latlej1
` |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> X ( le ` K ) ( X .\/ Y ) )`
13 7 12 syl3an1
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> X ( le ` K ) ( X .\/ Y ) )`
14 1 11 2 3 4 omllaw2N
` |-  ( ( K e. OML /\ X e. B /\ ( X .\/ Y ) e. B ) -> ( X ( le ` K ) ( X .\/ Y ) -> ( X .\/ ( ( ._|_ ` X ) ./\ ( X .\/ Y ) ) ) = ( X .\/ Y ) ) )`
15 10 13 14 sylc
` |-  ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X .\/ ( ( ._|_ ` X ) ./\ ( X .\/ Y ) ) ) = ( X .\/ Y ) )`