Metamath Proof Explorer

Theorem odudlatb

Description: The dual of a distributive lattice is a distributive lattice and conversely. (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Hypothesis odudlat.d 
|- D = ( ODual ` K )
Assertion odudlatb 
|- ( K e. V -> ( K e. DLat <-> D e. DLat ) )

Proof

Step Hyp Ref Expression
1 odudlat.d 
 |-  D = ( ODual ` K )
2 eqid 
 |-  ( Base ` K ) = ( Base ` K )
3 eqid 
 |-  ( join ` K ) = ( join ` K )
4 eqid 
 |-  ( meet ` K ) = ( meet ` K )
5 2 3 4 latdisd 
 |-  ( K e. Lat -> ( A. x e. ( Base ` K ) A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x ( join ` K ) ( y ( meet ` K ) z ) ) = ( ( x ( join ` K ) y ) ( meet ` K ) ( x ( join ` K ) z ) ) <-> A. x e. ( Base ` K ) A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x ( meet ` K ) ( y ( join ` K ) z ) ) = ( ( x ( meet ` K ) y ) ( join ` K ) ( x ( meet ` K ) z ) ) ) )
6 5 bicomd 
 |-  ( K e. Lat -> ( A. x e. ( Base ` K ) A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x ( meet ` K ) ( y ( join ` K ) z ) ) = ( ( x ( meet ` K ) y ) ( join ` K ) ( x ( meet ` K ) z ) ) <-> A. x e. ( Base ` K ) A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x ( join ` K ) ( y ( meet ` K ) z ) ) = ( ( x ( join ` K ) y ) ( meet ` K ) ( x ( join ` K ) z ) ) ) )
7 6 pm5.32i 
 |-  ( ( K e. Lat /\ A. x e. ( Base ` K ) A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x ( meet ` K ) ( y ( join ` K ) z ) ) = ( ( x ( meet ` K ) y ) ( join ` K ) ( x ( meet ` K ) z ) ) ) <-> ( K e. Lat /\ A. x e. ( Base ` K ) A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x ( join ` K ) ( y ( meet ` K ) z ) ) = ( ( x ( join ` K ) y ) ( meet ` K ) ( x ( join ` K ) z ) ) ) )
8 1 odulatb 
 |-  ( K e. V -> ( K e. Lat <-> D e. Lat ) )
9 8 anbi1d 
 |-  ( K e. V -> ( ( K e. Lat /\ A. x e. ( Base ` K ) A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x ( join ` K ) ( y ( meet ` K ) z ) ) = ( ( x ( join ` K ) y ) ( meet ` K ) ( x ( join ` K ) z ) ) ) <-> ( D e. Lat /\ A. x e. ( Base ` K ) A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x ( join ` K ) ( y ( meet ` K ) z ) ) = ( ( x ( join ` K ) y ) ( meet ` K ) ( x ( join ` K ) z ) ) ) ) )
10 7 9 syl5bb 
 |-  ( K e. V -> ( ( K e. Lat /\ A. x e. ( Base ` K ) A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x ( meet ` K ) ( y ( join ` K ) z ) ) = ( ( x ( meet ` K ) y ) ( join ` K ) ( x ( meet ` K ) z ) ) ) <-> ( D e. Lat /\ A. x e. ( Base ` K ) A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x ( join ` K ) ( y ( meet ` K ) z ) ) = ( ( x ( join ` K ) y ) ( meet ` K ) ( x ( join ` K ) z ) ) ) ) )
11 2 3 4 isdlat 
 |-  ( K e. DLat <-> ( K e. Lat /\ A. x e. ( Base ` K ) A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x ( meet ` K ) ( y ( join ` K ) z ) ) = ( ( x ( meet ` K ) y ) ( join ` K ) ( x ( meet ` K ) z ) ) ) )
12 1 2 odubas 
 |-  ( Base ` K ) = ( Base ` D )
13 1 4 odujoin 
 |-  ( meet ` K ) = ( join ` D )
14 1 3 odumeet 
 |-  ( join ` K ) = ( meet ` D )
15 12 13 14 isdlat 
 |-  ( D e. DLat <-> ( D e. Lat /\ A. x e. ( Base ` K ) A. y e. ( Base ` K ) A. z e. ( Base ` K ) ( x ( join ` K ) ( y ( meet ` K ) z ) ) = ( ( x ( join ` K ) y ) ( meet ` K ) ( x ( join ` K ) z ) ) ) )
16 10 11 15 3bitr4g 
 |-  ( K e. V -> ( K e. DLat <-> D e. DLat ) )