MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isdlat Structured version   Visualization version   GIF version

Theorem isdlat 18419
Description: Property of being a distributive lattice. (Contributed by Stefan O'Rear, 30-Jan-2015.)
Hypotheses
Ref Expression
isdlat.b 𝐡 = (Baseβ€˜πΎ)
isdlat.j ∨ = (joinβ€˜πΎ)
isdlat.m ∧ = (meetβ€˜πΎ)
Assertion
Ref Expression
isdlat (𝐾 ∈ DLat ↔ (𝐾 ∈ Lat ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 (π‘₯ ∧ (𝑦 ∨ 𝑧)) = ((π‘₯ ∧ 𝑦) ∨ (π‘₯ ∧ 𝑧))))
Distinct variable groups:   π‘₯,𝑦,𝑧,𝐾   π‘₯,𝐡,𝑦,𝑧   π‘₯, ∨ ,𝑦,𝑧   π‘₯, ∧ ,𝑦,𝑧

Proof of Theorem isdlat
Dummy variables π‘˜ 𝑏 𝑗 π‘š are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6846 . . . . 5 (π‘˜ = 𝐾 β†’ (Baseβ€˜π‘˜) = (Baseβ€˜πΎ))
2 isdlat.b . . . . 5 𝐡 = (Baseβ€˜πΎ)
31, 2eqtr4di 2791 . . . 4 (π‘˜ = 𝐾 β†’ (Baseβ€˜π‘˜) = 𝐡)
4 fveq2 6846 . . . . . 6 (π‘˜ = 𝐾 β†’ (joinβ€˜π‘˜) = (joinβ€˜πΎ))
5 isdlat.j . . . . . 6 ∨ = (joinβ€˜πΎ)
64, 5eqtr4di 2791 . . . . 5 (π‘˜ = 𝐾 β†’ (joinβ€˜π‘˜) = ∨ )
7 fveq2 6846 . . . . . . 7 (π‘˜ = 𝐾 β†’ (meetβ€˜π‘˜) = (meetβ€˜πΎ))
8 isdlat.m . . . . . . 7 ∧ = (meetβ€˜πΎ)
97, 8eqtr4di 2791 . . . . . 6 (π‘˜ = 𝐾 β†’ (meetβ€˜π‘˜) = ∧ )
109sbceq1d 3748 . . . . 5 (π‘˜ = 𝐾 β†’ ([(meetβ€˜π‘˜) / π‘š]βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 βˆ€π‘§ ∈ 𝑏 (π‘₯π‘š(𝑦𝑗𝑧)) = ((π‘₯π‘šπ‘¦)𝑗(π‘₯π‘šπ‘§)) ↔ [ ∧ / π‘š]βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 βˆ€π‘§ ∈ 𝑏 (π‘₯π‘š(𝑦𝑗𝑧)) = ((π‘₯π‘šπ‘¦)𝑗(π‘₯π‘šπ‘§))))
116, 10sbceqbid 3750 . . . 4 (π‘˜ = 𝐾 β†’ ([(joinβ€˜π‘˜) / 𝑗][(meetβ€˜π‘˜) / π‘š]βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 βˆ€π‘§ ∈ 𝑏 (π‘₯π‘š(𝑦𝑗𝑧)) = ((π‘₯π‘šπ‘¦)𝑗(π‘₯π‘šπ‘§)) ↔ [ ∨ / 𝑗][ ∧ / π‘š]βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 βˆ€π‘§ ∈ 𝑏 (π‘₯π‘š(𝑦𝑗𝑧)) = ((π‘₯π‘šπ‘¦)𝑗(π‘₯π‘šπ‘§))))
123, 11sbceqbid 3750 . . 3 (π‘˜ = 𝐾 β†’ ([(Baseβ€˜π‘˜) / 𝑏][(joinβ€˜π‘˜) / 𝑗][(meetβ€˜π‘˜) / π‘š]βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 βˆ€π‘§ ∈ 𝑏 (π‘₯π‘š(𝑦𝑗𝑧)) = ((π‘₯π‘šπ‘¦)𝑗(π‘₯π‘šπ‘§)) ↔ [𝐡 / 𝑏][ ∨ / 𝑗][ ∧ / π‘š]βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 βˆ€π‘§ ∈ 𝑏 (π‘₯π‘š(𝑦𝑗𝑧)) = ((π‘₯π‘šπ‘¦)𝑗(π‘₯π‘šπ‘§))))
132fvexi 6860 . . . 4 𝐡 ∈ V
145fvexi 6860 . . . 4 ∨ ∈ V
158fvexi 6860 . . . 4 ∧ ∈ V
16 raleq 3308 . . . . . . . 8 (𝑏 = 𝐡 β†’ (βˆ€π‘§ ∈ 𝑏 (π‘₯π‘š(𝑦𝑗𝑧)) = ((π‘₯π‘šπ‘¦)𝑗(π‘₯π‘šπ‘§)) ↔ βˆ€π‘§ ∈ 𝐡 (π‘₯π‘š(𝑦𝑗𝑧)) = ((π‘₯π‘šπ‘¦)𝑗(π‘₯π‘šπ‘§))))
1716raleqbi1dv 3306 . . . . . . 7 (𝑏 = 𝐡 β†’ (βˆ€π‘¦ ∈ 𝑏 βˆ€π‘§ ∈ 𝑏 (π‘₯π‘š(𝑦𝑗𝑧)) = ((π‘₯π‘šπ‘¦)𝑗(π‘₯π‘šπ‘§)) ↔ βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 (π‘₯π‘š(𝑦𝑗𝑧)) = ((π‘₯π‘šπ‘¦)𝑗(π‘₯π‘šπ‘§))))
1817raleqbi1dv 3306 . . . . . 6 (𝑏 = 𝐡 β†’ (βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 βˆ€π‘§ ∈ 𝑏 (π‘₯π‘š(𝑦𝑗𝑧)) = ((π‘₯π‘šπ‘¦)𝑗(π‘₯π‘šπ‘§)) ↔ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 (π‘₯π‘š(𝑦𝑗𝑧)) = ((π‘₯π‘šπ‘¦)𝑗(π‘₯π‘šπ‘§))))
19 simpr 486 . . . . . . . . . 10 ((𝑗 = ∨ ∧ π‘š = ∧ ) β†’ π‘š = ∧ )
20 eqidd 2734 . . . . . . . . . 10 ((𝑗 = ∨ ∧ π‘š = ∧ ) β†’ π‘₯ = π‘₯)
21 simpl 484 . . . . . . . . . . 11 ((𝑗 = ∨ ∧ π‘š = ∧ ) β†’ 𝑗 = ∨ )
2221oveqd 7378 . . . . . . . . . 10 ((𝑗 = ∨ ∧ π‘š = ∧ ) β†’ (𝑦𝑗𝑧) = (𝑦 ∨ 𝑧))
2319, 20, 22oveq123d 7382 . . . . . . . . 9 ((𝑗 = ∨ ∧ π‘š = ∧ ) β†’ (π‘₯π‘š(𝑦𝑗𝑧)) = (π‘₯ ∧ (𝑦 ∨ 𝑧)))
2419oveqd 7378 . . . . . . . . . 10 ((𝑗 = ∨ ∧ π‘š = ∧ ) β†’ (π‘₯π‘šπ‘¦) = (π‘₯ ∧ 𝑦))
2519oveqd 7378 . . . . . . . . . 10 ((𝑗 = ∨ ∧ π‘š = ∧ ) β†’ (π‘₯π‘šπ‘§) = (π‘₯ ∧ 𝑧))
2621, 24, 25oveq123d 7382 . . . . . . . . 9 ((𝑗 = ∨ ∧ π‘š = ∧ ) β†’ ((π‘₯π‘šπ‘¦)𝑗(π‘₯π‘šπ‘§)) = ((π‘₯ ∧ 𝑦) ∨ (π‘₯ ∧ 𝑧)))
2723, 26eqeq12d 2749 . . . . . . . 8 ((𝑗 = ∨ ∧ π‘š = ∧ ) β†’ ((π‘₯π‘š(𝑦𝑗𝑧)) = ((π‘₯π‘šπ‘¦)𝑗(π‘₯π‘šπ‘§)) ↔ (π‘₯ ∧ (𝑦 ∨ 𝑧)) = ((π‘₯ ∧ 𝑦) ∨ (π‘₯ ∧ 𝑧))))
2827ralbidv 3171 . . . . . . 7 ((𝑗 = ∨ ∧ π‘š = ∧ ) β†’ (βˆ€π‘§ ∈ 𝐡 (π‘₯π‘š(𝑦𝑗𝑧)) = ((π‘₯π‘šπ‘¦)𝑗(π‘₯π‘šπ‘§)) ↔ βˆ€π‘§ ∈ 𝐡 (π‘₯ ∧ (𝑦 ∨ 𝑧)) = ((π‘₯ ∧ 𝑦) ∨ (π‘₯ ∧ 𝑧))))
29282ralbidv 3209 . . . . . 6 ((𝑗 = ∨ ∧ π‘š = ∧ ) β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 (π‘₯π‘š(𝑦𝑗𝑧)) = ((π‘₯π‘šπ‘¦)𝑗(π‘₯π‘šπ‘§)) ↔ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 (π‘₯ ∧ (𝑦 ∨ 𝑧)) = ((π‘₯ ∧ 𝑦) ∨ (π‘₯ ∧ 𝑧))))
3018, 29sylan9bb 511 . . . . 5 ((𝑏 = 𝐡 ∧ (𝑗 = ∨ ∧ π‘š = ∧ )) β†’ (βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 βˆ€π‘§ ∈ 𝑏 (π‘₯π‘š(𝑦𝑗𝑧)) = ((π‘₯π‘šπ‘¦)𝑗(π‘₯π‘šπ‘§)) ↔ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 (π‘₯ ∧ (𝑦 ∨ 𝑧)) = ((π‘₯ ∧ 𝑦) ∨ (π‘₯ ∧ 𝑧))))
31303impb 1116 . . . 4 ((𝑏 = 𝐡 ∧ 𝑗 = ∨ ∧ π‘š = ∧ ) β†’ (βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 βˆ€π‘§ ∈ 𝑏 (π‘₯π‘š(𝑦𝑗𝑧)) = ((π‘₯π‘šπ‘¦)𝑗(π‘₯π‘šπ‘§)) ↔ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 (π‘₯ ∧ (𝑦 ∨ 𝑧)) = ((π‘₯ ∧ 𝑦) ∨ (π‘₯ ∧ 𝑧))))
3213, 14, 15, 31sbc3ie 3829 . . 3 ([𝐡 / 𝑏][ ∨ / 𝑗][ ∧ / π‘š]βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 βˆ€π‘§ ∈ 𝑏 (π‘₯π‘š(𝑦𝑗𝑧)) = ((π‘₯π‘šπ‘¦)𝑗(π‘₯π‘šπ‘§)) ↔ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 (π‘₯ ∧ (𝑦 ∨ 𝑧)) = ((π‘₯ ∧ 𝑦) ∨ (π‘₯ ∧ 𝑧)))
3312, 32bitrdi 287 . 2 (π‘˜ = 𝐾 β†’ ([(Baseβ€˜π‘˜) / 𝑏][(joinβ€˜π‘˜) / 𝑗][(meetβ€˜π‘˜) / π‘š]βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 βˆ€π‘§ ∈ 𝑏 (π‘₯π‘š(𝑦𝑗𝑧)) = ((π‘₯π‘šπ‘¦)𝑗(π‘₯π‘šπ‘§)) ↔ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 (π‘₯ ∧ (𝑦 ∨ 𝑧)) = ((π‘₯ ∧ 𝑦) ∨ (π‘₯ ∧ 𝑧))))
34 df-dlat 18418 . 2 DLat = {π‘˜ ∈ Lat ∣ [(Baseβ€˜π‘˜) / 𝑏][(joinβ€˜π‘˜) / 𝑗][(meetβ€˜π‘˜) / π‘š]βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 βˆ€π‘§ ∈ 𝑏 (π‘₯π‘š(𝑦𝑗𝑧)) = ((π‘₯π‘šπ‘¦)𝑗(π‘₯π‘šπ‘§))}
3533, 34elrab2 3652 1 (𝐾 ∈ DLat ↔ (𝐾 ∈ Lat ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 βˆ€π‘§ ∈ 𝐡 (π‘₯ ∧ (𝑦 ∨ 𝑧)) = ((π‘₯ ∧ 𝑦) ∨ (π‘₯ ∧ 𝑧))))
Colors of variables: wff setvar class
Syntax hints:   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  βˆ€wral 3061  [wsbc 3743  β€˜cfv 6500  (class class class)co 7361  Basecbs 17091  joincjn 18208  meetcmee 18209  Latclat 18328  DLatcdlat 18417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5267
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2941  df-ral 3062  df-rab 3407  df-v 3449  df-sbc 3744  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-br 5110  df-iota 6452  df-fv 6508  df-ov 7364  df-dlat 18418
This theorem is referenced by:  dlatmjdi  18420  dlatl  18421  odudlatb  18422  topdlat  47119
  Copyright terms: Public domain W3C validator