Theorem dihvalb 41198

Description: Value of isomorphism H for a lattice 𝐾 when 𝑋 ≤ 𝑊. (Contributed by NM, 4-Mar-2014.)

Hypotheses

Ref	Expression
dihvalb.b	⊢ 𝐵 = (Base‘𝐾)
dihvalb.l	⊢ ≤ = (le‘𝐾)
dihvalb.h	⊢ 𝐻 = (LHyp‘𝐾)
dihvalb.i	⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
dihvalb.d	⊢ 𝐷 = ((DIsoB‘𝐾)‘𝑊)

Assertion

Ref	Expression
dihvalb	⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) = (𝐷‘𝑋))

Proof of Theorem dihvalb

Dummy variables 𝑢 𝑞 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dihvalb.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
2		dihvalb.l	. . . 4 ⊢ ≤ = (le‘𝐾)
3		eqid 2734	. . . 4 ⊢ (join‘𝐾) = (join‘𝐾)
4		eqid 2734	. . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾)
5		eqid 2734	. . . 4 ⊢ (Atoms‘𝐾) = (Atoms‘𝐾)
6		dihvalb.h	. . . 4 ⊢ 𝐻 = (LHyp‘𝐾)
7		dihvalb.i	. . . 4 ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
8		dihvalb.d	. . . 4 ⊢ 𝐷 = ((DIsoB‘𝐾)‘𝑊)
9		eqid 2734	. . . 4 ⊢ ((DIsoC‘𝐾)‘𝑊) = ((DIsoC‘𝐾)‘𝑊)
10		eqid 2734	. . . 4 ⊢ ((DVecH‘𝐾)‘𝑊) = ((DVecH‘𝐾)‘𝑊)
11		eqid 2734	. . . 4 ⊢ (LSubSp‘((DVecH‘𝐾)‘𝑊)) = (LSubSp‘((DVecH‘𝐾)‘𝑊))
12		eqid 2734	. . . 4 ⊢ (LSSum‘((DVecH‘𝐾)‘𝑊)) = (LSSum‘((DVecH‘𝐾)‘𝑊))
13	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12	dihval 41193	. . 3 ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐼‘𝑋) = if(𝑋 ≤ 𝑊, (𝐷‘𝑋), (℩𝑢 ∈ (LSubSp‘((DVecH‘𝐾)‘𝑊))∀𝑞 ∈ (Atoms‘𝐾)((¬ 𝑞 ≤ 𝑊 ∧ (𝑞(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋) → 𝑢 = ((((DIsoC‘𝐾)‘𝑊)‘𝑞)(LSSum‘((DVecH‘𝐾)‘𝑊))(𝐷‘(𝑋(meet‘𝐾)𝑊)))))))
14		iftrue 4511	. . 3 ⊢ (𝑋 ≤ 𝑊 → if(𝑋 ≤ 𝑊, (𝐷‘𝑋), (℩𝑢 ∈ (LSubSp‘((DVecH‘𝐾)‘𝑊))∀𝑞 ∈ (Atoms‘𝐾)((¬ 𝑞 ≤ 𝑊 ∧ (𝑞(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋) → 𝑢 = ((((DIsoC‘𝐾)‘𝑊)‘𝑞)(LSSum‘((DVecH‘𝐾)‘𝑊))(𝐷‘(𝑋(meet‘𝐾)𝑊)))))) = (𝐷‘𝑋))
15	13, 14	sylan9eq 2789	. 2 ⊢ ((((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑋 ≤ 𝑊) → (𝐼‘𝑋) = (𝐷‘𝑋))
16	15	anasss 466	1 ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) = (𝐷‘𝑋))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2107  ∀wral 3050  ifcif 4505   class class class wbr 5123  ‘cfv 6541  ℩crio 7369  (class class class)co 7413  Basecbs 17229  lecple 17280  joincjn 18327  meetcmee 18328  LSSumclsm 19620  LSubSpclss 20897  Atomscatm 39223  LHypclh 39945  DVecHcdvh 41039  DIsoBcdib 41099  DIsoCcdic 41133  DIsoHcdih 41189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5259  ax-sep 5276  ax-nul 5286  ax-pr 5412

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-iun 4973  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7370  df-ov 7416  df-dih 41190

This theorem is referenced by:  dihopelvalbN  41199  dih1dimb  41201  dih2dimb  41205  dih2dimbALTN  41206  dihvalcq2  41208  dihlss  41211  dihord6apre  41217  dihord3  41218  dihord5b  41220  dihord5apre  41223  dih0  41241  dihwN  41250  dihglblem3N  41256  dihmeetlem2N  41260  dih1dimatlem  41290  dihjatcclem4  41382