MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lssacs Structured version   Visualization version   GIF version

Theorem lssacs 19474
Description: Submodules are an algebraic closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.)
Hypotheses
Ref Expression
lssacs.b 𝐵 = (Base‘𝑊)
lssacs.s 𝑆 = (LSubSp‘𝑊)
Assertion
Ref Expression
lssacs (𝑊 ∈ LMod → 𝑆 ∈ (ACS‘𝐵))

Proof of Theorem lssacs
Dummy variables 𝑎 𝑏 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lssacs.b . . . . . 6 𝐵 = (Base‘𝑊)
2 lssacs.s . . . . . 6 𝑆 = (LSubSp‘𝑊)
31, 2lssss 19443 . . . . 5 (𝑎𝑆𝑎𝐵)
43a1i 11 . . . 4 (𝑊 ∈ LMod → (𝑎𝑆𝑎𝐵))
5 inss2 4088 . . . . . . . 8 ((SubGrp‘𝑊) ∩ {𝑏 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑏 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑏}) ⊆ {𝑏 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑏 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑏}
6 ssrab2 3941 . . . . . . . 8 {𝑏 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑏 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑏} ⊆ 𝒫 𝐵
75, 6sstri 3862 . . . . . . 7 ((SubGrp‘𝑊) ∩ {𝑏 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑏 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑏}) ⊆ 𝒫 𝐵
87sseli 3849 . . . . . 6 (𝑎 ∈ ((SubGrp‘𝑊) ∩ {𝑏 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑏 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑏}) → 𝑎 ∈ 𝒫 𝐵)
98elpwid 4429 . . . . 5 (𝑎 ∈ ((SubGrp‘𝑊) ∩ {𝑏 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑏 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑏}) → 𝑎𝐵)
109a1i 11 . . . 4 (𝑊 ∈ LMod → (𝑎 ∈ ((SubGrp‘𝑊) ∩ {𝑏 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑏 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑏}) → 𝑎𝐵))
11 eqid 2773 . . . . . . . . 9 (Scalar‘𝑊) = (Scalar‘𝑊)
12 eqid 2773 . . . . . . . . 9 (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
13 eqid 2773 . . . . . . . . 9 ( ·𝑠𝑊) = ( ·𝑠𝑊)
1411, 12, 1, 13, 2islss4 19469 . . . . . . . 8 (𝑊 ∈ LMod → (𝑎𝑆 ↔ (𝑎 ∈ (SubGrp‘𝑊) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑎 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑎)))
1514adantr 473 . . . . . . 7 ((𝑊 ∈ LMod ∧ 𝑎𝐵) → (𝑎𝑆 ↔ (𝑎 ∈ (SubGrp‘𝑊) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑎 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑎)))
16 selpw 4424 . . . . . . . . . 10 (𝑎 ∈ 𝒫 𝐵𝑎𝐵)
17 eleq2w 2844 . . . . . . . . . . . . 13 (𝑏 = 𝑎 → ((𝑥( ·𝑠𝑊)𝑦) ∈ 𝑏 ↔ (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑎))
1817raleqbi1dv 3338 . . . . . . . . . . . 12 (𝑏 = 𝑎 → (∀𝑦𝑏 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑏 ↔ ∀𝑦𝑎 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑎))
1918ralbidv 3142 . . . . . . . . . . 11 (𝑏 = 𝑎 → (∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑏 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑏 ↔ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑎 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑎))
2019elrab3 3592 . . . . . . . . . 10 (𝑎 ∈ 𝒫 𝐵 → (𝑎 ∈ {𝑏 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑏 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑏} ↔ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑎 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑎))
2116, 20sylbir 227 . . . . . . . . 9 (𝑎𝐵 → (𝑎 ∈ {𝑏 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑏 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑏} ↔ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑎 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑎))
2221adantl 474 . . . . . . . 8 ((𝑊 ∈ LMod ∧ 𝑎𝐵) → (𝑎 ∈ {𝑏 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑏 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑏} ↔ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑎 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑎))
2322anbi2d 620 . . . . . . 7 ((𝑊 ∈ LMod ∧ 𝑎𝐵) → ((𝑎 ∈ (SubGrp‘𝑊) ∧ 𝑎 ∈ {𝑏 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑏 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑏}) ↔ (𝑎 ∈ (SubGrp‘𝑊) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑎 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑎)))
2415, 23bitr4d 274 . . . . . 6 ((𝑊 ∈ LMod ∧ 𝑎𝐵) → (𝑎𝑆 ↔ (𝑎 ∈ (SubGrp‘𝑊) ∧ 𝑎 ∈ {𝑏 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑏 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑏})))
25 elin 4052 . . . . . 6 (𝑎 ∈ ((SubGrp‘𝑊) ∩ {𝑏 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑏 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑏}) ↔ (𝑎 ∈ (SubGrp‘𝑊) ∧ 𝑎 ∈ {𝑏 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑏 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑏}))
2624, 25syl6bbr 281 . . . . 5 ((𝑊 ∈ LMod ∧ 𝑎𝐵) → (𝑎𝑆𝑎 ∈ ((SubGrp‘𝑊) ∩ {𝑏 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑏 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑏})))
2726ex 405 . . . 4 (𝑊 ∈ LMod → (𝑎𝐵 → (𝑎𝑆𝑎 ∈ ((SubGrp‘𝑊) ∩ {𝑏 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑏 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑏}))))
284, 10, 27pm5.21ndd 372 . . 3 (𝑊 ∈ LMod → (𝑎𝑆𝑎 ∈ ((SubGrp‘𝑊) ∩ {𝑏 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑏 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑏})))
2928eqrdv 2771 . 2 (𝑊 ∈ LMod → 𝑆 = ((SubGrp‘𝑊) ∩ {𝑏 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑏 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑏}))
301fvexi 6511 . . . 4 𝐵 ∈ V
31 mreacs 16800 . . . 4 (𝐵 ∈ V → (ACS‘𝐵) ∈ (Moore‘𝒫 𝐵))
3230, 31mp1i 13 . . 3 (𝑊 ∈ LMod → (ACS‘𝐵) ∈ (Moore‘𝒫 𝐵))
33 lmodgrp 19376 . . . 4 (𝑊 ∈ LMod → 𝑊 ∈ Grp)
341subgacs 18111 . . . 4 (𝑊 ∈ Grp → (SubGrp‘𝑊) ∈ (ACS‘𝐵))
3533, 34syl 17 . . 3 (𝑊 ∈ LMod → (SubGrp‘𝑊) ∈ (ACS‘𝐵))
361, 11, 13, 12lmodvscl 19386 . . . . . 6 ((𝑊 ∈ LMod ∧ 𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦𝐵) → (𝑥( ·𝑠𝑊)𝑦) ∈ 𝐵)
37363expb 1101 . . . . 5 ((𝑊 ∈ LMod ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦𝐵)) → (𝑥( ·𝑠𝑊)𝑦) ∈ 𝐵)
3837ralrimivva 3136 . . . 4 (𝑊 ∈ LMod → ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝐵 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝐵)
39 acsfn1c 16804 . . . 4 ((𝐵 ∈ V ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝐵 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝐵) → {𝑏 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑏 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑏} ∈ (ACS‘𝐵))
4030, 38, 39sylancr 579 . . 3 (𝑊 ∈ LMod → {𝑏 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑏 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑏} ∈ (ACS‘𝐵))
41 mreincl 16741 . . 3 (((ACS‘𝐵) ∈ (Moore‘𝒫 𝐵) ∧ (SubGrp‘𝑊) ∈ (ACS‘𝐵) ∧ {𝑏 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑏 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑏} ∈ (ACS‘𝐵)) → ((SubGrp‘𝑊) ∩ {𝑏 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑏 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑏}) ∈ (ACS‘𝐵))
4232, 35, 40, 41syl3anc 1352 . 2 (𝑊 ∈ LMod → ((SubGrp‘𝑊) ∩ {𝑏 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦𝑏 (𝑥( ·𝑠𝑊)𝑦) ∈ 𝑏}) ∈ (ACS‘𝐵))
4329, 42eqeltrd 2861 1 (𝑊 ∈ LMod → 𝑆 ∈ (ACS‘𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387   = wceq 1508  wcel 2051  wral 3083  {crab 3087  Vcvv 3410  cin 3823  wss 3824  𝒫 cpw 4417  cfv 6186  (class class class)co 6975  Basecbs 16338  Scalarcsca 16423   ·𝑠 cvsca 16424  Moorecmre 16724  ACScacs 16727  Grpcgrp 17904  SubGrpcsubg 18070  LModclmod 19369  LSubSpclss 19438
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 2745  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278  ax-cnex 10390  ax-resscn 10391  ax-1cn 10392  ax-icn 10393  ax-addcl 10394  ax-addrcl 10395  ax-mulcl 10396  ax-mulrcl 10397  ax-mulcom 10398  ax-addass 10399  ax-mulass 10400  ax-distr 10401  ax-i2m1 10402  ax-1ne0 10403  ax-1rid 10404  ax-rnegex 10405  ax-rrecex 10406  ax-cnre 10407  ax-pre-lttri 10408  ax-pre-lttrn 10409  ax-pre-ltadd 10410  ax-pre-mulgt0 10411
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-nel 3069  df-ral 3088  df-rex 3089  df-reu 3090  df-rmo 3091  df-rab 3092  df-v 3412  df-sbc 3677  df-csb 3782  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-pss 3840  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-tp 4441  df-op 4443  df-uni 4710  df-int 4747  df-iun 4791  df-iin 4792  df-br 4927  df-opab 4989  df-mpt 5006  df-tr 5028  df-id 5309  df-eprel 5314  df-po 5323  df-so 5324  df-fr 5363  df-we 5365  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-pred 5984  df-ord 6030  df-on 6031  df-lim 6032  df-suc 6033  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-riota 6936  df-ov 6978  df-oprab 6979  df-mpo 6980  df-om 7396  df-1st 7500  df-2nd 7501  df-wrecs 7749  df-recs 7811  df-rdg 7849  df-1o 7904  df-oadd 7908  df-er 8088  df-en 8306  df-dom 8307  df-sdom 8308  df-fin 8309  df-pnf 10475  df-mnf 10476  df-xr 10477  df-ltxr 10478  df-le 10479  df-sub 10671  df-neg 10672  df-nn 11439  df-2 11502  df-ndx 16341  df-slot 16342  df-base 16344  df-sets 16345  df-ress 16346  df-plusg 16433  df-0g 16570  df-mre 16728  df-mrc 16729  df-acs 16731  df-mgm 17723  df-sgrp 17765  df-mnd 17776  df-submnd 17817  df-grp 17907  df-minusg 17908  df-sbg 17909  df-subg 18073  df-mgp 18976  df-ur 18988  df-ring 19035  df-lmod 19371  df-lss 19439
This theorem is referenced by:  lssacsex  19651  lidlacs  19728
  Copyright terms: Public domain W3C validator