Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ltrnfset Structured version   Visualization version   GIF version

Theorem ltrnfset 36797
Description: The set of all lattice translations for a lattice 𝐾. (Contributed by NM, 11-May-2012.)
Hypotheses
Ref Expression
ltrnset.l = (le‘𝐾)
ltrnset.j = (join‘𝐾)
ltrnset.m = (meet‘𝐾)
ltrnset.a 𝐴 = (Atoms‘𝐾)
ltrnset.h 𝐻 = (LHyp‘𝐾)
Assertion
Ref Expression
ltrnfset (𝐾𝐶 → (LTrn‘𝐾) = (𝑤𝐻 ↦ {𝑓 ∈ ((LDil‘𝐾)‘𝑤) ∣ ∀𝑝𝐴𝑞𝐴 ((¬ 𝑝 𝑤 ∧ ¬ 𝑞 𝑤) → ((𝑝 (𝑓𝑝)) 𝑤) = ((𝑞 (𝑓𝑞)) 𝑤))}))
Distinct variable groups:   𝑞,𝑝,𝐴   𝑤,𝐻   𝑓,𝑝,𝑞,𝑤,𝐾
Allowed substitution hints:   𝐴(𝑤,𝑓)   𝐶(𝑤,𝑓,𝑞,𝑝)   𝐻(𝑓,𝑞,𝑝)   (𝑤,𝑓,𝑞,𝑝)   (𝑤,𝑓,𝑞,𝑝)   (𝑤,𝑓,𝑞,𝑝)

Proof of Theorem ltrnfset
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 elex 3454 . 2 (𝐾𝐶𝐾 ∈ V)
2 fveq2 6541 . . . . 5 (𝑘 = 𝐾 → (LHyp‘𝑘) = (LHyp‘𝐾))
3 ltrnset.h . . . . 5 𝐻 = (LHyp‘𝐾)
42, 3syl6eqr 2848 . . . 4 (𝑘 = 𝐾 → (LHyp‘𝑘) = 𝐻)
5 fveq2 6541 . . . . . 6 (𝑘 = 𝐾 → (LDil‘𝑘) = (LDil‘𝐾))
65fveq1d 6543 . . . . 5 (𝑘 = 𝐾 → ((LDil‘𝑘)‘𝑤) = ((LDil‘𝐾)‘𝑤))
7 fveq2 6541 . . . . . . 7 (𝑘 = 𝐾 → (Atoms‘𝑘) = (Atoms‘𝐾))
8 ltrnset.a . . . . . . 7 𝐴 = (Atoms‘𝐾)
97, 8syl6eqr 2848 . . . . . 6 (𝑘 = 𝐾 → (Atoms‘𝑘) = 𝐴)
10 fveq2 6541 . . . . . . . . . . . 12 (𝑘 = 𝐾 → (le‘𝑘) = (le‘𝐾))
11 ltrnset.l . . . . . . . . . . . 12 = (le‘𝐾)
1210, 11syl6eqr 2848 . . . . . . . . . . 11 (𝑘 = 𝐾 → (le‘𝑘) = )
1312breqd 4975 . . . . . . . . . 10 (𝑘 = 𝐾 → (𝑝(le‘𝑘)𝑤𝑝 𝑤))
1413notbid 319 . . . . . . . . 9 (𝑘 = 𝐾 → (¬ 𝑝(le‘𝑘)𝑤 ↔ ¬ 𝑝 𝑤))
1512breqd 4975 . . . . . . . . . 10 (𝑘 = 𝐾 → (𝑞(le‘𝑘)𝑤𝑞 𝑤))
1615notbid 319 . . . . . . . . 9 (𝑘 = 𝐾 → (¬ 𝑞(le‘𝑘)𝑤 ↔ ¬ 𝑞 𝑤))
1714, 16anbi12d 630 . . . . . . . 8 (𝑘 = 𝐾 → ((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) ↔ (¬ 𝑝 𝑤 ∧ ¬ 𝑞 𝑤)))
18 fveq2 6541 . . . . . . . . . . 11 (𝑘 = 𝐾 → (meet‘𝑘) = (meet‘𝐾))
19 ltrnset.m . . . . . . . . . . 11 = (meet‘𝐾)
2018, 19syl6eqr 2848 . . . . . . . . . 10 (𝑘 = 𝐾 → (meet‘𝑘) = )
21 fveq2 6541 . . . . . . . . . . . 12 (𝑘 = 𝐾 → (join‘𝑘) = (join‘𝐾))
22 ltrnset.j . . . . . . . . . . . 12 = (join‘𝐾)
2321, 22syl6eqr 2848 . . . . . . . . . . 11 (𝑘 = 𝐾 → (join‘𝑘) = )
2423oveqd 7036 . . . . . . . . . 10 (𝑘 = 𝐾 → (𝑝(join‘𝑘)(𝑓𝑝)) = (𝑝 (𝑓𝑝)))
25 eqidd 2795 . . . . . . . . . 10 (𝑘 = 𝐾𝑤 = 𝑤)
2620, 24, 25oveq123d 7040 . . . . . . . . 9 (𝑘 = 𝐾 → ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤) = ((𝑝 (𝑓𝑝)) 𝑤))
2723oveqd 7036 . . . . . . . . . 10 (𝑘 = 𝐾 → (𝑞(join‘𝑘)(𝑓𝑞)) = (𝑞 (𝑓𝑞)))
2820, 27, 25oveq123d 7040 . . . . . . . . 9 (𝑘 = 𝐾 → ((𝑞(join‘𝑘)(𝑓𝑞))(meet‘𝑘)𝑤) = ((𝑞 (𝑓𝑞)) 𝑤))
2926, 28eqeq12d 2809 . . . . . . . 8 (𝑘 = 𝐾 → (((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓𝑞))(meet‘𝑘)𝑤) ↔ ((𝑝 (𝑓𝑝)) 𝑤) = ((𝑞 (𝑓𝑞)) 𝑤)))
3017, 29imbi12d 346 . . . . . . 7 (𝑘 = 𝐾 → (((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓𝑞))(meet‘𝑘)𝑤)) ↔ ((¬ 𝑝 𝑤 ∧ ¬ 𝑞 𝑤) → ((𝑝 (𝑓𝑝)) 𝑤) = ((𝑞 (𝑓𝑞)) 𝑤))))
319, 30raleqbidv 3360 . . . . . 6 (𝑘 = 𝐾 → (∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓𝑞))(meet‘𝑘)𝑤)) ↔ ∀𝑞𝐴 ((¬ 𝑝 𝑤 ∧ ¬ 𝑞 𝑤) → ((𝑝 (𝑓𝑝)) 𝑤) = ((𝑞 (𝑓𝑞)) 𝑤))))
329, 31raleqbidv 3360 . . . . 5 (𝑘 = 𝐾 → (∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓𝑞))(meet‘𝑘)𝑤)) ↔ ∀𝑝𝐴𝑞𝐴 ((¬ 𝑝 𝑤 ∧ ¬ 𝑞 𝑤) → ((𝑝 (𝑓𝑝)) 𝑤) = ((𝑞 (𝑓𝑞)) 𝑤))))
336, 32rabeqbidv 3429 . . . 4 (𝑘 = 𝐾 → {𝑓 ∈ ((LDil‘𝑘)‘𝑤) ∣ ∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓𝑞))(meet‘𝑘)𝑤))} = {𝑓 ∈ ((LDil‘𝐾)‘𝑤) ∣ ∀𝑝𝐴𝑞𝐴 ((¬ 𝑝 𝑤 ∧ ¬ 𝑞 𝑤) → ((𝑝 (𝑓𝑝)) 𝑤) = ((𝑞 (𝑓𝑞)) 𝑤))})
344, 33mpteq12dv 5048 . . 3 (𝑘 = 𝐾 → (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∈ ((LDil‘𝑘)‘𝑤) ∣ ∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓𝑞))(meet‘𝑘)𝑤))}) = (𝑤𝐻 ↦ {𝑓 ∈ ((LDil‘𝐾)‘𝑤) ∣ ∀𝑝𝐴𝑞𝐴 ((¬ 𝑝 𝑤 ∧ ¬ 𝑞 𝑤) → ((𝑝 (𝑓𝑝)) 𝑤) = ((𝑞 (𝑓𝑞)) 𝑤))}))
35 df-ltrn 36785 . . 3 LTrn = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∈ ((LDil‘𝑘)‘𝑤) ∣ ∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓𝑞))(meet‘𝑘)𝑤))}))
3634, 35, 3mptfvmpt 6859 . 2 (𝐾 ∈ V → (LTrn‘𝐾) = (𝑤𝐻 ↦ {𝑓 ∈ ((LDil‘𝐾)‘𝑤) ∣ ∀𝑝𝐴𝑞𝐴 ((¬ 𝑝 𝑤 ∧ ¬ 𝑞 𝑤) → ((𝑝 (𝑓𝑝)) 𝑤) = ((𝑞 (𝑓𝑞)) 𝑤))}))
371, 36syl 17 1 (𝐾𝐶 → (LTrn‘𝐾) = (𝑤𝐻 ↦ {𝑓 ∈ ((LDil‘𝐾)‘𝑤) ∣ ∀𝑝𝐴𝑞𝐴 ((¬ 𝑝 𝑤 ∧ ¬ 𝑞 𝑤) → ((𝑝 (𝑓𝑝)) 𝑤) = ((𝑞 (𝑓𝑞)) 𝑤))}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396   = wceq 1522  wcel 2080  wral 3104  {crab 3108  Vcvv 3436   class class class wbr 4964  cmpt 5043  cfv 6228  (class class class)co 7019  lecple 16401  joincjn 17383  meetcmee 17384  Atomscatm 35943  LHypclh 36664  LDilcldil 36780  LTrncltrn 36781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-13 2343  ax-ext 2768  ax-rep 5084  ax-sep 5097  ax-nul 5104  ax-pr 5224
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-mo 2575  df-eu 2611  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-ne 2984  df-ral 3109  df-rex 3110  df-reu 3111  df-rab 3113  df-v 3438  df-sbc 3708  df-csb 3814  df-dif 3864  df-un 3866  df-in 3868  df-ss 3876  df-nul 4214  df-if 4384  df-sn 4475  df-pr 4477  df-op 4481  df-uni 4748  df-iun 4829  df-br 4965  df-opab 5027  df-mpt 5044  df-id 5351  df-xp 5452  df-rel 5453  df-cnv 5454  df-co 5455  df-dm 5456  df-rn 5457  df-res 5458  df-ima 5459  df-iota 6192  df-fun 6230  df-fn 6231  df-f 6232  df-f1 6233  df-fo 6234  df-f1o 6235  df-fv 6236  df-ov 7022  df-ltrn 36785
This theorem is referenced by:  ltrnset  36798
  Copyright terms: Public domain W3C validator