Metamath Proof Explorer

Theorem latdisd

Description: In a lattice, joins distribute over meets if and only if meets distribute over joins; the distributive property is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015)

Ref Expression
Hypotheses latdisd.b 
|- B = ( Base ` K )
latdisd.j 
|- .\/ = ( join ` K )
latdisd.m 
|- ./\ = ( meet ` K )
Assertion latdisd 
|- ( K e. Lat -> ( A. x e. B A. y e. B A. z e. B ( x .\/ ( y ./\ z ) ) = ( ( x .\/ y ) ./\ ( x .\/ z ) ) <-> A. x e. B A. y e. B A. z e. B ( x ./\ ( y .\/ z ) ) = ( ( x ./\ y ) .\/ ( x ./\ z ) ) ) )

Proof

Step Hyp Ref Expression
1 latdisd.b 
 |-  B = ( Base ` K )
2 latdisd.j 
 |-  .\/ = ( join ` K )
3 latdisd.m 
 |-  ./\ = ( meet ` K )
4 1 2 3 latdisdlem 
 |-  ( K e. Lat -> ( A. x e. B A. y e. B A. z e. B ( x .\/ ( y ./\ z ) ) = ( ( x .\/ y ) ./\ ( x .\/ z ) ) -> A. u e. B A. v e. B A. w e. B ( u ./\ ( v .\/ w ) ) = ( ( u ./\ v ) .\/ ( u ./\ w ) ) ) )
5 eqid 
 |-  ( ODual ` K ) = ( ODual ` K )
6 5 odulat 
 |-  ( K e. Lat -> ( ODual ` K ) e. Lat )
7 5 1 odubas 
 |-  B = ( Base ` ( ODual ` K ) )
8 5 3 odujoin 
 |-  ./\ = ( join ` ( ODual ` K ) )
9 5 2 odumeet 
 |-  .\/ = ( meet ` ( ODual ` K ) )
10 7 8 9 latdisdlem 
 |-  ( ( ODual ` K ) e. Lat -> ( A. u e. B A. v e. B A. w e. B ( u ./\ ( v .\/ w ) ) = ( ( u ./\ v ) .\/ ( u ./\ w ) ) -> A. x e. B A. y e. B A. z e. B ( x .\/ ( y ./\ z ) ) = ( ( x .\/ y ) ./\ ( x .\/ z ) ) ) )
11 6 10 syl 
 |-  ( K e. Lat -> ( A. u e. B A. v e. B A. w e. B ( u ./\ ( v .\/ w ) ) = ( ( u ./\ v ) .\/ ( u ./\ w ) ) -> A. x e. B A. y e. B A. z e. B ( x .\/ ( y ./\ z ) ) = ( ( x .\/ y ) ./\ ( x .\/ z ) ) ) )
12 4 11 impbid 
 |-  ( K e. Lat -> ( A. x e. B A. y e. B A. z e. B ( x .\/ ( y ./\ z ) ) = ( ( x .\/ y ) ./\ ( x .\/ z ) ) <-> A. u e. B A. v e. B A. w e. B ( u ./\ ( v .\/ w ) ) = ( ( u ./\ v ) .\/ ( u ./\ w ) ) ) )
13 oveq1 
 |-  ( u = x -> ( u ./\ ( v .\/ w ) ) = ( x ./\ ( v .\/ w ) ) )
14 oveq1 
 |-  ( u = x -> ( u ./\ v ) = ( x ./\ v ) )
15 oveq1 
 |-  ( u = x -> ( u ./\ w ) = ( x ./\ w ) )
16 14 15 oveq12d 
 |-  ( u = x -> ( ( u ./\ v ) .\/ ( u ./\ w ) ) = ( ( x ./\ v ) .\/ ( x ./\ w ) ) )
17 13 16 eqeq12d 
 |-  ( u = x -> ( ( u ./\ ( v .\/ w ) ) = ( ( u ./\ v ) .\/ ( u ./\ w ) ) <-> ( x ./\ ( v .\/ w ) ) = ( ( x ./\ v ) .\/ ( x ./\ w ) ) ) )
18 oveq1 
 |-  ( v = y -> ( v .\/ w ) = ( y .\/ w ) )
19 18 oveq2d 
 |-  ( v = y -> ( x ./\ ( v .\/ w ) ) = ( x ./\ ( y .\/ w ) ) )
20 oveq2 
 |-  ( v = y -> ( x ./\ v ) = ( x ./\ y ) )
21 20 oveq1d 
 |-  ( v = y -> ( ( x ./\ v ) .\/ ( x ./\ w ) ) = ( ( x ./\ y ) .\/ ( x ./\ w ) ) )
22 19 21 eqeq12d 
 |-  ( v = y -> ( ( x ./\ ( v .\/ w ) ) = ( ( x ./\ v ) .\/ ( x ./\ w ) ) <-> ( x ./\ ( y .\/ w ) ) = ( ( x ./\ y ) .\/ ( x ./\ w ) ) ) )
23 oveq2 
 |-  ( w = z -> ( y .\/ w ) = ( y .\/ z ) )
24 23 oveq2d 
 |-  ( w = z -> ( x ./\ ( y .\/ w ) ) = ( x ./\ ( y .\/ z ) ) )
25 oveq2 
 |-  ( w = z -> ( x ./\ w ) = ( x ./\ z ) )
26 25 oveq2d 
 |-  ( w = z -> ( ( x ./\ y ) .\/ ( x ./\ w ) ) = ( ( x ./\ y ) .\/ ( x ./\ z ) ) )
27 24 26 eqeq12d 
 |-  ( w = z -> ( ( x ./\ ( y .\/ w ) ) = ( ( x ./\ y ) .\/ ( x ./\ w ) ) <-> ( x ./\ ( y .\/ z ) ) = ( ( x ./\ y ) .\/ ( x ./\ z ) ) ) )
28 17 22 27 cbvral3vw 
 |-  ( A. u e. B A. v e. B A. w e. B ( u ./\ ( v .\/ w ) ) = ( ( u ./\ v ) .\/ ( u ./\ w ) ) <-> A. x e. B A. y e. B A. z e. B ( x ./\ ( y .\/ z ) ) = ( ( x ./\ y ) .\/ ( x ./\ z ) ) )
29 12 28 bitrdi 
 |-  ( K e. Lat -> ( A. x e. B A. y e. B A. z e. B ( x .\/ ( y ./\ z ) ) = ( ( x .\/ y ) ./\ ( x .\/ z ) ) <-> A. x e. B A. y e. B A. z e. B ( x ./\ ( y .\/ z ) ) = ( ( x ./\ y ) .\/ ( x ./\ z ) ) ) )