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

Theorem dihffval 40404
Description: The isomorphism H for a lattice 𝐾. Definition of isomorphism map in [Crawley] p. 122 line 3. (Contributed by NM, 28-Jan-2014.)
Hypotheses
Ref Expression
dihval.b 𝐵 = (Base‘𝐾)
dihval.l = (le‘𝐾)
dihval.j = (join‘𝐾)
dihval.m = (meet‘𝐾)
dihval.a 𝐴 = (Atoms‘𝐾)
dihval.h 𝐻 = (LHyp‘𝐾)
Assertion
Ref Expression
dihffval (𝐾𝑉 → (DIsoH‘𝐾) = (𝑤𝐻 ↦ (𝑥𝐵 ↦ if(𝑥 𝑤, (((DIsoB‘𝐾)‘𝑤)‘𝑥), (𝑢 ∈ (LSubSp‘((DVecH‘𝐾)‘𝑤))∀𝑞𝐴 ((¬ 𝑞 𝑤 ∧ (𝑞 (𝑥 𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝐾)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝐾)‘𝑤))(((DIsoB‘𝐾)‘𝑤)‘(𝑥 𝑤)))))))))
Distinct variable groups:   𝐴,𝑞   𝑤,𝐻   𝑢,𝑞,𝑤,𝑥,𝐾
Allowed substitution hints:   𝐴(𝑥,𝑤,𝑢)   𝐵(𝑥,𝑤,𝑢,𝑞)   𝐻(𝑥,𝑢,𝑞)   (𝑥,𝑤,𝑢,𝑞)   (𝑥,𝑤,𝑢,𝑞)   (𝑥,𝑤,𝑢,𝑞)   𝑉(𝑥,𝑤,𝑢,𝑞)

