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

Theorem dihwN 37910
Description: Value of isomorphism H at the fiducial hyperplane 𝑊. (Contributed by NM, 25-Aug-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
dihw.b 𝐵 = (Base‘𝐾)
dihw.h 𝐻 = (LHyp‘𝐾)
dihw.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
dihw.o 0 = (𝑓𝑇 ↦ ( I ↾ 𝐵))
dihw.i 𝐼 = ((DIsoH‘𝐾)‘𝑊)
dihw.k (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
Assertion
Ref Expression
dihwN (𝜑 → (𝐼𝑊) = (𝑇 × { 0 }))
Distinct variable groups:   𝑓,𝐾   𝑓,𝑊
Allowed substitution hints:   𝜑(𝑓)   𝐵(𝑓)   𝑇(𝑓)   𝐻(𝑓)   𝐼(𝑓)   0 (𝑓)

Proof of Theorem dihwN
Dummy variable 𝑔 is distinct from all other variables.
StepHypRef Expression
1 dihw.k . . 3 (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
21simprd 488 . . . . 5 (𝜑𝑊𝐻)
3 dihw.b . . . . . 6 𝐵 = (Base‘𝐾)
4 dihw.h . . . . . 6 𝐻 = (LHyp‘𝐾)
53, 4lhpbase 36619 . . . . 5 (𝑊𝐻𝑊𝐵)
62, 5syl 17 . . . 4 (𝜑𝑊𝐵)
71simpld 487 . . . . . 6 (𝜑𝐾 ∈ HL)
87hllatd 35985 . . . . 5 (𝜑𝐾 ∈ Lat)
9 eqid 2780 . . . . . 6 (le‘𝐾) = (le‘𝐾)
103, 9latref 17533 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑊𝐵) → 𝑊(le‘𝐾)𝑊)
118, 6, 10syl2anc 576 . . . 4 (𝜑𝑊(le‘𝐾)𝑊)
126, 11jca 504 . . 3 (𝜑 → (𝑊𝐵𝑊(le‘𝐾)𝑊))
13 dihw.i . . . 4 𝐼 = ((DIsoH‘𝐾)‘𝑊)
14 eqid 2780 . . . 4 ((DIsoB‘𝐾)‘𝑊) = ((DIsoB‘𝐾)‘𝑊)
153, 9, 4, 13, 14dihvalb 37858 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑊𝐵𝑊(le‘𝐾)𝑊)) → (𝐼𝑊) = (((DIsoB‘𝐾)‘𝑊)‘𝑊))
161, 12, 15syl2anc 576 . 2 (𝜑 → (𝐼𝑊) = (((DIsoB‘𝐾)‘𝑊)‘𝑊))
17 dihw.t . . . 4 𝑇 = ((LTrn‘𝐾)‘𝑊)
18 dihw.o . . . 4 0 = (𝑓𝑇 ↦ ( I ↾ 𝐵))
19 eqid 2780 . . . 4 ((DIsoA‘𝐾)‘𝑊) = ((DIsoA‘𝐾)‘𝑊)
203, 9, 4, 17, 18, 19, 14dibval2 37765 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑊𝐵𝑊(le‘𝐾)𝑊)) → (((DIsoB‘𝐾)‘𝑊)‘𝑊) = ((((DIsoA‘𝐾)‘𝑊)‘𝑊) × { 0 }))
211, 12, 20syl2anc 576 . 2 (𝜑 → (((DIsoB‘𝐾)‘𝑊)‘𝑊) = ((((DIsoA‘𝐾)‘𝑊)‘𝑊) × { 0 }))
22 eqid 2780 . . . . . 6 ((trL‘𝐾)‘𝑊) = ((trL‘𝐾)‘𝑊)
233, 9, 4, 17, 22, 19diaval 37653 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑊𝐵𝑊(le‘𝐾)𝑊)) → (((DIsoA‘𝐾)‘𝑊)‘𝑊) = {𝑔𝑇 ∣ (((trL‘𝐾)‘𝑊)‘𝑔)(le‘𝐾)𝑊})
241, 12, 23syl2anc 576 . . . 4 (𝜑 → (((DIsoA‘𝐾)‘𝑊)‘𝑊) = {𝑔𝑇 ∣ (((trL‘𝐾)‘𝑊)‘𝑔)(le‘𝐾)𝑊})
259, 4, 17, 22trlle 36805 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑔𝑇) → (((trL‘𝐾)‘𝑊)‘𝑔)(le‘𝐾)𝑊)
261, 25sylan 572 . . . . . 6 ((𝜑𝑔𝑇) → (((trL‘𝐾)‘𝑊)‘𝑔)(le‘𝐾)𝑊)
2726ralrimiva 3134 . . . . 5 (𝜑 → ∀𝑔𝑇 (((trL‘𝐾)‘𝑊)‘𝑔)(le‘𝐾)𝑊)
28 rabid2 3322 . . . . 5 (𝑇 = {𝑔𝑇 ∣ (((trL‘𝐾)‘𝑊)‘𝑔)(le‘𝐾)𝑊} ↔ ∀𝑔𝑇 (((trL‘𝐾)‘𝑊)‘𝑔)(le‘𝐾)𝑊)
2927, 28sylibr 226 . . . 4 (𝜑𝑇 = {𝑔𝑇 ∣ (((trL‘𝐾)‘𝑊)‘𝑔)(le‘𝐾)𝑊})
3024, 29eqtr4d 2819 . . 3 (𝜑 → (((DIsoA‘𝐾)‘𝑊)‘𝑊) = 𝑇)
3130xpeq1d 5440 . 2 (𝜑 → ((((DIsoA‘𝐾)‘𝑊)‘𝑊) × { 0 }) = (𝑇 × { 0 }))
3216, 21, 313eqtrd 2820 1 (𝜑 → (𝐼𝑊) = (𝑇 × { 0 }))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387   = wceq 1508  wcel 2051  wral 3090  {crab 3094  {csn 4444   class class class wbr 4934  cmpt 5013   I cid 5315   × cxp 5409  cres 5413  cfv 6193  Basecbs 16345  lecple 16434  Latclat 17525  HLchlt 35971  LHypclh 36605  LTrncltrn 36722  trLctrl 36779  DIsoAcdia 37649  DIsoBcdib 37759  DIsoHcdih 37849
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2752  ax-rep 5053  ax-sep 5064  ax-nul 5071  ax-pow 5123  ax-pr 5190  ax-un 7285
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2551  df-eu 2589  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3419  df-sbc 3684  df-csb 3789  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4182  df-if 4354  df-pw 4427  df-sn 4445  df-pr 4447  df-op 4451  df-uni 4718  df-iun 4799  df-br 4935  df-opab 4997  df-mpt 5014  df-id 5316  df-xp 5417  df-rel 5418  df-cnv 5419  df-co 5420  df-dm 5421  df-rn 5422  df-res 5423  df-ima 5424  df-iota 6157  df-fun 6195  df-fn 6196  df-f 6197  df-f1 6198  df-fo 6199  df-f1o 6200  df-fv 6201  df-riota 6943  df-ov 6985  df-oprab 6986  df-mpo 6987  df-map 8214  df-proset 17408  df-poset 17426  df-plt 17438  df-lub 17454  df-glb 17455  df-join 17456  df-meet 17457  df-p0 17519  df-p1 17520  df-lat 17526  df-oposet 35797  df-ol 35799  df-oml 35800  df-covers 35887  df-ats 35888  df-atl 35919  df-cvlat 35943  df-hlat 35972  df-lhyp 36609  df-laut 36610  df-ldil 36725  df-ltrn 36726  df-trl 36780  df-disoa 37650  df-dib 37760  df-dih 37850
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator