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

Theorem mgmcl 18610
Description: Closure of the operation of a magma. (Contributed by FL, 14-Sep-2010.) (Revised by AV, 13-Jan-2020.)
Hypotheses
Ref Expression
mgmcl.b 𝐵 = (Base‘𝑀)
mgmcl.o = (+g𝑀)
Assertion
Ref Expression
mgmcl ((𝑀 ∈ Mgm ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)

Proof of Theorem mgmcl
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mgmcl.b . . . . 5 𝐵 = (Base‘𝑀)
2 mgmcl.o . . . . 5 = (+g𝑀)
31, 2ismgm 18608 . . . 4 (𝑀 ∈ Mgm → (𝑀 ∈ Mgm ↔ ∀𝑥𝐵𝑦𝐵 (𝑥 𝑦) ∈ 𝐵))
43ibi 266 . . 3 (𝑀 ∈ Mgm → ∀𝑥𝐵𝑦𝐵 (𝑥 𝑦) ∈ 𝐵)
5 ovrspc2v 7452 . . . 4 (((𝑋𝐵𝑌𝐵) ∧ ∀𝑥𝐵𝑦𝐵 (𝑥 𝑦) ∈ 𝐵) → (𝑋 𝑌) ∈ 𝐵)
65expcom 412 . . 3 (∀𝑥𝐵𝑦𝐵 (𝑥 𝑦) ∈ 𝐵 → ((𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵))
74, 6syl 17 . 2 (𝑀 ∈ Mgm → ((𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵))
873impib 1113 1 ((𝑀 ∈ Mgm ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1084   = wceq 1533  wcel 2098  wral 3058  cfv 6553  (class class class)co 7426  Basecbs 17187  +gcplusg 17240  Mgmcmgm 18605
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699  ax-nul 5310
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-ral 3059  df-rab 3431  df-v 3475  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-iota 6505  df-fv 6561  df-ov 7429  df-mgm 18607
This theorem is referenced by:  isnmgm  18611  mgmsscl  18612  mgmplusf  18617  issstrmgm  18620  gsummgmpropd  18648  mgmhmf1o  18667  idmgmhm  18668  issubmgm2  18670  rabsubmgmd  18671  mgmhmco  18681  mgmhmeql  18683  submgmacs  18684  sgrpcl  18693  mndcl  18709  gsumsgrpccat  18799  smndex1sgrp  18867  dfgrp2  18926  dfgrp3e  19003  mulgnncl  19051  mulgnndir  19065  rngcl  20111  c0mgm  20405  c0snmgmhm  20408  psraddcl  21890  mgmplusgiopALT  47334
  Copyright terms: Public domain W3C validator