Proof of Theorem dihffval
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 elex 3491 . 2 (𝐾𝑉𝐾 ∈ V)
2 fveq2 6890 . . . . 5 (𝑘 = 𝐾 → (LHyp‘𝑘) = (LHyp‘𝐾))
3 dihval.h . . . . 5 𝐻 = (LHyp‘𝐾)
42, 3eqtr4di 2788 . . . 4 (𝑘 = 𝐾 → (LHyp‘𝑘) = 𝐻)
5 fveq2 6890 . . . . . 6 (𝑘 = 𝐾 → (Base‘𝑘) = (Base‘𝐾))
6 dihval.b . . . . . 6 𝐵 = (Base‘𝐾)
75, 6eqtr4di 2788 . . . . 5 (𝑘 = 𝐾 → (Base‘𝑘) = 𝐵)
8 fveq2 6890 . . . . . . . 8 (𝑘 = 𝐾 → (le‘𝑘) = (le‘𝐾))
9 dihval.l . . . . . . . 8 = (le‘𝐾)
108, 9eqtr4di 2788 . . . . . . 7 (𝑘 = 𝐾 → (le‘𝑘) = )
1110breqd 5158 . . . . . 6 (𝑘 = 𝐾 → (𝑥(le‘𝑘)𝑤𝑥 𝑤))
12 fveq2 6890 . . . . . . . 8 (𝑘 = 𝐾 → (DIsoB‘𝑘) = (DIsoB‘𝐾))
1312fveq1d 6892 . . . . . . 7 (𝑘 = 𝐾 → ((DIsoB‘𝑘)‘𝑤) = ((DIsoB‘𝐾)‘𝑤))
1413fveq1d 6892 . . . . . 6 (𝑘 = 𝐾 → (((DIsoB‘𝑘)‘𝑤)‘𝑥) = (((DIsoB‘𝐾)‘𝑤)‘𝑥))
15 fveq2 6890 . . . . . . . . 9 (𝑘 = 𝐾 → (DVecH‘𝑘) = (DVecH‘𝐾))
1615fveq1d 6892 . . . . . . . 8 (𝑘 = 𝐾 → ((DVecH‘𝑘)‘𝑤) = ((DVecH‘𝐾)‘𝑤))
1716fveq2d 6894 . . . . . . 7 (𝑘 = 𝐾 → (LSubSp‘((DVecH‘𝑘)‘𝑤)) = (LSubSp‘((DVecH‘𝐾)‘𝑤)))
18 fveq2 6890 . . . . . . . . 9 (𝑘 = 𝐾 → (Atoms‘𝑘) = (Atoms‘𝐾))
19 dihval.a . . . . . . . . 9 𝐴 = (Atoms‘𝐾)
2018, 19eqtr4di 2788 . . . . . . . 8 (𝑘 = 𝐾 → (Atoms‘𝑘) = 𝐴)
2110breqd 5158 . . . . . . . . . . 11 (𝑘 = 𝐾 → (𝑞(le‘𝑘)𝑤𝑞 𝑤))
2221notbid 317 . . . . . . . . . 10 (𝑘 = 𝐾 → (¬ 𝑞(le‘𝑘)𝑤 ↔ ¬ 𝑞 𝑤))
23 fveq2 6890 . . . . . . . . . . . . 13 (𝑘 = 𝐾 → (join‘𝑘) = (join‘𝐾))
24 dihval.j . . . . . . . . . . . . 13 = (join‘𝐾)
2523, 24eqtr4di 2788 . . . . . . . . . . . 12 (𝑘 = 𝐾 → (join‘𝑘) = )
26 eqidd 2731 . . . . . . . . . . . 12 (𝑘 = 𝐾𝑞 = 𝑞)
27 fveq2 6890 . . . . . . . . . . . . . 14 (𝑘 = 𝐾 → (meet‘𝑘) = (meet‘𝐾))
28 dihval.m . . . . . . . . . . . . . 14 = (meet‘𝐾)
2927, 28eqtr4di 2788 . . . . . . . . . . . . 13 (𝑘 = 𝐾 → (meet‘𝑘) = )
3029oveqd 7428 . . . . . . . . . . . 12 (𝑘 = 𝐾 → (𝑥(meet‘𝑘)𝑤) = (𝑥 𝑤))
3125, 26, 30oveq123d 7432 . . . . . . . . . . 11 (𝑘 = 𝐾 → (𝑞(join‘𝑘)(𝑥(meet‘𝑘)𝑤)) = (𝑞 (𝑥 𝑤)))
3231eqeq1d 2732 . . . . . . . . . 10 (𝑘 = 𝐾 → ((𝑞(join‘𝑘)(𝑥(meet‘𝑘)𝑤)) = 𝑥 ↔ (𝑞 (𝑥 𝑤)) = 𝑥))
3322, 32anbi12d 629 . . . . . . . . 9 (𝑘 = 𝐾 → ((¬ 𝑞(le‘𝑘)𝑤 ∧ (𝑞(join‘𝑘)(𝑥(meet‘𝑘)𝑤)) = 𝑥) ↔ (¬ 𝑞 𝑤 ∧ (𝑞 (𝑥 𝑤)) = 𝑥)))
3416fveq2d 6894 . . . . . . . . . . 11 (𝑘 = 𝐾 → (LSSum‘((DVecH‘𝑘)‘𝑤)) = (LSSum‘((DVecH‘𝐾)‘𝑤)))
35 fveq2 6890 . . . . . . . . . . . . 13 (𝑘 = 𝐾 → (DIsoC‘𝑘) = (DIsoC‘𝐾))
3635fveq1d 6892 . . . . . . . . . . . 12 (𝑘 = 𝐾 → ((DIsoC‘𝑘)‘𝑤) = ((DIsoC‘𝐾)‘𝑤))
3736fveq1d 6892 . . . . . . . . . . 11 (𝑘 = 𝐾 → (((DIsoC‘𝑘)‘𝑤)‘𝑞) = (((DIsoC‘𝐾)‘𝑤)‘𝑞))
3813, 30fveq12d 6897 . . . . . . . . . . 11 (𝑘 = 𝐾 → (((DIsoB‘𝑘)‘𝑤)‘(𝑥(meet‘𝑘)𝑤)) = (((DIsoB‘𝐾)‘𝑤)‘(𝑥 𝑤)))
3934, 37, 38oveq123d 7432 . . . . . . . . . 10 (𝑘 = 𝐾 → ((((DIsoC‘𝑘)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝑘)‘𝑤))(((DIsoB‘𝑘)‘𝑤)‘(𝑥(meet‘𝑘)𝑤))) = ((((DIsoC‘𝐾)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝐾)‘𝑤))(((DIsoB‘𝐾)‘𝑤)‘(𝑥 𝑤))))
4039eqeq2d 2741 . . . . . . . . 9 (𝑘 = 𝐾 → (𝑢 = ((((DIsoC‘𝑘)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝑘)‘𝑤))(((DIsoB‘𝑘)‘𝑤)‘(𝑥(meet‘𝑘)𝑤))) ↔ 𝑢 = ((((DIsoC‘𝐾)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝐾)‘𝑤))(((DIsoB‘𝐾)‘𝑤)‘(𝑥 𝑤)))))
4133, 40imbi12d 343 . . . . . . . 8 (𝑘 = 𝐾 → (((¬ 𝑞(le‘𝑘)𝑤 ∧ (𝑞(join‘𝑘)(𝑥(meet‘𝑘)𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝑘)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝑘)‘𝑤))(((DIsoB‘𝑘)‘𝑤)‘(𝑥(meet‘𝑘)𝑤)))) ↔ ((¬ 𝑞 𝑤 ∧ (𝑞 (𝑥 𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝐾)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝐾)‘𝑤))(((DIsoB‘𝐾)‘𝑤)‘(𝑥 𝑤))))))
4220, 41raleqbidv 3340 . . . . . . 7 (𝑘 = 𝐾 → (∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑞(le‘𝑘)𝑤 ∧ (𝑞(join‘𝑘)(𝑥(meet‘𝑘)𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝑘)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝑘)‘𝑤))(((DIsoB‘𝑘)‘𝑤)‘(𝑥(meet‘𝑘)𝑤)))) ↔ ∀𝑞𝐴 ((¬ 𝑞 𝑤 ∧ (𝑞 (𝑥 𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝐾)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝐾)‘𝑤))(((DIsoB‘𝐾)‘𝑤)‘(𝑥 𝑤))))))
4317, 42riotaeqbidv 7370 . . . . . 6 (𝑘 = 𝐾 → (𝑢 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤))∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑞(le‘𝑘)𝑤 ∧ (𝑞(join‘𝑘)(𝑥(meet‘𝑘)𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝑘)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝑘)‘𝑤))(((DIsoB‘𝑘)‘𝑤)‘(𝑥(meet‘𝑘)𝑤))))) = (𝑢 ∈ (LSubSp‘((DVecH‘𝐾)‘𝑤))∀𝑞𝐴 ((¬ 𝑞 𝑤 ∧ (𝑞 (𝑥 𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝐾)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝐾)‘𝑤))(((DIsoB‘𝐾)‘𝑤)‘(𝑥 𝑤))))))
4411, 14, 43ifbieq12d 4555 . . . . 5 (𝑘 = 𝐾 → if(𝑥(le‘𝑘)𝑤, (((DIsoB‘𝑘)‘𝑤)‘𝑥), (𝑢 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤))∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑞(le‘𝑘)𝑤 ∧ (𝑞(join‘𝑘)(𝑥(meet‘𝑘)𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝑘)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝑘)‘𝑤))(((DIsoB‘𝑘)‘𝑤)‘(𝑥(meet‘𝑘)𝑤)))))) = if(𝑥 𝑤, (((DIsoB‘𝐾)‘𝑤)‘𝑥), (𝑢 ∈ (LSubSp‘((DVecH‘𝐾)‘𝑤))∀𝑞𝐴 ((¬ 𝑞 𝑤 ∧ (𝑞 (𝑥 𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝐾)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝐾)‘𝑤))(((DIsoB‘𝐾)‘𝑤)‘(𝑥 𝑤)))))))
457, 44mpteq12dv 5238 . . . 4 (𝑘 = 𝐾 → (𝑥 ∈ (Base‘𝑘) ↦ if(𝑥(le‘𝑘)𝑤, (((DIsoB‘𝑘)‘𝑤)‘𝑥), (𝑢 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤))∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑞(le‘𝑘)𝑤 ∧ (𝑞(join‘𝑘)(𝑥(meet‘𝑘)𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝑘)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝑘)‘𝑤))(((DIsoB‘𝑘)‘𝑤)‘(𝑥(meet‘𝑘)𝑤))))))) = (𝑥𝐵 ↦ if(𝑥 𝑤, (((DIsoB‘𝐾)‘𝑤)‘𝑥), (𝑢 ∈ (LSubSp‘((DVecH‘𝐾)‘𝑤))∀𝑞𝐴 ((¬ 𝑞 𝑤 ∧ (𝑞 (𝑥 𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝐾)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝐾)‘𝑤))(((DIsoB‘𝐾)‘𝑤)‘(𝑥 𝑤))))))))
464, 45mpteq12dv 5238 . . 3 (𝑘 = 𝐾 → (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ (Base‘𝑘) ↦ if(𝑥(le‘𝑘)𝑤, (((DIsoB‘𝑘)‘𝑤)‘𝑥), (𝑢 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤))∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑞(le‘𝑘)𝑤 ∧ (𝑞(join‘𝑘)(𝑥(meet‘𝑘)𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝑘)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝑘)‘𝑤))(((DIsoB‘𝑘)‘𝑤)‘(𝑥(meet‘𝑘)𝑤)))))))) = (𝑤𝐻 ↦ (𝑥𝐵 ↦ if(𝑥 𝑤, (((DIsoB‘𝐾)‘𝑤)‘𝑥), (𝑢 ∈ (LSubSp‘((DVecH‘𝐾)‘𝑤))∀𝑞𝐴 ((¬ 𝑞 𝑤 ∧ (𝑞 (𝑥 𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝐾)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝐾)‘𝑤))(((DIsoB‘𝐾)‘𝑤)‘(𝑥 𝑤)))))))))
47 df-dih 40403 . . 3 DIsoH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ (Base‘𝑘) ↦ if(𝑥(le‘𝑘)𝑤, (((DIsoB‘𝑘)‘𝑤)‘𝑥), (𝑢 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤))∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑞(le‘𝑘)𝑤 ∧ (𝑞(join‘𝑘)(𝑥(meet‘𝑘)𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝑘)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝑘)‘𝑤))(((DIsoB‘𝑘)‘𝑤)‘(𝑥(meet‘𝑘)𝑤)))))))))
4846, 47, 3mptfvmpt 7231 . 2 (𝐾 ∈ V → (DIsoH‘𝐾) = (𝑤𝐻 ↦ (𝑥𝐵 ↦ if(𝑥 𝑤, (((DIsoB‘𝐾)‘𝑤)‘𝑥), (𝑢 ∈ (LSubSp‘((DVecH‘𝐾)‘𝑤))∀𝑞𝐴 ((¬ 𝑞 𝑤 ∧ (𝑞 (𝑥 𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝐾)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝐾)‘𝑤))(((DIsoB‘𝐾)‘𝑤)‘(𝑥 𝑤)))))))))
491, 48syl 17 1 (𝐾𝑉 → (DIsoH‘𝐾) = (𝑤𝐻 ↦ (𝑥𝐵 ↦ if(𝑥 𝑤, (((DIsoB‘𝐾)‘𝑤)‘𝑥), (𝑢 ∈ (LSubSp‘((DVecH‘𝐾)‘𝑤))∀𝑞𝐴 ((¬ 𝑞 𝑤 ∧ (𝑞 (𝑥 𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝐾)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝐾)‘𝑤))(((DIsoB‘𝐾)‘𝑤)‘(𝑥 𝑤)))))))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394   = wceq 1539  wcel 2104  wral 3059  Vcvv 3472  ifcif 4527   class class class wbr 5147  cmpt 5230  cfv 6542  crio 7366  (class class class)co 7411  Basecbs 17148  lecple 17208  joincjn 18268  meetcmee 18269  LSSumclsm 19543  LSubSpclss 20686  Atomscatm 38436  LHypclh 39158  DVecHcdvh 40252  DIsoBcdib 40312  DIsoCcdic 40346  DIsoHcdih 40402
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-dih 40403
This theorem is referenced by:  dihfval  40405
  Copyright terms: Public domain W3C validator