| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > grpcl | Structured version Visualization version GIF version | ||
| Description: Closure of the operation of a group. (Contributed by NM, 14-Aug-2011.) |
| Ref | Expression |
|---|---|
| grpcl.b | ⊢ 𝐵 = (Base‘𝐺) |
| grpcl.p | ⊢ + = (+g‘𝐺) |
| Ref | Expression |
|---|---|
| grpcl | ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | grpmnd 18870 | . 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | |
| 2 | grpcl.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
| 3 | grpcl.p | . . 3 ⊢ + = (+g‘𝐺) | |
| 4 | 2, 3 | mndcl 18667 | . 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) |
| 5 | 1, 4 | syl3an1 1163 | 1 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ‘cfv 6492 (class class class)co 7358 Basecbs 17136 +gcplusg 17177 Mndcmnd 18659 Grpcgrp 18863 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-ext 2708 ax-nul 5251 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-sb 2068 df-clab 2715 df-cleq 2728 df-clel 2811 df-ne 2933 df-ral 3052 df-rex 3061 df-rab 3400 df-v 3442 df-sbc 3741 df-dif 3904 df-un 3906 df-ss 3918 df-nul 4286 df-if 4480 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-br 5099 df-iota 6448 df-fv 6500 df-ov 7361 df-mgm 18565 df-sgrp 18644 df-mnd 18660 df-grp 18866 |
| This theorem is referenced by: grpcld 18877 grprcan 18903 grprinv 18920 grplmulf1o 18943 grpinvadd 18948 grpsubf 18949 grpsubadd 18958 grpaddsubass 18960 grpnpcan 18962 grpsubsub4 18963 grppnpcan2 18964 grplactcnv 18973 imasgrp 18986 mulgcl 19021 mulgaddcomlem 19027 mulgdir 19036 subgcl 19066 nsgacs 19091 nmzsubg 19094 nsgid 19099 eqgcpbl 19111 qusgrp 19115 qusadd 19117 ecqusaddcl 19122 qus0subgadd 19128 ghmrn 19158 idghm 19160 ghmpreima 19167 ghmnsgima 19169 ghmnsgpreima 19170 ghmf1o 19177 conjghm 19178 qusghm 19184 gaid 19228 subgga 19229 gass 19230 gaorber 19237 gastacl 19238 gastacos 19239 cntzsubg 19268 galactghm 19333 lactghmga 19334 symgsssg 19396 symgfisg 19397 symggen 19399 sylow1lem2 19528 sylow2blem1 19549 sylow2blem2 19550 sylow2blem3 19551 sylow3lem1 19556 sylow3lem2 19557 subgdisj1 19620 ablsub4 19739 abladdsub4 19740 mulgdi 19755 mulgghm 19757 invghm 19762 ghmplusg 19775 odadd1 19777 odadd2 19778 odadd 19779 gex2abl 19780 gexexlem 19781 torsubg 19783 oddvdssubg 19784 frgpnabllem2 19803 ogrpaddltbi 20068 ogrpaddltrbid 20070 ogrpinvlt 20073 rngacl 20097 rngpropd 20109 ringacl 20213 ringpropd 20223 dvrdir 20348 drngmclOLD 20684 abvtrivd 20765 idsrngd 20789 lmodacl 20823 lmodvacl 20826 lmodprop2d 20875 rmodislmod 20881 prdslmodd 20920 pwssplit2 21012 evpmodpmf1o 21551 frlmplusgvalb 21724 asclghm 21838 psraddclOLD 21895 mplind 22025 evlslem1 22037 evl1addd 22285 scmataddcl 22460 mdetralt 22552 mdetunilem6 22561 opnsubg 24052 ghmcnp 24059 qustgpopn 24064 ngprcan 24554 ngpocelbl 24648 nmotri 24683 ncvspi 25112 cphipval2 25197 4cphipval2 25198 cphipval 25199 efsubm 26516 abvcxp 27582 ttgcontlem1 28957 abliso 33118 cyc3co2 33222 cyc3genpmlem 33233 cycpmconjs 33238 cyc3conja 33239 archiabllem2a 33276 archiabllem2c 33277 archiabllem2b 33278 imaslmod 33434 quslmod 33439 qusxpid 33444 nsgmgclem 33492 drgextlsp 33750 matunitlindflem1 37817 fldhmf1 42344 primrootsunit1 42351 aks6d1c1p2 42363 aks6d1c1p3 42364 nelsubgcld 42752 evlsaddval 42814 fsuppssind 42836 gicabl 43341 isnumbasgrplem2 43346 mendlmod 43431 |
| Copyright terms: Public domain | W3C validator |