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