# Metamath Proof Explorer

## Theorem isoml

Description: The predicate "is an orthomodular lattice." (Contributed by NM, 18-Sep-2011)

Ref Expression
Hypotheses isoml.b
`|- B = ( Base ` K )`
isoml.l
`|- .<_ = ( le ` K )`
isoml.j
`|- .\/ = ( join ` K )`
isoml.m
`|- ./\ = ( meet ` K )`
isoml.o
`|- ._|_ = ( oc ` K )`
Assertion isoml
`|- ( K e. OML <-> ( K e. OL /\ A. x e. B A. y e. B ( x .<_ y -> y = ( x .\/ ( y ./\ ( ._|_ ` x ) ) ) ) ) )`

### Proof

Step Hyp Ref Expression
1 isoml.b
` |-  B = ( Base ` K )`
2 isoml.l
` |-  .<_ = ( le ` K )`
3 isoml.j
` |-  .\/ = ( join ` K )`
4 isoml.m
` |-  ./\ = ( meet ` K )`
5 isoml.o
` |-  ._|_ = ( oc ` K )`
6 fveq2
` |-  ( k = K -> ( Base ` k ) = ( Base ` K ) )`
7 6 1 eqtr4di
` |-  ( k = K -> ( Base ` k ) = B )`
8 fveq2
` |-  ( k = K -> ( le ` k ) = ( le ` K ) )`
9 8 2 eqtr4di
` |-  ( k = K -> ( le ` k ) = .<_ )`
10 9 breqd
` |-  ( k = K -> ( x ( le ` k ) y <-> x .<_ y ) )`
11 fveq2
` |-  ( k = K -> ( join ` k ) = ( join ` K ) )`
12 11 3 eqtr4di
` |-  ( k = K -> ( join ` k ) = .\/ )`
13 eqidd
` |-  ( k = K -> x = x )`
14 fveq2
` |-  ( k = K -> ( meet ` k ) = ( meet ` K ) )`
15 14 4 eqtr4di
` |-  ( k = K -> ( meet ` k ) = ./\ )`
16 eqidd
` |-  ( k = K -> y = y )`
17 fveq2
` |-  ( k = K -> ( oc ` k ) = ( oc ` K ) )`
18 17 5 eqtr4di
` |-  ( k = K -> ( oc ` k ) = ._|_ )`
19 18 fveq1d
` |-  ( k = K -> ( ( oc ` k ) ` x ) = ( ._|_ ` x ) )`
20 15 16 19 oveq123d
` |-  ( k = K -> ( y ( meet ` k ) ( ( oc ` k ) ` x ) ) = ( y ./\ ( ._|_ ` x ) ) )`
21 12 13 20 oveq123d
` |-  ( k = K -> ( x ( join ` k ) ( y ( meet ` k ) ( ( oc ` k ) ` x ) ) ) = ( x .\/ ( y ./\ ( ._|_ ` x ) ) ) )`
22 21 eqeq2d
` |-  ( k = K -> ( y = ( x ( join ` k ) ( y ( meet ` k ) ( ( oc ` k ) ` x ) ) ) <-> y = ( x .\/ ( y ./\ ( ._|_ ` x ) ) ) ) )`
23 10 22 imbi12d
` |-  ( k = K -> ( ( x ( le ` k ) y -> y = ( x ( join ` k ) ( y ( meet ` k ) ( ( oc ` k ) ` x ) ) ) ) <-> ( x .<_ y -> y = ( x .\/ ( y ./\ ( ._|_ ` x ) ) ) ) ) )`
24 7 23 raleqbidv
` |-  ( k = K -> ( A. y e. ( Base ` k ) ( x ( le ` k ) y -> y = ( x ( join ` k ) ( y ( meet ` k ) ( ( oc ` k ) ` x ) ) ) ) <-> A. y e. B ( x .<_ y -> y = ( x .\/ ( y ./\ ( ._|_ ` x ) ) ) ) ) )`
25 7 24 raleqbidv
` |-  ( k = K -> ( A. x e. ( Base ` k ) A. y e. ( Base ` k ) ( x ( le ` k ) y -> y = ( x ( join ` k ) ( y ( meet ` k ) ( ( oc ` k ) ` x ) ) ) ) <-> A. x e. B A. y e. B ( x .<_ y -> y = ( x .\/ ( y ./\ ( ._|_ ` x ) ) ) ) ) )`
26 df-oml
` |-  OML = { k e. OL | A. x e. ( Base ` k ) A. y e. ( Base ` k ) ( x ( le ` k ) y -> y = ( x ( join ` k ) ( y ( meet ` k ) ( ( oc ` k ) ` x ) ) ) ) }`
27 25 26 elrab2
` |-  ( K e. OML <-> ( K e. OL /\ A. x e. B A. y e. B ( x .<_ y -> y = ( x .\/ ( y ./\ ( ._|_ ` x ) ) ) ) ) )`