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 DLat K Lat x B y B z 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]˙ x b y b z b x m y j z = x m y j x m z [˙ ˙ / m]˙ x b y b z 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]˙ x b y b z b x m y j z = x m y j x m z [˙ ˙ / j]˙ [˙ ˙ / m]˙ x b y b z 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]˙ x b y b z b x m y j z = x m y j x m z [˙B / b]˙ [˙ ˙ / j]˙ [˙ ˙ / m]˙ x b y b z b x m y j z = x m y j x m z
13 1 fvexi B V
14 2 fvexi ˙ V
15 3 fvexi ˙ V
16 raleq b = B z b x m y j z = x m y j x m z z B x m y j z = x m y j x m z
17 16 raleqbi1dv b = B y b z b x m y j z = x m y j x m z y B z B x m y j z = x m y j x m z
18 17 raleqbi1dv b = B x b y b z b x m y j z = x m y j x m z x B y B z 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 = ˙ z B x m y j z = x m y j x m z z B x ˙ y ˙ z = x ˙ y ˙ x ˙ z
29 28 2ralbidv j = ˙ m = ˙ x B y B z B x m y j z = x m y j x m z x B y B z B x ˙ y ˙ z = x ˙ y ˙ x ˙ z
30 18 29 sylan9bb b = B j = ˙ m = ˙ x b y b z b x m y j z = x m y j x m z x B y B z B x ˙ y ˙ z = x ˙ y ˙ x ˙ z
31 30 3impb b = B j = ˙ m = ˙ x b y b z b x m y j z = x m y j x m z x B y B z B x ˙ y ˙ z = x ˙ y ˙ x ˙ z
32 13 14 15 31 sbc3ie [˙B / b]˙ [˙ ˙ / j]˙ [˙ ˙ / m]˙ x b y b z b x m y j z = x m y j x m z x B y B z B x ˙ y ˙ z = x ˙ y ˙ x ˙ z
33 12 32 bitrdi k = K [˙Base k / b]˙ [˙ join k / j]˙ [˙ meet k / m]˙ x b y b z b x m y j z = x m y j x m z x B y B z B x ˙ y ˙ z = x ˙ y ˙ x ˙ z
34 df-dlat DLat = k Lat | [˙Base k / b]˙ [˙ join k / j]˙ [˙ meet k / m]˙ x b y b z b x m y j z = x m y j x m z
35 33 34 elrab2 K DLat K Lat x B y B z B x ˙ y ˙ z = x ˙ y ˙ x ˙ z