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

Theorem diaffval 36138
 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 3207 . 2 (𝐾𝑉𝐾 ∈ V)
2 fveq2 6178 . . . . 5 (𝑘 = 𝐾 → (LHyp‘𝑘) = (LHyp‘𝐾))
3 diaval.h . . . . 5 𝐻 = (LHyp‘𝐾)
42, 3syl6eqr 2672 . . . 4 (𝑘 = 𝐾 → (LHyp‘𝑘) = 𝐻)
5 fveq2 6178 . . . . . . 7 (𝑘 = 𝐾 → (Base‘𝑘) = (Base‘𝐾))
6 diaval.b . . . . . . 7 𝐵 = (Base‘𝐾)
75, 6syl6eqr 2672 . . . . . 6 (𝑘 = 𝐾 → (Base‘𝑘) = 𝐵)
8 fveq2 6178 . . . . . . . 8 (𝑘 = 𝐾 → (le‘𝑘) = (le‘𝐾))
9 diaval.l . . . . . . . 8 = (le‘𝐾)
108, 9syl6eqr 2672 . . . . . . 7 (𝑘 = 𝐾 → (le‘𝑘) = )
1110breqd 4655 . . . . . 6 (𝑘 = 𝐾 → (𝑦(le‘𝑘)𝑤𝑦 𝑤))
127, 11rabeqbidv 3190 . . . . 5 (𝑘 = 𝐾 → {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} = {𝑦𝐵𝑦 𝑤})
13 fveq2 6178 . . . . . . 7 (𝑘 = 𝐾 → (LTrn‘𝑘) = (LTrn‘𝐾))
1413fveq1d 6180 . . . . . 6 (𝑘 = 𝐾 → ((LTrn‘𝑘)‘𝑤) = ((LTrn‘𝐾)‘𝑤))
15 fveq2 6178 . . . . . . . . 9 (𝑘 = 𝐾 → (trL‘𝑘) = (trL‘𝐾))
1615fveq1d 6180 . . . . . . . 8 (𝑘 = 𝐾 → ((trL‘𝑘)‘𝑤) = ((trL‘𝐾)‘𝑤))
1716fveq1d 6180 . . . . . . 7 (𝑘 = 𝐾 → (((trL‘𝑘)‘𝑤)‘𝑓) = (((trL‘𝐾)‘𝑤)‘𝑓))
18 eqidd 2621 . . . . . . 7 (𝑘 = 𝐾𝑥 = 𝑥)
1917, 10, 18breq123d 4658 . . . . . 6 (𝑘 = 𝐾 → ((((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥 ↔ (((trL‘𝐾)‘𝑤)‘𝑓) 𝑥))
2014, 19rabeqbidv 3190 . . . . 5 (𝑘 = 𝐾 → {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥} = {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) 𝑥})
2112, 20mpteq12dv 4724 . . . 4 (𝑘 = 𝐾 → (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥}) = (𝑥 ∈ {𝑦𝐵𝑦 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) 𝑥}))
224, 21mpteq12dv 4724 . . 3 (𝑘 = 𝐾 → (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥})) = (𝑤𝐻 ↦ (𝑥 ∈ {𝑦𝐵𝑦 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) 𝑥})))
23 df-disoa 36137 . . 3 DIsoA = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥})))
24 fvex 6188 . . . . 5 (LHyp‘𝐾) ∈ V
253, 24eqeltri 2695 . . . 4 𝐻 ∈ V
2625mptex 6471 . . 3 (𝑤𝐻 ↦ (𝑥 ∈ {𝑦𝐵𝑦 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) 𝑥})) ∈ V
2722, 23, 26fvmpt 6269 . 2 (𝐾 ∈ V → (DIsoA‘𝐾) = (𝑤𝐻 ↦ (𝑥 ∈ {𝑦𝐵𝑦 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) 𝑥})))
281, 27syl 17 1 (𝐾𝑉 → (DIsoA‘𝐾) = (𝑤𝐻 ↦ (𝑥 ∈ {𝑦𝐵𝑦 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) 𝑥})))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1481   ∈ wcel 1988  {crab 2913  Vcvv 3195   class class class wbr 4644   ↦ cmpt 4720  ‘cfv 5876  Basecbs 15838  lecple 15929  LHypclh 35089  LTrncltrn 35206  trLctrl 35264  DIsoAcdia 36136 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pr 4897 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-reu 2916  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-disoa 36137 This theorem is referenced by:  diafval  36139
 Copyright terms: Public domain W3C validator