Metamath Proof Explorer

Theorem isdlat

Description: Property of being a distributive lattice. (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Hypotheses isdlat.b 
|- B = ( Base ` K )
isdlat.j 
|- .\/ = ( join ` K )
isdlat.m 
|- ./\ = ( meet ` K )
Assertion isdlat 
|- ( K e. DLat <-> ( K e. Lat /\ 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 isdlat.b 
 |-  B = ( Base ` K )
2 isdlat.j 
 |-  .\/ = ( join ` K )
3 isdlat.m 
 |-  ./\ = ( meet ` K )
4 fveq2 
 |-  ( k = K -> ( Base ` k ) = ( Base ` K ) )
5 4 1 eqtr4di 
 |-  ( k = K -> ( Base ` k ) = B )
6 fveq2 
 |-  ( k = K -> ( join ` k ) = ( join ` K ) )
7 6 2 eqtr4di 
 |-  ( k = K -> ( join ` k ) = .\/ )
8 fveq2 
 |-  ( k = K -> ( meet ` k ) = ( meet ` K ) )
9 8 3 eqtr4di 
 |-  ( k = K -> ( meet ` k ) = ./\ )
10 9 sbceq1d 
 |-  ( k = K -> ( [. ( meet ` k ) / m ]. A. x e. b A. y e. b A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) ) <-> [. ./\ / m ]. A. x e. b A. y e. b A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) ) ) )
11 7 10 sbceqbid 
 |-  ( k = K -> ( [. ( join ` k ) / j ]. [. ( meet ` k ) / m ]. A. x e. b A. y e. b A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) ) <-> [. .\/ / j ]. [. ./\ / m ]. A. x e. b A. y e. b A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) ) ) )
12 5 11 sbceqbid 
 |-  ( k = K -> ( [. ( Base ` k ) / b ]. [. ( join ` k ) / j ]. [. ( meet ` k ) / m ]. A. x e. b A. y e. b A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) ) <-> [. B / b ]. [. .\/ / j ]. [. ./\ / m ]. A. x e. b A. y e. b A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) ) ) )
13 1 fvexi 
 |-  B e. _V
14 2 fvexi 
 |-  .\/ e. _V
15 3 fvexi 
 |-  ./\ e. _V
16 raleq 
 |-  ( b = B -> ( A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) ) <-> A. z e. B ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) ) ) )
17 16 raleqbi1dv 
 |-  ( b = B -> ( A. y e. b A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) ) <-> A. y e. B A. z e. B ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) ) ) )
18 17 raleqbi1dv 
 |-  ( b = B -> ( A. x e. b A. y e. b A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) ) <-> A. x e. B A. y e. B A. z e. B ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) ) ) )
19 simpr 
 |-  ( ( j = .\/ /\ m = ./\ ) -> m = ./\ )
20 eqidd 
 |-  ( ( j = .\/ /\ m = ./\ ) -> x = x )
21 simpl 
 |-  ( ( j = .\/ /\ m = ./\ ) -> j = .\/ )
22 21 oveqd 
 |-  ( ( j = .\/ /\ m = ./\ ) -> ( y j z ) = ( y .\/ z ) )
23 19 20 22 oveq123d 
 |-  ( ( j = .\/ /\ m = ./\ ) -> ( x m ( y j z ) ) = ( x ./\ ( y .\/ z ) ) )
24 19 oveqd 
 |-  ( ( j = .\/ /\ m = ./\ ) -> ( x m y ) = ( x ./\ y ) )
25 19 oveqd 
 |-  ( ( j = .\/ /\ m = ./\ ) -> ( x m z ) = ( x ./\ z ) )
26 21 24 25 oveq123d 
 |-  ( ( j = .\/ /\ m = ./\ ) -> ( ( x m y ) j ( x m z ) ) = ( ( x ./\ y ) .\/ ( x ./\ z ) ) )
27 23 26 eqeq12d 
 |-  ( ( j = .\/ /\ m = ./\ ) -> ( ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) ) <-> ( x ./\ ( y .\/ z ) ) = ( ( x ./\ y ) .\/ ( x ./\ z ) ) ) )
28 27 ralbidv 
 |-  ( ( j = .\/ /\ m = ./\ ) -> ( A. z e. B ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) ) <-> A. z e. B ( x ./\ ( y .\/ z ) ) = ( ( x ./\ y ) .\/ ( x ./\ z ) ) ) )
29 28 2ralbidv 
 |-  ( ( j = .\/ /\ m = ./\ ) -> ( A. x e. B A. y e. B A. z e. B ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) ) <-> A. x e. B A. y e. B A. z e. B ( x ./\ ( y .\/ z ) ) = ( ( x ./\ y ) .\/ ( x ./\ z ) ) ) )
30 18 29 sylan9bb 
 |-  ( ( b = B /\ ( j = .\/ /\ m = ./\ ) ) -> ( A. x e. b A. y e. b A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) ) <-> A. x e. B A. y e. B A. z e. B ( x ./\ ( y .\/ z ) ) = ( ( x ./\ y ) .\/ ( x ./\ z ) ) ) )
31 30 3impb 
 |-  ( ( b = B /\ j = .\/ /\ m = ./\ ) -> ( A. x e. b A. y e. b A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) ) <-> A. x e. B A. y e. B A. z e. B ( x ./\ ( y .\/ z ) ) = ( ( x ./\ y ) .\/ ( x ./\ z ) ) ) )
32 13 14 15 31 sbc3ie 
 |-  ( [. B / b ]. [. .\/ / j ]. [. ./\ / m ]. A. x e. b A. y e. b A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) ) <-> A. x e. B A. y e. B A. z e. B ( x ./\ ( y .\/ z ) ) = ( ( x ./\ y ) .\/ ( x ./\ z ) ) )
33 12 32 bitrdi 
 |-  ( k = K -> ( [. ( Base ` k ) / b ]. [. ( join ` k ) / j ]. [. ( meet ` k ) / m ]. A. x e. b A. y e. b A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) ) <-> A. x e. B A. y e. B A. z e. B ( x ./\ ( y .\/ z ) ) = ( ( x ./\ y ) .\/ ( x ./\ z ) ) ) )
34 df-dlat 
 |-  DLat = { k e. Lat | [. ( Base ` k ) / b ]. [. ( join ` k ) / j ]. [. ( meet ` k ) / m ]. A. x e. b A. y e. b A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) ) }
35 33 34 elrab2 
 |-  ( K e. DLat <-> ( K e. Lat /\ A. x e. B A. y e. B A. z e. B ( x ./\ ( y .\/ z ) ) = ( ( x ./\ y ) .\/ ( x ./\ z ) ) ) )