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.

Step	Hyp	Ref	Expression
1		dihw.k	. . 3 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2	1	simprd 488	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ 𝐻)
3		dihw.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐾)
4		dihw.h	. . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾)
5	3, 4	lhpbase 36619	. . . . 5 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
6	2, 5	syl 17	. . . 4 ⊢ (𝜑 → 𝑊 ∈ 𝐵)
7	1	simpld 487	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ HL)
8	7	hllatd 35985	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ Lat)
9		eqid 2780	. . . . . 6 ⊢ (le‘𝐾) = (le‘𝐾)
10	3, 9	latref 17533	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐵) → 𝑊(le‘𝐾)𝑊)
11	8, 6, 10	syl2anc 576	. . . 4 ⊢ (𝜑 → 𝑊(le‘𝐾)𝑊)
12	6, 11	jca 504	. . 3 ⊢ (𝜑 → (𝑊 ∈ 𝐵 ∧ 𝑊(le‘𝐾)𝑊))
13		dihw.i	. . . 4 ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
14		eqid 2780	. . . 4 ⊢ ((DIsoB‘𝐾)‘𝑊) = ((DIsoB‘𝐾)‘𝑊)
15	3, 9, 4, 13, 14	dihvalb 37858	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑊 ∈ 𝐵 ∧ 𝑊(le‘𝐾)𝑊)) → (𝐼‘𝑊) = (((DIsoB‘𝐾)‘𝑊)‘𝑊))
16	1, 12, 15	syl2anc 576	. 2 ⊢ (𝜑 → (𝐼‘𝑊) = (((DIsoB‘𝐾)‘𝑊)‘𝑊))
17		dihw.t	. . . 4 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
18		dihw.o	. . . 4 ⊢ 0 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))
19		eqid 2780	. . . 4 ⊢ ((DIsoA‘𝐾)‘𝑊) = ((DIsoA‘𝐾)‘𝑊)
20	3, 9, 4, 17, 18, 19, 14	dibval2 37765	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑊 ∈ 𝐵 ∧ 𝑊(le‘𝐾)𝑊)) → (((DIsoB‘𝐾)‘𝑊)‘𝑊) = ((((DIsoA‘𝐾)‘𝑊)‘𝑊) × { 0 }))
21	1, 12, 20	syl2anc 576	. 2 ⊢ (𝜑 → (((DIsoB‘𝐾)‘𝑊)‘𝑊) = ((((DIsoA‘𝐾)‘𝑊)‘𝑊) × { 0 }))
22		eqid 2780	. . . . . 6 ⊢ ((trL‘𝐾)‘𝑊) = ((trL‘𝐾)‘𝑊)
23	3, 9, 4, 17, 22, 19	diaval 37653	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑊 ∈ 𝐵 ∧ 𝑊(le‘𝐾)𝑊)) → (((DIsoA‘𝐾)‘𝑊)‘𝑊) = {𝑔 ∈ 𝑇 ∣ (((trL‘𝐾)‘𝑊)‘𝑔)(le‘𝐾)𝑊})
24	1, 12, 23	syl2anc 576	. . . 4 ⊢ (𝜑 → (((DIsoA‘𝐾)‘𝑊)‘𝑊) = {𝑔 ∈ 𝑇 ∣ (((trL‘𝐾)‘𝑊)‘𝑔)(le‘𝐾)𝑊})
25	9, 4, 17, 22	trlle 36805	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑔 ∈ 𝑇) → (((trL‘𝐾)‘𝑊)‘𝑔)(le‘𝐾)𝑊)
26	1, 25	sylan 572	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → (((trL‘𝐾)‘𝑊)‘𝑔)(le‘𝐾)𝑊)
27	26	ralrimiva 3134	. . . . 5 ⊢ (𝜑 → ∀𝑔 ∈ 𝑇 (((trL‘𝐾)‘𝑊)‘𝑔)(le‘𝐾)𝑊)
28		rabid2 3322	. . . . 5 ⊢ (𝑇 = {𝑔 ∈ 𝑇 ∣ (((trL‘𝐾)‘𝑊)‘𝑔)(le‘𝐾)𝑊} ↔ ∀𝑔 ∈ 𝑇 (((trL‘𝐾)‘𝑊)‘𝑔)(le‘𝐾)𝑊)
29	27, 28	sylibr 226	. . . 4 ⊢ (𝜑 → 𝑇 = {𝑔 ∈ 𝑇 ∣ (((trL‘𝐾)‘𝑊)‘𝑔)(le‘𝐾)𝑊})
30	24, 29	eqtr4d 2819	. . 3 ⊢ (𝜑 → (((DIsoA‘𝐾)‘𝑊)‘𝑊) = 𝑇)
31	30	xpeq1d 5440	. 2 ⊢ (𝜑 → ((((DIsoA‘𝐾)‘𝑊)‘𝑊) × { 0 }) = (𝑇 × { 0 }))
32	16, 21, 31	3eqtrd 2820	1 ⊢ (𝜑 → (𝐼‘𝑊) = (𝑇 × { 0 }))

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)