![]() |
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 17614 | . 2 ⊢ (𝐺 ∈ Mnd → 𝐺 ∈ Mgm) | |
2 | mndcl.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
3 | mndcl.p | . . 3 ⊢ + = (+g‘𝐺) | |
4 | 2, 3 | mgmcl 17559 | . 2 ⊢ ((𝐺 ∈ Mgm ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) |
5 | 1, 4 | syl3an1 1203 | 1 ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1108 = wceq 1653 ∈ wcel 2157 ‘cfv 6102 (class class class)co 6879 Basecbs 16183 +gcplusg 16266 Mgmcmgm 17554 Mndcmnd 17608 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2378 ax-ext 2778 ax-nul 4984 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2592 df-eu 2610 df-clab 2787 df-cleq 2793 df-clel 2796 df-nfc 2931 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3388 df-sbc 3635 df-dif 3773 df-un 3775 df-in 3777 df-ss 3784 df-nul 4117 df-if 4279 df-sn 4370 df-pr 4372 df-op 4376 df-uni 4630 df-br 4845 df-iota 6065 df-fv 6110 df-ov 6882 df-mgm 17556 df-sgrp 17598 df-mnd 17609 |
This theorem is referenced by: mnd4g 17621 mndpropd 17630 issubmnd 17632 prdsplusgcl 17635 imasmnd 17642 idmhm 17658 mhmf1o 17659 issubmd 17663 0mhm 17672 mhmco 17676 mhmeql 17678 submacs 17679 mrcmndind 17680 prdspjmhm 17681 pwsdiagmhm 17683 pwsco1mhm 17684 pwsco2mhm 17685 gsumccat 17692 gsumwmhm 17697 grpcl 17745 mhmmnd 17852 mulgnn0cl 17872 cntzsubm 18079 oppgmnd 18095 lsmssv 18370 frgp0 18487 frgpadd 18490 mulgnn0di 18545 mulgmhm 18547 gsumval3eu 18619 gsumval3 18622 gsumzcl2 18625 gsumzaddlem 18635 gsumzmhm 18651 gsummptfzcl 18682 srgcl 18827 srgacl 18839 srgbinomlem 18859 srgbinom 18860 ringcl 18876 ringpropd 18897 mndvcl 20521 mhmvlin 20527 mat2pmatghm 20862 pm2mpghm 20948 cpmadugsumlemF 21008 tsmsadd 22277 omndadd2d 30223 omndadd2rd 30224 slmdacl 30277 slmdvacl 30280 gsumncl 31130 c0mhm 42704 ofaddmndmap 42916 lincsum 43012 |
Copyright terms: Public domain | W3C validator |