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

Theorem dihord2b 38583
 Description: Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.)
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‘𝑈)
Assertion
Ref Expression
dihord2b ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ (𝑋𝐵𝑌𝐵) ∧ ((𝐽𝑄) (𝐼‘(𝑋 𝑊))) ⊆ ((𝐽𝑅) (𝐼‘(𝑌 𝑊)))) → (𝐼‘(𝑋 𝑊)) ⊆ ((𝐽𝑅) (𝐼‘(𝑌 𝑊))))

Proof of Theorem dihord2b
StepHypRef Expression
1 dihjust.h . . . . . 6 𝐻 = (LHyp‘𝐾)
2 dihjust.u . . . . . 6 𝑈 = ((DVecH‘𝐾)‘𝑊)
3 simp11 1200 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ (𝑋𝐵𝑌𝐵) ∧ ((𝐽𝑄) (𝐼‘(𝑋 𝑊))) ⊆ ((𝐽𝑅) (𝐼‘(𝑌 𝑊)))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
41, 2, 3dvhlmod 38473 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ (𝑋𝐵𝑌𝐵) ∧ ((𝐽𝑄) (𝐼‘(𝑋 𝑊))) ⊆ ((𝐽𝑅) (𝐼‘(𝑌 𝑊)))) → 𝑈 ∈ LMod)
5 eqid 2798 . . . . . 6 (LSubSp‘𝑈) = (LSubSp‘𝑈)
65lsssssubg 19741 . . . . 5 (𝑈 ∈ LMod → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
74, 6syl 17 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ (𝑋𝐵𝑌𝐵) ∧ ((𝐽𝑄) (𝐼‘(𝑋 𝑊))) ⊆ ((𝐽𝑅) (𝐼‘(𝑌 𝑊)))) → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
8 simp12 1201 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ (𝑋𝐵𝑌𝐵) ∧ ((𝐽𝑄) (𝐼‘(𝑋 𝑊))) ⊆ ((𝐽𝑅) (𝐼‘(𝑌 𝑊)))) → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))
9 dihjust.l . . . . . 6 = (le‘𝐾)
10 dihjust.a . . . . . 6 𝐴 = (Atoms‘𝐾)
11 dihjust.J . . . . . 6 𝐽 = ((DIsoC‘𝐾)‘𝑊)
129, 10, 1, 2, 11, 5diclss 38556 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (𝐽𝑄) ∈ (LSubSp‘𝑈))
133, 8, 12syl2anc 587 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ (𝑋𝐵𝑌𝐵) ∧ ((𝐽𝑄) (𝐼‘(𝑋 𝑊))) ⊆ ((𝐽𝑅) (𝐼‘(𝑌 𝑊)))) → (𝐽𝑄) ∈ (LSubSp‘𝑈))
147, 13sseldd 3917 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ (𝑋𝐵𝑌𝐵) ∧ ((𝐽𝑄) (𝐼‘(𝑋 𝑊))) ⊆ ((𝐽𝑅) (𝐼‘(𝑌 𝑊)))) → (𝐽𝑄) ∈ (SubGrp‘𝑈))
15 simp11l 1281 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ (𝑋𝐵𝑌𝐵) ∧ ((𝐽𝑄) (𝐼‘(𝑋 𝑊))) ⊆ ((𝐽𝑅) (𝐼‘(𝑌 𝑊)))) → 𝐾 ∈ HL)
1615hllatd 36727 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ (𝑋𝐵𝑌𝐵) ∧ ((𝐽𝑄) (𝐼‘(𝑋 𝑊))) ⊆ ((𝐽𝑅) (𝐼‘(𝑌 𝑊)))) → 𝐾 ∈ Lat)
17 simp2l 1196 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ (𝑋𝐵𝑌𝐵) ∧ ((𝐽𝑄) (𝐼‘(𝑋 𝑊))) ⊆ ((𝐽𝑅) (𝐼‘(𝑌 𝑊)))) → 𝑋𝐵)
18 simp11r 1282 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ (𝑋𝐵𝑌𝐵) ∧ ((𝐽𝑄) (𝐼‘(𝑋 𝑊))) ⊆ ((𝐽𝑅) (𝐼‘(𝑌 𝑊)))) → 𝑊𝐻)
19 dihjust.b . . . . . . . 8 𝐵 = (Base‘𝐾)
2019, 1lhpbase 37361 . . . . . . 7 (𝑊𝐻𝑊𝐵)
2118, 20syl 17 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ (𝑋𝐵𝑌𝐵) ∧ ((𝐽𝑄) (𝐼‘(𝑋 𝑊))) ⊆ ((𝐽𝑅) (𝐼‘(𝑌 𝑊)))) → 𝑊𝐵)
22 dihjust.m . . . . . . 7 = (meet‘𝐾)
2319, 22latmcl 17671 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑊𝐵) → (𝑋 𝑊) ∈ 𝐵)
2416, 17, 21, 23syl3anc 1368 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ (𝑋𝐵𝑌𝐵) ∧ ((𝐽𝑄) (𝐼‘(𝑋 𝑊))) ⊆ ((𝐽𝑅) (𝐼‘(𝑌 𝑊)))) → (𝑋 𝑊) ∈ 𝐵)
2519, 9, 22latmle2 17696 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑊𝐵) → (𝑋 𝑊) 𝑊)
2616, 17, 21, 25syl3anc 1368 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ (𝑋𝐵𝑌𝐵) ∧ ((𝐽𝑄) (𝐼‘(𝑋 𝑊))) ⊆ ((𝐽𝑅) (𝐼‘(𝑌 𝑊)))) → (𝑋 𝑊) 𝑊)
27 dihjust.i . . . . . 6 𝐼 = ((DIsoB‘𝐾)‘𝑊)
2819, 9, 1, 2, 27, 5diblss 38533 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑋 𝑊) ∈ 𝐵 ∧ (𝑋 𝑊) 𝑊)) → (𝐼‘(𝑋 𝑊)) ∈ (LSubSp‘𝑈))
293, 24, 26, 28syl12anc 835 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ (𝑋𝐵𝑌𝐵) ∧ ((𝐽𝑄) (𝐼‘(𝑋 𝑊))) ⊆ ((𝐽𝑅) (𝐼‘(𝑌 𝑊)))) → (𝐼‘(𝑋 𝑊)) ∈ (LSubSp‘𝑈))
307, 29sseldd 3917 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ (𝑋𝐵𝑌𝐵) ∧ ((𝐽𝑄) (𝐼‘(𝑋 𝑊))) ⊆ ((𝐽𝑅) (𝐼‘(𝑌 𝑊)))) → (𝐼‘(𝑋 𝑊)) ∈ (SubGrp‘𝑈))
31 dihjust.s . . . 4 = (LSSum‘𝑈)
3231lsmub2 18793 . . 3 (((𝐽𝑄) ∈ (SubGrp‘𝑈) ∧ (𝐼‘(𝑋 𝑊)) ∈ (SubGrp‘𝑈)) → (𝐼‘(𝑋 𝑊)) ⊆ ((𝐽𝑄) (𝐼‘(𝑋 𝑊))))
3314, 30, 32syl2anc 587 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ (𝑋𝐵𝑌𝐵) ∧ ((𝐽𝑄) (𝐼‘(𝑋 𝑊))) ⊆ ((𝐽𝑅) (𝐼‘(𝑌 𝑊)))) → (𝐼‘(𝑋 𝑊)) ⊆ ((𝐽𝑄) (𝐼‘(𝑋 𝑊))))
34 simp3 1135 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ (𝑋𝐵𝑌𝐵) ∧ ((𝐽𝑄) (𝐼‘(𝑋 𝑊))) ⊆ ((𝐽𝑅) (𝐼‘(𝑌 𝑊)))) → ((𝐽𝑄) (𝐼‘(𝑋 𝑊))) ⊆ ((𝐽𝑅) (𝐼‘(𝑌 𝑊))))
3533, 34sstrd 3926 1 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ (𝑋𝐵𝑌𝐵) ∧ ((𝐽𝑄) (𝐼‘(𝑋 𝑊))) ⊆ ((𝐽𝑅) (𝐼‘(𝑌 𝑊)))) → (𝐼‘(𝑋 𝑊)) ⊆ ((𝐽𝑅) (𝐼‘(𝑌 𝑊))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ⊆ wss 3882   class class class wbr 5033  ‘cfv 6329  (class class class)co 7142  Basecbs 16492  lecple 16581  joincjn 17563  meetcmee 17564  Latclat 17664  SubGrpcsubg 18283  LSSumclsm 18769  LModclmod 19645  LSubSpclss 19714  Atomscatm 36626  HLchlt 36713  LHypclh 37347  DVecHcdvh 38441  DIsoBcdib 38501  DIsoCcdic 38535 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7451  ax-cnex 10597  ax-resscn 10598  ax-1cn 10599  ax-icn 10600  ax-addcl 10601  ax-addrcl 10602  ax-mulcl 10603  ax-mulrcl 10604  ax-mulcom 10605  ax-addass 10606  ax-mulass 10607  ax-distr 10608  ax-i2m1 10609  ax-1ne0 10610  ax-1rid 10611  ax-rnegex 10612  ax-rrecex 10613  ax-cnre 10614  ax-pre-lttri 10615  ax-pre-lttrn 10616  ax-pre-ltadd 10617  ax-pre-mulgt0 10618  ax-riotaBAD 36316 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3722  df-csb 3830  df-dif 3885  df-un 3887  df-in 3889  df-ss 3899  df-pss 3901  df-nul 4246  df-if 4428  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4804  df-int 4842  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5441  df-so 5442  df-fr 5481  df-we 5483  df-xp 5528  df-rel 5529  df-cnv 5530  df-co 5531  df-dm 5532  df-rn 5533  df-res 5534  df-ima 5535  df-pred 6121  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-iota 6288  df-fun 6331  df-fn 6332  df-f 6333  df-f1 6334  df-fo 6335  df-f1o 6336  df-fv 6337  df-riota 7100  df-ov 7145  df-oprab 7146  df-mpo 7147  df-om 7571  df-1st 7681  df-2nd 7682  df-tpos 7890  df-undef 7937  df-wrecs 7945  df-recs 8006  df-rdg 8044  df-1o 8100  df-oadd 8104  df-er 8287  df-map 8406  df-en 8508  df-dom 8509  df-sdom 8510  df-fin 8511  df-pnf 10681  df-mnf 10682  df-xr 10683  df-ltxr 10684  df-le 10685  df-sub 10876  df-neg 10877  df-nn 11641  df-2 11703  df-3 11704  df-4 11705  df-5 11706  df-6 11707  df-n0 11901  df-z 11987  df-uz 12249  df-fz 12903  df-struct 16494  df-ndx 16495  df-slot 16496  df-base 16498  df-sets 16499  df-ress 16500  df-plusg 16587  df-mulr 16588  df-sca 16590  df-vsca 16591  df-0g 16724  df-proset 17547  df-poset 17565  df-plt 17577  df-lub 17593  df-glb 17594  df-join 17595  df-meet 17596  df-p0 17658  df-p1 17659  df-lat 17665  df-clat 17727  df-mgm 17861  df-sgrp 17910  df-mnd 17921  df-submnd 17966  df-grp 18115  df-minusg 18116  df-sbg 18117  df-subg 18286  df-lsm 18771  df-mgp 19251  df-ur 19263  df-ring 19310  df-oppr 19387  df-dvdsr 19405  df-unit 19406  df-invr 19436  df-dvr 19447  df-drng 19515  df-lmod 19647  df-lss 19715  df-lvec 19886  df-oposet 36539  df-ol 36541  df-oml 36542  df-covers 36629  df-ats 36630  df-atl 36661  df-cvlat 36685  df-hlat 36714  df-llines 36861  df-lplanes 36862  df-lvols 36863  df-lines 36864  df-psubsp 36866  df-pmap 36867  df-padd 37159  df-lhyp 37351  df-laut 37352  df-ldil 37467  df-ltrn 37468  df-trl 37522  df-tendo 38118  df-edring 38120  df-disoa 38392  df-dvech 38442  df-dib 38502  df-dic 38536 This theorem is referenced by:  dihord11b  38585
 Copyright terms: Public domain W3C validator