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

Theorem issubm 18683
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 6891 . . . . . 6 (π‘š = 𝑀 β†’ (Baseβ€˜π‘š) = (Baseβ€˜π‘€))
21pweqd 4619 . . . . 5 (π‘š = 𝑀 β†’ 𝒫 (Baseβ€˜π‘š) = 𝒫 (Baseβ€˜π‘€))
3 fveq2 6891 . . . . . . 7 (π‘š = 𝑀 β†’ (0gβ€˜π‘š) = (0gβ€˜π‘€))
43eleq1d 2818 . . . . . 6 (π‘š = 𝑀 β†’ ((0gβ€˜π‘š) ∈ 𝑑 ↔ (0gβ€˜π‘€) ∈ 𝑑))
5 fveq2 6891 . . . . . . . . 9 (π‘š = 𝑀 β†’ (+gβ€˜π‘š) = (+gβ€˜π‘€))
65oveqd 7425 . . . . . . . 8 (π‘š = 𝑀 β†’ (π‘₯(+gβ€˜π‘š)𝑦) = (π‘₯(+gβ€˜π‘€)𝑦))
76eleq1d 2818 . . . . . . 7 (π‘š = 𝑀 β†’ ((π‘₯(+gβ€˜π‘š)𝑦) ∈ 𝑑 ↔ (π‘₯(+gβ€˜π‘€)𝑦) ∈ 𝑑))
872ralbidv 3218 . . . . . 6 (π‘š = 𝑀 β†’ (βˆ€π‘₯ ∈ 𝑑 βˆ€π‘¦ ∈ 𝑑 (π‘₯(+gβ€˜π‘š)𝑦) ∈ 𝑑 ↔ βˆ€π‘₯ ∈ 𝑑 βˆ€π‘¦ ∈ 𝑑 (π‘₯(+gβ€˜π‘€)𝑦) ∈ 𝑑))
94, 8anbi12d 631 . . . . 5 (π‘š = 𝑀 β†’ (((0gβ€˜π‘š) ∈ 𝑑 ∧ βˆ€π‘₯ ∈ 𝑑 βˆ€π‘¦ ∈ 𝑑 (π‘₯(+gβ€˜π‘š)𝑦) ∈ 𝑑) ↔ ((0gβ€˜π‘€) ∈ 𝑑 ∧ βˆ€π‘₯ ∈ 𝑑 βˆ€π‘¦ ∈ 𝑑 (π‘₯(+gβ€˜π‘€)𝑦) ∈ 𝑑)))
102, 9rabeqbidv 3449 . . . 4 (π‘š = 𝑀 β†’ {𝑑 ∈ 𝒫 (Baseβ€˜π‘š) ∣ ((0gβ€˜π‘š) ∈ 𝑑 ∧ βˆ€π‘₯ ∈ 𝑑 βˆ€π‘¦ ∈ 𝑑 (π‘₯(+gβ€˜π‘š)𝑦) ∈ 𝑑)} = {𝑑 ∈ 𝒫 (Baseβ€˜π‘€) ∣ ((0gβ€˜π‘€) ∈ 𝑑 ∧ βˆ€π‘₯ ∈ 𝑑 βˆ€π‘¦ ∈ 𝑑 (π‘₯(+gβ€˜π‘€)𝑦) ∈ 𝑑)})
11 df-submnd 18671 . . . 4 SubMnd = (π‘š ∈ Mnd ↦ {𝑑 ∈ 𝒫 (Baseβ€˜π‘š) ∣ ((0gβ€˜π‘š) ∈ 𝑑 ∧ βˆ€π‘₯ ∈ 𝑑 βˆ€π‘¦ ∈ 𝑑 (π‘₯(+gβ€˜π‘š)𝑦) ∈ 𝑑)})
12 fvex 6904 . . . . . 6 (Baseβ€˜π‘€) ∈ V
1312pwex 5378 . . . . 5 𝒫 (Baseβ€˜π‘€) ∈ V
1413rabex 5332 . . . 4 {𝑑 ∈ 𝒫 (Baseβ€˜π‘€) ∣ ((0gβ€˜π‘€) ∈ 𝑑 ∧ βˆ€π‘₯ ∈ 𝑑 βˆ€π‘¦ ∈ 𝑑 (π‘₯(+gβ€˜π‘€)𝑦) ∈ 𝑑)} ∈ V
1510, 11, 14fvmpt 6998 . . 3 (𝑀 ∈ Mnd β†’ (SubMndβ€˜π‘€) = {𝑑 ∈ 𝒫 (Baseβ€˜π‘€) ∣ ((0gβ€˜π‘€) ∈ 𝑑 ∧ βˆ€π‘₯ ∈ 𝑑 βˆ€π‘¦ ∈ 𝑑 (π‘₯(+gβ€˜π‘€)𝑦) ∈ 𝑑)})
1615eleq2d 2819 . 2 (𝑀 ∈ Mnd β†’ (𝑆 ∈ (SubMndβ€˜π‘€) ↔ 𝑆 ∈ {𝑑 ∈ 𝒫 (Baseβ€˜π‘€) ∣ ((0gβ€˜π‘€) ∈ 𝑑 ∧ βˆ€π‘₯ ∈ 𝑑 βˆ€π‘¦ ∈ 𝑑 (π‘₯(+gβ€˜π‘€)𝑦) ∈ 𝑑)}))
17 eleq2 2822 . . . . 5 (𝑑 = 𝑆 β†’ ((0gβ€˜π‘€) ∈ 𝑑 ↔ (0gβ€˜π‘€) ∈ 𝑆))
18 eleq2 2822 . . . . . . 7 (𝑑 = 𝑆 β†’ ((π‘₯(+gβ€˜π‘€)𝑦) ∈ 𝑑 ↔ (π‘₯(+gβ€˜π‘€)𝑦) ∈ 𝑆))
1918raleqbi1dv 3333 . . . . . 6 (𝑑 = 𝑆 β†’ (βˆ€π‘¦ ∈ 𝑑 (π‘₯(+gβ€˜π‘€)𝑦) ∈ 𝑑 ↔ βˆ€π‘¦ ∈ 𝑆 (π‘₯(+gβ€˜π‘€)𝑦) ∈ 𝑆))
2019raleqbi1dv 3333 . . . . 5 (𝑑 = 𝑆 β†’ (βˆ€π‘₯ ∈ 𝑑 βˆ€π‘¦ ∈ 𝑑 (π‘₯(+gβ€˜π‘€)𝑦) ∈ 𝑑 ↔ βˆ€π‘₯ ∈ 𝑆 βˆ€π‘¦ ∈ 𝑆 (π‘₯(+gβ€˜π‘€)𝑦) ∈ 𝑆))
2117, 20anbi12d 631 . . . 4 (𝑑 = 𝑆 β†’ (((0gβ€˜π‘€) ∈ 𝑑 ∧ βˆ€π‘₯ ∈ 𝑑 βˆ€π‘¦ ∈ 𝑑 (π‘₯(+gβ€˜π‘€)𝑦) ∈ 𝑑) ↔ ((0gβ€˜π‘€) ∈ 𝑆 ∧ βˆ€π‘₯ ∈ 𝑆 βˆ€π‘¦ ∈ 𝑆 (π‘₯(+gβ€˜π‘€)𝑦) ∈ 𝑆)))
2221elrab 3683 . . 3 (𝑆 ∈ {𝑑 ∈ 𝒫 (Baseβ€˜π‘€) ∣ ((0gβ€˜π‘€) ∈ 𝑑 ∧ βˆ€π‘₯ ∈ 𝑑 βˆ€π‘¦ ∈ 𝑑 (π‘₯(+gβ€˜π‘€)𝑦) ∈ 𝑑)} ↔ (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ ((0gβ€˜π‘€) ∈ 𝑆 ∧ βˆ€π‘₯ ∈ 𝑆 βˆ€π‘¦ ∈ 𝑆 (π‘₯(+gβ€˜π‘€)𝑦) ∈ 𝑆)))
23 issubm.b . . . . . 6 𝐡 = (Baseβ€˜π‘€)
2423sseq2i 4011 . . . . 5 (𝑆 βŠ† 𝐡 ↔ 𝑆 βŠ† (Baseβ€˜π‘€))
25 issubm.z . . . . . . 7 0 = (0gβ€˜π‘€)
2625eleq1i 2824 . . . . . 6 ( 0 ∈ 𝑆 ↔ (0gβ€˜π‘€) ∈ 𝑆)
27 issubm.p . . . . . . . . 9 + = (+gβ€˜π‘€)
2827oveqi 7421 . . . . . . . 8 (π‘₯ + 𝑦) = (π‘₯(+gβ€˜π‘€)𝑦)
2928eleq1i 2824 . . . . . . 7 ((π‘₯ + 𝑦) ∈ 𝑆 ↔ (π‘₯(+gβ€˜π‘€)𝑦) ∈ 𝑆)
30292ralbii 3128 . . . . . 6 (βˆ€π‘₯ ∈ 𝑆 βˆ€π‘¦ ∈ 𝑆 (π‘₯ + 𝑦) ∈ 𝑆 ↔ βˆ€π‘₯ ∈ 𝑆 βˆ€π‘¦ ∈ 𝑆 (π‘₯(+gβ€˜π‘€)𝑦) ∈ 𝑆)
3126, 30anbi12i 627 . . . . 5 (( 0 ∈ 𝑆 ∧ βˆ€π‘₯ ∈ 𝑆 βˆ€π‘¦ ∈ 𝑆 (π‘₯ + 𝑦) ∈ 𝑆) ↔ ((0gβ€˜π‘€) ∈ 𝑆 ∧ βˆ€π‘₯ ∈ 𝑆 βˆ€π‘¦ ∈ 𝑆 (π‘₯(+gβ€˜π‘€)𝑦) ∈ 𝑆))
3224, 31anbi12i 627 . . . 4 ((𝑆 βŠ† 𝐡 ∧ ( 0 ∈ 𝑆 ∧ βˆ€π‘₯ ∈ 𝑆 βˆ€π‘¦ ∈ 𝑆 (π‘₯ + 𝑦) ∈ 𝑆)) ↔ (𝑆 βŠ† (Baseβ€˜π‘€) ∧ ((0gβ€˜π‘€) ∈ 𝑆 ∧ βˆ€π‘₯ ∈ 𝑆 βˆ€π‘¦ ∈ 𝑆 (π‘₯(+gβ€˜π‘€)𝑦) ∈ 𝑆)))
33 3anass 1095 . . . 4 ((𝑆 βŠ† 𝐡 ∧ 0 ∈ 𝑆 ∧ βˆ€π‘₯ ∈ 𝑆 βˆ€π‘¦ ∈ 𝑆 (π‘₯ + 𝑦) ∈ 𝑆) ↔ (𝑆 βŠ† 𝐡 ∧ ( 0 ∈ 𝑆 ∧ βˆ€π‘₯ ∈ 𝑆 βˆ€π‘¦ ∈ 𝑆 (π‘₯ + 𝑦) ∈ 𝑆)))
3412elpw2 5345 . . . . 5 (𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ↔ 𝑆 βŠ† (Baseβ€˜π‘€))
3534anbi1i 624 . . . 4 ((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ ((0gβ€˜π‘€) ∈ 𝑆 ∧ βˆ€π‘₯ ∈ 𝑆 βˆ€π‘¦ ∈ 𝑆 (π‘₯(+gβ€˜π‘€)𝑦) ∈ 𝑆)) ↔ (𝑆 βŠ† (Baseβ€˜π‘€) ∧ ((0gβ€˜π‘€) ∈ 𝑆 ∧ βˆ€π‘₯ ∈ 𝑆 βˆ€π‘¦ ∈ 𝑆 (π‘₯(+gβ€˜π‘€)𝑦) ∈ 𝑆)))
3632, 33, 353bitr4ri 303 . . 3 ((𝑆 ∈ 𝒫 (Baseβ€˜π‘€) ∧ ((0gβ€˜π‘€) ∈ 𝑆 ∧ βˆ€π‘₯ ∈ 𝑆 βˆ€π‘¦ ∈ 𝑆 (π‘₯(+gβ€˜π‘€)𝑦) ∈ 𝑆)) ↔ (𝑆 βŠ† 𝐡 ∧ 0 ∈ 𝑆 ∧ βˆ€π‘₯ ∈ 𝑆 βˆ€π‘¦ ∈ 𝑆 (π‘₯ + 𝑦) ∈ 𝑆))
3722, 36bitri 274 . 2 (𝑆 ∈ {𝑑 ∈ 𝒫 (Baseβ€˜π‘€) ∣ ((0gβ€˜π‘€) ∈ 𝑑 ∧ βˆ€π‘₯ ∈ 𝑑 βˆ€π‘¦ ∈ 𝑑 (π‘₯(+gβ€˜π‘€)𝑦) ∈ 𝑑)} ↔ (𝑆 βŠ† 𝐡 ∧ 0 ∈ 𝑆 ∧ βˆ€π‘₯ ∈ 𝑆 βˆ€π‘¦ ∈ 𝑆 (π‘₯ + 𝑦) ∈ 𝑆))
3816, 37bitrdi 286 1 (𝑀 ∈ Mnd β†’ (𝑆 ∈ (SubMndβ€˜π‘€) ↔ (𝑆 βŠ† 𝐡 ∧ 0 ∈ 𝑆 ∧ βˆ€π‘₯ ∈ 𝑆 βˆ€π‘¦ ∈ 𝑆 (π‘₯ + 𝑦) ∈ 𝑆)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  βˆ€wral 3061  {crab 3432   βŠ† wss 3948  π’« cpw 4602  β€˜cfv 6543  (class class class)co 7408  Basecbs 17143  +gcplusg 17196  0gc0g 17384  Mndcmnd 18624  SubMndcsubmnd 18669
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-iota 6495  df-fun 6545  df-fv 6551  df-ov 7411  df-submnd 18671
This theorem is referenced by:  issubm2  18684  issubmd  18686  mndissubm  18687  submcl  18692  0subm  18697  insubm  18698  mhmima  18705  mhmeql  18706  submacs  18707  gsumwspan  18726  frmdsssubm  18741  sursubmefmnd  18776  injsubmefmnd  18777  issubg3  19023  cycsubm  19078  cntzsubm  19201  oppgsubm  19228  lsmsubm  19520  issubrg3  20346  xrge0subm  20985  cnsubmlem  20992  nn0srg  21014  rge0srg  21015  efsubm  26059  iistmd  32877  isdomn3  41936  mon1psubm  41938
  Copyright terms: Public domain W3C validator