![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > dihvalb | Structured version Visualization version GIF version |
Description: Value of isomorphism H for a lattice 𝐾 when 𝑋 ≤ 𝑊. (Contributed by NM, 4-Mar-2014.) |
Ref | Expression |
---|---|
dihvalb.b | ⊢ 𝐵 = (Base‘𝐾) |
dihvalb.l | ⊢ ≤ = (le‘𝐾) |
dihvalb.h | ⊢ 𝐻 = (LHyp‘𝐾) |
dihvalb.i | ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) |
dihvalb.d | ⊢ 𝐷 = ((DIsoB‘𝐾)‘𝑊) |
Ref | Expression |
---|---|
dihvalb | ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) = (𝐷‘𝑋)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dihvalb.b | . . . 4 ⊢ 𝐵 = (Base‘𝐾) | |
2 | dihvalb.l | . . . 4 ⊢ ≤ = (le‘𝐾) | |
3 | eqid 2779 | . . . 4 ⊢ (join‘𝐾) = (join‘𝐾) | |
4 | eqid 2779 | . . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾) | |
5 | eqid 2779 | . . . 4 ⊢ (Atoms‘𝐾) = (Atoms‘𝐾) | |
6 | dihvalb.h | . . . 4 ⊢ 𝐻 = (LHyp‘𝐾) | |
7 | dihvalb.i | . . . 4 ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) | |
8 | dihvalb.d | . . . 4 ⊢ 𝐷 = ((DIsoB‘𝐾)‘𝑊) | |
9 | eqid 2779 | . . . 4 ⊢ ((DIsoC‘𝐾)‘𝑊) = ((DIsoC‘𝐾)‘𝑊) | |
10 | eqid 2779 | . . . 4 ⊢ ((DVecH‘𝐾)‘𝑊) = ((DVecH‘𝐾)‘𝑊) | |
11 | eqid 2779 | . . . 4 ⊢ (LSubSp‘((DVecH‘𝐾)‘𝑊)) = (LSubSp‘((DVecH‘𝐾)‘𝑊)) | |
12 | eqid 2779 | . . . 4 ⊢ (LSSum‘((DVecH‘𝐾)‘𝑊)) = (LSSum‘((DVecH‘𝐾)‘𝑊)) | |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 | dihval 37810 | . . 3 ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐼‘𝑋) = if(𝑋 ≤ 𝑊, (𝐷‘𝑋), (℩𝑢 ∈ (LSubSp‘((DVecH‘𝐾)‘𝑊))∀𝑞 ∈ (Atoms‘𝐾)((¬ 𝑞 ≤ 𝑊 ∧ (𝑞(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋) → 𝑢 = ((((DIsoC‘𝐾)‘𝑊)‘𝑞)(LSSum‘((DVecH‘𝐾)‘𝑊))(𝐷‘(𝑋(meet‘𝐾)𝑊))))))) |
14 | iftrue 4356 | . . 3 ⊢ (𝑋 ≤ 𝑊 → if(𝑋 ≤ 𝑊, (𝐷‘𝑋), (℩𝑢 ∈ (LSubSp‘((DVecH‘𝐾)‘𝑊))∀𝑞 ∈ (Atoms‘𝐾)((¬ 𝑞 ≤ 𝑊 ∧ (𝑞(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋) → 𝑢 = ((((DIsoC‘𝐾)‘𝑊)‘𝑞)(LSSum‘((DVecH‘𝐾)‘𝑊))(𝐷‘(𝑋(meet‘𝐾)𝑊)))))) = (𝐷‘𝑋)) | |
15 | 13, 14 | sylan9eq 2835 | . 2 ⊢ ((((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑋 ≤ 𝑊) → (𝐼‘𝑋) = (𝐷‘𝑋)) |
16 | 15 | anasss 459 | 1 ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) = (𝐷‘𝑋)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 387 = wceq 1507 ∈ wcel 2050 ∀wral 3089 ifcif 4350 class class class wbr 4929 ‘cfv 6188 ℩crio 6936 (class class class)co 6976 Basecbs 16339 lecple 16428 joincjn 17412 meetcmee 17413 LSSumclsm 18520 LSubSpclss 19425 Atomscatm 35841 LHypclh 36562 DVecHcdvh 37656 DIsoBcdib 37716 DIsoCcdic 37750 DIsoHcdih 37806 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2751 ax-rep 5049 ax-sep 5060 ax-nul 5067 ax-pr 5186 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2760 df-cleq 2772 df-clel 2847 df-nfc 2919 df-ne 2969 df-ral 3094 df-rex 3095 df-reu 3096 df-rab 3098 df-v 3418 df-sbc 3683 df-csb 3788 df-dif 3833 df-un 3835 df-in 3837 df-ss 3844 df-nul 4180 df-if 4351 df-sn 4442 df-pr 4444 df-op 4448 df-uni 4713 df-iun 4794 df-br 4930 df-opab 4992 df-mpt 5009 df-id 5312 df-xp 5413 df-rel 5414 df-cnv 5415 df-co 5416 df-dm 5417 df-rn 5418 df-res 5419 df-ima 5420 df-iota 6152 df-fun 6190 df-fn 6191 df-f 6192 df-f1 6193 df-fo 6194 df-f1o 6195 df-fv 6196 df-riota 6937 df-ov 6979 df-dih 37807 |
This theorem is referenced by: dihopelvalbN 37816 dih1dimb 37818 dih2dimb 37822 dih2dimbALTN 37823 dihvalcq2 37825 dihlss 37828 dihord6apre 37834 dihord3 37835 dihord5b 37837 dihord5apre 37840 dih0 37858 dihwN 37867 dihglblem3N 37873 dihmeetlem2N 37877 dih1dimatlem 37907 dihjatcclem4 37999 |
Copyright terms: Public domain | W3C validator |