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

Theorem dihord2cN 39229
Description: Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. TODO: needed? shorten other proof with it? (Contributed by NM, 3-Mar-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
dihjust.b 𝐵 = (Base‘𝐾)
dihjust.l = (le‘𝐾)
dihjust.j = (join‘𝐾)
dihjust.m = (meet‘𝐾)
dihjust.a 𝐴 = (Atoms‘𝐾)
dihjust.h 𝐻 = (LHyp‘𝐾)
dihjust.i 𝐼 = ((DIsoB‘𝐾)‘𝑊)
dihjust.J 𝐽 = ((DIsoC‘𝐾)‘𝑊)
dihjust.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
dihjust.s = (LSSum‘𝑈)
dihord2c.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
dihord2c.r 𝑅 = ((trL‘𝐾)‘𝑊)
dihord2c.o 𝑂 = (𝑇 ↦ ( I ↾ 𝐵))
Assertion
Ref Expression
dihord2cN (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋𝐵 ∧ (𝑓𝑇 ∧ (𝑅𝑓) (𝑋 𝑊))) → ⟨𝑓, 𝑂⟩ ∈ (𝐼‘(𝑋 𝑊)))
Distinct variable groups:   ,𝑓   ,𝑓   ,𝑓   𝑓,,𝐴   𝑓,𝐼   𝑓,𝐽   𝑅,𝑓   𝐵,𝑓,   𝑓,𝐻,   𝑓,𝐾,   ,𝑓,   𝑇,𝑓,   𝑓,𝑊,   𝑓,𝑋
Allowed substitution hints:   ()   𝑅()   𝑈(𝑓,)   𝐼()   𝐽()   ()   ()   𝑂(𝑓,)   𝑋()

Proof of Theorem dihord2cN
StepHypRef Expression
1 simp3 1137 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋𝐵 ∧ (𝑓𝑇 ∧ (𝑅𝑓) (𝑋 𝑊))) → (𝑓𝑇 ∧ (𝑅𝑓) (𝑋 𝑊)))
2 eqidd 2741 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋𝐵 ∧ (𝑓𝑇 ∧ (𝑅𝑓) (𝑋 𝑊))) → 𝑂 = 𝑂)
3 simp1 1135 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋𝐵 ∧ (𝑓𝑇 ∧ (𝑅𝑓) (𝑋 𝑊))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
4 simp1l 1196 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋𝐵 ∧ (𝑓𝑇 ∧ (𝑅𝑓) (𝑋 𝑊))) → 𝐾 ∈ HL)
54hllatd 37372 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋𝐵 ∧ (𝑓𝑇 ∧ (𝑅𝑓) (𝑋 𝑊))) → 𝐾 ∈ Lat)
6 simp2 1136 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋𝐵 ∧ (𝑓𝑇 ∧ (𝑅𝑓) (𝑋 𝑊))) → 𝑋𝐵)
7 simp1r 1197 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋𝐵 ∧ (𝑓𝑇 ∧ (𝑅𝑓) (𝑋 𝑊))) → 𝑊𝐻)
8 dihjust.b . . . . . 6 𝐵 = (Base‘𝐾)
9 dihjust.h . . . . . 6 𝐻 = (LHyp‘𝐾)
108, 9lhpbase 38006 . . . . 5 (𝑊𝐻𝑊𝐵)
117, 10syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋𝐵 ∧ (𝑓𝑇 ∧ (𝑅𝑓) (𝑋 𝑊))) → 𝑊𝐵)
12 dihjust.m . . . . 5 = (meet‘𝐾)
138, 12latmcl 18154 . . . 4 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑊𝐵) → (𝑋 𝑊) ∈ 𝐵)
145, 6, 11, 13syl3anc 1370 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋𝐵 ∧ (𝑓𝑇 ∧ (𝑅𝑓) (𝑋 𝑊))) → (𝑋 𝑊) ∈ 𝐵)
15 dihjust.l . . . . 5 = (le‘𝐾)
168, 15, 12latmle2 18179 . . . 4 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑊𝐵) → (𝑋 𝑊) 𝑊)
175, 6, 11, 16syl3anc 1370 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋𝐵 ∧ (𝑓𝑇 ∧ (𝑅𝑓) (𝑋 𝑊))) → (𝑋 𝑊) 𝑊)
18 dihord2c.t . . . 4 𝑇 = ((LTrn‘𝐾)‘𝑊)
19 dihord2c.r . . . 4 𝑅 = ((trL‘𝐾)‘𝑊)
20 dihord2c.o . . . 4 𝑂 = (𝑇 ↦ ( I ↾ 𝐵))
21 dihjust.i . . . 4 𝐼 = ((DIsoB‘𝐾)‘𝑊)
228, 15, 9, 18, 19, 20, 21dibopelval3 39156 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑋 𝑊) ∈ 𝐵 ∧ (𝑋 𝑊) 𝑊)) → (⟨𝑓, 𝑂⟩ ∈ (𝐼‘(𝑋 𝑊)) ↔ ((𝑓𝑇 ∧ (𝑅𝑓) (𝑋 𝑊)) ∧ 𝑂 = 𝑂)))
233, 14, 17, 22syl12anc 834 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋𝐵 ∧ (𝑓𝑇 ∧ (𝑅𝑓) (𝑋 𝑊))) → (⟨𝑓, 𝑂⟩ ∈ (𝐼‘(𝑋 𝑊)) ↔ ((𝑓𝑇 ∧ (𝑅𝑓) (𝑋 𝑊)) ∧ 𝑂 = 𝑂)))
241, 2, 23mpbir2and 710 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋𝐵 ∧ (𝑓𝑇 ∧ (𝑅𝑓) (𝑋 𝑊))) → ⟨𝑓, 𝑂⟩ ∈ (𝐼‘(𝑋 𝑊)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1542  wcel 2110  cop 4573   class class class wbr 5079  cmpt 5162   I cid 5488  cres 5591  cfv 6431  (class class class)co 7269  Basecbs 16908  lecple 16965  joincjn 18025  meetcmee 18026  Latclat 18145  LSSumclsm 19235  Atomscatm 37271  HLchlt 37358  LHypclh 37992  LTrncltrn 38109  trLctrl 38166  DVecHcdvh 39086  DIsoBcdib 39146  DIsoCcdic 39180
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-rep 5214  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7580
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-ral 3071  df-rex 3072  df-reu 3073  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6389  df-fun 6433  df-fn 6434  df-f 6435  df-f1 6436  df-fo 6437  df-f1o 6438  df-fv 6439  df-riota 7226  df-ov 7272  df-oprab 7273  df-lub 18060  df-glb 18061  df-join 18062  df-meet 18063  df-lat 18146  df-atl 37306  df-cvlat 37330  df-hlat 37359  df-lhyp 37996  df-disoa 39037  df-dib 39147
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator