Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mndass | Structured version Visualization version GIF version |
Description: A monoid operation is associative. (Contributed by NM, 14-Aug-2011.) (Proof shortened by AV, 8-Feb-2020.) |
Ref | Expression |
---|---|
mndcl.b | ⊢ 𝐵 = (Base‘𝐺) |
mndcl.p | ⊢ + = (+g‘𝐺) |
Ref | Expression |
---|---|
mndass | ⊢ ((𝐺 ∈ Mnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mndsgrp 18046 | . 2 ⊢ (𝐺 ∈ Mnd → 𝐺 ∈ Smgrp) | |
2 | mndcl.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
3 | mndcl.p | . . 3 ⊢ + = (+g‘𝐺) | |
4 | 2, 3 | sgrpass 18036 | . 2 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) |
5 | 1, 4 | sylan 583 | 1 ⊢ ((𝐺 ∈ Mnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1088 = wceq 1542 ∈ wcel 2114 ‘cfv 6350 (class class class)co 7183 Basecbs 16599 +gcplusg 16681 Smgrpcsgrp 18029 Mndcmnd 18040 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2711 ax-nul 5184 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2541 df-eu 2571 df-clab 2718 df-cleq 2731 df-clel 2812 df-ral 3059 df-rex 3060 df-rab 3063 df-v 3402 df-sbc 3686 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-nul 4222 df-sn 4527 df-pr 4529 df-op 4533 df-uni 4807 df-br 5041 df-iota 6308 df-fv 6358 df-ov 7186 df-sgrp 18030 df-mnd 18041 |
This theorem is referenced by: mnd32g 18052 mnd12g 18053 mnd4g 18054 issubmnd 18067 mndinvmod 18070 prdsmndd 18073 imasmnd 18078 mndind 18121 gsumccatOLD 18134 grpass 18241 mhmmnd 18352 cntzsubm 18597 oppgmnd 18613 frgp0 19017 mulgnn0di 19078 gsumval3eu 19156 gsumval3 19159 srgass 19395 ringass 19449 mndvass 21158 chfacfscmulgsum 21624 chfacfpmmulgsum 21628 slmdass 31056 lsmssass 31175 lidlmsgrp 45066 invginvrid 45285 mndtccatid 45875 |
Copyright terms: Public domain | W3C validator |