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 ) ) ) ) ) )