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

Theorem dihmeetlem9N 41295
Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
dihmeetlem9.b 𝐵 = (Base‘𝐾)
dihmeetlem9.l = (le‘𝐾)
dihmeetlem9.h 𝐻 = (LHyp‘𝐾)
dihmeetlem9.j = (join‘𝐾)
dihmeetlem9.m = (meet‘𝐾)
dihmeetlem9.a 𝐴 = (Atoms‘𝐾)
dihmeetlem9.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
dihmeetlem9.s = (LSSum‘𝑈)
dihmeetlem9.i 𝐼 = ((DIsoH‘𝐾)‘𝑊)
Assertion
Ref Expression
dihmeetlem9N (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑌𝐵) ∧ 𝑝𝐴) → (((𝐼𝑝) (𝐼‘(𝑋 𝑌))) ∩ (𝐼𝑌)) = ((𝐼‘(𝑋 𝑌)) ((𝐼𝑝) ∩ (𝐼𝑌))))

Proof of Theorem dihmeetlem9N
StepHypRef Expression
1 dihmeetlem9.h . . . . . 6 𝐻 = (LHyp‘𝐾)
2 dihmeetlem9.u . . . . . 6 𝑈 = ((DVecH‘𝐾)‘𝑊)
3 simp1 1137 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑌𝐵) ∧ 𝑝𝐴) → (𝐾 ∈ HL ∧ 𝑊𝐻))
41, 2, 3dvhlmod 41090 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑌𝐵) ∧ 𝑝𝐴) → 𝑈 ∈ LMod)
5 eqid 2736 . . . . . 6 (LSubSp‘𝑈) = (LSubSp‘𝑈)
65lsssssubg 20948 . . . . 5 (𝑈 ∈ LMod → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
74, 6syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑌𝐵) ∧ 𝑝𝐴) → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
8 simp1l 1198 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑌𝐵) ∧ 𝑝𝐴) → 𝐾 ∈ HL)
98hllatd 39343 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑌𝐵) ∧ 𝑝𝐴) → 𝐾 ∈ Lat)
10 simp2l 1200 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑌𝐵) ∧ 𝑝𝐴) → 𝑋𝐵)
11 simp2r 1201 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑌𝐵) ∧ 𝑝𝐴) → 𝑌𝐵)
12 dihmeetlem9.b . . . . . . 7 𝐵 = (Base‘𝐾)
13 dihmeetlem9.m . . . . . . 7 = (meet‘𝐾)
1412, 13latmcl 18481 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
159, 10, 11, 14syl3anc 1373 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑌𝐵) ∧ 𝑝𝐴) → (𝑋 𝑌) ∈ 𝐵)
16 dihmeetlem9.i . . . . . 6 𝐼 = ((DIsoH‘𝐾)‘𝑊)
1712, 1, 16, 2, 5dihlss 41230 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 𝑌) ∈ 𝐵) → (𝐼‘(𝑋 𝑌)) ∈ (LSubSp‘𝑈))
183, 15, 17syl2anc 584 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑌𝐵) ∧ 𝑝𝐴) → (𝐼‘(𝑋 𝑌)) ∈ (LSubSp‘𝑈))
197, 18sseldd 3983 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑌𝐵) ∧ 𝑝𝐴) → (𝐼‘(𝑋 𝑌)) ∈ (SubGrp‘𝑈))
20 dihmeetlem9.a . . . . . . 7 𝐴 = (Atoms‘𝐾)
2112, 20atbase 39268 . . . . . 6 (𝑝𝐴𝑝𝐵)
22213ad2ant3 1136 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑌𝐵) ∧ 𝑝𝐴) → 𝑝𝐵)
2312, 1, 16, 2, 5dihlss 41230 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑝𝐵) → (𝐼𝑝) ∈ (LSubSp‘𝑈))
243, 22, 23syl2anc 584 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑌𝐵) ∧ 𝑝𝐴) → (𝐼𝑝) ∈ (LSubSp‘𝑈))
257, 24sseldd 3983 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑌𝐵) ∧ 𝑝𝐴) → (𝐼𝑝) ∈ (SubGrp‘𝑈))
2612, 1, 16, 2, 5dihlss 41230 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑌𝐵) → (𝐼𝑌) ∈ (LSubSp‘𝑈))
273, 11, 26syl2anc 584 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑌𝐵) ∧ 𝑝𝐴) → (𝐼𝑌) ∈ (LSubSp‘𝑈))
287, 27sseldd 3983 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑌𝐵) ∧ 𝑝𝐴) → (𝐼𝑌) ∈ (SubGrp‘𝑈))
29 dihmeetlem9.l . . . . . 6 = (le‘𝐾)
3012, 29, 13latmle2 18506 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) 𝑌)
319, 10, 11, 30syl3anc 1373 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑌𝐵) ∧ 𝑝𝐴) → (𝑋 𝑌) 𝑌)
3212, 29, 1, 16dihord 41244 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 𝑌) ∈ 𝐵𝑌𝐵) → ((𝐼‘(𝑋 𝑌)) ⊆ (𝐼𝑌) ↔ (𝑋 𝑌) 𝑌))
333, 15, 11, 32syl3anc 1373 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑌𝐵) ∧ 𝑝𝐴) → ((𝐼‘(𝑋 𝑌)) ⊆ (𝐼𝑌) ↔ (𝑋 𝑌) 𝑌))
3431, 33mpbird 257 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑌𝐵) ∧ 𝑝𝐴) → (𝐼‘(𝑋 𝑌)) ⊆ (𝐼𝑌))
35 dihmeetlem9.s . . . 4 = (LSSum‘𝑈)
3635lsmmod 19689 . . 3 ((((𝐼‘(𝑋 𝑌)) ∈ (SubGrp‘𝑈) ∧ (𝐼𝑝) ∈ (SubGrp‘𝑈) ∧ (𝐼𝑌) ∈ (SubGrp‘𝑈)) ∧ (𝐼‘(𝑋 𝑌)) ⊆ (𝐼𝑌)) → ((𝐼‘(𝑋 𝑌)) ((𝐼𝑝) ∩ (𝐼𝑌))) = (((𝐼‘(𝑋 𝑌)) (𝐼𝑝)) ∩ (𝐼𝑌)))
3719, 25, 28, 34, 36syl31anc 1375 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑌𝐵) ∧ 𝑝𝐴) → ((𝐼‘(𝑋 𝑌)) ((𝐼𝑝) ∩ (𝐼𝑌))) = (((𝐼‘(𝑋 𝑌)) (𝐼𝑝)) ∩ (𝐼𝑌)))
38 lmodabl 20899 . . . . 5 (𝑈 ∈ LMod → 𝑈 ∈ Abel)
394, 38syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑌𝐵) ∧ 𝑝𝐴) → 𝑈 ∈ Abel)
4035lsmcom 19872 . . . 4 ((𝑈 ∈ Abel ∧ (𝐼‘(𝑋 𝑌)) ∈ (SubGrp‘𝑈) ∧ (𝐼𝑝) ∈ (SubGrp‘𝑈)) → ((𝐼‘(𝑋 𝑌)) (𝐼𝑝)) = ((𝐼𝑝) (𝐼‘(𝑋 𝑌))))
4139, 19, 25, 40syl3anc 1373 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑌𝐵) ∧ 𝑝𝐴) → ((𝐼‘(𝑋 𝑌)) (𝐼𝑝)) = ((𝐼𝑝) (𝐼‘(𝑋 𝑌))))
4241ineq1d 4218 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑌𝐵) ∧ 𝑝𝐴) → (((𝐼‘(𝑋 𝑌)) (𝐼𝑝)) ∩ (𝐼𝑌)) = (((𝐼𝑝) (𝐼‘(𝑋 𝑌))) ∩ (𝐼𝑌)))
4337, 42eqtr2d 2777 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑌𝐵) ∧ 𝑝𝐴) → (((𝐼𝑝) (𝐼‘(𝑋 𝑌))) ∩ (𝐼𝑌)) = ((𝐼‘(𝑋 𝑌)) ((𝐼𝑝) ∩ (𝐼𝑌))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wcel 2108  cin 3949  wss 3950   class class class wbr 5141  cfv 6559  (class class class)co 7429  Basecbs 17243  lecple 17300  joincjn 18353  meetcmee 18354  Latclat 18472  SubGrpcsubg 19134  LSSumclsm 19648  Abelcabl 19795  LModclmod 20850  LSubSpclss 20921  Atomscatm 39242  HLchlt 39329  LHypclh 39964  DVecHcdvh 41058  DIsoHcdih 41208
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5277  ax-sep 5294  ax-nul 5304  ax-pow 5363  ax-pr 5430  ax-un 7751  ax-cnex 11207  ax-resscn 11208  ax-1cn 11209  ax-icn 11210  ax-addcl 11211  ax-addrcl 11212  ax-mulcl 11213  ax-mulrcl 11214  ax-mulcom 11215  ax-addass 11216  ax-mulass 11217  ax-distr 11218  ax-i2m1 11219  ax-1ne0 11220  ax-1rid 11221  ax-rnegex 11222  ax-rrecex 11223  ax-cnre 11224  ax-pre-lttri 11225  ax-pre-lttrn 11226  ax-pre-ltadd 11227  ax-pre-mulgt0 11228  ax-riotaBAD 38932
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4906  df-int 4945  df-iun 4991  df-iin 4992  df-br 5142  df-opab 5204  df-mpt 5224  df-tr 5258  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5635  df-we 5637  df-xp 5689  df-rel 5690  df-cnv 5691  df-co 5692  df-dm 5693  df-rn 5694  df-res 5695  df-ima 5696  df-pred 6319  df-ord 6385  df-on 6386  df-lim 6387  df-suc 6388  df-iota 6512  df-fun 6561  df-fn 6562  df-f 6563  df-f1 6564  df-fo 6565  df-f1o 6566  df-fv 6567  df-riota 7386  df-ov 7432  df-oprab 7433  df-mpo 7434  df-om 7884  df-1st 8010  df-2nd 8011  df-tpos 8247  df-undef 8294  df-frecs 8302  df-wrecs 8333  df-recs 8407  df-rdg 8446  df-1o 8502  df-2o 8503  df-er 8741  df-map 8864  df-en 8982  df-dom 8983  df-sdom 8984  df-fin 8985  df-pnf 11293  df-mnf 11294  df-xr 11295  df-ltxr 11296  df-le 11297  df-sub 11490  df-neg 11491  df-nn 12263  df-2 12325  df-3 12326  df-4 12327  df-5 12328  df-6 12329  df-n0 12523  df-z 12610  df-uz 12875  df-fz 13544  df-struct 17180  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17244  df-ress 17271  df-plusg 17306  df-mulr 17307  df-sca 17309  df-vsca 17310  df-0g 17482  df-mre 17625  df-mrc 17626  df-acs 17628  df-proset 18336  df-poset 18355  df-plt 18371  df-lub 18387  df-glb 18388  df-join 18389  df-meet 18390  df-p0 18466  df-p1 18467  df-lat 18473  df-clat 18540  df-mgm 18649  df-sgrp 18728  df-mnd 18744  df-submnd 18793  df-grp 18950  df-minusg 18951  df-sbg 18952  df-subg 19137  df-cntz 19331  df-lsm 19650  df-cmn 19796  df-abl 19797  df-mgp 20134  df-rng 20146  df-ur 20175  df-ring 20228  df-oppr 20326  df-dvdsr 20349  df-unit 20350  df-invr 20380  df-dvr 20393  df-drng 20723  df-lmod 20852  df-lss 20922  df-lsp 20962  df-lvec 21094  df-oposet 39155  df-ol 39157  df-oml 39158  df-covers 39245  df-ats 39246  df-atl 39277  df-cvlat 39301  df-hlat 39330  df-llines 39478  df-lplanes 39479  df-lvols 39480  df-lines 39481  df-psubsp 39483  df-pmap 39484  df-padd 39776  df-lhyp 39968  df-laut 39969  df-ldil 40084  df-ltrn 40085  df-trl 40139  df-tendo 40735  df-edring 40737  df-disoa 41009  df-dvech 41059  df-dib 41119  df-dic 41153  df-dih 41209
This theorem is referenced by:  dihmeetlem12N  41298
  Copyright terms: Public domain W3C validator