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

Theorem issubm 17968
Description: Expand definition of a submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.)
Hypotheses
Ref Expression
issubm.b 𝐵 = (Base‘𝑀)
issubm.z 0 = (0g𝑀)
issubm.p + = (+g𝑀)
Assertion
Ref Expression
issubm (𝑀 ∈ Mnd → (𝑆 ∈ (SubMnd‘𝑀) ↔ (𝑆𝐵0𝑆 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆)))
Distinct variable groups:   𝑥,𝑀,𝑦   𝑥,𝑆,𝑦
Allowed substitution hints:   𝐵(𝑥,𝑦)   + (𝑥,𝑦)   0 (𝑥,𝑦)

Proof of Theorem issubm
Dummy variables 𝑚 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6661 . . . . . 6 (𝑚 = 𝑀 → (Base‘𝑚) = (Base‘𝑀))
21pweqd 4541 . . . . 5 (𝑚 = 𝑀 → 𝒫 (Base‘𝑚) = 𝒫 (Base‘𝑀))
3 fveq2 6661 . . . . . . 7 (𝑚 = 𝑀 → (0g𝑚) = (0g𝑀))
43eleq1d 2900 . . . . . 6 (𝑚 = 𝑀 → ((0g𝑚) ∈ 𝑡 ↔ (0g𝑀) ∈ 𝑡))
5 fveq2 6661 . . . . . . . . 9 (𝑚 = 𝑀 → (+g𝑚) = (+g𝑀))
65oveqd 7166 . . . . . . . 8 (𝑚 = 𝑀 → (𝑥(+g𝑚)𝑦) = (𝑥(+g𝑀)𝑦))
76eleq1d 2900 . . . . . . 7 (𝑚 = 𝑀 → ((𝑥(+g𝑚)𝑦) ∈ 𝑡 ↔ (𝑥(+g𝑀)𝑦) ∈ 𝑡))
872ralbidv 3194 . . . . . 6 (𝑚 = 𝑀 → (∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑚)𝑦) ∈ 𝑡 ↔ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑀)𝑦) ∈ 𝑡))
94, 8anbi12d 633 . . . . 5 (𝑚 = 𝑀 → (((0g𝑚) ∈ 𝑡 ∧ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑚)𝑦) ∈ 𝑡) ↔ ((0g𝑀) ∈ 𝑡 ∧ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑀)𝑦) ∈ 𝑡)))
102, 9rabeqbidv 3471 . . . 4 (𝑚 = 𝑀 → {𝑡 ∈ 𝒫 (Base‘𝑚) ∣ ((0g𝑚) ∈ 𝑡 ∧ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑚)𝑦) ∈ 𝑡)} = {𝑡 ∈ 𝒫 (Base‘𝑀) ∣ ((0g𝑀) ∈ 𝑡 ∧ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑀)𝑦) ∈ 𝑡)})
11 df-submnd 17957 . . . 4 SubMnd = (𝑚 ∈ Mnd ↦ {𝑡 ∈ 𝒫 (Base‘𝑚) ∣ ((0g𝑚) ∈ 𝑡 ∧ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑚)𝑦) ∈ 𝑡)})
12 fvex 6674 . . . . . 6 (Base‘𝑀) ∈ V
1312pwex 5268 . . . . 5 𝒫 (Base‘𝑀) ∈ V
1413rabex 5221 . . . 4 {𝑡 ∈ 𝒫 (Base‘𝑀) ∣ ((0g𝑀) ∈ 𝑡 ∧ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑀)𝑦) ∈ 𝑡)} ∈ V
1510, 11, 14fvmpt 6759 . . 3 (𝑀 ∈ Mnd → (SubMnd‘𝑀) = {𝑡 ∈ 𝒫 (Base‘𝑀) ∣ ((0g𝑀) ∈ 𝑡 ∧ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑀)𝑦) ∈ 𝑡)})
1615eleq2d 2901 . 2 (𝑀 ∈ Mnd → (𝑆 ∈ (SubMnd‘𝑀) ↔ 𝑆 ∈ {𝑡 ∈ 𝒫 (Base‘𝑀) ∣ ((0g𝑀) ∈ 𝑡 ∧ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑀)𝑦) ∈ 𝑡)}))
17 eleq2 2904 . . . . 5 (𝑡 = 𝑆 → ((0g𝑀) ∈ 𝑡 ↔ (0g𝑀) ∈ 𝑆))
18 eleq2 2904 . . . . . . 7 (𝑡 = 𝑆 → ((𝑥(+g𝑀)𝑦) ∈ 𝑡 ↔ (𝑥(+g𝑀)𝑦) ∈ 𝑆))
1918raleqbi1dv 3394 . . . . . 6 (𝑡 = 𝑆 → (∀𝑦𝑡 (𝑥(+g𝑀)𝑦) ∈ 𝑡 ↔ ∀𝑦𝑆 (𝑥(+g𝑀)𝑦) ∈ 𝑆))
2019raleqbi1dv 3394 . . . . 5 (𝑡 = 𝑆 → (∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑀)𝑦) ∈ 𝑡 ↔ ∀𝑥𝑆𝑦𝑆 (𝑥(+g𝑀)𝑦) ∈ 𝑆))
2117, 20anbi12d 633 . . . 4 (𝑡 = 𝑆 → (((0g𝑀) ∈ 𝑡 ∧ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑀)𝑦) ∈ 𝑡) ↔ ((0g𝑀) ∈ 𝑆 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥(+g𝑀)𝑦) ∈ 𝑆)))
2221elrab 3666 . . 3 (𝑆 ∈ {𝑡 ∈ 𝒫 (Base‘𝑀) ∣ ((0g𝑀) ∈ 𝑡 ∧ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑀)𝑦) ∈ 𝑡)} ↔ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ((0g𝑀) ∈ 𝑆 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥(+g𝑀)𝑦) ∈ 𝑆)))
23 issubm.b . . . . . 6 𝐵 = (Base‘𝑀)
2423sseq2i 3982 . . . . 5 (𝑆𝐵𝑆 ⊆ (Base‘𝑀))
25 issubm.z . . . . . . 7 0 = (0g𝑀)
2625eleq1i 2906 . . . . . 6 ( 0𝑆 ↔ (0g𝑀) ∈ 𝑆)
27 issubm.p . . . . . . . . 9 + = (+g𝑀)
2827oveqi 7162 . . . . . . . 8 (𝑥 + 𝑦) = (𝑥(+g𝑀)𝑦)
2928eleq1i 2906 . . . . . . 7 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑥(+g𝑀)𝑦) ∈ 𝑆)
30292ralbii 3161 . . . . . 6 (∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆 ↔ ∀𝑥𝑆𝑦𝑆 (𝑥(+g𝑀)𝑦) ∈ 𝑆)
3126, 30anbi12i 629 . . . . 5 (( 0𝑆 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆) ↔ ((0g𝑀) ∈ 𝑆 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥(+g𝑀)𝑦) ∈ 𝑆))
3224, 31anbi12i 629 . . . 4 ((𝑆𝐵 ∧ ( 0𝑆 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆)) ↔ (𝑆 ⊆ (Base‘𝑀) ∧ ((0g𝑀) ∈ 𝑆 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥(+g𝑀)𝑦) ∈ 𝑆)))
33 3anass 1092 . . . 4 ((𝑆𝐵0𝑆 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆) ↔ (𝑆𝐵 ∧ ( 0𝑆 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆)))
3412elpw2 5234 . . . . 5 (𝑆 ∈ 𝒫 (Base‘𝑀) ↔ 𝑆 ⊆ (Base‘𝑀))
3534anbi1i 626 . . . 4 ((𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ((0g𝑀) ∈ 𝑆 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥(+g𝑀)𝑦) ∈ 𝑆)) ↔ (𝑆 ⊆ (Base‘𝑀) ∧ ((0g𝑀) ∈ 𝑆 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥(+g𝑀)𝑦) ∈ 𝑆)))
3632, 33, 353bitr4ri 307 . . 3 ((𝑆 ∈ 𝒫 (Base‘𝑀) ∧ ((0g𝑀) ∈ 𝑆 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥(+g𝑀)𝑦) ∈ 𝑆)) ↔ (𝑆𝐵0𝑆 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆))
3722, 36bitri 278 . 2 (𝑆 ∈ {𝑡 ∈ 𝒫 (Base‘𝑀) ∣ ((0g𝑀) ∈ 𝑡 ∧ ∀𝑥𝑡𝑦𝑡 (𝑥(+g𝑀)𝑦) ∈ 𝑡)} ↔ (𝑆𝐵0𝑆 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆))
3816, 37syl6bb 290 1 (𝑀 ∈ Mnd → (𝑆 ∈ (SubMnd‘𝑀) ↔ (𝑆𝐵0𝑆 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥 + 𝑦) ∈ 𝑆)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2115  wral 3133  {crab 3137  wss 3919  𝒫 cpw 4522  cfv 6343  (class class class)co 7149  Basecbs 16483  +gcplusg 16565  0gc0g 16713  Mndcmnd 17911  SubMndcsubmnd 17955
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5447  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-iota 6302  df-fun 6345  df-fv 6351  df-ov 7152  df-submnd 17957
This theorem is referenced by:  issubm2  17969  issubmd  17971  mndissubm  17972  submcl  17977  0subm  17982  insubm  17983  mhmima  17989  mhmeql  17990  submacs  17991  gsumwspan  18011  frmdsssubm  18026  sursubmefmnd  18061  injsubmefmnd  18062  issubg3  18297  cycsubm  18345  cntzsubm  18466  oppgsubm  18490  lsmsubm  18778  issubrg3  19563  xrge0subm  20586  cnsubmlem  20593  nn0srg  20615  rge0srg  20616  efsubm  25146  iistmd  31202  isdomn3  40064  mon1psubm  40066
  Copyright terms: Public domain W3C validator