![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mndcl | Structured version Visualization version GIF version |
Description: Closure of the operation of a monoid. (Contributed by NM, 14-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Proof shortened by AV, 8-Feb-2020.) |
Ref | Expression |
---|---|
mndcl.b | ⊢ 𝐵 = (Base‘𝐺) |
mndcl.p | ⊢ + = (+g‘𝐺) |
Ref | Expression |
---|---|
mndcl | ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mndmgm 18668 | . 2 ⊢ (𝐺 ∈ Mnd → 𝐺 ∈ Mgm) | |
2 | mndcl.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
3 | mndcl.p | . . 3 ⊢ + = (+g‘𝐺) | |
4 | 2, 3 | mgmcl 18570 | . 2 ⊢ ((𝐺 ∈ Mgm ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) |
5 | 1, 4 | syl3an1 1161 | 1 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1085 = wceq 1539 ∈ wcel 2104 ‘cfv 6544 (class class class)co 7413 Basecbs 17150 +gcplusg 17203 Mgmcmgm 18565 Mndcmnd 18661 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-ext 2701 ax-nul 5307 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-ne 2939 df-ral 3060 df-rex 3069 df-rab 3431 df-v 3474 df-sbc 3779 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-iota 6496 df-fv 6552 df-ov 7416 df-mgm 18567 df-sgrp 18646 df-mnd 18662 |
This theorem is referenced by: mnd4g 18675 mndpropd 18686 issubmnd 18688 prdsplusgcl 18692 imasmnd 18699 xpsmnd0 18702 idmhm 18719 mhmf1o 18720 issubmd 18725 0mhm 18738 mhmco 18742 mhmeql 18745 submacs 18746 mndind 18747 prdspjmhm 18748 pwsdiagmhm 18750 pwsco1mhm 18751 pwsco2mhm 18752 gsumwmhm 18764 grpcl 18865 mhmmnd 18985 mulgnn0cl 19008 cntzsubm 19245 oppgmnd 19264 lsmssv 19554 frgp0 19671 frgpadd 19674 mulgnn0di 19736 mulgmhm 19738 gsumval3eu 19815 gsumval3 19818 gsumzcl2 19821 gsumzaddlem 19832 gsumzmhm 19848 gsummptfzcl 19880 srgcl 20089 srgacl 20101 srgbinomlem 20126 srgbinom 20127 ringcl 20146 ringpropd 20178 c0mhm 20353 mndvcl 22115 mhmvlin 22121 mat2pmatghm 22454 pm2mpghm 22540 cpmadugsumlemF 22600 tsmsadd 23873 omndadd2d 32494 omndadd2rd 32495 slmdacl 32622 slmdvacl 32625 gsumncl 33847 ofaddmndmap 47109 lincsum 47199 mndtccatid 47802 |
Copyright terms: Public domain | W3C validator |