Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > grpass | Structured version Visualization version GIF version |
Description: A group operation is associative. (Contributed by NM, 14-Aug-2011.) |
Ref | Expression |
---|---|
grpcl.b | ⊢ 𝐵 = (Base‘𝐺) |
grpcl.p | ⊢ + = (+g‘𝐺) |
Ref | Expression |
---|---|
grpass | ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | grpmnd 18565 | . 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | |
2 | grpcl.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
3 | grpcl.p | . . 3 ⊢ + = (+g‘𝐺) | |
4 | 2, 3 | mndass 18375 | . 2 ⊢ ((𝐺 ∈ Mnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) |
5 | 1, 4 | sylan 579 | 1 ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1085 = wceq 1541 ∈ wcel 2109 ‘cfv 6430 (class class class)co 7268 Basecbs 16893 +gcplusg 16943 Mndcmnd 18366 Grpcgrp 18558 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1801 ax-4 1815 ax-5 1916 ax-6 1974 ax-7 2014 ax-8 2111 ax-9 2119 ax-10 2140 ax-11 2157 ax-12 2174 ax-ext 2710 ax-nul 5233 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1544 df-fal 1554 df-ex 1786 df-nf 1790 df-sb 2071 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-ral 3070 df-rex 3071 df-rab 3074 df-v 3432 df-sbc 3720 df-dif 3894 df-un 3896 df-in 3898 df-ss 3908 df-nul 4262 df-if 4465 df-sn 4567 df-pr 4569 df-op 4573 df-uni 4845 df-br 5079 df-iota 6388 df-fv 6438 df-ov 7271 df-sgrp 18356 df-mnd 18367 df-grp 18561 |
This theorem is referenced by: grprcan 18594 grprinv 18610 grpinvid1 18611 grpinvid2 18612 grplcan 18618 grpasscan1 18619 grpasscan2 18620 grplmulf1o 18630 grpinvadd 18634 grpsubadd 18644 grpaddsubass 18646 grpsubsub4 18649 dfgrp3 18655 grplactcnv 18659 imasgrp 18672 mulgaddcomlem 18707 mulgaddcom 18708 mulgdirlem 18715 issubg2 18751 isnsg3 18769 nmzsubg 18774 ssnmz 18775 eqger 18787 eqgcpbl 18791 qusgrp 18792 conjghm 18846 conjnmz 18849 subgga 18887 cntzsubg 18924 sylow1lem2 19185 sylow2blem1 19206 sylow2blem2 19207 sylow2blem3 19208 sylow3lem1 19213 sylow3lem2 19214 lsmass 19256 lsmmod 19262 lsmdisj2 19269 gex2abl 19433 ringcom 19799 lmodass 20119 evpmodpmf1o 20782 psrgrp 21148 ghmcnp 23247 qustgpopn 23252 cnncvsaddassdemo 24308 ogrpaddltbi 31323 ogrpaddltrbid 31325 ogrpinvlt 31328 cyc3genpmlem 31397 archiabllem2c 31428 quslsm 31572 lfladdass 37066 dvhvaddass 39090 |
Copyright terms: Public domain | W3C validator |