![]() |
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 17868 | . 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | |
2 | grpcl.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
3 | grpcl.p | . . 3 ⊢ + = (+g‘𝐺) | |
4 | 2, 3 | mndcl 17740 | . 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) |
5 | 1, 4 | syl3an1 1156 | 1 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1080 = wceq 1522 ∈ wcel 2081 ‘cfv 6225 (class class class)co 7016 Basecbs 16312 +gcplusg 16394 Mndcmnd 17733 Grpcgrp 17861 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 ax-nul 5101 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-sbc 3707 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-sn 4473 df-pr 4475 df-op 4479 df-uni 4746 df-br 4963 df-iota 6189 df-fv 6233 df-ov 7019 df-mgm 17681 df-sgrp 17723 df-mnd 17734 df-grp 17864 |
This theorem is referenced by: grprcan 17894 grprinv 17910 grplmulf1o 17930 grpinvadd 17934 grpsubf 17935 grpsubadd 17944 grpaddsubass 17946 grpnpcan 17948 grpsubsub4 17949 grppnpcan2 17950 dfgrp3 17955 grplactcnv 17959 imasgrp 17972 mulgcl 18000 mulgaddcomlem 18004 mulgdir 18013 subgcl 18043 grpissubg 18053 nsgacs 18069 nmzsubg 18074 nsgid 18079 eqger 18083 eqgcpbl 18087 qusgrp 18088 qusadd 18090 ghmrn 18112 idghm 18114 ghmpreima 18121 ghmnsgima 18123 ghmnsgpreima 18124 ghmf1o 18129 conjghm 18130 conjnmz 18133 qusghm 18136 gaid 18170 subgga 18171 gass 18172 gaorber 18179 gastacl 18180 gastacos 18181 cntzsubg 18208 galactghm 18262 lactghmga 18263 symgsssg 18326 symgfisg 18327 symggen 18329 sylow1lem2 18454 sylow2blem1 18475 sylow2blem2 18476 sylow2blem3 18477 sylow3lem1 18482 sylow3lem2 18483 subgdisj1 18544 ablsub4 18658 abladdsub4 18659 mulgdi 18672 mulgghm 18674 invghm 18679 ghmplusg 18689 odadd1 18691 odadd2 18692 odadd 18693 gex2abl 18694 gexexlem 18695 torsubg 18697 oddvdssubg 18698 frgpnabllem2 18717 ringacl 19018 ringpropd 19022 drngmcl 19205 abvtrivd 19301 idsrngd 19323 lmodacl 19335 lmodvacl 19338 lmodprop2d 19386 rmodislmod 19392 prdslmodd 19431 pwssplit2 19522 asclghm 19800 psraddcl 19851 mplind 19969 evlslem1 19982 mhpaddcl 20021 evl1addd 20186 evpmodpmf1o 20422 frlmplusgvalb 20595 scmataddcl 20809 mdetralt 20901 mdetunilem6 20910 opnsubg 22399 ghmcnp 22406 qustgpopn 22411 ngprcan 22902 ngpocelbl 22996 nmotri 23031 ncvspi 23443 cphipval2 23527 4cphipval2 23528 cphipval 23529 efsubm 24816 abvcxp 25873 ttgcontlem1 26354 abliso 30357 ogrpaddltbi 30379 ogrpaddltrbid 30381 ogrpinvlt 30384 cyc3co2 30419 cyc3genpmlem 30431 cycpmconjs 30436 cyc3conja 30437 archiabllem2a 30461 archiabllem2c 30462 archiabllem2b 30463 dvrdir 30515 imaslmod 30576 quslmod 30577 drgextlsp 30600 matunitlindflem1 34438 nelsubgcld 38678 gicabl 39203 isnumbasgrplem2 39208 mendlmod 39297 |
Copyright terms: Public domain | W3C validator |