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

Theorem diaffval 38477
 Description: The partial isomorphism A for a lattice 𝐾. (Contributed by NM, 15-Oct-2013.)
Hypotheses
Ref Expression
diaval.b 𝐵 = (Base‘𝐾)
diaval.l = (le‘𝐾)
diaval.h 𝐻 = (LHyp‘𝐾)
Assertion
Ref Expression
diaffval (𝐾𝑉 → (DIsoA‘𝐾) = (𝑤𝐻 ↦ (𝑥 ∈ {𝑦𝐵𝑦 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) 𝑥})))
Distinct variable groups:   𝑥,𝑤,𝑦,   𝑤,𝐵,𝑥,𝑦   𝑤,𝐻   𝑤,𝑓,𝑥,𝑦,𝐾
Allowed substitution hints:   𝐵(𝑓)   𝐻(𝑥,𝑦,𝑓)   (𝑓)   𝑉(𝑥,𝑦,𝑤,𝑓)

Proof of Theorem diaffval
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 elex 3460 . 2 (𝐾𝑉𝐾 ∈ V)
2 fveq2 6655 . . . . 5 (𝑘 = 𝐾 → (LHyp‘𝑘) = (LHyp‘𝐾))
3 diaval.h . . . . 5 𝐻 = (LHyp‘𝐾)
42, 3eqtr4di 2851 . . . 4 (𝑘 = 𝐾 → (LHyp‘𝑘) = 𝐻)
5 fveq2 6655 . . . . . . 7 (𝑘 = 𝐾 → (Base‘𝑘) = (Base‘𝐾))
6 diaval.b . . . . . . 7 𝐵 = (Base‘𝐾)
75, 6eqtr4di 2851 . . . . . 6 (𝑘 = 𝐾 → (Base‘𝑘) = 𝐵)
8 fveq2 6655 . . . . . . . 8 (𝑘 = 𝐾 → (le‘𝑘) = (le‘𝐾))
9 diaval.l . . . . . . . 8 = (le‘𝐾)
108, 9eqtr4di 2851 . . . . . . 7 (𝑘 = 𝐾 → (le‘𝑘) = )
1110breqd 5045 . . . . . 6 (𝑘 = 𝐾 → (𝑦(le‘𝑘)𝑤𝑦 𝑤))
127, 11rabeqbidv 3434 . . . . 5 (𝑘 = 𝐾 → {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} = {𝑦𝐵𝑦 𝑤})
13 fveq2 6655 . . . . . . 7 (𝑘 = 𝐾 → (LTrn‘𝑘) = (LTrn‘𝐾))
1413fveq1d 6657 . . . . . 6 (𝑘 = 𝐾 → ((LTrn‘𝑘)‘𝑤) = ((LTrn‘𝐾)‘𝑤))
15 fveq2 6655 . . . . . . . . 9 (𝑘 = 𝐾 → (trL‘𝑘) = (trL‘𝐾))
1615fveq1d 6657 . . . . . . . 8 (𝑘 = 𝐾 → ((trL‘𝑘)‘𝑤) = ((trL‘𝐾)‘𝑤))
1716fveq1d 6657 . . . . . . 7 (𝑘 = 𝐾 → (((trL‘𝑘)‘𝑤)‘𝑓) = (((trL‘𝐾)‘𝑤)‘𝑓))
18 eqidd 2799 . . . . . . 7 (𝑘 = 𝐾𝑥 = 𝑥)
1917, 10, 18breq123d 5048 . . . . . 6 (𝑘 = 𝐾 → ((((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥 ↔ (((trL‘𝐾)‘𝑤)‘𝑓) 𝑥))
2014, 19rabeqbidv 3434 . . . . 5 (𝑘 = 𝐾 → {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥} = {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) 𝑥})
2112, 20mpteq12dv 5119 . . . 4 (𝑘 = 𝐾 → (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥}) = (𝑥 ∈ {𝑦𝐵𝑦 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) 𝑥}))
224, 21mpteq12dv 5119 . . 3 (𝑘 = 𝐾 → (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥})) = (𝑤𝐻 ↦ (𝑥 ∈ {𝑦𝐵𝑦 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) 𝑥})))
23 df-disoa 38476 . . 3 DIsoA = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥})))
2422, 23, 3mptfvmpt 6978 . 2 (𝐾 ∈ V → (DIsoA‘𝐾) = (𝑤𝐻 ↦ (𝑥 ∈ {𝑦𝐵𝑦 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) 𝑥})))
251, 24syl 17 1 (𝐾𝑉 → (DIsoA‘𝐾) = (𝑤𝐻 ↦ (𝑥 ∈ {𝑦𝐵𝑦 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) 𝑥})))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  {crab 3110  Vcvv 3442   class class class wbr 5034   ↦ cmpt 5114  ‘cfv 6332  Basecbs 16495  lecple 16584  LHypclh 37431  LTrncltrn 37548  trLctrl 37605  DIsoAcdia 38475 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5158  ax-sep 5171  ax-nul 5178  ax-pr 5299 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4805  df-iun 4887  df-br 5035  df-opab 5097  df-mpt 5115  df-id 5429  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-fv 6340  df-disoa 38476 This theorem is referenced by:  diafval  38478
 Copyright terms: Public domain W3C validator