![]() |
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 18822 | . 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | |
2 | grpcl.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
3 | grpcl.p | . . 3 ⊢ + = (+g‘𝐺) | |
4 | 2, 3 | mndcl 18629 | . 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) |
5 | 1, 4 | syl3an1 1163 | 1 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ‘cfv 6540 (class class class)co 7405 Basecbs 17140 +gcplusg 17193 Mndcmnd 18621 Grpcgrp 18815 |
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-ext 2703 ax-nul 5305 |
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-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3433 df-v 3476 df-sbc 3777 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-iota 6492 df-fv 6548 df-ov 7408 df-mgm 18557 df-sgrp 18606 df-mnd 18622 df-grp 18818 |
This theorem is referenced by: grpcld 18829 grprcan 18854 grprinv 18871 grplmulf1o 18893 grpinvadd 18897 grpsubf 18898 grpsubadd 18907 grpaddsubass 18909 grpnpcan 18911 grpsubsub4 18912 grppnpcan2 18913 grplactcnv 18922 imasgrp 18935 mulgcl 18965 mulgaddcomlem 18971 mulgdir 18980 subgcl 19010 nsgacs 19036 nmzsubg 19039 nsgid 19044 eqgcpbl 19056 qusgrp 19059 qusadd 19061 qus0subgadd 19070 ghmrn 19099 idghm 19101 ghmpreima 19108 ghmnsgima 19110 ghmnsgpreima 19111 ghmf1o 19116 conjghm 19117 conjnmz 19120 qusghm 19123 gaid 19157 subgga 19158 gass 19159 gaorber 19166 gastacl 19167 gastacos 19168 cntzsubg 19197 galactghm 19266 lactghmga 19267 symgsssg 19329 symgfisg 19330 symggen 19332 sylow1lem2 19461 sylow2blem1 19482 sylow2blem2 19483 sylow2blem3 19484 sylow3lem1 19489 sylow3lem2 19490 subgdisj1 19553 ablsub4 19672 abladdsub4 19673 mulgdi 19688 mulgghm 19690 invghm 19695 ghmplusg 19708 odadd1 19710 odadd2 19711 odadd 19712 gex2abl 19713 gexexlem 19714 torsubg 19716 oddvdssubg 19717 frgpnabllem2 19736 ringacl 20088 ringpropd 20095 dvrdir 20218 drngmcl 20324 abvtrivd 20440 idsrngd 20462 lmodacl 20475 lmodvacl 20478 lmodprop2d 20526 rmodislmod 20532 rmodislmodOLD 20533 prdslmodd 20572 pwssplit2 20663 evpmodpmf1o 21140 frlmplusgvalb 21315 asclghm 21428 psraddcl 21493 mplind 21622 evlslem1 21636 mhpaddcl 21685 evl1addd 21851 scmataddcl 22009 mdetralt 22101 mdetunilem6 22110 opnsubg 23603 ghmcnp 23610 qustgpopn 23615 ngprcan 24110 ngpocelbl 24212 nmotri 24247 ncvspi 24664 cphipval2 24749 4cphipval2 24750 cphipval 24751 efsubm 26051 abvcxp 27107 ttgcontlem1 28131 abliso 32184 ogrpaddltbi 32223 ogrpaddltrbid 32225 ogrpinvlt 32228 cyc3co2 32286 cyc3genpmlem 32297 cycpmconjs 32302 cyc3conja 32303 archiabllem2a 32327 archiabllem2c 32328 archiabllem2b 32329 imaslmod 32456 quslmod 32457 qusxpid 32463 nsgmgclem 32510 drgextlsp 32669 matunitlindflem1 36472 fldhmf1 40943 nelsubgcld 41068 evlsaddval 41137 fsuppssind 41162 gicabl 41826 isnumbasgrplem2 41831 mendlmod 41920 rngacl 46647 rngpropd 46659 ecqusaddcl 46750 |
Copyright terms: Public domain | W3C validator |