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 17429 | . 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | |
2 | grpcl.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
3 | grpcl.p | . . 3 ⊢ + = (+g‘𝐺) | |
4 | 2, 3 | mndcl 17301 | . 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) |
5 | 1, 4 | syl3an1 1359 | 1 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ‘cfv 5888 (class class class)co 6650 Basecbs 15857 +gcplusg 15941 Mndcmnd 17294 Grpcgrp 17422 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-nul 4789 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-iota 5851 df-fv 5896 df-ov 6653 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-grp 17425 |
This theorem is referenced by: grprcan 17455 grprinv 17469 grplmulf1o 17489 grpinvadd 17493 grpsubf 17494 grpsubadd 17503 grpaddsubass 17505 grpnpcan 17507 grpsubsub4 17508 grppnpcan2 17509 dfgrp3 17514 grplactcnv 17518 imasgrp 17531 mulgcl 17559 mulgaddcomlem 17563 mulgdir 17573 subgcl 17604 grpissubg 17614 nsgacs 17630 nmzsubg 17635 nsgid 17640 eqger 17644 eqgcpbl 17648 qusgrp 17649 qusadd 17651 ghmrn 17673 idghm 17675 ghmpreima 17682 ghmnsgima 17684 ghmnsgpreima 17685 ghmf1o 17690 conjghm 17691 conjnmz 17694 qusghm 17697 gaid 17732 subgga 17733 gass 17734 gaorber 17741 gastacl 17742 gastacos 17743 cntzsubg 17769 galactghm 17823 lactghmga 17824 symgsssg 17887 symgfisg 17888 symggen 17890 sylow1lem2 18014 sylow2blem1 18035 sylow2blem2 18036 sylow2blem3 18037 sylow3lem1 18042 sylow3lem2 18043 subgdisj1 18104 ablsub4 18218 abladdsub4 18219 mulgdi 18232 mulgghm 18234 invghm 18239 ghmplusg 18249 odadd1 18251 odadd2 18252 odadd 18253 gex2abl 18254 gexexlem 18255 torsubg 18257 oddvdssubg 18258 frgpnabllem2 18277 ringacl 18578 ringpropd 18582 drngmcl 18760 abvtrivd 18840 idsrngd 18862 lmodacl 18874 lmodvacl 18877 lmodprop2d 18925 rmodislmod 18931 prdslmodd 18969 pwssplit2 19060 asclghm 19338 psraddcl 19383 mplind 19502 evlslem1 19515 evl1addd 19705 evpmodpmf1o 19942 scmataddcl 20322 mdetralt 20414 mdetunilem6 20423 opnsubg 21911 ghmcnp 21918 qustgpopn 21923 ngprcan 22414 ngpocelbl 22508 nmotri 22543 ncvspi 22956 cphipval2 23040 4cphipval2 23041 cphipval 23042 efsubm 24297 abvcxp 25304 ttgcontlem1 25765 abliso 29696 ogrpaddltbi 29719 ogrpaddltrbid 29721 ogrpinvlt 29724 archiabllem2a 29748 archiabllem2c 29749 archiabllem2b 29750 dvrdir 29790 matunitlindflem1 33405 gicabl 37669 isnumbasgrplem2 37674 mendlmod 37763 |
Copyright terms: Public domain | W3C validator |